Crate chalk_ir

source ·
Expand description

Defines the IR for types and logical predicates.



  • Upcasts, to avoid writing out wrapper types.
  • Fast matching check for zippable values.
  • Debug impls for types.
  • Traits for transforming bits of IR.
  • Encapsulates the concrete representation of core types such as types and goals.
  • Traits for visiting bits of IR.
  • Traits for “zipping” types, walking through two structures and checking that they match.



  • The id for an Abstract Data Type (i.e. structs, unions and enums).
  • Proves equality between an alias and a type.
  • The resulting substitution after solving a goal.
  • The id for the associated type member of a trait. The details of the type can be found by invoking the associated_ty_data method.
  • Indicates that the value is universally quantified over N parameters of the given kinds, where N == self.binders.len(). A variable with depth i < N refers to the value at self.binders[i]. Variables with depth >= N are free.
  • IntoIterator for binders.
  • Identifies a particular bound variable within a binder. Variables are identified by the combination of a DebruijnIndex, which identifies the binder, and an index within that binder.
  • Wraps a “canonicalized item”. Items are canonicalized as follows:
  • List of interned elements.
  • Id for a specific clause.
  • Id for Rust closures.
  • Concrete constant, whose value is known (as opposed to inferred constants and placeholders).
  • Constants.
  • Constant data, containing the constant’s type and value.
  • Combines a substitution (subst) with a set of region constraints (constraints). This represents the result of a query; the substitution stores the values for the query’s unknown variables, and the constraints represents any region constraints that must additionally be solved.
  • List of interned elements.
  • References the binder at the given depth. The index is a de Bruijn index, so it counts back through the in-scope binders, with 0 being the innermost binder. This is used in impls and the like. For example, if we had a rule like for<T> { (T: Clone) :- (T: Copy) }, then T would be represented as a BoundVar(0) (as the for is the innermost binder).
  • A “DynTy” represents a trait object (dyn Trait). Trait objects are conceptually very related to an “existential type” of the form exists<T> { T: Trait } (another example of such type is impl Trait). DynTy represents the bounds on that type.
  • The set of assumptions we’ve made so far, and the current number of universal (forall) quantifiers we’re within.
  • Equality goal: tries to prove that two values are equal.
  • Indicates that the complete set of program clauses for this goal cannot be enumerated.
  • Function definition id.
  • for<’a…’z> X – all binders are instantiated at once, and we use deBruijn indices within self.ty
  • A function signature.
  • A wrapper for the substs on a Fn.
  • Id for foreign types.
  • Id for Rust generators.
  • A generic argument, see GenericArgData for more information.
  • A general goal; this is the full range of questions you can pose to Chalk.
  • List of interned elements.
  • The id for an impl.
  • A goal with an environment to solve it in.
  • A type, lifetime or constant whose value is being inferred.
  • A Rust lifetime.
  • Lifetime outlives, which for 'a: 'b`` checks that the lifetime ’ais a superset of the value of’b`.
  • Indicates that the attempted operation has “no solution” – i.e., cannot be performed.
  • Proves that the given type alias normalizes to the given type. A projection T::Foo normalizes to the type U if we can match it to an impl and that impl has a type Foo = V where U = V.
  • An opaque type opaque type T<..>: Trait = HiddenTy.
  • Id for an opaque type.
  • Index of an universally quantified parameter in the environment. Two indexes are required, the one of the universe itself and the relative index inside the universe.
  • A program clause is a logic expression used to describe a part of the program.
  • Contains the data for a program clause.
  • Represents one clause of the form consequence :- conditions where conditions = cond_1 && cond_2 && ... is the conjunction of the individual conditions.
  • List of interned elements.
  • A projection <P0 as TraitName<P1..Pn>>::AssocItem<Pn+1..Pm>.
  • List of interned elements.
  • List of interned elements.
  • Subtype goal: tries to prove that a is a subtype of b
  • The id of a trait definition; could be used to load the trait datum by invoking the trait_datum method.
  • A trait reference describes the relationship between a type and a trait. This can be used in two forms:
  • A Rust type. The actual type data is stored in TyKind.
  • Contains the data for a Ty
  • Contains flags indicating various properties of a Ty
  • Type outlives, which for T: 'a checks that the type T lives at least as long as the lifetime 'a
  • A “universe canonical” value. This is a wrapper around a Canonical, indicating that the universes within have been “renumbered” to start from 0 and collapse unimportant distinctions.
  • An universe index is how a universally quantified parameter is represented when it’s binder is moved into the environment. An example chain of transformations would be: forall<T> { Goal(T) } (syntactical representation) forall { Goal(?0) } (used a DeBruijn index) Goal(!U1) (the quantifier was moved to the environment and replaced with a universe index) See for more.
  • Maps the universes found in the u_canonicalize result (the “canonical” universes) to the universes found in the original value (and vice versa). When used as a folder – i.e., from outside this module – converts from “canonical” universes to the original (but see the UMapToCanonical folder).
  • List of interned elements.
  • List of interned elements.
  • A value with an associated variable kind.


  • An alias, which is a trait indirection such as a projection or opaque type.
  • Specifies how important an implication is.
  • A constant value, not necessarily concrete.
  • A constraint on lifetimes.
  • A “domain goal” is a goal that is directly about Rust, rather than a pure logical statement. As much as possible, the Chalk solver should avoid decomposing this enum, and instead treat its values opaquely.
  • A combination of Fallible and Floundered.
  • Different kinds of float types.
  • Checks whether a type or trait ref can be derived from the contents of the environment.
  • Generic arguments data.
  • A general goal; this is the full range of questions you can pose to Chalk.
  • Different signed int types.
  • Lifetime data, including what kind of lifetime it is and what it points to.
  • Whether a type is mutable or not.
  • Kinds of quantifiers in the logic, such as forall and exists.
  • Whether a function is safe or not.
  • Types of scalar values.
  • Type data, which holds the actual type information.
  • Represents some extra knowledge we may have about the type variable.
  • Different unsigned int types.
  • The “kind” of variable. Type, lifetime or constant.
  • Variance
  • Uninhabited (empty) type, used in combination with PhantomData.
  • Checks whether a type or trait ref is well-formed.
  • Where clauses that can be written by a Rust programmer.


  • Convert a value to a list of parameters.
  • An extension trait to anything that can be represented as list of GenericArgs that signifies that it can applied as a substituion to a value
  • Utility for converting a list of all the binders into scope into references to those binders. Simply pair the binders with the indices, and invoke to_generic_arg() on the (binder, index) pair. The result will be a reference to a bound variable of appropriate kind at the corresponding index.
  • Logic to decide the Variance for a given subst

Type Aliases

  • A variable kind with universe index.
  • Many of our internal operations (e.g., unification) are an attempt to perform some operation which may not complete.
  • A where clause that can contain forall<> or exists<> quantifiers.