Skip to content

Commit fe8dc67

Browse files
committed
types: introduce 'Incomplete' type to represent incomplete type bounds
Right now our types::Error enum has a couple variants that include bare `Type`s in them which are intended to represent invalid types. It isn't good hygeine to do this, because these Types carry with them information about the type context (which is supposed to be an ephemeral thing created during parsing and destroyed before parsing completes). It also limits our ability to provide useful representation of incomplete types in error messages, because the bare Bound type does not contain any data about why a bound was invalid. The user is also forced to be careful with these invalid objects, especially in the case of an occurs-check failure, when any attempt to iterate on the type will infinite-loop. This commit does the bare minimum to define a new type for use in error messages. In a followup we probably want to clean things up a bit -- at the very least we should try to construct some sort of rich "occurs check failure" information. We may also want to define an IncompleteArrow, which would make the code in human_encoding a bit tidier. The attentive reviewer may notice calls to `lock.drop()` inserted before calls to Incomplete::from_bound_ref. Without these calls, the code deadlocks. There is no compiler help or anything to keep track of this. This kind of bullshit is why I'm so excited to use GhostCell, where the compiler (and borrowck) will do all the work for us. Finally, in the next commit when we add a 'brand lifetime marker to Type, we will be forced to avoid saving this type in our Error enum, because then Type will be unable to outlive its type context (and errors must outlive the context, since the context is ephemeral and the error is something we return to the user).
1 parent c473b17 commit fe8dc67

File tree

5 files changed

+216
-55
lines changed

5 files changed

+216
-55
lines changed

src/human_encoding/error.rs

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -244,7 +244,8 @@ pub enum Error {
244244
/// us from knowing the whole program.
245245
HoleAtCommitTime {
246246
name: Arc<str>,
247-
arrow: types::arrow::Arrow,
247+
arrow_source: Arc<types::Incomplete>,
248+
arrow_target: Arc<types::Incomplete>,
248249
},
249250
/// When converting to a `CommitNode`, a disconnect node had an actual node rather
250251
/// than a hole.
@@ -303,11 +304,12 @@ impl fmt::Display for Error {
303304
),
304305
Error::HoleAtCommitTime {
305306
ref name,
306-
ref arrow,
307+
ref arrow_source,
308+
ref arrow_target,
307309
} => write!(
308310
f,
309-
"unfilled hole ?{} at commitment time; type arrow {}",
310-
name, arrow
311+
"unfilled hole ?{} at commitment time; type arrow {} -> {}",
312+
name, arrow_source, arrow_target,
311313
),
312314
Error::HoleFilledAtCommitTime => {
313315
f.write_str("disconnect node has a non-hole child at commit time")

src/human_encoding/named_node.rs

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -347,11 +347,15 @@ impl<J: Jet> NamedConstructNode<J> {
347347
self.errors.add(position, error);
348348
}
349349
if let node::Inner::Witness(WitnessOrHole::TypedHole(name)) = inner {
350+
let arrow_source = data.node.arrow().source.to_incomplete();
351+
let arrow_target = data.node.arrow().source.to_incomplete();
352+
350353
self.pending_hole_error = Some((
351354
data.node.position(),
352355
Error::HoleAtCommitTime {
353356
name: Arc::clone(name),
354-
arrow: data.node.arrow().shallow_clone(),
357+
arrow_source,
358+
arrow_target,
355359
},
356360
));
357361
}

src/types/context.rs

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ use std::sync::{Arc, Mutex, MutexGuard};
1919

2020
use crate::dag::{Dag, DagLike};
2121

22-
use super::{Bound, CompleteBound, Error, Final, Type, TypeInner};
22+
use super::{Bound, CompleteBound, Error, Final, Incomplete, Type, TypeInner};
2323

2424
/// Type inference context, or handle to a context.
2525
///
@@ -211,9 +211,10 @@ impl Context {
211211
let mut lock = self.lock();
212212
lock.bind(existing_root, new_bound).map_err(|e| {
213213
let new_bound = lock.alloc_bound(e.new);
214+
drop(lock);
214215
Error::Bind {
215-
existing_bound: Type::wrap_bound(self, e.existing),
216-
new_bound: Type::wrap_bound(self, new_bound),
216+
existing_bound: Incomplete::from_bound_ref(self, e.existing),
217+
new_bound: Incomplete::from_bound_ref(self, new_bound),
217218
hint,
218219
}
219220
})
@@ -228,9 +229,10 @@ impl Context {
228229
let mut lock = self.lock();
229230
lock.unify(&ty1.inner, &ty2.inner).map_err(|e| {
230231
let new_bound = lock.alloc_bound(e.new);
232+
drop(lock);
231233
Error::Bind {
232-
existing_bound: Type::wrap_bound(self, e.existing),
233-
new_bound: Type::wrap_bound(self, new_bound),
234+
existing_bound: Incomplete::from_bound_ref(self, e.existing),
235+
new_bound: Incomplete::from_bound_ref(self, new_bound),
234236
hint,
235237
}
236238
})

src/types/incomplete.rs

Lines changed: 185 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,185 @@
1+
// SPDX-License-Identifier: CC0-1.0
2+
3+
//! "Finalized" Incomplete Type Data
4+
//!
5+
//! This structure is essentially the same as [types::Final](super::Final) except
6+
//! that it has free variables (represented by strings) and supports self-reference.
7+
//! The purpose of this structure is to provide a useful representation of a type
8+
//! in error messages.
9+
//!
10+
11+
use crate::dag::{Dag, DagLike, NoSharing};
12+
use crate::types::union_bound::PointerLike;
13+
14+
use super::{Bound, BoundRef, Context};
15+
16+
use std::fmt;
17+
use std::sync::Arc;
18+
19+
/// An incomplete type bound for use in error messages.
20+
#[derive(Clone)]
21+
pub enum Incomplete {
22+
/// A free variable.
23+
Free(String),
24+
/// A type containing this type.
25+
Cycle,
26+
/// A sum of two other types
27+
Sum(Arc<Incomplete>, Arc<Incomplete>),
28+
/// A product of two other types
29+
Product(Arc<Incomplete>, Arc<Incomplete>),
30+
/// A complete type (including unit)
31+
Final(Arc<super::Final>),
32+
}
33+
34+
impl DagLike for &'_ Incomplete {
35+
type Node = Incomplete;
36+
fn data(&self) -> &Incomplete {
37+
self
38+
}
39+
fn as_dag_node(&self) -> Dag<Self> {
40+
match *self {
41+
Incomplete::Free(_) | Incomplete::Cycle | Incomplete::Final(_) => Dag::Nullary,
42+
Incomplete::Sum(ref left, ref right) | Incomplete::Product(ref left, ref right) => {
43+
Dag::Binary(left, right)
44+
}
45+
}
46+
}
47+
}
48+
49+
impl fmt::Debug for Incomplete {
50+
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
51+
fmt::Display::fmt(self, f)
52+
}
53+
}
54+
55+
impl fmt::Display for Incomplete {
56+
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
57+
let mut skip_next = false;
58+
for data in self.verbose_pre_order_iter::<NoSharing>(None) {
59+
if skip_next {
60+
skip_next = false;
61+
continue;
62+
}
63+
64+
match (data.node, data.n_children_yielded) {
65+
(Incomplete::Free(ref s), _) => f.write_str(s)?,
66+
(Incomplete::Cycle, _) => f.write_str("<self-reference>")?,
67+
// special-case 1 + A as A?
68+
(Incomplete::Sum(ref left, _), 0) if left.is_unit() => {
69+
skip_next = true;
70+
}
71+
(Incomplete::Sum(ref left, _), 1) if left.is_unit() => {}
72+
(Incomplete::Sum(ref left, _), 2) if left.is_unit() => {
73+
f.write_str("?")?;
74+
}
75+
// other sums and products
76+
(Incomplete::Sum(..), 0) | (Incomplete::Product(..), 0) => {
77+
if data.index > 0 {
78+
f.write_str("(")?;
79+
}
80+
}
81+
(Incomplete::Sum(..), 2) | (Incomplete::Product(..), 2) => {
82+
if data.index > 0 {
83+
f.write_str(")")?;
84+
}
85+
}
86+
(Incomplete::Sum(..), _) => f.write_str(" + ")?,
87+
(Incomplete::Product(..), _) => f.write_str(" × ")?,
88+
(Incomplete::Final(ref fnl), _) => fnl.fmt(f)?,
89+
}
90+
}
91+
Ok(())
92+
}
93+
}
94+
95+
impl Incomplete {
96+
/// Whether this "incomplete bound" is the unit type.
97+
pub fn is_unit(&self) -> bool {
98+
if let Incomplete::Final(ref fnl) = self {
99+
fnl.is_unit()
100+
} else {
101+
false
102+
}
103+
}
104+
105+
/// Does the occurs-check on a type bound.
106+
///
107+
/// Returns None on success, and a Some(Incomplete) indicating the occurs-check
108+
/// failure if there is a cyclic reference.
109+
pub(super) fn occurs_check(ctx: &Context, bound_ref: BoundRef) -> Option<Arc<Self>> {
110+
use std::collections::HashSet;
111+
112+
use super::context::OccursCheckId;
113+
use super::BoundRef;
114+
115+
/// Helper type for the occurs-check.
116+
enum OccursCheckStack {
117+
Iterate(BoundRef),
118+
Complete(OccursCheckId),
119+
}
120+
121+
// First, do occurs-check to ensure that we have no infinitely sized types.
122+
let mut stack = vec![OccursCheckStack::Iterate(bound_ref)];
123+
let mut in_progress = HashSet::new();
124+
let mut completed = HashSet::new();
125+
while let Some(top) = stack.pop() {
126+
let bound = match top {
127+
OccursCheckStack::Complete(id) => {
128+
in_progress.remove(&id);
129+
completed.insert(id);
130+
continue;
131+
}
132+
OccursCheckStack::Iterate(b) => b,
133+
};
134+
135+
let id = bound.occurs_check_id();
136+
if completed.contains(&id) {
137+
// Once we have iterated through a type, we don't need to check it again.
138+
// Without this shortcut the occurs-check would take exponential time.
139+
continue;
140+
}
141+
if !in_progress.insert(id) {
142+
// FIXME unwind the stack to somehow provide a more useful trace of the occurs-check failure
143+
return Some(Arc::new(Self::Cycle));
144+
}
145+
146+
stack.push(OccursCheckStack::Complete(id));
147+
if let Some((_, child)) = (ctx, bound.shallow_clone()).right_child() {
148+
stack.push(OccursCheckStack::Iterate(child));
149+
}
150+
if let Some((_, child)) = (ctx, bound).left_child() {
151+
stack.push(OccursCheckStack::Iterate(child));
152+
}
153+
}
154+
155+
None
156+
}
157+
158+
pub(super) fn from_bound_ref(ctx: &Context, bound_ref: BoundRef) -> Arc<Self> {
159+
if let Some(err) = Self::occurs_check(ctx, bound_ref.shallow_clone()) {
160+
return err;
161+
}
162+
163+
// Now that we know our bound has finite size, we can safely use a
164+
// post-order iterator on it.
165+
let mut finalized = vec![];
166+
for data in (ctx, bound_ref).post_order_iter::<NoSharing>() {
167+
let bound_get = data.node.0.get(&data.node.1);
168+
let final_data = match bound_get {
169+
Bound::Free(s) => Incomplete::Free(s),
170+
Bound::Complete(ref arc) => Incomplete::Final(Arc::clone(arc)),
171+
Bound::Sum(..) => Incomplete::Sum(
172+
Arc::clone(&finalized[data.left_index.unwrap()]),
173+
Arc::clone(&finalized[data.right_index.unwrap()]),
174+
),
175+
Bound::Product(..) => Incomplete::Product(
176+
Arc::clone(&finalized[data.left_index.unwrap()]),
177+
Arc::clone(&finalized[data.right_index.unwrap()]),
178+
),
179+
};
180+
181+
finalized.push(Arc::new(final_data));
182+
}
183+
finalized.pop().unwrap()
184+
}
185+
}

src/types/mod.rs

Lines changed: 13 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -75,28 +75,29 @@ use self::union_bound::{PointerLike, UbElement};
7575
use crate::dag::{DagLike, NoSharing};
7676
use crate::Tmr;
7777

78-
use std::collections::HashSet;
7978
use std::fmt;
8079
use std::sync::Arc;
8180

8281
pub mod arrow;
8382
mod context;
8483
mod final_data;
84+
mod incomplete;
8585
mod precomputed;
8686
mod union_bound;
8787
mod variable;
8888

8989
pub use context::{BoundRef, Context};
9090
pub use final_data::{CompleteBound, Final};
91+
pub use incomplete::Incomplete;
9192

9293
/// Error type for simplicity
9394
#[non_exhaustive]
9495
#[derive(Clone, Debug)]
9596
pub enum Error {
9697
/// An attempt to bind a type conflicted with an existing bound on the type
9798
Bind {
98-
existing_bound: Type,
99-
new_bound: Type,
99+
existing_bound: Arc<Incomplete>,
100+
new_bound: Arc<Incomplete>,
100101
hint: &'static str,
101102
},
102103
/// Two unequal complete types were attempted to be unified
@@ -106,7 +107,7 @@ pub enum Error {
106107
hint: &'static str,
107108
},
108109
/// A type is recursive (i.e., occurs within itself), violating the "occurs check"
109-
OccursCheck { infinite_bound: Type },
110+
OccursCheck { infinite_bound: Arc<Incomplete> },
110111
/// Attempted to combine two nodes which had different type inference
111112
/// contexts. This is probably a programming error.
112113
InferenceContextMismatch,
@@ -274,56 +275,23 @@ impl Type {
274275
self.final_data().is_some()
275276
}
276277

278+
/// Converts a type as-is to an `Incomplete` type for use in an error.
279+
pub fn to_incomplete(&self) -> Arc<Incomplete> {
280+
let root = self.inner.bound.root();
281+
Incomplete::from_bound_ref(&self.ctx, root)
282+
}
283+
277284
/// Attempts to finalize the type. Returns its TMR on success.
278285
pub fn finalize(&self) -> Result<Arc<Final>, Error> {
279-
use context::OccursCheckId;
280-
281-
/// Helper type for the occurs-check.
282-
enum OccursCheckStack {
283-
Iterate(BoundRef),
284-
Complete(OccursCheckId),
285-
}
286-
287-
// Done with sharing tracker. Actual algorithm follows.
288286
let root = self.inner.bound.root();
289287
let bound = self.ctx.get(&root);
290288
if let Bound::Complete(ref data) = bound {
291289
return Ok(Arc::clone(data));
292290
}
293291

294292
// First, do occurs-check to ensure that we have no infinitely sized types.
295-
let mut stack = vec![OccursCheckStack::Iterate(root)];
296-
let mut in_progress = HashSet::new();
297-
let mut completed = HashSet::new();
298-
while let Some(top) = stack.pop() {
299-
let bound = match top {
300-
OccursCheckStack::Complete(id) => {
301-
in_progress.remove(&id);
302-
completed.insert(id);
303-
continue;
304-
}
305-
OccursCheckStack::Iterate(b) => b,
306-
};
307-
308-
let id = bound.occurs_check_id();
309-
if completed.contains(&id) {
310-
// Once we have iterated through a type, we don't need to check it again.
311-
// Without this shortcut the occurs-check would take exponential time.
312-
continue;
313-
}
314-
if !in_progress.insert(id) {
315-
return Err(Error::OccursCheck {
316-
infinite_bound: Type::wrap_bound(&self.ctx, bound),
317-
});
318-
}
319-
320-
stack.push(OccursCheckStack::Complete(id));
321-
if let Some((_, child)) = (&self.ctx, bound.shallow_clone()).right_child() {
322-
stack.push(OccursCheckStack::Iterate(child));
323-
}
324-
if let Some((_, child)) = (&self.ctx, bound).left_child() {
325-
stack.push(OccursCheckStack::Iterate(child));
326-
}
293+
if let Some(infinite_bound) = Incomplete::occurs_check(&self.ctx, root) {
294+
return Err(Error::OccursCheck { infinite_bound });
327295
}
328296

329297
// Now that we know our types have finite size, we can safely use a

0 commit comments

Comments
 (0)