Module canonicalize

A canonical type is a type where all existentials and constraint predicates are hoisted to the top level. For example, the canonical version of ∃a. {∃b. i32[a + b] | b > 0} is ∃a,b. {i32[a + b] | b > 0}.

Type constructors introduce scopes that can limit the hoisting. For instance, it is generally not permitted to hoist an existential out of a generic argument. For example, in Vec<∃v. i32[v]> the existential inside the Vec cannot be hoisted out.

However, some type constructors are more “lenient” with respect to hoisting. Consider the tuple (∃a. i32[a], ∃b. i32[b]). Hoisting the existentials results in ∃a,b. (i32[a], i32[b]) which is an equivalent type (in the sense that subtyping holds both ways). The same applies to shared references: &∃a. i32[a] is equivalent to ∃a. &i32[a]. We refer to this class of type constructors as transparent. Hoisting existential out of transparent type constructors is useful as it allows the logical information to be extracted from the type.

And important case is mutable references. In some situations, it is sound to hoist out of mutable references. For example, if we have a variable in the environment of type &mut ∃v. T[v], it is sound to treat it as &mut T[a] for a freshly generated a (assuming the lifetime of the reference is alive). However, this may result in a type that is too specific because the index a cannot be updated anymore.

By default, we do shallow hoisting, i.e., we stop at the first type constructor. This is enough for cases where we need to inspect a type structurally one level. The amount of hoisting can be controlled by configuring the Hoister struct.

It’s also important to note that canonizalization doesn’t imply any form of semantic equality and it is just a best effort to facilitate syntactic manipulation. For example, the types ∃a,b. (i32[a], i32[b]) and ∃a,b. (i32[b], i32[a]) are semantically equal but hoisting won’t account for it.

Modules

• pretty 🔒

Structs

• CanonicalConstrTy
• Hoister
  The Hoister struct is responsible for hoisting existentials and predicates out of a type. It can be configured to stop hoisting at specific type constructors.
• LocalHoister

Enums

• CanonicalTy
  A (shallowly) canonicalized type. This can be either of the form {T | p} or ∃v0,…,vn. {T | p}, where T doesnt have any (shallow) existential or constraint types.

Traits

• HoisterDelegate