What is Chalk?

Chalk is under heavy development, so if any of these links are broken or if any of the information is inconsistent with the code or outdated, please open an issue so we can fix it. If you are able to fix the issue yourself, we would love your contribution!

Chalk is a library that implements the Rust trait system. The implementation is meant to be practical and usable, but also high-level enough to map easily to a full specification. It is also meant to be an independent library that can be integrated both into the main rustc compiler and also other programs and contexts.

High-level view of how chalk works

graph TD
    Query["Does `Vec<u8>` implement `Debug`?"]
    HighLevelInfo["How is the trait `Debug` declared?"]
    Response["Yes, `Vec<u8>` implements `Debug`."]
    Chalk
    Query --> Chalk
    HighLevelInfo --> Chalk
    Chalk --> Response

Chalk is designed to answer queries about traits, such as "Does the type Vec<u8> implement Debug"? (Yes!). It can in some cases give inference feedback, such as "Is there a unique type T such that str: AsRef<T>"? In that case, the answer might be "Yes, T = str."

To do this, it takes as input key information about a Rust program, such as:

• For a given trait, what are its type parameters, where clauses, and associated items
• For a given impl, what are the types that appear in the impl header
• For a given struct, what are the types of its fields

Chalk works by converting Rust goals into logical inference rules

Internally, Chalk works by converting the Rust-specific information, like traits and impls, into logical predicates. This process is called "lowering", and you can learn more about it in the Lowering to Logic and Lowering Rules) sections.

After lowering to logical predicates, Chalk then deploys a logical solver to find the answer to the original query; this solver is similar to a Prolog engine, though different in its particulars.

The following sequence diagram helps to illustrate the flow of information that occurs when Chalk is solving a particular goal. It involves three participants:

• The host program, which might be rustc, rust-analyzer, or chalk's internal testing harness. The host program, importantly, only thinks about things in Rust terms, like traits and impls.
• The chalk-solve crate, which converts between Rust terms and logical clauses.
• The logic engine layer, which knows how to solve logical clauses but knows nothing specific to Rust.

sequenceDiagram
  participant rustc as host program
  participant chalkSolve as chalk-solve
  participant chalkEngine as logic engine
  rustc->>chalkSolve: Does Vec[u32] implement Debug?
  chalkSolve->>chalkEngine: (Vec[u32]: Debug)?
  chalkEngine->>chalkSolve: What clauses can I use?
  chalkSolve->>rustc: What is the definition of `Debug`?<br>(via RustIrDatabase)
  rustc-->>chalkSolve: `trait Debug { .. }`<br>(a TraitDatum)
  chalkSolve->>rustc: What impls are there for Vec?
  rustc-->>chalkSolve: `impl[T]: Debug] Debug for Vec[T]`<br>(an ImplDatum)
  Note right of chalkSolve: "lowers" rust <br>declarations to logic
  chalkSolve-->>chalkEngine: (Vec[T]: Debug) :- (T: Debug)
  chalkSolve-->>chalkEngine: ... and other clauses ...
  activate chalkEngine
  Note right of chalkEngine: explores each clause<br>to see if it works
  chalkEngine-->>chalkSolve: (Vec[u32]: Debug) is provable
  deactivate chalkEngine
  chalkSolve-->>rustc: Yes, Vec[u32] implements Debug

Chalk repl

In addition to being embedded into host programs, chalk also has its own testing harness along with an associated REPL. This allows us to write unit tests that use a "Rust-like" syntax. The REPL then makes it easy to experiment and get a better feel for how chalk works. See the walkthrough for more details.

Walkthrough

This section shows a sample session in the chalk repl, and then gives a tour through the code to give you an idea of the phases involved.

?- program
Enter a program; press Ctrl-D when finished
| struct Foo { }
| struct Bar { }
| struct Vec<T> { }
| trait Clone { }
| impl<T> Clone for Vec<T> where T: Clone { }
| impl Clone for Foo { }

?- Vec<Foo>: Clone
Unique; substitution [], lifetime constraints []

?- Vec<Bar>: Clone
No possible solution.

?- exists<T> { Vec<T>: Clone }
Ambiguous; no inference guidance

You can see more examples of programs and queries in the unit tests.

Next we'll go through each stage required to produce the output above.

Parsing (chalk_parse)

Chalk is designed to be incorporated with the Rust compiler, so the syntax and concepts it deals with heavily borrow from Rust. It is convenient for the sake of testing to be able to run chalk on its own, so chalk includes a parser for a Rust-like syntax. This syntax is orthogonal to the Rust AST and grammar. It is not intended to look exactly like it or support the exact same syntax.

The parser takes that syntax and produces an Abstract Syntax Tree (AST). You can find the complete definition of the AST in the source code.

The syntax contains things from Rust that we know and love, for example: traits, impls, and struct definitions. Parsing is often the first "phase" of transformation that a program goes through in order to become a format that chalk can understand.

Rust Intermediate Representation (chalk_solve::rust_ir)

After getting the AST we convert it to a more convenient intermediate representation called chalk_rust_ir. This is sort of analogous to the HIR in Rust. The process of converting to IR is called lowering.

The chalk::program::Program struct contains some "rust things" but indexed and accessible in a different way. For example, if you have a type like Foo<Bar>, we would represent Foo as a string in the AST but in chalk::program::Program, we use numeric indices (ItemId).

The IR source code contains the complete definition.

Chalk Intermediate Representation (chalk_ir)

Once we have Rust IR it is time to convert it to "program clauses". A ProgramClause is essentially one of the following:

• A clause of the form consequence :- conditions where :- is read as "if" and conditions = cond1 && cond2 && ...
• A universally quantified clause of the form forall<T> { consequence :- conditions }
  • forall<T> { ... } is used to represent universal quantification. See the section on Lowering to logic for more information.
  • A key thing to note about forall is that we don't allow you to "quantify" over traits, only types and regions (lifetimes). That is, you can't make a rule like forall<Trait> { u32: Trait } which would say "u32 implements all traits". You can however say forall<T> { T: Trait } meaning "Trait is implemented by all types".
  • forall<T> { ... } is represented in the code using the Binders<T> struct.

See also: Goals and Clauses

This is where we encode the rules of the trait system into logic. For example, if we have the following Rust:

impl<T: Clone> Clone for Vec<T> {}

We generate the following program clause:

forall<T> { (Vec<T>: Clone) :- (T: Clone) }

This rule dictates that Vec<T>: Clone is only satisfied if T: Clone is also satisfied (i.e. "provable").

Similar to chalk::program::Program which has "rust-like things", chalk_ir defines ProgramEnvironment which is "pure logic". The main field in that struct is program_clauses, which contains the ProgramClauses generated by the rules module.

Rules (chalk_solve)

The chalk_solve crate (source code) defines the logic rules we use for each item in the Rust IR. It works by iterating over every trait, impl, etc. and emitting the rules that come from each one.

See also: Lowering Rules

Well-formedness checks

As part of lowering to logic, we also do some "well formedness" checks. See the chalk_solve::wf source code for where those are done.

See also: Well-formedness checking

Coherence

The method CoherenceSolver::specialization_priorities in the coherence module (source code) checks "coherence", which means that it ensures that two impls of the same trait for the same type cannot exist.

Solver (chalk_solve)

Finally, when we've collected all the program clauses we care about, we want to perform queries on it. The component that finds the answer to these queries is called the solver.

See also: The SLG Solver

Crates

Chalk's functionality is broken up into the following crates:

• chalk_engine: Defines the core SLG solver.
• chalk_ir: Defines chalk's internal representation of types, lifetimes, and goals.
• chalk_solve: Combines chalk_ir and chalk_engine, effectively, which implements logic rules converting chalk_rust_ir to chalk_ir
  • Contains the rust_ir module, which defines the "HIR-like" Rust IR
  • Defines the coherence module, which implements coherence rules
  • chalk_engine::context provides the necessary hooks.
• chalk_parse: Defines the raw AST and a parser.
• chalk: Brings everything together. Defines the following modules:
  • chalk::lowering, which converts AST to chalk_rust_ir
  • Also includes chalki, chalk's REPL.

Browse source code on GitHub

Testing

chalk has a test framework for lowering programs to logic, checking the lowered logic, and performing queries on it. This is how we test the implementation of chalk itself, and the viability of the lowering rules.

The main kind of tests in chalk are goal tests. They contain a program, which is expected to lower to logic successfully, and a set of queries (goals) along with the expected output. Here's an example. Since chalk's output can be quite long, goal tests support specifying only a prefix of the output.

Lowering tests check the stages that occur before we can issue queries to the solver: the lowering to chalk_rust_ir, and the well-formedness checks that occur after that.

Testing internals

Goal tests use a test! macro that takes chalk's Rust-like syntax and runs it through the full pipeline described above. The macro ultimately calls the solve_goal function.

Likewise, lowering tests use the lowering_success! and lowering_error! macros.

More Resources

• Chalk Source Code
• Chalk Glossary

Crate breakdown

Chalk is broken up into a number of crates. This chapter explains the role of each crate. This crate structure helps to serve Chalk's two goals:

• To serve as the trait engine for compilers and tools like rustc and rust-analyzer
• To be usable as a standalone REPL and testing harness

Crates for embedding chalk into other programs

The following crates are "public facing" crates that you may use when embedding chalk into other programs:

• The chalk-solve crate, which defines the IR representing Rust concepts like traits and impls and the rules that translate Rust IR into logical predicates.
• The chalk-ir crate, which defines the IR representing types and logical predicates.

The following crate is an implementation detail, used internally by chalk-solve:

• The chalk-engine crate, which defines the actual engine that solves logical predicate. This engine is quite general and not really specific to Rust.
• The chalk-derive crate defines custom derives for the chalk_ir::fold::TypeFoldable trait and other such things.

Crates for standalone REPL and testing

The following crates are used to define the REPL and internal testing harness. These crates build on the crates above. Essentially, they define a kind of "minimal embedding" of chalk.

• The chalk-parser crate can parse Rust syntax to produce an AST.
• The chalk-integration crate can take that AST and use it to drive the chalk-solve crate above. The AST is converted into Rust IR by a process called "lowering".
• Finally, the main chalk crate, along with the testing crate in the tests directory, define the actual entry points.

The chalk-solve crate

The chalk-solve crate exposes a key type called Solver. This is a solver that, given a goal (expressed in chalk-ir) will solve the goal and yield up a Solution. The solver caches intermediate data between invocations, so solving the same goal twice in a row (or solving goals with common subgoals) is faster.

The solver is configured by a type that implements the RustIrDatabase trait. This trait contains some callbacks that provide needed context for the solver -- notably, the solver can ask:

• What are the program clauses that might solve given rule? This is answered by the code in the chalk-solve crate.
• Is this trait coinductive? This is answered by the chalk-ir.

The chalk-engine crate

For the purposes of chalk, the chalk-engine crate is effectively encapsulated by chalk-solve. It defines the base SLG engine. It is written in a very generic style that knows next to nothing about Rust itself. The engine can be configured via the traits defined in chalk_engine::context::Context, which contain (for example) associated types that define what a goal or clause is, as well as functions that operate on those things.

REPL

There is a repl mainly for debugging purposes which can be run by cargo run. Some basic examples are in libstd.chalk:

$ cargo run
?- load libstd.chalk
?- Vec<Box<i32>>: Clone
Unique; substitution [], lifetime constraints []

Contribution guide

Thank you for your interest in contributing to chalk! There are many ways to contribute, and we appreciate all of them.

• Bug Reports
• Running and Debugging
• Pull Requests
• Writing Documentation

If you'd like to contribute, consider joining the Traits Working Group. We hang out on the rust-lang zulip in the #wg-traits stream.

As a reminder, all contributors are expected to follow our Code of Conduct.

Bug Reports

While bugs are unfortunate, they're a reality in software. We can't fix what we don't know about, so please report liberally. If you're not sure if something is a bug or not, feel free to file a bug anyway.

If you have the chance, before reporting a bug, please search existing issues, as it's possible that someone else has already reported your error. This doesn't always work, and sometimes it's hard to know what to search for, so consider this extra credit. We won't mind if you accidentally file a duplicate report.

Sometimes, a backtrace is helpful, and so including that is nice. To get a backtrace, set the RUST_BACKTRACE environment variable to a value other than 0. The easiest way to do this is to invoke chalk like this:

$ RUST_BACKTRACE=1 chalk ...

Running and Debugging

There is a repl mainly for debugging purposes which can be run by cargo run. Some basic examples are in libstd.chalk:

$ cargo run
?- load libstd.chalk
?- Vec<Box<i32>>: Clone
Unique; substitution [], lifetime constraints []

More logging can be enabled by setting the CHALK_DEBUG environment variable. Set CHALK_DEBUG=3 or CHALK_DEBUG=info to see info!(...) output, and CHALK_DEBUG=4 or CHALK_DEBUG=debug to see debug!(...) output as well. In addition, logs may be filtered in a number of ways. The syntax for filtering logs is:

 target[span{field=value}]=level

(Note: all parts of the filter are optional )

In more detail, the filter may consist of:

• A target (location of origin)
  • For example setting CHALK_DEBUG='chalk_solve::infer::unify' will filter logs to show only output originating from chalk_solve::infer::unify.
• A span (name provided to the logging macros, for instance unify_var_ty in debug_span!("unify_var_ty"))
  • For example setting CHALK_DEBUG='[unify_ty_ty]' will show only logs where the span contains unify_ty_ty.
• A list of fields (variables recorded in the logs), for instance ty in debug!("unify_var_ty", ?ty) with values optionally specified
  • For example setting CHALK_DEBUG='[{ty}]' will show only logs which contain a variable ty
  • Setting CHALK_DEBUG='[{ty=Bar}]' will show only logs which contain a variable ty with the value Bar
• A maximum log level (one of info, debug, trace) which shows logs at or below the given level

More documentation on the syntax and options can be found here.

Pull Requests

Pull requests are the primary mechanism we use to change Rust. GitHub itself has some great documentation on using the Pull Request feature. We use the "fork and pull" model described here, where contributors push changes to their personal fork and create pull requests to bring those changes into the source repository.

Please make pull requests against the master branch.

Writing Documentation

Documentation improvements are very welcome. Documentation pull requests function in the same way as other pull requests.

You can find documentation style guidelines in RFC 1574.

Representing and manipulating Rust types

Intermediate representations

Intermediate representations (IR) are used to represent parts of Rust programs such as traits and impls.

Chalk contains three levels of IR:

• The AST. This is used purely for writing test cases with a Rust-like syntax. This is consumed by lowering code, which takes AST and produces Rust IR (the next bullet point).
• The Rust IR. This is a "HIR-like" notation that defines the interesting properties of things like traits, impls, and structs. It is an input to the rules code, which produces Chalk IR (the next bullet point).
• The Chalk IR. This is most "Prolog-like" of the various IRs. It contains the definition of types as well as prolog-like concepts such as goals (things that must be proven true) and clauses (things that are assumed to be true).

Goal of the chalk-ir crate

To have an ergonomic, flexible library that can abstractly represent Rust types and logical predicates. The library should be expose a "minimal" set of types that is nonetheless able to capture the full range of Rust types. "Minimal" here means that some of the surface differences in Rust types -- e.g., the distinction between built-in types like u32 and user-defined types like a struct -- ought to be minimized, so that code that works with these types (e.g., trait solving) can focus on the most important differences.

Goal: support embedding and a variety of contexts

One of our goals is to create a type representation that can be readily embedded into a variety of contexts. Most specifically, we would like to be able to embed into rustc and rust-analyzer, and permit those two projects to use distinct memory management strategies. This is primarily achieved via the Interner trait.

Initially, at least in rustc, the goal is to be able to easily and "reasonably efficiently" convert back and forth between rustc's native type representation and chalk's representation. Once chalk's design has stabilized, however, the goal would be for rustc to adopt this format as its "native" representation.

Note that even if the chalk type library were used everywhere, however, it would still be useful for rustc to be able to control the memory management strategy. (In other words, different consumers might wish to use it in different ways.)

Note on status

At the moment, this documentation is a "proposal". That means that it diverges in some places from what is actually implemented. It has also not been thoroughly discussed by the Rust compiler team as a whole.

Here is a (partial) list of some things that have to be adapted in Chalk as of today to match this document:

• Extract TypeName into something opaque to chalk-ir.
• Dyn type equality should probably be driven by entailment.
• Projections need to be renamed to aliases.
• The variant we use for impl traits should be removed and folded into type aliases.
• Remove placeholders and projection placeholders from apply and create placeholder types.
• Move Error from a TypeName to its own variant.
• Introduce GeneratorWitness into chalk
• Complete transition from ForAll to Fn in chalk

The role of the Interner

Most everything in the IR is parameterized by the Interner trait:

trait Interner: Copy + Clone + Debug + Eq + Ord {
    ..
}

We'll go over the details later, but for now it suffices to say that the interner is defined by the embedder and can be used to control (to a certain extent) the actual representation of types, goals, and other things in memory. For example, the Interner trait could be used to intern all the types, as rustc does, or it could be used to Box them instead, as the chalk testing harness currently does.

Controlling representation with Interner

The purpose of the Interner trait is to give control over how types and other bits of chalk-ir are represented in memory. This is done via an "indirection" strategy. We'll explain that strategy here in terms of Ty and TyKind, the two types used to represent Rust types, but the same pattern is repeated for many other things.

Types are represented by a Ty<I> type and the TyKind<I> enum. There is no direct connection between them. The link is rather made by the Interner trait, via the InternedTy associated type:

struct Ty<I: Interner>(I::InternedTy);
enum TyKind<I: Interner> { .. }

The way this works is that the Interner trait has an associated type InternedTy and two related methods, intern_ty and ty_data:

trait Interner {
    type InternedTy;

    fn intern_ty(&self, data: &TyKind<Self>) -> Self::InternedTy;
    fn ty_data(data: &Self::InternedTy) -> &TyData<Self>;
}

However, as a user you are not meant to use these directly. Rather, they are encapsulated in methods on the Ty and TyKind types:

impl<I: Interner> Ty<I> {
  fn data(&self) -> &TyKind<I> {
    I::lookup_ty(self)
  }
}

and

impl<I: Interner> TyKind<I> {
  fn intern(&self, i: &I) -> Ty<I> {
    Ty(i.intern_ty(self))
  }
}

Note that there is an assumption here that ty_data needs no context. This effectively constrains the InternedTy representation to be a Box or & type. To be more general, at the cost of some convenience, we could make that a method as well, so that one would invoke ty.data(i) instead of just ty.data(). This would permit us to use (for example) integers to represent interned types, which might be nice (e.g., to permit using generational indices).

Rust types

Rust types are represented by the Ty and TyKind types. You use Ty to represent "some Rust type". But to actually inspect what sort of type you have, you invoke the kind method, which returns a TyKind. As described earlier, the actual in-memory representation of types is controlled by the Interner trait.

The TyKind variants and how they map to Rust syntax

This section covers the variants we use to categorize types. We have endeavored to create a breakdown that simplifies the Rust "surface syntax" of types to their "essence". In particular, the goal is to group together types that are largely treated identically by the system and to separate types when there are important semantic differences in how they are handled.

Justification for each variant

Each variant of TyKind generally wraps a single struct, which represents a type known to be of that particular variant. This section goes through the variants in a bit more detail, and in particular describes why each variant exists.

Application types

Most of "normal rust types" like Vec<u32> or (f32, Vec<isize>) are represented with TyKind variants containing some type-specific info ("type name") and a substitution that is "applied" to that type. In this case, type names are Vec and "tuple of arity 2", and substitutions are [u32] and [f32, Vec<isize>].

They are equal to other types (modulo aliases, see below) iff they have the same "type name" and the generic arguments are recursively equal

Placeholders

The Placeholder variant contains a PlaceholderIndex type. It represents a generic type that is being treated abstractly or -- more generally -- the result of a "type function" that cannot be evaluated. For example, when typing the body of a generic function like fn foo<T: Iterator>, the type T would be represented with a placeholder. Similarly, in that same function, the associated type T::Item might be represented with a placeholder.

Like application types, placeholder types are only known to be equal.

When proving negative goals, e.g., not { Implemented(T: Trait) }, placeholders are treated quite differently from application types, since they do not (in fact) represent a known type. When solving negative goals, placeholders are replaced with inference variables -- the idea is that this goal is only true if there is no type T that implements Trait. Therefore, if we can find no answers for exists<T> { Implemented(T: Trait) }, then we know that the negation is true. (Note that this means that e.g. forall<X> { X = i32 } is false but so is forall<X> { not { X = i32 } }.)

Inference variables

The InferenceVar variant wraps an InferenceVar type. This represents a type whose value is being inferred. The value of an inference variables may be "known" or "not known", but that state is stored externally, in the inference context (see the section on inference below).

When equating, inference variables are treated specially in that they become bound (or, if they have already been bound, they are replaced with their value).

Inference variables are also integral to canonicalization and other types.

Dyn types

The Dyn variant wraps a DynTy and represents a dyn Trait type. In chalk, these are represented as an existential type where we store the predicates that are known to be true. So a type like dyn Write would be represented as, effectively, an exists<T> { T: Write } type.

When equating, two dyn P and dyn Q types are equal if P = Q -- i.e., they have the same bounds. Note that -- for this purpose -- ordering of bounds is significant. That means that if you create a dyn Foo + Send and a dyn Send + Foo, chalk would consider them distinct types. The assumption is that bounds are ordered in some canonical fashion somewhere else. This may want to change.

There are "automatic" rules for proving that dyn P: P and so forth, but that is outside the scope of the chalk-ir crate.

Function pointer types

The Function variant wraps a FnPointer struct and represents a fn() type (in other words, a function pointer). In some ways, fn types are like application types, but with one crucial difference: they also contain a forall binder that for lifetimes whose value is determined when the function is called. Consider e.g. a type like fn(&u32) or -- more explicitly -- for<'a> fn(&'a u32).

Two Function types A, B are equal A = B if A <: B and B <: A

Two Function types A, B are subtypes A <: B if

• After instantiating the lifetime parameters on B universally...
  • You can instantiate the lifetime parameters on A existentially...
    • And then you find that P_B <: P_A for every parameter type P on A and B and R_A <: R_B for the return type R of A and B.

We currently handle type inference with a bit of a hack (same as rustc); when relating a Fn type F to an unbounded type variable V, we instantiate V with F. But in practice because of the above subtyping rules there are actually a range of values that V could have and still be equal with F. This may or may not be something to consider revisiting.

Alias types

The Alias variant wraps an AliasTy and is used to represent some form of type alias. They are used to represent a number of related Rust concepts, include actual type aliases, associated types, and opaque types -- you can read about them in the aliases chapter.

Bound variables

The BoundVar variant represents some variable that is bound in an outer term. For example, given a term like forall<X> { Implemented(X: Trait) }, the X is bound. Bound variables in chalk (like rustc) use De Bruijn indices (See below).

Bound variables are never directly equated, as any bound variables would have been instantiated with either inference variables or placeholders.

They do appear in canonical forms and other terms that contain binders.

Error types

The Error variant represents a type that resulted from some erroneous expression. Error types generally propagate eagerly in an attempt to suppress nonsense errors that are derived by interactions with buggy code.

Error should be its own variant because most bits of code will want to handle it somewhat specially -- e.g., maybe it can "unify" with any other type without any effect, and so forth.

Mapping to rustc types

The rustc TyKind enum is almost equivalent to chalk's. This section describes how the rustc types can be mapped to chalk types. The intention is that, at least when transitioning, rustc would implement the Interner trait and would map from the TyKind enum to chalk's TyKind on the fly, when data() is invoked.

Alias types

Alias types are used in chalk to handle a number of distinct Rust concepts:

• Explicit type aliases like type Foo = u32 (in theory)
• Associated types like impl Iterator for Foo { type Item = Bar }
• Opaque types generated by impl Traits, like type Foo = impl Iterator<Item = u32> or fn foo() -> impl Iterator<Item = u32>.

What all these aliases have in common is that they let the user write the name of one type that turns out to be equivalent to another, although the equivalent type is not always known:

• In an explicit type alias like type Foo = u32, the user writes Foo but it is always known to be equivalent to u32
• In an associated type, the user might write <vec::IntoIter<u32> as Iterator>::Item, but the compiler knows that can be normalized (see below) to u32. In generic functions, though, you might have a type like T::Item where we can't normalize, because we don't know what T is. Even in that case, though, we still know that T::Item: Sized, because that bound is declared in the Iterator trait (by default, as it happens). We describe how both cases are handled in more detail in the section on associated types.
• In an opaque type like type Foo = impl Iterator<Item = u32>, the user might write Foo (which indirectly references the opaque type) but they never get to rely on the precise underlying type. However, when generating code, the compiler does need to be able to normalize Foo to the precise underlying type, so normalization still does occur. We describe this in more detail in the opaque types section.

How aliases work

All aliases have a few parts:

• The Alias type, which represents what the user wrote directly, but where there is some underlying type.
• Normalization rules, which indicate when the alias type can be converted into its underlying type.
• A corresponding Placeholder type, which is used in cases where the alias cannot be converted into its underlying type.

Equating an alias

Alias types are integrated specially into unification. Whenever there is an attempt to unify an Alias type A with some other type T, we generate an AliasEq that must be solved:

AliasEq(A = T)

The rules for how to solve an AliasEq goal will be generated by lowering the alias definition, and depend a bit on the kind of alias. We describe that lowering in the clauses section.

Alias placeholders

For each kind of alias (except for explicit type aliases), there is also a corresponding placeholder variant in the TyKind enum. In those cases where we cannot normalize the alias to something specific, it can be equated to the placeholder type (see e.g. AssociatedType, which is the placeholder variant for associated type projections). Note that placeholders are application types -- unlike an alias, a placeholder is only known to be equal with itself, just like an application type.

Application types

TyKind variants that consist of some type-specific info ("type name") and a substitution are usually referred to as application types. These include most of the "normal Rust types", such as Vec and (f32, u32). Such types are only "equal" to themselves (modulo aliases, see below). Scalar types (and some others) also fall into this category, despite having no substitutions: we treat them as having zero-length substitutions. Note that we group together both user-defined structs/enums/unions (like Vec) as well as built-in types like f32, which effectively behave the same.

We used to have application types in chalk as a separate notion in the codebase, but have since moved away from that; nevertheless, the term is still useful in discussions.

Notable application types

Coroutine

A Coroutine represents a Rust coroutine. There are three major components to a coroutine:

• Upvars - similar to closure upvars, they reference values outside of the coroutine, and are stored across all yield points.
• Resume/yield/return types - the types produced/consumed by various coroutine methods. These are not stored in the coroutine across yield points - they are only used when the coroutine is running.
• Coroutine witness - see the Coroutine Witness section below.

Of these types, only upvars and resume/yield/return are stored directly in CoroutineDatum (which is accessed via RustIrDatabase). The coroutine witness is implicitly associated with the coroutine by virtue of sharing the same CoroutineId. It is only used when determining auto trait impls, where it is considered a 'constituent type'.

For example:

// This is not "real" syntax at the moment.
fn gen() -> Bar {
  let a = yield 0usize;
  use(a)
}

fn use(_: usize) -> Bar {}

The type of yield would be usize, the resume type would be the type of a and the return type would be Bar.

Coroutine witness types

The CoroutineWitness variant represents the coroutine witness of the coroutine with id CoroutineId.

The coroutine witness contains multiple witness types, which represent the types that may be part of a coroutine state - that is, the types of all variables that may be live across a yield point.

Unlike other types, witnesses include bound, existential lifetimes, which refer to lifetimes within the suspended stack frame. You can think of it as a type like exists<'a> { (T...) }. As an example, imagine that a type that isn't Send lives across a yield, then the coroutine itself can't be Send.

Witnesses have a binder for the erased lifetime(s), which must be handled specifically in equating and so forth. In many ways, witnesses are also quite similar to Function types, and it is not out of the question that these two could be unified; however, they are quite distinct semantically and so that would be an annoying mismatch in other parts of the system. Witnesses are also similar to a Dyn type, in that they represent an existential type, but in contrast to Dyn, what we know here is not a predicate but rather some upper bound on the set of types contained within.

Rust lifetimes

Lifetimes are represented by the Lifetime<I> and LifetimeData<I> types. As with types, the actual representation of a lifetime is defined by the associated type I::InternedLifetime.

The LifetimeData variants

This section covers the variants we use to categorize lifetimes.

Variants and their equivalents in Rust syntax

Operations

This chapter describes various patterns and utilities for manipulating Rust types.

TypeFoldable and the TypeFolder trait

The TypeFoldable trait permits one to traverse a type or other term in the chalk-ir and make a copy of it, possibly making small substitutions or alterations along the way. Folding also allows copying a term from one interner to another.

To use the TypeFoldable trait, one invokes the TypeFoldable::fold_with method, supplying some "folder" as well as the number of "in scope binders" for that term (typically 0 to start):

let output_ty = input_ty.fold_with(&mut folder, 0);

The folder is some instance of the TypeFolder trait. This trait defines a few key callbacks that allow you to substitute different values as the fold proceeds. For example, when a type is folded, the folder can substitute a new type in its place.

Uses for folders

A common use for TypeFoldable is to permit a substitution -- that is, replacing generic type parameters with their values.

From TypeFoldable to TypeFolder to TypeSuperFoldable and back again

The overall flow of folding is like this.

1. TypeFoldable::fold_with is invoked on the outermost term. It recursively walks the term.
2. For those sorts of terms (types, lifetimes, goals, program clauses) that have callbacks in the TypeFolder trait, invoking TypeFoldable::fold_with will in turn invoke the corresponding method on the TypeFolder trait, such as TypeFolder::fold_ty.
3. The default implementation of TypeFolder::fold_ty, in turn, invokes TypeSuperFoldable::super_fold_with. This will recursively fold the contents of the type. In some cases, the super_fold_with implementation invokes more specialized methods on TypeFolder, such as TypeFolder::fold_free_var_ty, which makes it easier to write folders that just intercept certain types.

Thus, as a user, you can customize folding by:

• Defining your own TypeFolder type
• Implementing the appropriate methods to "intercept" types/lifetimes/etc at the right level of detail
• In those methods, if you find a case where you would prefer not to substitute a new value, then invoke TypeSuperFoldable::super_fold_with to return to the default behavior.

The binders argument

Each callback in the TypeFolder trait takes a binders argument. This indicates the number of binders that we have traversed during folding, which is relevant for De Bruijn indices. So e.g. a bound variable with depth 1, if invoked with a binders value of 1, indicates something that was bound to something external to the fold.

For example, consider:

Foo<'a>: for<'b> Bar<'b>

In this case, Foo<'a> gets visited with depth 0 and Bar<'b> gets visited with depth 1.

The TypeFoldable::Result associated type

The TypeFoldable trait defines a Result associated type, indicating the type that will result from folding.

When to implement the TypeFoldable and TypeSuperFoldable traits

Any piece of IR that represents a kind of "term" (e.g., a type, part of a type, or a goal, etc) in the logic should implement TypeFoldable. We also implement TypeFoldable for common collection types like Vec as well as tuples, references, etc.

The TypeSuperFoldable trait should only be implemented for those types that have a callback defined on the TypeFolder trait (e.g., types and lifetimes).

Derives

Using the chalk-derive crate, you can auto-derive the TypeFoldable trait. There isn't presently a derive for TypeSuperFoldable since it is very rare to require it. The derive for TypeFoldable is a bit cludgy and requires:

• You must import TypeFoldable into scope.
• The type you are deriving TypeFoldable on must have either:
  • A type parameter that has a Interner bound, like I: Interner
  • A type parameter that has a HasInterner bound, like I: HasInterner
  • The has_interner(XXX) attribute.

Lowering Rust IR to logic

The key observation here is that the Rust trait system is basically a kind of logic, and it can be mapped onto standard logical inference rules. We can then look for solutions to those inference rules in a very similar fashion to how e.g. a Prolog solver works. It turns out that we can't quite use Prolog rules (also called Horn clauses) but rather need a somewhat more expressive variant.

Rust traits and logic

One of the first observations is that the Rust trait system is basically a kind of logic. As such, we can map our struct, trait, and impl declarations into logical inference rules. For the most part, these are basically Horn clauses, though we'll see that to capture the full richness of Rust – and in particular to support generic programming – we have to go a bit further than standard Horn clauses.

To see how this mapping works, let's start with an example. Imagine we declare a trait and a few impls, like so:

#![allow(unused)]
fn main() {
trait Clone { }
impl Clone for usize { }
impl<T> Clone for Vec<T> where T: Clone { }
}

We could map these declarations to some Horn clauses, written in a Prolog-like notation, as follows:

Clone(usize).
Clone(Vec<?T>) :- Clone(?T).

// The notation `A :- B` means "A is true if B is true".
// Or, put another way, B implies A.

In Prolog terms, we might say that Clone(Foo) – where Foo is some Rust type – is a predicate that represents the idea that the type Foo implements Clone. These rules are program clauses; they state the conditions under which that predicate can be proven (i.e., considered true). So the first rule just says "Clone is implemented for usize". The next rule says "for any type ?T, Clone is implemented for Vec<?T> if clone is implemented for ?T". So e.g. if we wanted to prove that Clone(Vec<Vec<usize>>), we would do so by applying the rules recursively:

• Clone(Vec<Vec<usize>>) is provable if:
  • Clone(Vec<usize>) is provable if:
    • Clone(usize) is provable. (Which it is, so we're all good.)

But now suppose we tried to prove that Clone(Vec<Bar>). This would fail (after all, I didn't give an impl of Clone for Bar):

• Clone(Vec<Bar>) is provable if:
  • Clone(Bar) is provable. (But it is not, as there are no applicable rules.)

We can easily extend the example above to cover generic traits with more than one input type. So imagine the Eq<T> trait, which declares that Self is equatable with a value of type T:

trait Eq<T> { ... }
impl Eq<usize> for usize { }
impl<T: Eq<U>> Eq<Vec<U>> for Vec<T> { }

That could be mapped as follows:

Eq(usize, usize).
Eq(Vec<?T>, Vec<?U>) :- Eq(?T, ?U).

So far so good.

Type-checking normal functions

OK, now that we have defined some logical rules that are able to express when traits are implemented and to handle associated types, let's turn our focus a bit towards type-checking. Type-checking is interesting because it is what gives us the goals that we need to prove. That is, everything we've seen so far has been about how we derive the rules by which we can prove goals from the traits and impls in the program; but we are also interested in how to derive the goals that we need to prove, and those come from type-checking.

Consider type-checking the function foo() here:

fn foo() { bar::<usize>() }
fn bar<U: Eq<U>>() { }

This function is very simple, of course: all it does is to call bar::<usize>(). Now, looking at the definition of bar(), we can see that it has one where-clause U: Eq<U>. So, that means that foo() will have to prove that usize: Eq<usize> in order to show that it can call bar() with usize as the type argument.

If we wanted, we could write a Prolog predicate that defines the conditions under which bar() can be called. We'll say that those conditions are called being "well-formed":

barWellFormed(?U) :- Eq(?U, ?U).

Then we can say that foo() type-checks if the reference to bar::<usize> (that is, bar() applied to the type usize) is well-formed:

fooTypeChecks :- barWellFormed(usize).

If we try to prove the goal fooTypeChecks, it will succeed:

• fooTypeChecks is provable if:
  • barWellFormed(usize), which is provable if:
    • Eq(usize, usize), which is provable because of an impl.

Ok, so far so good. Let's move on to type-checking a more complex function.

Type-checking generic functions: beyond Horn clauses

In the last section, we used standard Prolog horn-clauses (augmented with Rust's notion of type equality) to type-check some simple Rust functions. But that only works when we are type-checking non-generic functions. If we want to type-check a generic function, it turns out we need a stronger notion of goal than what Prolog can provide. To see what I'm talking about, let's revamp our previous example to make foo generic:

fn foo<T: Eq<T>>() { bar::<T>() }
fn bar<U: Eq<U>>() { }

To type-check the body of foo, we need to be able to hold the type T "abstract". That is, we need to check that the body of foo is type-safe for all types T, not just for some specific type. We might express this like so:

fooTypeChecks :-
  // for all types T...
  forall<T> {
    // ...if we assume that Eq(T, T) is provable...
    if (Eq(T, T)) {
      // ...then we can prove that `barWellFormed(T)` holds.
      barWellFormed(T)
    }
  }.

This notation I'm using here is the notation I've been using in my prototype implementation; it's similar to standard mathematical notation but a bit Rustified. Anyway, the problem is that standard Horn clauses don't allow universal quantification (forall) or implication (if) in goals (though many Prolog engines do support them, as an extension). For this reason, we need to accept something called "first-order hereditary harrop" (FOHH) clauses – this long name basically means "standard Horn clauses with forall and if in the body". But it's nice to know the proper name, because there is a lot of work describing how to efficiently handle FOHH clauses; see for example Gopalan Nadathur's excellent "A Proof Procedure for the Logic of Hereditary Harrop Formulas" in the bibliography.

It turns out that supporting FOHH is not really all that hard. And once we are able to do that, we can easily describe the type-checking rule for generic functions like foo in our logic.

Source

This page is a lightly adapted version of a blog post by Nicholas Matsakis.

Goals and clauses

In logic programming terms, a goal is something that you must prove and a clause is something that you know is true. As described in the lowering to logic chapter, Rust's trait solver is based on an extension of hereditary harrop (HH) clauses, which extend traditional Prolog Horn clauses with a few new superpowers.

Goals and clauses meta structure

In Rust's solver, goals and clauses have the following forms (note that the two definitions reference one another):

Goal = DomainGoal           // defined in the section below
        | Goal && Goal
        | Goal || Goal
        | exists<K> { Goal }   // existential quantification
        | forall<K> { Goal }   // universal quantification
        | if (Clause) { Goal } // implication
        | true                 // something that's trivially true
        | ambiguous            // something that's never provable

Clause = DomainGoal
        | Clause :- Goal     // if can prove Goal, then Clause is true
        | Clause && Clause
        | forall<K> { Clause }

K = <type>     // a "kind"
    | <lifetime>

The proof procedure for these sorts of goals is actually quite straightforward. Essentially, it's a form of depth-first search. The paper "A Proof Procedure for the Logic of Hereditary Harrop Formulas" gives the details.

In terms of code, these types are defined in compiler/rustc_middle/src/traits/mod.rs in rustc, and in chalk-ir/src/lib.rs in chalk.

Domain goals

Domain goals are the atoms of the trait logic. As can be seen in the definitions given above, general goals basically consist in a combination of domain goals.

Moreover, flattening a bit the definition of clauses given previously, one can see that clauses are always of the form:

forall<K1, ..., Kn> { DomainGoal :- Goal }

hence domain goals are in fact clauses' LHS. That is, at the most granular level, domain goals are what the trait solver will end up trying to prove.

To define the set of domain goals in our system, we need to first introduce a few simple formulations. A trait reference consists of the name of a trait along with a suitable set of inputs P0..Pn:

TraitRef = P0: TraitName<P1..Pn>

So, for example, u32: Display is a trait reference, as is Vec<T>: IntoIterator. Note that Rust surface syntax also permits some extra things, like associated type bindings (Vec<T>: IntoIterator<Item = T>), that are not part of a trait reference.

A projection consists of an associated item reference along with its inputs P0..Pm:

Projection = <P0 as TraitName<P1..Pn>>::AssocItem<Pn+1..Pm>

Given these, we can define a DomainGoal as follows:

DomainGoal = Holds(WhereClause)
            | FromEnv(TraitRef)
            | FromEnv(Type)
            | WellFormed(TraitRef)
            | WellFormed(Type)
            | Normalize(Projection -> Type)

WhereClause = Implemented(TraitRef)
            | AliasEq(Projection = Type)
            | Outlives(Type: Region)
            | Outlives(Region: Region)

WhereClause refers to a where clause that a Rust user would actually be able to write in a Rust program. This abstraction exists only as a convenience as we sometimes want to only deal with domain goals that are effectively writable in Rust.

Let's break down each one of these, one-by-one.

Implemented(TraitRef)

e.g. Implemented(i32: Copy)

True if the given trait is implemented for the given input types and lifetimes.

AliasEq(Projection = Type)

e.g. AliasEq<T as Iterator>::Item = u8

The given associated type Projection is equal to Type; this can be proved with either normalization or using placeholder associated types and is handled as a special kind of type aliases. See the section on associated types.

Normalize(Projection -> Type)

e.g. Normalize<T as Iterator>::Item -> u8

The given associated type Projection can be normalized to Type.

As discussed in the section on associated types, Normalize implies AliasEq, but not vice versa. In general, proving Normalize(<T as Trait>::Item -> U) also requires proving Implemented(T: Trait).

FromEnv(TraitRef)

e.g. FromEnv(Self: Add<i32>)

True if the inner TraitRef is assumed to be true, that is, if it can be derived from the in-scope where clauses.

For example, given the following function:

#![allow(unused)]
fn main() {
fn loud_clone<T: Clone>(stuff: &T) -> T {
    println!("cloning!");
    stuff.clone()
}
}

Inside the body of our function, we would have FromEnv(T: Clone). In-scope where clauses nest, so a function body inside an impl body inherits the impl body's where clauses, too.

This and the next rule are used to implement implied bounds. As we'll see in the section on lowering, FromEnv(TraitRef) implies Implemented(TraitRef), but not vice versa. This distinction is crucial to implied bounds.

FromEnv(Type)

e.g. FromEnv(HashSet<K>)

True if the inner Type is assumed to be well-formed, that is, if it is an input type of a function or an impl.

For example, given the following code:

struct HashSet<K> where K: Hash { ... }

fn loud_insert<K>(set: &mut HashSet<K>, item: K) {
    println!("inserting!");
    set.insert(item);
}

HashSet<K> is an input type of the loud_insert function. Hence, we assume it to be well-formed, so we would have FromEnv(HashSet<K>) inside the body of our function. As we'll see in the section on lowering, FromEnv(HashSet<K>) implies Implemented(K: Hash) because the HashSet declaration was written with a K: Hash where clause. Hence, we don't need to repeat that bound on the loud_insert function: we rather automatically assume that it is true.

WellFormed(Item)

These goals imply that the given item is well-formed.

We can talk about different types of items being well-formed:

• Types, like WellFormed(Vec<i32>), which is true in Rust, or WellFormed(Vec<str>), which is not (because str is not Sized.)

• TraitRefs, like WellFormed(Vec<i32>: Clone).

Well-formedness is important to implied bounds. In particular, the reason it is okay to assume FromEnv(T: Clone) in the loud_clone example is that we also verify WellFormed(T: Clone) for each call site of loud_clone. Similarly, it is okay to assume FromEnv(HashSet<K>) in the loud_insert example because we will verify WellFormed(HashSet<K>) for each call site of loud_insert.

Outlives(Type: Region), Outlives(Region: Region)

e.g. Outlives(&'a str: 'b), Outlives('a: 'static)

True if the given type or region on the left outlives the right-hand region.

Coinductive goals

Most goals in our system are "inductive". In an inductive goal, circular reasoning is disallowed. Consider this example clause:

    Implemented(Foo: Bar) :-
        Implemented(Foo: Bar).

Considered inductively, this clause is useless: if we are trying to prove Implemented(Foo: Bar), we would then recursively have to prove Implemented(Foo: Bar), and that cycle would continue ad infinitum (the trait solver will terminate here, it would just consider that Implemented(Foo: Bar) is not known to be true).

However, some goals are co-inductive. Simply put, this means that cycles are OK. So, if Bar were a co-inductive trait, then the rule above would be perfectly valid, and it would indicate that Implemented(Foo: Bar) is true.

Auto traits are one example in Rust where co-inductive goals are used. Consider the Send trait, and imagine that we have this struct:

#![allow(unused)]
fn main() {
struct Foo {
    next: Option<Box<Foo>>
}
}

The default rules for auto traits say that Foo is Send if the types of its fields are Send. Therefore, we would have a rule like

Implemented(Foo: Send) :-
    Implemented(Option<Box<Foo>>: Send).

As you can probably imagine, proving that Option<Box<Foo>>: Send is going to wind up circularly requiring us to prove that Foo: Send again. So this would be an example where we wind up in a cycle – but that's ok, we do consider Foo: Send to hold, even though it references itself.

In general, co-inductive traits are used in Rust trait solving when we want to enumerate a fixed set of possibilities. In the case of auto traits, we are enumerating the set of reachable types from a given starting point (i.e., Foo can reach values of type Option<Box<Foo>>, which implies it can reach values of type Box<Foo>, and then of type Foo, and then the cycle is complete).

In addition to auto traits, WellFormed predicates are co-inductive. These are used to achieve a similar "enumerate all the cases" pattern, as described in the section on implied bounds.

Type equality and unification

This section covers how the trait system handles equality between associated types. The full system consists of several moving parts, which we will introduce one by one:

• Projection and the Normalize predicate
• Placeholder associated type projections
• The AliasEq predicate
• Integration with unification

Associated type projection and normalization

When a trait defines an associated type (e.g., the Item type in the IntoIterator trait), that type can be referenced by the user using an associated type projection like <Option<u32> as IntoIterator>::Item.

Often, people will use the shorthand syntax T::Item. Presently, that syntax is expanded during "type collection" into the explicit form, though that is something we may want to change in the future.

In some cases, associated type projections can be normalized – that is, simplified – based on the types given in an impl. So, to continue with our example, the impl of IntoIterator for Option<T> declares (among other things) that Item = T:

impl<T> IntoIterator for Option<T> {
  type Item = T;
  ...
}

This means we can normalize the projection <Option<u32> as IntoIterator>::Item to just u32.

In this case, the projection was a "monomorphic" one – that is, it did not have any type parameters. Monomorphic projections are special because they can always be fully normalized.

Often, we can normalize other associated type projections as well. For example, <Option<?T> as IntoIterator>::Item, where ?T is an inference variable, can be normalized to just ?T.

In our logic, normalization is defined by a predicate Normalize. The Normalize clauses arise only from impls. For example, the impl of IntoIterator for Option<T> that we saw above would be lowered to a program clause like so:

forall<T> {
    Normalize(<Option<T> as IntoIterator>::Item -> T) :-
        Implemented(Option<T>: IntoIterator)
}

where in this case, the one Implemented condition is always true.

Since we do not permit quantification over traits, this is really more like a family of program clauses, one for each associated type.

We could apply that rule to normalize either of the examples that we've seen so far.

Placeholder associated types

Sometimes however we want to work with associated types that cannot be normalized. For example, consider this function:

fn foo<T: IntoIterator>(...) { ... }

In this context, how would we normalize the type T::Item?

Without knowing what T is, we can't really do so. To represent this case, we introduce a type called a placeholder associated type projection. This is written like so: (IntoIterator::Item)<T>.

You may note that it looks a lot like a regular type (e.g., Option<T>), except that the "name" of the type is (IntoIterator::Item). This is not an accident: placeholder associated type projections work just like ordinary types like Vec<T> when it comes to unification. That is, they are only considered equal if (a) they are both references to the same associated type, like IntoIterator::Item and (b) their type arguments are equal.

Placeholder associated types are never written directly by the user. They are used internally by the trait system only, as we will see shortly.

In rustc, they correspond to the TyKind::UnnormalizedProjectionTy enum variant, declared in compiler/rustc_middle/src/ty/sty.rs. In chalk, we use an AssociatedType.

Projection equality

So far we have seen two ways to answer the question of "When can we consider an associated type projection equal to another type?":

• the Normalize predicate could be used to transform projections when we knew which impl applied;
• placeholder associated types can be used when we don't. This is also known as lazy normalization.

These two cases are brought together by the AliasEq predicate introduced before (where the AliasTy is Projection). The instantiated predicate for projection equality looks then like so:

AliasEq(<T as IntoIterator>::Item = U)

and we will see that it can be proven either via normalization or via the placeholder type. As part of lowering an associated type declaration from some trait, we create two program clauses for AliasEq:

forall<T, U> {
    AliasEq(<T as IntoIterator>::Item = U) :-
        Normalize(<T as IntoIterator>::Item -> U)
}

forall<T> {
    AliasEq(<T as IntoIterator>::Item = (IntoIterator::Item)<T>)
}

These are the only two AliasEq program clauses we ever make for any given associated item.

Integration with unification

Now we are ready to discuss how associated type equality integrates with unification. As described in the type inference section, unification is basically a procedure with a signature like this:

Unify(A, B) = Result<Subgoals, NoSolution>

In other words, we try to unify two things A and B. That procedure might just fail, in which case we get back Err(NoSolution). This would happen, for example, if we tried to unify u32 and i32.

The key point is that, on success, unification can also give back to us a set of subgoals that still remain to be proven.

Whenever unification encounters a non-placeholder associated type projection P being equated with some other type T, it always succeeds, but it produces a subgoal AliasEq(P = T) that is propagated back up. Thus it falls to the ordinary workings of the trait system to process that constraint.

If we unify two projections P1 and P2, then unification produces a variable X and asks us to prove that AliasEq(P1 = X) and AliasEq(P2 = X). (That used to be needed in an older system to prevent cycles; I rather doubt it still is. -nmatsakis)

Implied Bounds

Implied bounds remove the need to repeat where clauses written on a type declaration or a trait declaration. For example, say we have the following type declaration:

struct HashSet<K: Hash> {
    ...
}

then everywhere we use HashSet<K> as an "input" type, that is appearing in the receiver type of an impl or in the arguments of a function, we don't want to have to repeat the where K: Hash bound, as in:

// I don't want to have to repeat `where K: Hash` here.
impl<K> HashSet<K> {
    ...
}

// Same here.
fn loud_insert<K>(set: &mut HashSet<K>, item: K) {
    println!("inserting!");
    set.insert(item);
}

Note that in the loud_insert example, HashSet<K> is not the type of the set argument of loud_insert, it only appears in the argument type &mut HashSet<K>: we care about every type appearing in the function's header (the header is the signature without the return type), not only types of the function's arguments.

The rationale for applying implied bounds to input types is that, for example, in order to call the loud_insert function above, the programmer must have produced the type HashSet<K> already, hence the compiler already verified that HashSet<K> was well-formed, i.e. that K effectively implemented Hash, as in the following example:

fn main() {
    // I am producing a value of type `HashSet<i32>`.
    // If `i32` was not `Hash`, the compiler would report an error here.
    let set: HashSet<i32> = HashSet::new();
    loud_insert(&mut set, 5);
}

Hence, we don't want to repeat where clauses for input types because that would sort of duplicate the work of the programmer, having to verify that their types are well-formed both when calling the function and when using them in the arguments of their function. The same reasoning applies when using an impl.

Similarly, given the following trait declaration:

trait Copy where Self: Clone { // desugared version of `Copy: Clone`
    ...
}

then everywhere we bound over SomeType: Copy, we would like to be able to use the fact that SomeType: Clone without having to write it explicitly, as in:

fn loud_clone<T: Clone>(x: T) {
    println!("cloning!");
    x.clone();
}

fn fun_with_copy<T: Copy>(x: T) {
    println!("will clone a `Copy` type soon...");

    // I'm using `loud_clone<T: Clone>` with `T: Copy`, I know this
    // implies `T: Clone` so I don't want to have to write it explicitly.
    loud_clone(x);
}

The rationale for implied bounds for traits is that if a type implements Copy, that is, if there exists an impl Copy for that type, there ought to exist an impl Clone for that type, otherwise the compiler would have reported an error in the first place. So again, if we were forced to repeat the additional where SomeType: Clone everywhere whereas we already know that SomeType: Copy hold, we would kind of duplicate the verification work.

Implied bounds are not yet completely enforced in rustc, at the moment it only works for outlive requirements, super trait bounds, and bounds on associated types. The full RFC can be found here. We'll give here a brief view of how implied bounds work and why we chose to implement it that way. The complete set of lowering rules can be found in the corresponding chapter.

Implied bounds and lowering rules

Now we need to express implied bounds in terms of logical rules. We will start with exposing a naive way to do it. Suppose that we have the following traits:

trait Foo {
    ...
}

trait Bar where Self: Foo {
    ...
}

So we would like to say that if a type implements Bar, then necessarily it must also implement Foo. We might think that a clause like this would work:

forall<Type> {
    Implemented(Type: Foo) :- Implemented(Type: Bar).
}

Now suppose that we just write this impl:

struct X;

impl Bar for X { }

Clearly this should not be allowed: indeed, we wrote a Bar impl for X, but the Bar trait requires that we also implement Foo for X, which we never did. In terms of what the compiler does, this would look like this:

struct X;

impl Bar for X {
    // We are in a `Bar` impl for the type `X`.
    // There is a `where Self: Foo` bound on the `Bar` trait declaration.
    // Hence I need to prove that `X` also implements `Foo` for that impl
    // to be legal.
}

So the compiler would try to prove Implemented(X: Foo). Of course it will not find any impl Foo for X since we did not write any. However, it will see our implied bound clause:

forall<Type> {
    Implemented(Type: Foo) :- Implemented(Type: Bar).
}

so that it may be able to prove Implemented(X: Foo) if Implemented(X: Bar) holds. And it turns out that Implemented(X: Bar) does hold since we wrote a Bar impl for X! Hence the compiler will accept the Bar impl while it should not.

Implied bounds coming from the environment

So the naive approach does not work. What we need to do is to somehow decouple implied bounds from impls. Suppose we know that a type SomeType<...> implements Bar and we want to deduce that SomeType<...> must also implement Foo.

There are two possibilities: first, we have enough information about SomeType<...> to see that there exists a Bar impl in the program which covers SomeType<...>, for example a plain impl<...> Bar for SomeType<...>. Then if the compiler has done its job correctly, there must exist a Foo impl which covers SomeType<...>, e.g. another plain impl<...> Foo for SomeType<...>. In that case then, we can just use this impl and we do not need implied bounds at all.

Second possibility: we do not know enough about SomeType<...> in order to find a Bar impl which covers it, for example if SomeType<...> is just a type parameter in a function:

fn foo<T: Bar>() {
    // We'd like to deduce `Implemented(T: Foo)`.
}

That is, the information that T implements Bar here comes from the environment. The environment is the set of things that we assume to be true when we type check some Rust declaration. In that case, what we assume is that T: Bar. Then at that point, we might authorize ourselves to have some kind of "local" implied bound reasoning which would say Implemented(T: Foo) :- Implemented(T: Bar). This reasoning would only be done within our foo function in order to avoid the earlier problem where we had a global clause.

We can apply this local reasoning everywhere we can have an environment -- i.e. when we can write where clauses -- that is, inside impls, trait declarations, and type declarations.

Computing implied bounds with FromEnv

The previous subsection showed that it was only useful to compute implied bounds for facts coming from the environment. We talked about "local" rules, but there are multiple possible strategies to indeed implement the locality of implied bounds.

In rustc, the current strategy is to elaborate bounds: that is, each time we have a fact in the environment, we recursively derive all the other things that are implied by this fact until we reach a fixed point. For example, if we have the following declarations:

trait A { }
trait B where Self: A { }
trait C where Self: B { }

fn foo<T: C>() {
    ...
}

then inside the foo function, we start with an environment containing only Implemented(T: C). Then because of implied bounds for the C trait, we elaborate Implemented(T: B) and add it to our environment. Because of implied bounds for the B trait, we elaborate Implemented(T: A)and add it to our environment as well. We cannot elaborate anything else, so we conclude that our final environment consists of Implemented(T: A + B + C).

In the new-style trait system, we like to encode as many things as possible with logical rules. So rather than "elaborating", we have a set of global program clauses defined like so:

forall<T> { Implemented(T: A) :- FromEnv(T: A). }

forall<T> { Implemented(T: B) :- FromEnv(T: B). }
forall<T> { FromEnv(T: A) :- FromEnv(T: B). }

forall<T> { Implemented(T: C) :- FromEnv(T: C). }
forall<T> { FromEnv(T: B) :- FromEnv(T: C). }

So these clauses are defined globally (that is, they are available from everywhere in the program) but they cannot be used because the hypothesis is always of the form FromEnv(...) which is a bit special. Indeed, as indicated by the name, FromEnv(...) facts can only come from the environment. How it works is that in the foo function, instead of having an environment containing Implemented(T: C), we replace this environment with FromEnv(T: C). From here and thanks to the above clauses, we see that we are able to reach any of Implemented(T: A), Implemented(T: B) or Implemented(T: C), which is what we wanted.

Implied bounds and well-formedness checking

Implied bounds are tightly related with well-formedness checking. Well-formedness checking is the process of checking that the impls the programmer wrote are legal, what we referred to earlier as "the compiler doing its job correctly".

We already saw examples of illegal and legal impls:

trait Foo { }
trait Bar where Self: Foo { }

struct X;
struct Y;

impl Bar for X {
    // This impl is not legal: the `Bar` trait requires that we also
    // implement `Foo`, and we didn't.
}

impl Foo for Y {
    // This impl is legal: there is nothing to check as there are no where
    // clauses on the `Foo` trait.
}

impl Bar for Y {
    // This impl is legal: we have a `Foo` impl for `Y`.
}

We must define what "legal" and "illegal" mean. For this, we introduce another predicate: WellFormed(Type: Trait). We say that the trait reference Type: Trait is well-formed if Type meets the bounds written on the Trait declaration. For each impl we write, assuming that the where clauses declared on the impl hold, the compiler tries to prove that the corresponding trait reference is well-formed. The impl is legal if the compiler manages to do so.

Coming to the definition of WellFormed(Type: Trait), it would be tempting to define it as:

trait Trait where WC1, WC2, ..., WCn {
    ...
}

forall<Type> {
    WellFormed(Type: Trait) :- WC1 && WC2 && .. && WCn.
}

and indeed this was basically what was done in rustc until it was noticed that this mixed badly with implied bounds. The key thing is that implied bounds allows someone to derive all bounds implied by a fact in the environment, and this transitively as we've seen with the A + B + C traits example. However, the WellFormed predicate as defined above only checks that the direct superbounds hold. That is, if we come back to our A + B + C example:

trait A { }
// No where clauses, always well-formed.
// forall<Type> { WellFormed(Type: A). }

trait B where Self: A { }
// We only check the direct superbound `Self: A`.
// forall<Type> { WellFormed(Type: B) :- Implemented(Type: A). }

trait C where Self: B { }
// We only check the direct superbound `Self: B`. We do not check
// the `Self: A` implied bound  coming from the `Self: B` superbound.
// forall<Type> { WellFormed(Type: C) :- Implemented(Type: B). }

There is an asymmetry between the recursive power of implied bounds and the shallow checking of WellFormed. It turns out that this asymmetry can be exploited. Indeed, suppose that we define the following traits:

trait Partial where Self: Copy { }
// WellFormed(Self: Partial) :- Implemented(Self: Copy).

trait Complete where Self: Partial { }
// WellFormed(Self: Complete) :- Implemented(Self: Partial).

impl<T> Partial for T where T: Complete { }

impl<T> Complete for T { }

For the Partial impl, what the compiler must prove is:

forall<T> {
    if (T: Complete) { // assume that the where clauses hold
        WellFormed(T: Partial) // show that the trait reference is well-formed
    }
}

Proving WellFormed(T: Partial) amounts to proving Implemented(T: Copy). However, we have Implemented(T: Complete) in our environment: thanks to implied bounds, we can deduce Implemented(T: Partial). Using implied bounds one level deeper, we can deduce Implemented(T: Copy). Finally, the Partial impl is legal.

For the Complete impl, what the compiler must prove is:

forall<T> {
    WellFormed(T: Complete) // show that the trait reference is well-formed
}

Proving WellFormed(T: Complete) amounts to proving Implemented(T: Partial). We see that the impl Partial for T applies if we can prove Implemented(T: Complete), and it turns out we can prove this fact since our impl<T> Complete for T is a blanket impl without any where clauses.

So both impls are legal and the compiler accepts the program. Moreover, thanks to the Complete blanket impl, all types implement Complete. So we could now use this impl like so:

fn eat<T>(x: T) { }

fn copy_everything<T: Complete>(x: T) {
    eat(x);
    eat(x);
}

fn main() {
    let not_copiable = vec![1, 2, 3, 4];
    copy_everything(not_copiable);
}

In this program, we use the fact that Vec<i32> implements Complete, as any other type. Hence we can call copy_everything with an argument of type Vec<i32>. Inside the copy_everything function, we have the Implemented(T: Complete) bound in our environment. Thanks to implied bounds, we can deduce Implemented(T: Partial). Using implied bounds again, we deduce Implemented(T: Copy) and we can indeed call the eat function which moves the argument twice since its argument is Copy. Problem: the T type was in fact Vec<i32> which is not copy at all, hence we will double-free the underlying vec storage so we have a memory unsoundness in safe Rust.

Of course, disregarding the asymmetry between WellFormed and implied bounds, this bug was possible only because we had some kind of self-referencing impls. But self-referencing impls are very useful in practice and are not the real culprits in this affair.

Co-inductiveness of WellFormed

So the solution is to fix this asymmetry between WellFormed and implied bounds. For that, we need for the WellFormed predicate to not only require that the direct superbounds hold, but also all the bounds transitively implied by the superbounds. What we can do is to have the following rules for the WellFormed predicate:

trait A { }
// WellFormed(Self: A) :- Implemented(Self: A).

trait B where Self: A { }
// WellFormed(Self: B) :- Implemented(Self: B) && WellFormed(Self: A).

trait C where Self: B { }
// WellFormed(Self: C) :- Implemented(Self: C) && WellFormed(Self: B).

Notice that we are now also requiring Implemented(Self: Trait) for WellFormed(Self: Trait) to be true: this is to simplify the process of traversing all the implied bounds transitively. This does not change anything when checking whether impls are legal, because since we assume that the where clauses hold inside the impl, we know that the corresponding trait reference does hold. Thanks to this setup, you can see that we indeed require to prove the set of all bounds transitively implied by the where clauses.

However there is still a catch. Suppose that we have the following trait definition:

trait Foo where <Self as Foo>::Item: Foo {
    type Item;
}

so this definition is a bit more involved than the ones we've seen already because it defines an associated item. However, the well-formedness rule would not be more complicated:

WellFormed(Self: Foo) :-
    Implemented(Self: Foo) &&
    WellFormed(<Self as Foo>::Item: Foo).

Now we would like to write the following impl:

impl Foo for i32 {
    type Item = i32;
}

The Foo trait definition and the impl Foo for i32 are perfectly valid Rust: we're kind of recursively using our Foo impl in order to show that the associated value indeed implements Foo, but that's ok. But if we translate this to our well-formedness setting, the compiler proof process inside the Foo impl is the following: it starts with proving that the well-formedness goal WellFormed(i32: Foo) is true. In order to do that, it must prove the following goals: Implemented(i32: Foo) and WellFormed(<i32 as Foo>::Item: Foo). Implemented(i32: Foo) holds because there is our impl and there are no where clauses on it so it's always true. However, because of the associated type value we used, WellFormed(<i32 as Foo>::Item: Foo) simplifies to just WellFormed(i32: Foo). So in order to prove its original goal WellFormed(i32: Foo), the compiler needs to prove WellFormed(i32: Foo): this clearly is a cycle and cycles are usually rejected by the trait solver, unless... if the WellFormed predicate was made to be co-inductive.

A co-inductive predicate, as discussed in the chapter on goals and clauses, are predicates for which the trait solver accepts cycles. In our setting, this would be a valid thing to do: indeed, the WellFormed predicate just serves as a way of enumerating all the implied bounds. Hence, it's like a fixed point algorithm: it tries to grow the set of implied bounds until there is nothing more to add. Here, a cycle in the chain of WellFormed predicates just means that there is no more bounds to add in that direction, so we can just accept this cycle and focus on other directions. It's easy to prove that under these co-inductive semantics, we are effectively visiting all the transitive implied bounds, and only these.

Implied bounds on types

We mainly talked about implied bounds for traits, but implied bounds on types are very similar. Suppose we have the following definition:

struct Type<...> where WC1, ..., WCn {
    ...
}

To prove that Type<...> is well-formed, we would need to prove a goal of the form WellFormed(Type<...>).. The WellFormed(Type<...>) predicate is defined by the rule:

forall<...> {
    WellFormed(Type<...>) :- WellFormed(WC1), ..., WellFormed(WCn).
}

Conversely, if we know a type is well-formed from our environment (for example because it appears as an argument of one of our functions), we can have implied bounds thanks to the below set of rules:

forall<...> {
    FromEnv(WC1) :- FromEnv(Type<...>).
    ...
    FromEnv(WCn) :- FromEnv(Type<...>).
}

Looking at the above rules, we see that we can never encounter a chain of deductions of the form WellFormed(Type<...>) :- ... :- WellFormed(Type<...>). So in contrast with traits, the WellFormed(Type<...>) predicate does not need to be co-inductive.

Lowering rules

This section gives the complete lowering rules for Rust traits into program clauses. It is a kind of reference. These rules reference the domain goals defined in an earlier section.

Notation

The nonterminal Pi is used to mean some generic parameter, either a named lifetime like 'a or a type parameter like A.

The nonterminal Ai is used to mean some generic argument, which might be a lifetime like 'a or a type like Vec<A>.

When defining the lowering rules, we will give goals and clauses in the notation given in this section. We sometimes insert "macros" like LowerWhereClause! into these definitions; these macros reference other sections within this chapter.

Rule names and cross-references

Each of these lowering rules is given a name, documented with a comment like so:

// Rule Foo-Bar-Baz

The reference implementation of these rules is to be found in chalk/chalk-solve/src/clauses.rs. They are also ported in rustc in the rustc_traits crate.

Lowering where clauses

When used in a goal position, where clauses can be mapped directly to the Holds variant of domain goals, as follows:

• A0: Foo<A1..An> maps to Implemented(A0: Foo<A1..An>)
• T: 'r maps to Outlives(T, 'r)
• 'a: 'b maps to Outlives('a, 'b)
• A0: Foo<A1..An, Item = T> is a bit special and expands to two distinct goals, namely Implemented(A0: Foo<A1..An>) and AliasEq(<A0 as Foo<A1..An>>::Item = T)

In the rules below, we will use WC to indicate where clauses that appear in Rust syntax; we will then use the same WC to indicate where those where clauses appear as goals in the program clauses that we are producing. In that case, the mapping above is used to convert from the Rust syntax into goals.

Transforming the lowered where clauses

In addition, in the rules below, we sometimes do some transformations on the lowered where clauses, as defined here:

• FromEnv(WC) – this indicates that:
  • Implemented(TraitRef) becomes FromEnv(TraitRef)
  • other where-clauses are left intact
• WellFormed(WC) – this indicates that:
  • Implemented(TraitRef) becomes WellFormed(TraitRef)
  • other where-clauses are left intact

TODO: I suspect that we want to alter the outlives relations too, but Chalk isn't modeling those right now.

Lowering traits

Given a trait definition

trait Trait<P1..Pn> // P0 == Self
where WC
{
    // trait items
}

we will produce a number of declarations. This section is focused on the program clauses for the trait header (i.e., the stuff outside the {}); the section on trait items covers the stuff inside the {}.

Trait header

From the trait itself we mostly make "meta" rules that setup the relationships between different kinds of domain goals. The first such rule from the trait header creates the mapping between the FromEnv and Implemented predicates:

// Rule Implemented-From-Env
forall<Self, P1..Pn> {
  Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>)
}

Implied bounds

The next few clauses have to do with implied bounds (see also RFC 2089 and the implied bounds chapter for a more in depth cover). For each trait, we produce two clauses:

// Rule Implied-Bound-From-Trait
//
// For each where clause WC:
forall<Self, P1..Pn> {
  FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)
}

This clause says that if we are assuming that the trait holds, then we can also assume that its where-clauses hold. It's perhaps useful to see an example:

trait Eq: PartialEq { ... }

In this case, the PartialEq supertrait is equivalent to a where Self: PartialEq where clause, in our simplified model. The program clause above therefore states that if we can prove FromEnv(T: Eq) – e.g., if we are in some function with T: Eq in its where clauses – then we also know that FromEnv(T: PartialEq). Thus the set of things that follow from the environment are not only the direct where clauses but also things that follow from them.

The next rule is related; it defines what it means for a trait reference to be well-formed:

// Rule WellFormed-TraitRef
forall<Self, P1..Pn> {
  WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)
}

This WellFormed rule states that T: Trait is well-formed if (a) T: Trait is implemented and (b) all the where-clauses declared on Trait are well-formed (and hence they are implemented). Remember that the WellFormed predicate is coinductive; in this case, it is serving as a kind of "carrier" that allows us to enumerate all the where clauses that are transitively implied by T: Trait.

An example:

trait Foo: A + Bar { }
trait Bar: B + Foo { }
trait A { }
trait B { }

Here, the transitive set of implications for T: Foo are T: A, T: Bar, and T: B. And indeed if we were to try to prove WellFormed(T: Foo), we would have to prove each one of those:

• WellFormed(T: Foo)
  • Implemented(T: Foo)
  • WellFormed(T: A)
    • Implemented(T: A)
  • WellFormed(T: Bar)
    • Implemented(T: Bar)
    • WellFormed(T: B)
      • Implemented(T: Bar)
    • WellFormed(T: Foo) -- cycle, true coinductively

This WellFormed predicate is only used when proving that impls are well-formed – basically, for each impl of some trait ref TraitRef, we must show that WellFormed(TraitRef). This in turn justifies the implied bounds rules that allow us to extend the set of FromEnv items.

Lowering type definitions

We also want to have some rules which define when a type is well-formed. For example, given this type:

struct Set<K> where K: Hash { ... }

then Set<i32> is well-formed because i32 implements Hash, but Set<NotHash> would not be well-formed. Basically, a type is well-formed if its parameters verify the where clauses written on the type definition.

Hence, for every type definition:

struct Type<P1..Pn> where WC { ... }

we produce the following rule:

// Rule WellFormed-Type
forall<P1..Pn> {
  WellFormed(Type<P1..Pn>) :- WellFormed(WC)
}

Note that we use struct to define a type, but this should be understood as a general type definition (it could be e.g. a generic enum).

Conversely, we define rules which say that if we assume that a type is well-formed, we can also assume that its where clauses hold. That is, we produce the following family of rules:

// Rule Implied-Bound-From-Type
//
// For each where clause `WC`
forall<P1..Pn> {
  FromEnv(WC) :- FromEnv(Type<P1..Pn>)
}

As for the implied bounds RFC, functions will assume that their arguments are well-formed. For example, suppose we have the following bit of code:

trait Hash: Eq { }
struct Set<K: Hash> { ... }

fn foo<K>(collection: Set<K>, x: K, y: K) {
    // `x` and `y` can be equalized even if we did not explicitly write
    // `where K: Eq`
    if x == y {
        ...
    }
}

In the foo function, we assume that Set<K> is well-formed, i.e. we have FromEnv(Set<K>) in our environment. Because of the previous rule, we get FromEnv(K: Hash) without needing an explicit where clause. And because of the Hash trait definition, there also exists a rule which says:

forall<K> {
  FromEnv(K: Eq) :- FromEnv(K: Hash)
}

which means that we finally get FromEnv(K: Eq) and then can compare x and y without needing an explicit where clause.

Lowering trait items

Associated type declarations

Given a trait that declares a (possibly generic) associated type:

trait Trait<P1..Pn> // P0 == Self
where WC
{
    type AssocType<Pn+1..Pm>: Bounds where WC1;
}

We will produce a number of program clauses. The first two define the rules by which AliasEq for associated type projections can succeed; these two clauses are discussed in detail in the section on associated types, but reproduced here for reference:

// Rule AliasEq-Normalize
//
// AliasEq can succeed by normalizing:
forall<Self, P1..Pn, Pn+1..Pm, U> {
  AliasEq(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> = U) :-
      Normalize(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> -> U)
}

// Rule AliasEq-Placeholder
//
// AliasEq can succeed through the placeholder associated type,
// see "associated type" chapter for more:
forall<Self, P1..Pn, Pn+1..Pm> {
  AliasEq(
    <Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> =
    (Trait::AssocType)<Self, P1..Pn, Pn+1..Pm>
  )
}

The next rule covers implied bounds for the projection. In particular, the Bounds declared on the associated type must have been proven to hold to show that the impl is well-formed, and hence we can rely on them elsewhere.

// Rule Implied-Bound-From-AssocTy
//
// For each `Bound` in `Bounds`:
forall<Self, P1..Pn, Pn+1..Pm> {
    FromEnv(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm>>: Bound) :-
      FromEnv(Self: Trait<P1..Pn>) && WC1
}

Next, we define the requirements for an instantiation of our associated type to be well-formed...

// Rule WellFormed-AssocTy
forall<Self, P1..Pn, Pn+1..Pm> {
    WellFormed((Trait::AssocType)<Self, P1..Pn, Pn+1..Pm>) :-
      WellFormed(Self: Trait<P1..Pn>) && WellFormed(WC1)
}

...along with the reverse implications, when we can assume that it is well-formed.

// Rule Implied-WC-From-AssocTy
//
// For each where clause WC1:
forall<Self, P1..Pn, Pn+1..Pm> {
    FromEnv(WC1) :- FromEnv((Trait::AssocType)<Self, P1..Pn, Pn+1..Pm>)
}

// Rule Implied-Trait-From-AssocTy
forall<Self, P1..Pn, Pn+1..Pm> {
    FromEnv(Self: Trait<P1..Pn>) :-
      FromEnv((Trait::AssocType)<Self, P1..Pn, Pn+1..Pm>)
}

Lowering function and constant declarations

Chalk didn't model functions and constants, but I would eventually like to treat them exactly like normalization. See the section on function/constant values below for more details.

Lowering impls

Given an impl of a trait:

impl<P0..Pn> Trait<A1..An> for A0
where WC
{
    // zero or more impl items
}

Let TraitRef be the trait reference A0: Trait<A1..An>. Then we will create the following rules:

// Rule Implemented-From-Impl
forall<P0..Pn> {
  Implemented(TraitRef) :- WC
}

In addition, we will lower all of the impl items.

Lowering impl items

Associated type values

Given an impl that contains:

impl<P0..Pn> Trait<P1..Pn> for P0
where WC_impl
{
    type AssocType<Pn+1..Pm> = T;
}

and our where clause WC1 on the trait associated type from above, we produce the following rule:

// Rule Normalize-From-Impl
forall<P0..Pm> {
  forall<Pn+1..Pm> {
    Normalize(<P0 as Trait<P1..Pn>>::AssocType<Pn+1..Pm> -> T) :-
      Implemented(P0 as Trait) && WC1
  }
}

Note that WC_impl and WC1 both encode where-clauses that the impl can rely on. (WC_impl is not used here, because it is implied by Implemented(P0 as Trait).)

Function and constant values

Chalk didn't model functions and constants, but I would eventually like to treat them exactly like normalization. This presumably involves adding a new kind of parameter (constant), and then having a NormalizeValue domain goal. This is to be written because the details are a bit up in the air.

Opaque types (impl Trait)

This chapter describes how "opaque types" are modeled in chalk. Opaque types are the underlying concept used to implement "existential impl Trait" in Rust. They don't have a direct surface syntax, but uses of impl Trait in particular source locations create a hidden opaque type:

fn as_u32s<'a, T: Copy + Into<u32>>(
    elements: &'a [T],
) -> impl Iterator<Item = u32> + 'a {
    elements.iter().cloned().map(|e| -> u32 { e.into() })
}

fn main() {
   let x: &[u16] = &[1, 2, 3];
   let y = as_u32s(&x);
   for e in y {
       println!("e = {}", e);
   }
}

Conceptually, the function as_u32s is desugared to return a reference to an opaque type, let's call it AsU32sReturn (note that this is not valid Rust syntax):

opaque type AsU32sReturn<'a, T>: IntoIterator<Item = u32> + 'a
where
    T: Copy + Into<u32>;

fn as_u32s<'a, T: Copy + Into<u32>>(
    elements: &'a [T],
) -> AsU32sReturn<'a, T> {
    ...
}

Opaque types are a kind of type alias. They are called opaque because, unlike an ordinary type alias, most Rust code (e.g., the callers of as_u32s) doesn't know what type AsU32sReturn represents. It only knows what traits that type implements (e.g., IntoIterator<Item = u32>). The actual type that is inferred for AsU32sReturn is called the "hidden type".

Chalk syntax for an opaque type declaration

Although the above is not valid Rust syntax, it is quite close to the format that chalk unit tests use, which looks something like this:

opaque type OpaqueTypeName<P0..Pn>: /* bounds */
where
    /* where clauses */
= /* hidden type */;

A chalk opaque type declaration has several parts:

• The name OpaqueTypeName, which is the name we use to refer to the opaque type within the chalk file. In real Rust opaque types are not explicitly declared and hence they are identified just by internal ids (i.e., they are anonymous in the same way that a closure type is anonymous), so this is just for unit testing.
• The generic parameters P0..Pn. In real Rust, these parameters are inherited from the context in which the impl Trait appeared. In our example, these parameters come from the surrounding function. Note that in real Rust the set of generic parameters is a subset of those that appear on the surrounding function: in particular, lifetime parameters may not appear unless they explicitly appear in the opaque type's bounds.
• The bounds, which would be IntoIterator<Item = u32> + 'a in our example. These are traits that the hidden type (see below) is supposed to implement. They come from the impl IntoIterator<Item = u32> + 'a type. Even when the hidden type is, well, hidden, we can assume that the bounds hold.
• The where clauses, which would be T: Copy and T: Into<u32> in our example. These are conditions that must hold on V0..Vn for OpaqueTypeName<V0..Vn> to be a valid type.
  • Note that this contrasts with bounds: bounds are things that the hidden type must meet but which the rest of the code can assume to be true. Where clauses are things that the rest of the code must prove to be true in order to use the opaque type. In our example, then, a type like AsU32sReturn<'a, String> would be invalid because String: Copy does not hold.

Representing opaque types in chalk types

We represent opaque types as a kind of type alias. Like any type alias, we have to define the conditions in which they can be normalized:

Placeholder rules

Well known traits

For most traits, the question of whether some type T implements the trait is determined by looking solely at the impls that exist for the trait. But there are some well-known traits where we have "built-in" impls that are never expressly written in the compiler, they are built-in to the language itself. In some cases, these impls also encode complex conditions that an ordinary impl cannot express. To address this, chalk has a notion of a WellKnownTrait -- basically, a trait which is inherent to the language and where we will generate custom logic.

As an example, consider the logic for Sized in regards to structs: A struct can have at most one !Sized field, and it must be the last. And the last field isn't Sized, then neither is the struct itself.

Chalk has two main places that deal with well known trait logic:

1. chalk-solve\clauses\builtin_traits, which generates built-in implementations for well-known traits.
2. well-formedness checks, some of which need to know about well known traits.

Auto traits

Auto traits, while not exactly well known traits, do also have special logic. The idea is that the type implements an auto trait if all data owned by that type implements it, with an ability to specifically opt-out or opt-in. Additionally, auto traits are coinductive. Some common examples of auto traits are Send and Sync.

Current state

legend:
⚬ - not applicable
✅ - implemented
📚 - implementation provided in libcore
❌ - not implemented

❌ after a type name means that type is not yet in chalk

Well-formedness checking

WF checking has the job of checking that the various declarations in a Rust program are well-formed. This is the basis for implied bounds, and partly for that reason, this checking can be surprisingly subtle! For example, we have to be sure that each impl proves the WF conditions declared on the trait.

For each declaration in a Rust program, we will generate a logical goal and try to prove it using the lowered rules we described in the lowering rules chapter. If we are able to prove it, we say that the construct is well-formed. If not, we report an error to the user.

Well-formedness checking happens in the chalk/chalk-solve/src/wf.rs module in chalk. After you have read this chapter, you may find useful to see an extended set of examples in the chalk/tests/test/wf_lowering.rs submodule.

The new-style WF checking has not been implemented in rustc yet.

We give here a complete reference of the generated goals for each Rust declaration.

In addition to the notations introduced in the chapter about lowering rules, we'll introduce another notation: when checking WF of a declaration, we'll often have to prove that all types that appear are well-formed, except type parameters that we always assume to be WF. Hence, we'll use the following notation: for a type SomeType<...>, we define InputTypes(SomeType<...>) to be the set of all non-parameter types appearing in SomeType<...>, including SomeType<...> itself.

Examples:

• InputTypes((u32, f32)) = [u32, f32, (u32, f32)]
• InputTypes(Box<T>) = [Box<T>] (assuming that T is a type parameter)
• InputTypes(Box<Box<T>>) = [Box<T>, Box<Box<T>>]

We also extend the InputTypes notation to where clauses in the natural way. So, for example InputTypes(A0: Trait<A1,...,An>) is the union of InputTypes(A0), InputTypes(A1), ..., InputTypes(An).

Type definitions

Given a general type definition:

struct Type<P...> where WC_type {
    field1: A1,
    ...
    fieldn: An,
}

we generate the following goal, which represents its well-formedness condition:

forall<P...> {
    if (FromEnv(WC_type)) {
        WellFormed(InputTypes(WC_type)) &&
            WellFormed(InputTypes(A1)) &&
            ...
            WellFormed(InputTypes(An))
    }
}

which in English states: assuming that the where clauses defined on the type hold, prove that every type appearing in the type definition is well-formed.

Some examples:

struct OnlyClone<T> where T: Clone {
    clonable: T,
}
// The only types appearing are type parameters: we have nothing to check,
// the type definition is well-formed.

struct Foo<T> where T: Clone {
    foo: OnlyClone<T>,
}
// The only non-parameter type which appears in this definition is
// `OnlyClone<T>`. The generated goal is the following:
// ```
// forall<T> {
//     if (FromEnv(T: Clone)) {
//          WellFormed(OnlyClone<T>)
//     }
// }
// ```
// which is provable.

struct Bar<T> where <T as Iterator>::Item: Debug {
    bar: i32,
}
// The only non-parameter types which appear in this definition are
// `<T as Iterator>::Item` and `i32`. The generated goal is the following:
// ```
// forall<T> {
//     if (FromEnv(<T as Iterator>::Item: Debug)) {
//          WellFormed(<T as Iterator>::Item) &&
//               WellFormed(i32)
//     }
// }
// ```
// which is not provable since `WellFormed(<T as Iterator>::Item)` requires
// proving `Implemented(T: Iterator)`, and we are unable to prove that for an
// unknown `T`.
//
// Hence, this type definition is considered illegal. An additional
// `where T: Iterator` would make it legal.

Trait definitions

Given a general trait definition:

trait Trait<P1...> where WC_trait {
    type Assoc<P2...>: Bounds_assoc where WC_assoc;
}

we generate the following goal:

forall<P1...> {
    if (FromEnv(WC_trait)) {
        WellFormed(InputTypes(WC_trait)) &&

            forall<P2...> {
                if (FromEnv(WC_assoc)) {
                    WellFormed(InputTypes(Bounds_assoc)) &&
                        WellFormed(InputTypes(WC_assoc))
                }
            }
    }
}

There is not much to verify in a trait definition. We just want to prove that the types appearing in the trait definition are well-formed, under the assumption that the different where clauses hold.

Some examples:

trait Foo<T> where T: Iterator, <T as Iterator>::Item: Debug {
    ...
}
// The only non-parameter type which appears in this definition is
// `<T as Iterator>::Item`. The generated goal is the following:
// ```
// forall<T> {
//     if (FromEnv(T: Iterator), FromEnv(<T as Iterator>::Item: Debug)) {
//         WellFormed(<T as Iterator>::Item)
//     }
// }
// ```
// which is provable thanks to the `FromEnv(T: Iterator)` assumption.

trait Bar {
    type Assoc<T>: From<<T as Iterator>::Item>;
}
// The only non-parameter type which appears in this definition is
// `<T as Iterator>::Item`. The generated goal is the following:
// ```
// forall<T> {
//     WellFormed(<T as Iterator>::Item)
// }
// ```
// which is not provable, hence the trait definition is considered illegal.

trait Baz {
    type Assoc<T>: From<<T as Iterator>::Item> where T: Iterator;
}
// The generated goal is now:
// ```
// forall<T> {
//     if (FromEnv(T: Iterator)) {
//         WellFormed(<T as Iterator>::Item)
//     }
// }
// ```
// which is now provable.

Impls

Now we give ourselves a general impl for the trait defined above:

impl<P1...> Trait<A1...> for SomeType<A2...> where WC_impl {
    type Assoc<P2...> = SomeValue<A3...> where WC_assoc;
}

Note that here, WC_assoc are the same where clauses as those defined on the associated type definition in the trait declaration, except that type parameters from the trait are substituted with values provided by the impl (see example below). You cannot add new where clauses. You may omit to write the where clauses if you want to emphasize the fact that you are actually not relying on them.

Some examples to illustrate that:

trait Foo<T> {
    type Assoc where T: Clone;
}

struct OnlyClone<T: Clone> { ... }

impl<U> Foo<Option<U>> for () {
    // We substitute type parameters from the trait by the ones provided
    // by the impl, that is instead of having a `T: Clone` where clause,
    // we have an `Option<U>: Clone` one.
    type Assoc = OnlyClone<Option<U>> where Option<U>: Clone;
}

impl<T> Foo<T> for i32 {
    // I'm not using the `T: Clone` where clause from the trait, so I can
    // omit it.
    type Assoc = u32;
}

impl<T> Foo<T> for f32 {
    type Assoc = OnlyClone<Option<T>> where Option<T>: Clone;
    //                                ^^^^^^^^^^^^^^^^^^^^^^
    //                                this where clause does not exist
    //                                on the original trait decl: illegal
}

So in Rust, where clauses on associated types work exactly like where clauses on trait methods: in an impl, we must substitute the parameters from the traits with values provided by the impl, we may omit them if we don't need them, but we cannot add new where clauses.

Now let's see the generated goal for this general impl:

forall<P1...> {
    // Well-formedness of types appearing in the impl
    if (FromEnv(WC_impl), FromEnv(InputTypes(SomeType<A2...>: Trait<A1...>))) {
        WellFormed(InputTypes(WC_impl)) &&

            forall<P2...> {
                if (FromEnv(WC_assoc)) {
                        WellFormed(InputTypes(SomeValue<A3...>))
                }
            }
    }

    // Implied bounds checking
    if (FromEnv(WC_impl), FromEnv(InputTypes(SomeType<A2...>: Trait<A1...>))) {
        WellFormed(SomeType<A2...>: Trait<A1...>) &&

            forall<P2...> {
                if (FromEnv(WC_assoc)) {
                    WellFormed(SomeValue<A3...>: Bounds_assoc)
                }
            }
    }
}

Here is the most complex goal. As always, first, assuming that the various where clauses hold, we prove that every type appearing in the impl is well-formed, except types appearing in the impl header SomeType<A2...>: Trait<A1...>. Instead, we assume that those types are well-formed (hence the if (FromEnv(InputTypes(SomeType<A2...>: Trait<A1...>))) conditions). This is part of the implied bounds proposal, so that we can rely on the bounds written on the definition of e.g. the SomeType<A2...> type (and that we don't need to repeat those bounds).

Note that we don't need to check well-formedness of types appearing in WC_assoc because we already did that in the trait decl (they are just repeated with some substitutions of values which we already assume to be well-formed)

Next, still assuming that the where clauses on the impl WC_impl hold and that the input types of SomeType<A2...> are well-formed, we prove that WellFormed(SomeType<A2...>: Trait<A1...>) hold. That is, we want to prove that SomeType<A2...> verify all the where clauses that might transitively be required by the Trait definition (see this subsection).

Lastly, assuming in addition that the where clauses on the associated type WC_assoc hold, we prove that WellFormed(SomeValue<A3...>: Bounds_assoc) hold. Again, we are not only proving Implemented(SomeValue<A3...>: Bounds_assoc), but also all the facts that might transitively come from Bounds_assoc. We must do this because we allow the use of implied bounds on associated types: if we have FromEnv(SomeType: Trait) in our environment, the lowering rules chapter indicates that we are able to deduce FromEnv(<SomeType as Trait>::Assoc: Bounds_assoc) without knowing what the precise value of <SomeType as Trait>::Assoc is.

Some examples for the generated goal:

// Trait Program Clauses

// These are program clauses that come from the trait definitions below
// and that the trait solver can use for its reasonings. I'm just restating
// them here so that we have them in mind.

trait Copy { }
// This is a program clause that comes from the trait definition above
// and that the trait solver can use for its reasonings. I'm just restating
// it here (and also the few other ones coming just after) so that we have
// them in mind.
// `WellFormed(Self: Copy) :- Implemented(Self: Copy).`

trait Partial where Self: Copy { }
// ```
// WellFormed(Self: Partial) :-
//     Implemented(Self: Partial) &&
//     WellFormed(Self: Copy).
// ```

trait Complete where Self: Partial { }
// ```
// WellFormed(Self: Complete) :-
//     Implemented(Self: Complete) &&
//     WellFormed(Self: Partial).
// ```

// Impl WF Goals

impl<T> Partial for T where T: Complete { }
// The generated goal is:
// ```
// forall<T> {
//     if (FromEnv(T: Complete)) {
//         WellFormed(T: Partial)
//     }
// }
// ```
// Then proving `WellFormed(T: Partial)` amounts to proving
// `Implemented(T: Partial)` and `Implemented(T: Copy)`.
// Both those facts can be deduced from the `FromEnv(T: Complete)` in our
// environment: this impl is legal.

impl<T> Complete for T { }
// The generated goal is:
// ```
// forall<T> {
//     WellFormed(T: Complete)
// }
// ```
// Then proving `WellFormed(T: Complete)` amounts to proving
// `Implemented(T: Complete)`, `Implemented(T: Partial)` and
// `Implemented(T: Copy)`.
//
// `Implemented(T: Complete)` can be proved thanks to the
// `impl<T> Complete for T` blanket impl.
//
// `Implemented(T: Partial)` can be proved thanks to the
// `impl<T> Partial for T where T: Complete` impl and because we know
// `T: Complete` holds.

// However, `Implemented(T: Copy)` cannot be proved: the impl is illegal.
// An additional `where T: Copy` bound would be sufficient to make that impl
// legal.

trait Bar { }

impl<T> Bar for T where <T as Iterator>::Item: Bar { }
// We have a non-parameter type appearing in the where clauses:
// `<T as Iterator>::Item`. The generated goal is:
// ```
// forall<T> {
//     if (FromEnv(<T as Iterator>::Item: Bar)) {
//         WellFormed(T: Bar) &&
//             WellFormed(<T as Iterator>::Item: Bar)
//     }
// }
// ```
// And `WellFormed(<T as Iterator>::Item: Bar)` is not provable: we'd need
// an additional `where T: Iterator` for example.

trait Foo { }

trait Bar {
    type Item: Foo;
}

struct Stuff<T> { }

impl<T> Bar for Stuff<T> where T: Foo {
    type Item = T;
}
// The generated goal is:
// ```
// forall<T> {
//     if (FromEnv(T: Foo)) {
//         WellFormed(T: Foo).
//     }
// }
// ```
// which is provable.

trait Debug { ... }
// `WellFormed(Self: Debug) :- Implemented(Self: Debug).`

struct Box<T> { ... }
impl<T> Debug for Box<T> where T: Debug { ... }

trait PointerFamily {
    type Pointer<T>: Debug where T: Debug;
}
// `WellFormed(Self: PointerFamily) :- Implemented(Self: PointerFamily).`

struct BoxFamily;

impl PointerFamily for BoxFamily {
    type Pointer<T> = Box<T> where T: Debug;
}
// The generated goal is:
// ```
// forall<T> {
//     WellFormed(BoxFamily: PointerFamily) &&
//
//     if (FromEnv(T: Debug)) {
//         WellFormed(Box<T>: Debug) &&
//             WellFormed(Box<T>)
//     }
// }
// ```
// `WellFormed(BoxFamily: PointerFamily)` amounts to proving
// `Implemented(BoxFamily: PointerFamily)`, which is ok thanks to our impl.
//
// `WellFormed(Box<T>)` is always true (there are no where clauses on the
// `Box` type definition).
//
// Moreover, we have an `impl<T: Debug> Debug for Box<T>`, hence
// we can prove `WellFormed(Box<T>: Debug)` and the impl is indeed legal.

trait Foo {
    type Assoc<T>;
}

struct OnlyClone<T: Clone> { ... }

impl Foo for i32 {
    type Assoc<T> = OnlyClone<T>;
}
// The generated goal is:
// ```
// forall<T> {
//     WellFormed(i32: Foo) &&
//        WellFormed(OnlyClone<T>)
// }
// ```
// however `WellFormed(OnlyClone<T>)` is not provable because it requires
// `Implemented(T: Clone)`. It would be tempting to just add a `where T: Clone`
// bound inside the `impl Foo for i32` block, however we saw that it was
// illegal to add where clauses that didn't come from the trait definition.

Chalk Coherence

This document was previously prepared for the initial design of coherence rules in Chalk. It was copy-pasted here on 2020-10-06, but has not been vetted for accuracy of the current implementation or edited for clarity.

Coherence

The idea of trait coherence is that, given a trait and some set of types for its type parameters, there should be exactly one impl that applies. So if we think of the trait Display, we want to guarantee that if we have a trait reference like MyType : Display, we can uniquely identify a particular impl.

The role of the orphan rules in particular is basically to prevent you from implementing external traits for external types. So continuing our simple example of Display, if you are defining your own library, you could not implement Display for Vec<T>, because both Display and Vec are defined in the standard library. But you can implement Display for MyType, because you defined MyType. However, if you define your own trait MyTrait, then you can implement MyTrait for any type you like, including external types like Vec<T>. To this end, the orphan rule intuitively says “either the trait must be local or the self-type must be local”.

-- Little Orphan Impls by Niko Matsakis

To check for coherence, the Rust compiler completes two separate but related checks:

• orphan check - ensures that each impl abides by the orphan rules, or in other words, that an impl is potentially implementable by the crate adding it
  • A consequence of the orphan rules: for every impl that could exist, it only exists in one place — this is key to having a coherent system
• overlap check - ensures that no two impls overlap in your program or in any compatible world
  • compatible - any semver compatible world

Resources About Coherence

• Coherence - talk by withoutboats
• Little Orphan Impls
• RFC 1023 Rebalancing Coherence
• Type classes: confluence, coherence and global uniqueness

Axioms & Properties of Coherence

Historical Note: We used to use the term “external” instead of “upstream”.

• Axiom 1: crates upstream to you should be able to implement their own traits for their own types
• Axiom 2: crates downstream from you should be able to implement your traits
• Property: Upstream crates must assume that downstream crates will add any impls that compile. Downstream crates are allowed to assume that upstream crates will not add any semver incompatible impls.

Chalk: Orphan Check

The purpose of the orphan check is to ensure that an impl is only definable in a single crate. This check is what makes it impossible for other crates to define impls of your traits for your types.

We want to capture some rule: Given impl<T0…Tn> for Trait<P1…Pn> for P0, LocalImplAllowed(P0: Trait<P1…Pn>) is true if and only if this impl is allowed in the current (local) crate.

This check is applied to all impls in the current crate. Upstream impls are not checked with this rule.

The Orphan Rules

In order to model the orphan check in chalk, we need a precise description of the orphan rules as they are implemented in rustc today.

There are several resources which can be used to figure out the orphan rules in rustc.

• RFC 1023: Rebalancing Coherence
• Trait Implementation Coherence in the Rust Reference
• E0210: A violation of the orphan rules in the Rust Error Index
• Little Orphan Impls by Niko Matsakis

Of all of these, RFC 1023 is probably considered the most authoritative source on the orphan rules. The orphan rules as proposed in that RFC are as follows:

Given an impl impl<T1...Tn> Trait<P1...Pn> for P0, either Trait must be local to the current crate, or:

1. At least one type must meet the LT pattern defined above. Let Pi be the first such type.
2. No type parameters T1...Tn may appear in the type parameters that precede Pi (that is, Pj where j < i).

The LT pattern being referred to basically means that the type is a “local type” including the affects of fundamental types. That means that Ti is either a local type, or a fundamental type whose first parameter is a local type.

This definition is good. Once you read it a few times and it makes sense, it is fairly unambiguous. That being said, the RFC was written quite a while ago and we have since found unsoundness in some of the parts of the compiler that were implemented based on that RFC.

Thus, it is probably best to look at the only truly authoritative source on the Rust compiler: the rustc source code itself! Indeed, if you think of the rustc source code as an executable specification of how the Rust programming language is meant to work, you can look at it and determine the true behaviour of the orphan rules.

The Orphan Check in rustc

The orphan check as implemented today in the Rust compiler takes place in the orphan_check function which is called for every declared impl. Since implementations for locally defined traits are always defined, that function returns OK if the trait being implemented is local. Otherwise, it dispatches to the orphan_check_trait_ref function which does the major orphan rules checking.

Recall that the impls we are dealing with are in the form impl<T0…Tn> Trait<P1…Pn> for P0.

The orphan_check_trait_ref function takes a trait ref which is essentially Trait and its parameters P0…Pn (notice that the Self type P0 is included). The parameters P0…Pn are known as the input types of the trait. The function goes through each input type from P0 to Pn looking for the first local type Pi. For each type parameter Pj found before that, the function checks that it does not contain any of the placeholder types T0…Tn at any level. That means that Pj cannot have any of the types T0…Tn at any level recursively. When the first local type Pi is found, we check to make sure any type parameters used in it are covered by a local type. Since we don’t have any fundamental types with more than one type parameter, this check is probably extraneous.

The Orphan Rules in rustc

Thus, based on the source code, the orphan rules in Rust are as follows:

Given an impl of the form impl<T0…Tn> Trait<P1…Pn> for P0, the impl is allowed if:

• Trait is local to the current crate
• Trait is upstream to the current crate and:
  • There is at least one type parameter Pi which, taking fundamental types into account, is local to the current crate
  • Within the type Pi, all type parameters are covered by Pi
    • This only really applies if we allowed fundamental types with multiple type parameters
    • Since we don’t do that yet, we can ignore this for the time being
  • All types Pj such that j < i do not contain T0…Tn at any level of depth (i.e. the types are fully visible — “visible” meaning that the type is a known type and not a type parameter or variable)

Modeling The Orphan Check

Determining how to model these rules in chalk is actually quite straightforward at this point. We have an exact specification of how the rules are meant to work and we can translate that directly.

Here’s how the lowering rules would look:

For each trait Trait,

• If Trait is local to the current crate, we generate: forall<Self, P1…Pn> { LocalImplAllowed(Self: Trait<P1...Pn>) } This models that any impls are allowed if the trait is local to the current crate.
• If Trait is upstream to the current crate, we need a rule which models the additional conditions on which impls are allowed:

forall<Self, P1...Pn> { LocalImplAllowed(Self: Trait<P1...Pn>) :- IsLocal(Self) }
forall<Self, P1...Pn> {
  LocalImplAllowed(Self: Trait<P1...Pn>) :- IsFullyVisible(Self), IsLocal(P1)
}
forall<Self, P1...Pn> {
  LocalImplAllowed(Self: Trait<P1...Pn>) :-
    IsFullyVisible(Self),
    IsFullyVisible(P1),
    IsLocal(P2)
}
forall<Self, P1...Pn> {
  LocalImplAllowed(Self: Trait<P1...Pn>) :-
    IsFullyVisible(Self),
    IsFullyVisible(P1),
    IsFullyVisible(P2),
    IsLocal(P3)
}
...
forall<Self, P1...Pn> {
  LocalImplAllowed(Self: Trait<P1...Pn>) :-
    IsFullyVisible(Self),
    IsFullyVisible(P1),
    IsFullyVisible(P2),
    ...
    IsFullyVisible(Pn-1),
    IsLocal(Pn)
}

Here, we have modeled every possible case of P1 to Pn being local and then checked if all prior type parameters are fully visible. This truly is a direct translation of the rules listed above!

Now, to complete the orphan check, we can iterate over each impl of the same form as before and check if LocalImplAllowed(P0: Trait<P1…Pn>) is provable.

Chalk: Overlap Check

Note: A key assumption for the overlap check is that the orphan check runs before it. That means that any impl that the overlap check encounters already abides by the orphan rules. This is very important to how the check works and it wouldn’t work without the orphan check also present before it.

The purpose of the overlap check is to ensure that there is only up to one impl that can apply to a method call at a given time. In order to accomplish this, the overlap check looks at all pairs of impls and tries to ensure that there is no “overlap” between the sets of types that both impls can apply to. It accomplishes this by attempting to take the “intersection” of the constraints of both impls and then ensuring that this intersection cannot possibly apply to any types. If this turns out to be provable, the types are truly disjoint.

This is a simple application of the mathematical law:

If two sets A and B are disjoint, then A ∩ B = ∅

More concretely, let’s say you have the following two impls: (example from RFC 1023)

impl<T: Copy> Clone for T { /* ... */ }
impl<U> Clone for MyType<U> { /* ... */ }

Then we’ll try to solve the following:

not { exists<T, U> { T = MyType<U>, T: Copy } }

One way to read this is to say “try to prove that there is no MyType<U> for any U that implements the Copy trait”. The reason we’re trying to prove this is because if there is such an implementation, then the second impl would overlap with the first one. The first impl applies to any type that implements Copy.

The issue is that there may very well not be any such impl at this current time. In that case, chalk will conclude that these two impls do not overlap. This is an issue because that is certainly an impl that could be added later, so this conclusion may be too strong.

Why is that we’re only saying that this conclusion may be too strong? Well we’re using “may” because it depends on what we want to assume about different crates. The orphan rules make it so that upstream crates can add certain impls to themselves in a semver compatible way. In particular, upstream crates can add impls of upstream traits for their own upstream types without having to worry about breaking downstream code. That means that we can’t just assume that upstream type doesn’t implement an upstream trait. This particular assumption is too strong.

On the other hand, the orphan rules permit the current crate to add certain impls as well. A property of the orphan rules is that the impls it allows are only allowed to be defined in a single crate. So that means that if the impls allowed by the orphan rules in the current crate don’t exist, it is perfectly safe to assume that they are not there.

The conclusion from all of this is that it is perfectly safe to rule out impls that can be defined in the current crate, but we can’t do the same for impls in any other crate. That means that we need to come up with a way to model all possible impls in upstream, downstream and even sibling crates so we can make sure that our overlap check isn’t making assumptions that are too strong.

Clarification: One caveat to all of this is that we can’t simply model “all possible impls” because then the current crate wouldn’t be able to add any impls at all for upstream traits. After all, it is possible for an upstream crate to add any impl for its upstream trait. A more precise version of what we’re looking for is to model impls that an upstream crate could add in a compatible way. These are impls that we may not be able to current see, but also cannot ignore since that would be too strong of an assumption.

We are specifically trying to avoid a situation where a semver compatible upgrade of a dependency breaks the current crate because the current crate was able to add an impl that only the dependency was meant to be able to add.

Sibling Crates: Furthermore, we can immediately rule out sibling crates because by definition they are unable to use each other’s types or traits. If two crates are unable to interact at all, they cannot possibly add a conflicting implementation in any coherent world. Proof: Suppose that a sibling crate could add an impl that would conflict with a conclusion drawn by the overlap check in the current crate. Then the sibling crate would have to be able to implement a trait that was available to the current crate for a type that was available for the current crate. Since the sibling crate by definition does not have access to the current crate’s types or traits, the conflicting type and trait must be upstream. By the orphan rules, the sibling crate cannot implement a trait for upstream types and traits. Thus, the conflicting implementation in the sibling crate is impossible and no such implementation can exist.

Downstream Crates: Downstream crates come into play because all traits in upstream crates and in the current crate can potentially be implemented by downstream crates using the forms allowed by the orphan rules. In essence, we always need to assume that downstream crates will implement traits in all ways that compile.

Discussion: Modeling the Overlap Check

Aaron’s excellent blog post talks about this exact problem from the point of view of negative reasoning. It also describes a potential solution which we will apply here to solve our problem.

The compatible modality (compat in Aaron’s blog post) is necessary because we don’t always want to assume that all compatible impls exist. In particular, there are certain phases of compilation (e.g. trans) where the closed-world assumption is entirely necessary and sufficient.

To start addressing the problem at hand, the question is: what implementations are crates other than the current crate allowed to add in a semver compatible way?

Since we already ruled out sibling crates, this only leaves upstream crates and downstream crates. Upstream crates only have access to upstream types and traits. That means that the only impls they can add are impls for upstream types or blanket impls over type parameters. Downstream crates have access to all upstream traits and types in addition to all traits and types in the current crate.

Claim: No impl containing generic types can be added in a semver compatible way. Proof: If the impl contains only generic types, it is considered a blanket impl and it may already be that a downstream trait implements that trait. So by adding a blanket impl, it now conflicts with the potential downstream implementation and is thus a breaking change. If the impl contains a generic type and also some number of upstream types, then a downstream crate may still have implemented that trait for all of the same values of the type parameters but with the generic types filled with downstream types. Thus, adding such an impl would also be a breaking change that would conflict with that potential downstream impl.

The only situation where an impl containing generic types can be added in a way that is not a breaking change is if in addition to the impl, a new type is also added to the upstream crate. In that case, downstream crates would not have had an opportunity to implement that trait for those types just yet. All of that being said, from the perspective of the current crate looking at potential upstream impls, this case does not matter at all because the current crate can never query for a type that doesn’t exist yet. That means that this situation doesn’t actually impact the potential impls that we need to account for even though it is a valid example of a situation where a new blanket impl is possible.

Thus, for all intents and purposes, impls containing generic type parameters cannot be added in semver compatible ways. This only leaves a single option: impls containing only upstream types. These are compatible because by the orphan rules, the current crate and any further downstream crates is not allowed to implement upstream traits for all upstream types. Thus, adding these impls cannot possibly break anything.

This significantly narrows down our set of potential impls that we need to account for to only impls of upstream traits for upstream types.

For downstream crates, we need to add rules for all possible impls that they could potentially add using any upstream traits or traits in the current crate. We can do this by enumerating the possibilities generated from the orphan rules specified above:

// Given a trait MyTrait<P1...Pn> where WCs

forall<Self, P1...Pn> {
  Implemented(Self: MyTrait<P1...Pn>) :-
    WCs,                  // where clauses
    Compatible,
    DownstreamType(Self), // local to a downstream crate
    CannotProve,
}
forall<Self, P1...Pn> {
  Implemented(Self: MyTrait<P1...Pn>) :-
    WCs,
    Compatible,
    IsFullyVisible(Self),
    DownstreamType(P1),
    CannotProve,
}
...
forall<Self, P1...Pn> {
  Implemented(Self: MyTrait<P1...Pn>) :-
    WCs,
    Compatible,
    IsFullyVisible(Self),
    IsFullyVisible(P1),
    ...,
    IsFullyVisible(Pn-1),
    DownstreamType(Pn),
    CannotProve,
}

Perhaps somewhat surprisingly, IsFullyVisible works here too. This is because our previous definition of the lowering for IsFullyVisible was quite broad. By lowering all types in the current crate and in upstream crates with IsFullyVisible, that predicate covers the correct set of types here too. The orphan rules only require that there are no types parameters prior to the first local type. Types that are not type parameters and also by definition not downstream types are all of the types in the current crate and in upstream crates. This is exactly what IsFullyVisible covers.

Fundamental types in both the current crate and in upstream crates can be considered local in a downstream crate if they are provided with a downstream type. To model this, we can add an additional rule for fundamental types:

forall<T> { DownstreamType(MyFundamentalType<T>) :- DownstreamType(T) }

Where clauses: Traits can have where clauses.

#[upstream] trait Foo<T, U, V> where Self: Eq<T> { /* ... */ }

The question is: do we need to bring these where clauses down into the rule that we generate for the overlap check? Answer: Yes. Since the trait can only be implemented for types that satisfy its where clauses, it makes sense to also limit our assumption of compatible impls to impls that can exist.

Associated types: Traits can have associated types. We do not need to worry about them in our discussion because associated types are output types and trait matching is done on input types. This is also why the orphan rules do not mention associated types at all.

Overlap Check in Chalk

Thus, based on the discussion above, the overlap check with coherence in mind can be modeled in chalk with the following:

• All disjoint queries take place inside of compatible

• compatible { G } desugars into forall<T> { (Compatible, DownstreamType(T)) => G }, thus introducing a Compatible predicate using implication

• For each upstream trait MyTrait<P1…Pn>, we lower it into the following rule:

  forall<Self, P1...Pn> {
    Implemented(Self: MyTrait<P1...Pn>) :-
      Compatible,
      IsUpstream(Self),
      IsUpstream(P1),
      ...,
      IsUpstream(Pn),
      CannotProve
  }
  

  This will accomplish our goal of returning an ambiguous answer whenever the overlap check query asks about any impls that an upstream crate may add in a compatible way. We determined in the discussion above that these are the only impls in any crate that can be added compatibly.

  Note: Trait where clauses are lowered into the rule’s conditions as well as a prerequisite to everything else.

• For all traits MyTrait<P1…Pn> where WCs in the current crate and in upstream traits,

  forall<Self, P1...Pn> {
    Implemented(Self: MyTrait<P1...Pn>) :-
      WCs,                  // where clauses
      Compatible,
      DownstreamType(Self), // local to a downstream crate
      CannotProve,
  }
  forall<Self, P1...Pn> {
    Implemented(Self: MyTrait<P1...Pn>) :-
      WCs,
      Compatible,
      IsFullyVisible(Self),
      DownstreamType(P1),
      CannotProve,
  }
  ...
  forall<Self, P1...Pn> {
    Implemented(Self: MyTrait<P1...Pn>) :-
      WCs,
      Compatible,
      IsFullyVisible(Self),
      IsFullyVisible(P1),
      ...,
      IsFullyVisible(Pn-1),
      DownstreamType(Pn),
      CannotProve,
  }
  

• For fundamental types in both the current crate and in upstream crates,

  forall<T> { DownstreamType(MyFundamentalType<T>) :- DownstreamType(T) }
  

Alternative Designs

Initially, when Niko and I started working on this, Niko suggested the following implementation:

For each upstream trait, MyTrait<P1…Pn>, we lower it into the following rule:

forall<Self, P1...Pn> {
  Implemented(Self: MyTrait<P1...Pn>) :-
    Compatible,
    not { LocalImplAllowed(Self: MyTrait<P1...Pn>) },
    CannotProve
}

This appears to make sense because we need to assume that any impls that the current crate cannot add itself may exist somewhere else. By using not { LocalImplAllowed(…) }, we modeled exactly that. The problem is, that this assumption is actually too strong. What we actually need to model is that any compatible impls that the current crate cannot add itself may exist somewhere else. This is a subset of the impls covered by not { LocalImplAllowed(…) }.

Notes to be added somewhere:

• For impls that are definable in the current crate, we assume that the only ones that exist are the ones that are actually present. If the current crate does not define an impl that it could define, for our purposes, that impl does not exist. This is in contrast to how we treat upstream impls. For those, we assume that impls may exist even if we don’t know that they do.
• Struct/Trait privacy (e.g. pub) does not matter. For better or for worse, we always assume that everything is public or is going to be public someday, so we do not consider privacy at all.
• Fundamental traits - tend to be traits that you generally wouldn't implement yourself. The compiler is the one generating implementations for those traits, so it was decided that it was okay to definitively conclude whether or not an impl exists for them

Canonical queries

The "start" of the trait system is the canonical query (these are both queries in the more general sense of the word – something you would like to know the answer to – and in the rustc-specific sense). The idea is that the type checker or other parts of the system, may in the course of doing their thing want to know whether some trait is implemented for some type (e.g., is u32: Debug true?). Or they may want to normalize some associated type.

This section covers queries at a fairly high level of abstraction. The subsections look a bit more closely at how these ideas are implemented in rustc.

The traditional, interactive Prolog query

In a traditional Prolog system, when you start a query, the solver will run off and start supplying you with every possible answer it can find. So given something like this:

?- Vec<i32>: AsRef<?U>

The solver might answer:

Vec<i32>: AsRef<[i32]>
    continue? (y/n)

This continue bit is interesting. The idea in Prolog is that the solver is finding all possible instantiations of your query that are true. In this case, if we instantiate ?U = [i32], then the query is true (note that a traditional Prolog interface does not, directly, tell us a value for ?U, but we can infer one by unifying the response with our original query – Rust's solver gives back a substitution instead). If we were to hit y, the solver might then give us another possible answer:

Vec<i32>: AsRef<Vec<i32>>
    continue? (y/n)

This answer derives from the fact that there is a reflexive impl (impl<T> AsRef<T> for T) for AsRef. If were to hit y again, then we might get back a negative response:

no

Naturally, in some cases, there may be no possible answers, and hence the solver will just give me back no right away:

?- Box<i32>: Copy
    no

In some cases, there might be an infinite number of responses. So for example if I gave this query, and I kept hitting y, then the solver would never stop giving me back answers:

?- Vec<?U>: Clone
    Vec<i32>: Clone
        continue? (y/n)
    Vec<Box<i32>>: Clone
        continue? (y/n)
    Vec<Box<Box<i32>>>: Clone
        continue? (y/n)
    Vec<Box<Box<Box<i32>>>>: Clone
        continue? (y/n)

As you can imagine, the solver will gleefully keep adding another layer of Box until we ask it to stop, or it runs out of memory.

Another interesting thing is that queries might still have variables in them. For example:

?- Rc<?T>: Clone

might produce the answer:

Rc<?T>: Clone
    continue? (y/n)

After all, Rc<?T> is true no matter what type ?T is.

A trait query in rustc

The trait queries in rustc work somewhat differently. Instead of trying to enumerate all possible answers for you, they are looking for an unambiguous answer. In particular, when they tell you the value for a type variable, that means that this is the only possible instantiation that you could use, given the current set of impls and where-clauses, that would be provable. (Internally within the solver, though, they can potentially enumerate all possible answers. See the description of the SLG solver for details.)

The response to a trait query in rustc is typically a Result<QueryResult<T>, NoSolution> (where the T will vary a bit depending on the query itself). The Err(NoSolution) case indicates that the query was false and had no answers (e.g., Box<i32>: Copy). Otherwise, the QueryResult gives back information about the possible answer(s) we did find. It consists of four parts:

• Certainty: tells you how sure we are of this answer. It can have two values:
  • Proven means that the result is known to be true.
    • This might be the result for trying to prove Vec<i32>: Clone, say, or Rc<?T>: Clone.
  • Ambiguous means that there were things we could not yet prove to be either true or false, typically because more type information was needed. (We'll see an example shortly.)
    • This might be the result for trying to prove Vec<?T>: Clone.
• Var values: Values for each of the unbound inference variables (like ?T) that appeared in your original query. (Remember that in Prolog, we had to infer these.)
  • As we'll see in the example below, we can get back var values even for Ambiguous cases.
• Region constraints: these are relations that must hold between the lifetimes that you supplied as inputs. We'll ignore these here, but see the section on handling regions in traits for more details.
• Value: The query result also comes with a value of type T. For some specialized queries – like normalizing associated types – this is used to carry back an extra result, but it's often just ().

Examples

Let's work through an example query to see what all the parts mean. Consider the Borrow trait. This trait has a number of impls; among them, there are these two (for clarity, I've written the Sized bounds explicitly):

impl<T> Borrow<T> for T where T: ?Sized
impl<T> Borrow<[T]> for Vec<T> where T: Sized

Example 1. Imagine we are type-checking this (rather artificial) bit of code:

fn foo<A, B>(a: A, vec_b: Option<B>) where A: Borrow<B> { }

fn main() {
    let mut t: Vec<_> = vec![]; // Type: Vec<?T>
    let mut u: Option<_> = None; // Type: Option<?U>
    foo(t, u); // Example 1: requires `Vec<?T>: Borrow<?U>`
    ...
}

As the comments indicate, we first create two variables t and u; t is an empty vector and u is a None option. Both of these variables have unbound inference variables in their type: ?T represents the elements in the vector t and ?U represents the value stored in the option u. Next, we invoke foo; comparing the signature of foo to its arguments, we wind up with A = Vec<?T> and B = ?U. Therefore, the where clause on foo requires that Vec<?T>: Borrow<?U>. This is thus our first example trait query.

There are many possible solutions to the query Vec<?T>: Borrow<?U>; for example:

• ?U = Vec<?T>,
• ?U = [?T],
• ?T = u32, ?U = [u32]
• and so forth.

Therefore, the result we get back would be as follows (I'm going to ignore region constraints and the "value"):

• Certainty: Ambiguous – we're not sure yet if this holds
• Var values: [?T = ?T, ?U = ?U] – we learned nothing about the values of the variables

In short, the query result says that it is too soon to say much about whether this trait is proven. During type-checking, this is not an immediate error: instead, the type checker would hold on to this requirement (Vec<?T>: Borrow<?U>) and wait. As we'll see in the next example, it may happen that ?T and ?U wind up constrained from other sources, in which case we can try the trait query again.

Example 2. We can now extend our previous example a bit, and assign a value to u:

fn foo<A, B>(a: A, vec_b: Option<B>) where A: Borrow<B> { }

fn main() {
    // What we saw before:
    let mut t: Vec<_> = vec![]; // Type: Vec<?T>
    let mut u: Option<_> = None; // Type: Option<?U>
    foo(t, u); // `Vec<?T>: Borrow<?U>` => ambiguous

    // New stuff:
    u = Some(vec![]); // ?U = Vec<?V>
}

As a result of this assignment, the type of u is forced to be Option<Vec<?V>>, where ?V represents the element type of the vector. This in turn implies that ?U is unified to Vec<?V>.

Let's suppose that the type checker decides to revisit the "as-yet-unproven" trait obligation we saw before, Vec<?T>: Borrow<?U>. ?U is no longer an unbound inference variable; it now has a value, Vec<?V>. So, if we "refresh" the query with that value, we get:

Vec<?T>: Borrow<Vec<?V>>

This time, there is only one impl that applies, the reflexive impl:

impl<T> Borrow<T> for T where T: ?Sized

Therefore, the trait checker will answer:

• Certainty: Proven
• Var values: [?T = ?T, ?V = ?T]

Here, it is saying that we have indeed proven that the obligation holds, and we also know that ?T and ?V are the same type (but we don't know what that type is yet!).

(In fact, as the function ends here, the type checker would give an error at this point, since the element types of t and u are still not yet known, even though they are known to be the same.)

Canonicalization

Canonicalization is the process of isolating an inference value from its context. It is a key part of implementing canonical queries, and you may wish to read the parent chapter to get more context.

Canonicalization is really based on a very simple concept: every inference variable is always in one of two states: either it is unbound, in which case we don't know yet what type it is, or it is bound, in which case we do. So to isolate some data-structure T that contains types/regions from its environment, we just walk down and find the unbound variables that appear in T; those variables get replaced with "canonical variables", starting from zero and numbered in a fixed order (left to right, for the most part, but really it doesn't matter as long as it is consistent).

So, for example, if we have the type X = (?T, ?U), where ?T and ?U are distinct, unbound inference variables, then the canonical form of X would be (?0, ?1), where ?0 and ?1 represent these canonical placeholders. Note that the type Y = (?U, ?T) also canonicalizes to (?0, ?1). But the type Z = (?T, ?T) would canonicalize to (?0, ?0) (as would (?U, ?U)). In other words, the exact identity of the inference variables is not important – unless they are repeated.

We use this to improve caching as well as to detect cycles and other things during trait resolution. Roughly speaking, the idea is that if two trait queries have the same canonical form, then they will get the same answer. That answer will be expressed in terms of the canonical variables (?0, ?1), which we can then map back to the original variables (?T, ?U).

Canonicalizing the query

To see how it works, imagine that we are asking to solve the following trait query: ?A: Foo<'static, ?B>, where ?A and ?B are unbound. This query contains two unbound variables, but it also contains the lifetime 'static. The trait system generally ignores all lifetimes and treats them equally, so when canonicalizing, we will also replace any free lifetime with a canonical variable (Note that 'static is actually a free lifetime variable here. We are not considering it in the typing context of the whole program but only in the context of this trait reference. Mathematically, we are not quantifying over the whole program, but only this obligation). Therefore, we get the following result:

?0: Foo<'?1, ?2>

Sometimes we write this differently, like so:

for<T,L,T> { ?0: Foo<'?1, ?2> }

This for<> gives some information about each of the canonical variables within. In this case, each T indicates a type variable, so ?0 and ?2 are types; the L indicates a lifetime variable, so ?1 is a lifetime. The canonicalize method also gives back a CanonicalVarValues array OV with the "original values" for each canonicalized variable:

[?A, 'static, ?B]

We'll need this vector OV later, when we process the query response.

Executing the query

Once we've constructed the canonical query, we can try to solve it. To do so, we will wind up creating a fresh inference context and instantiating the canonical query in that context. The idea is that we create a substitution S from the canonical form containing a fresh inference variable (of suitable kind) for each canonical variable. So, for our example query:

for<T,L,T> { ?0: Foo<'?1, ?2> }

the substitution S might be:

S = [?A, '?B, ?C]

We can then replace the bound canonical variables (?0, etc) with these inference variables, yielding the following fully instantiated query:

?A: Foo<'?B, ?C>

Remember that substitution S though! We're going to need it later.

OK, now that we have a fresh inference context and an instantiated query, we can go ahead and try to solve it. The trait solver itself is explained in more detail in another section, but suffice to say that it will compute a certainty value (Proven or Ambiguous) and have side-effects on the inference variables we've created. For example, if there were only one impl of Foo, like so:

impl<'a, X> Foo<'a, X> for Vec<X>
where X: 'a
{ ... }

then we might wind up with a certainty value of Proven, as well as creating fresh inference variables '?D and ?E (to represent the parameters on the impl) and unifying as follows:

• '?B = '?D
• ?A = Vec<?E>
• ?C = ?E

We would also accumulate the region constraint ?E: '?D, due to the where clause.

In order to create our final query result, we have to "lift" these values out of the query's inference context and into something that can be reapplied in our original inference context. We do that by re-applying canonicalization, but to the query result.

Canonicalizing the query result

As discussed in the parent section, most trait queries wind up with a result that brings together a "certainty value" certainty, a result substitution var_values, and some region constraints. To create this, we wind up re-using the substitution S that we created when first instantiating our query. To refresh your memory, we had a query

for<T,L,T> { ?0: Foo<'?1, ?2> }

for which we made a substitution S:

S = [?A, '?B, ?C]

We then did some work which unified some of those variables with other things. If we "refresh" S with the latest results, we get:

S = [Vec<?E>, '?D, ?E]

These are precisely the new values for the three input variables from our original query. Note though that they include some new variables (like ?E). We can make those go away by canonicalizing again! We don't just canonicalize S, though, we canonicalize the whole query response QR:

QR = {
    certainty: Proven,             // or whatever
    var_values: [Vec<?E>, '?D, ?E] // this is S
    region_constraints: [?E: '?D], // from the impl
    value: (),                     // for our purposes, just (), but
                                   // in some cases this might have
                                   // a type or other info
}

The result would be as follows:

Canonical(QR) = for<T, L> {
    certainty: Proven,
    var_values: [Vec<?0>, '?1, ?0]
    region_constraints: [?0: '?1],
    value: (),
}

(One subtle point: when we canonicalize the query result, we do not use any special treatment for free lifetimes. Note that both references to '?D, for example, were converted into the same canonical variable (?1). This is in contrast to the original query, where we canonicalized every free lifetime into a fresh canonical variable.)

Now, this result must be reapplied in each context where needed.

Processing the canonicalized query result

In the previous section we produced a canonical query result. We now have to apply that result in our original context. If you recall, way back in the beginning, we were trying to prove this query:

?A: Foo<'static, ?B>

We canonicalized that into this:

for<T,L,T> { ?0: Foo<'?1, ?2> }

and now we got back a canonical response:

for<T, L> {
    certainty: Proven,
    var_values: [Vec<?0>, '?1, ?0]
    region_constraints: [?0: '?1],
    value: (),
}

We now want to apply that response to our context. Conceptually, how we do that is to (a) instantiate each of the canonical variables in the result with a fresh inference variable, (b) unify the values in the result with the original values, and then (c) record the region constraints for later. Doing step (a) would yield a result of

{
      certainty: Proven,
      var_values: [Vec<?C>, '?D, ?C]
                       ^^   ^^^ fresh inference variables
      region_constraints: [?C: '?D],
      value: (),
}

Step (b) would then unify:

?A with Vec<?C>
'static with '?D
?B with ?C

And finally the region constraint of ?C: 'static would be recorded for later verification.

(What we actually do is a mildly optimized variant of that: Rather than eagerly instantiating all of the canonical values in the result with variables, we instead walk the vector of values, looking for cases where the value is just a canonical variable. In our example, values[2] is ?C, so that means we can deduce that ?C := ?B and '?D := 'static. This gives us a partial set of values. Anything for which we do not find a value, we create an inference variable.)

Chalk engine

The chalk-engine crate is the core PROLOG-like solver for logical predicates. Importantly, it is very general and not specific to Rust, Rust types, or Rust logic.

Implemented PROLOG concepts

The engine implements the following PROLOG logic concepts. Some of these have been published on previously, and some are Chalk-specific. This isn't necessarily an exhaustive list:

• Basic logic
• Negation
• Floundering
• Coinductive solving

Note

Throughout most of this chapter, the specifics in regards to Canonicalization and UCanonicalization are avoided. These are important concepts to understand, but don't particularly help to understand how chalk-engine works. In a few places, it may be highlighted if it is important.

Major concepts

This section goes over a few different concepts that are crucial to understanding how chalk-engine works, without going over the exact solving logic.

Goals

A "goal" in Chalk can be thought of as "something we want to prove". The engine itself understands GoalDatas. GoalDatas consist of the most basic logic, such as introducing Binders (Forall or Exists) or combining goals (All). On the other hand, DomainGoal represents an opaque goal generated externally. As such, it may contain any extra information or may be interned. When solving a logic predicate, Chalk will lazily convert DomainGoals into GoalDatas.

There are three types of completely opaque GoalDatas that Chalk can solve: Unify, DomainGoal, and CannotProve. Unlike the other types of goals, these three cannot be simplified any further. Unify is the goal of unifying any two types. DomainGoal is any goal that can solve by applying a ProgramClause. To solve this, more Goals may generated. Finally, CannotProve is a special goal that cannot be proven true or false.

Answers and Solutions

For every Goal, there are zero or more Answers. Each Answer contains values for the inference variables in the goal.

For example, given the following program:

trait Clone {}
struct A {}
struct B {}
impl Clone for A {}
impl Clone for B {}

With the following goal: exists<T> { T: Clone } The following solutions would be given:

T = A
T = B

In other words, either A or B can substituted for T and the goal will hold true. Moreover, either answer could be used when further solving other goals that depend on this goal.

However, oftentimes, this is not what external crates want when solving for a goal. Instead, the may want a unique solution to this goal. Indeed, when we solve for a given root Goal, we return a single Solution. The AntiUnifier struct from chalk-solve then finds that solution, by finding a minimal generalization of answers which don't unify. (For the example above, it would return only Ambiguous, since A and B can't unify.)

ExClauses and Strands

An ExClause is described in literature as A :- D | G or A holds given that G holds with D delayed goals. In chalk-engine, an ExClause stores the current state of proving a goal, including existing substitutions already found, subgoals yet to be proven, or delayed subgoals. A Strand wraps both an ExClause and an InferenceTable together.

Tables and Forests

A Strand represents a single direction to find an Answer - for example, an implementation of a trait with a set of where clauses. However, in a program, there may be multiple possible implementations that match a goal - e.g. multiple impls with different where clauses. Every Table has a goal, and stores existing Answers, as well as all Strands that may result in more answers.

A Forest holds all the Tables that program generates, and is what most of the logic is implemented on. It also stores the current state of solving (the stack).

Logic

Overview

chalk-engine solves a Goal using a hybrid search strategy with elements of depth- and breadth-first search. When asked to solve a particular Goal it hasn't seen before, it will first try to generate a set of program clauses, that get turned into Strands, that could solve that goal. Otherwise, if asked to solve a Goal it has seen before, it will select the existing table.

Once a table is selected, it will pick a Strand and a subgoal of that Strand, try to solve that Goal, repeating the process.

When an Answer is found for a Goal, it is merged into the parent Strand, or returned if it was the root Goal. It will then go on to pick the next subgoal of the Strand and continue on.

If at any point the solving stops being "successful" (i.e. we definitely found something to be unsolvable), the solving is restarted at the root Goal.

The stack

In order to detect cycles (talked more about later), as well as keep track of the selected Strand for each table, chalk-engine stores a Stack on the Forest. Whenever a new goal is selected, a StackEntry is pushed onto the Stack, as well as the "time" (which also gets incremented) that it was pushed. This "time" can be compared later to check if all the Strands of a Table have been checked in a single solve.

As either Answers are found for the selected Table, entries on the stack are poped. If something is found to be unsolvable, the complete stack is unwound.

Table creation

As mentioned before, whenever a new Goal is encountered, a new Table is created to store current and future answers. First, the Goal is converted into an GoalData. If it can be simplified, then a Strand with one or more subgoals will be generated and can be followed as above. Otherwise, if it is a DomainGoal (see above), then program_clauses_for_goal is called and each clause is converted into a Strand and can be followed.

root_answer and ensure_root_answer

The root_answer function is the entry point to solve a Goal. Up until now, the idea of Answer versus CompleteAnswer have been ignored. However, in reality Answers to Goals may actually have delayed subgoals (see ExClause and Coinduction and refinement strands), whereas CompleteAnswers may not. root_answer essentially just wraps ensure_root_answer and converts the Goal's Answer to a CompleteAnswer.

The ensure_root_answer function contains the core skeleton of the logic around Strand and subgoal selection. The majority of the logic, however, is split out into separate functions that branch out from ensure_root_answer.

Subgoal selection

Once a given Strand for a table has been selected, a subgoal has to be selected. If there are no subgoals left, then there is nothing to do. Otherwise, if there are subgoals left, then a subgoal will attempt to be selected (from next_subgoal_index). If the table for that subgoal had previously floundered (see next section), then we mark that subgoal as floundered and try the next subgoal. If all subgoals are marked as floundered, then this entire Strand is marked as floundered. If a subgoal is successfully selected, there is nothing left to do.

Floundering

There a couple cases where we "give up" - here called floundering - on trying to solve a goal. The most easy to understand case is if the types for a Goal or Answer are too large. (Side note, we could actually handle this - by generalizing - but turns out to be quite buggy and probably unnecessary). Another case where we flounder is if we try to solve a Goal where we try to enumerate non-enumerable types (like auto traits). In general, floundering just means that we can't know any more answers about a Goal, for some reason. However, if there are other Strands that don't flounder, there may still be other Answers available.

Answers

After an answer has been found for a subgoal, it must be applied to the parent Strand. Specifically, it must be able to unify with any existing Answers. If the Answers are incompatible, the Strand is dropped since it can't lead anywhere.

Cycles

If while pursuing a Goal, the engine encounters the same Table twice, then a cycle has occurred. If the cycle is not coinductive (see next), then there is nothing that can be gained from taking this route. We mark how far up the stack is in the cycle, and try the next Strand. If all Strands for a table encounter a cycle, then we know that the current selected Goal has no more answers.

Coinduction and refinement strands

Coinduction basically means that two statements can rely on each other being true, unless either is proven false.

For example with the following program:

#[coinductive]
trait C1<T> { }
forall<A, B> { A: C1<B> if B: C1<A> }

Then the goal exists<T, U> { T: C1<U> } holds for all T and U. If the C1 trait was not coinductive, this would be a simple cycle.

To implement coinduction in the engine, delayed subgoals were introduced. Essentially, if a cycle is found, and the Goal is coinductive, then this is "delayed" until the stack unwinds back to the top Goal and all other non-coinductive cycles have been proven. Then, Goal has been proven itself. In some cases, it is the root Goal that has delayed coinductive subgoals (see above example). In this case, we create another "Refinement Strand" where the only subgoals are the delayed coinductive subgoals. If this new Strand can be proven, then any Answers from that are valid answers for the root Goal. However, since there are currently delayed coinductive subgoals, there are no answers available yet.

For much more in-depth

Coinduction

This sub-chapter was originally prepared for wg-traits design meeting on 2019-11-08 (see the Hackmd doc). It briefly covers some tricky (and previously incorrectly handled) cases of coinduction, as well as two proposed solutions. The resulting and current solution ended up being something pretty close to Niko's solution. However, this is basically a copy-paste from the original document, and so shouldn't necessarily be taken as 100% truth as far as implementation.

The problem

See chalk#248 for details. The short version is that we fail to handle a case like this correctly, where Ci are all co-inductive goals:

C1 :- C2, C3.
C2 :- C1.

What happens is that we

• start to prove C1
• start to prove C2
• see a recursive attempt to prove C1, assume it is successful
• consider C2 proved and cache this
• start to prove C3, fail
• consider C1 unproven

Now we incorrectly have a result that C2 is true -- but that result was made on the assumption that C1 was true, and it was not.

Some other tricky cases to consider

Unification failures

One thing to consider is that even when we have "coinduction obligations" to prove, we have to remember their substitutions too:

C1(X) :- C2(Y), X = 22.
C2(X) :- C3(X), X = 44.
C3(X) :- C1(X), C2(X).

None of these predicates should be provable, because C1(X) and C2(X) don't hold for the same X.

If we're not careful, we might:

• start to prove C1
• start to prove C2
• start to prove C3, see the recursive calls to C1 and C2
  • maybe we wait to consider it proven until C1 and C2 complete

In this case, it's not enough that C1 and C2 are provable at all, they have to be provable for the same X.

Non-trivial self-cycles

C1(A) :- C1(B), B = 22, C2(A).
C2(44).

This case is not provable, even though the only cycle is C1(X) :- C1(Y) -- but it turns out that X must not be 22. The catch is that while this might appear to be a trivial self-cycle, it is not!

Actually I have to think about the best way to handle this case, as my proposed solution doesn't quite cut it. It wouldn't be wrong but it seems not ideal. -- Niko

Delayed trivial cycles

C1(A, B) :- C2(A, B), A = 22, B = 22.
C2(A, B) :- C1(B, A).

This should be provable, but the cycle from C2 to C1 is not immediately visible as a trivial cycle, at least if subgoals are solved in order.

Delayed trivial cycles, variant 2

C1(A, B) :- C2(A, B), A = 22.
C2(A, B) :- C1(B, A).

As above, here the only complete answer is C1(22, 22). This is because the C1, C2 cycle effectively guarantees equality.

Delayed trivial cycles, variant 3

C1(A, B) :- C1(B, A).

This is true for all A, B

Other cases?

Approach in existing PR

High-level idea

• When we encounter a co-inductive subgoal, we delay them in the current Strand
• When all subgoals have been tested, and there are remaining delayed co-inductive subgoals, this is propagated up, marking the current Strand as co-inductive
• When the co-inductive Strands reach the root table, we only then pursue an answer

Niko's proposed solution

High-level idea

• We only consider a co-induction subgoal proven for trivial recursion -- i.e., self-recursion where you have C1 :- C1.
• For non-trivial recursion, we propagate the co-inductive subgoal to the parent. This continues until it becomes trivial.

Implementation steps

Extend Answer in two ways.

Currently Answer has a "constrained substitution" that includes values for the table's substitution + region constraints:

struct Answer {
    constrained_subst: Canonical<ConstrainedSubst>,
    is_ambiguous: bool
}

struct ConstrainedSubst {
    substitution: Substitution,
    region_constraints: Vec<RegionConstraint>,
}

we would first extend ConstrainedSubst to include as yet unproven co-inductive subgoals (this might actually be better done as a new type):

struct ConstrainedSubst {
    substitution: Substitution,
    delayed_subgoals: Vec<Literal>,
    region_constraints: Vec<RegionConstraint>,
}

then we would extend Answer slightly as well so it can be "ok" or ambiguous, as today, but also an error case

enum AnswerMode {
    OK,
    Ambiguous,
    Error,
}

struct Answer {
    constrained_subst: Canonical<ConstrainedSubst>,
    mode: AnswerMode
}

We won't need this error case till later, so let's ignore it for now. (And in a way, we never need it.)

Deferring coinductive subgoals

When we encounter a co-inductive subgoal, we check if it is trivial cycle or not. A trivial cycle is a case like C1 :- C1. We can simply consider such cycles to be true (but note the distinction between a trivial cycle and a self-cycle -- see the "non-trivial self-cycle" example above).

For non-trivial cycles, we will want to store the cycle to be validated later. To accommodate that, we extend ExClause to include a delayed_subgoals list as well. We can write this the same way SLG does, so Goal :- DelayedSubgoals | Subgoals

In our example, proving C2 :- C1 would result in adding C1 to the list of delayed subgoals.

When we reach the end of the list of subgoals, we can create an answer that contains the delayed subgoals. We don't have to add all the goals -- we can check for those that are trivial self-cycles again and remove them (in some cases, something which was not trivial to start may have become trivial through later unifications, see Delayed Trivial Self-Cycle case). Note that we do have to add all non-trivial cycles, including non-trivial self-cycles -- see the walkthrough of Non-trivial self-cycle variant 3.

So the answer to C2 would be

substitution: [] // no variables
delayed_subgoals: ["C1"]
region_constraints: []

We can denote this as C2 :- C1 |, to use SLG notation.

Incorporating an answer with deferred subgoals.

When a table gets back an answer that has deferred sub-goals, they get added to the current list of subgoals.

So e.g. in our case, we had a ExClause like:

C1 :- | C2, C3

and we get the answer C2 :- C1 |, so we would convert it to

C1 :- | C3, C1

i.e., we have added C1 to the list of goals to prove. When we go to prove C3, of course, we will fail -- but it had succeeded, we would go on to prove C1 but encounter a trivial cycle and hence succeed.

Extending root answer

So we failed to prove C1, but we do have a (conditional) answer to C2 -- C2 :- C1 |, even though C2 is unprovable. What happens if ensure_root_answer is invoked on C2?

What we have here is a conditional answer. We know that C1 must have ultimately resolved itself somehow (although it might not yet be proven). What we can do is create a strand in C2 to evaluate C1 again -- if this strand succeeds, it can actually overwrite the C2 :- C1 | answer in place with C2 :- (i.e., an unconditional answer). This is just a refinement of what we had. If the strand fails, though, we'll want to remember the error.

I think when we get a new answer, we want it to overwrite the old answer in place, rather than create a new answer. This is valid because it's not a new answer, it's just a more refined form of the old answer (although note that it might have different substitutions and other details, see the "delayed trivial cycle" case).

In particular, it could be that the table already has a "complete" set of answers -- i.e., somebody invoked ensure_answer(N) and got back None. We don't want to be adding new answers which would change the result of that call. It is a bit strange that we are changing the result of ensure_answer(i) for the current i, but then the result is the same answer, just a bit more elaborated.

The idea then would be to create a strand associated with this answer somehow (it doesn't, I don't think, live in the normal strand table; we probably have a separate "refinement strand" table). This strand has as its subgoals the delayed subgoals. It pursues them. This either results in an answer (which replaces the existing answer) or an error (in which case the existing answer is marked as error). This may require extending strand with an optional answer index that it should overwrite, or perhaps we thread it down as an argument to pursue_strand (optional because, in the normal mode, we are just appending a new answer).

(Question: What distinguishes root answer? Nothing -- we could actually do this process for any answer, so long as the delayed subgoals are not to tables actively on the stack. This just happens to be trivially true for root answers. The key part though is that the answer must be registered in the table first before the refinement strand is created, see Delayed Self-Cycle Variant 3.)

This is complex, so let's walk through an example or two.

The original problem. When we finish solving C1, we leave C2 with a single answer C2 :- C1 |. If someone invokes ensure_root_answer(C2, 0), we would see the delayed literal and create a refinement strand for the answer: C2 :- | C1. We would pursue C1 and get back the successful answer. So the refinement strand would terminate and we can overwrite with the answer C2 :- |.

Delayed trivial self-cycle. Similar to above, but the answer is C2(?A, ?B) :- C1(?B, ?A) |. In other words, in the canonical answer, we have a (identity) substitution of [^0, ^1] and a delayed goal of C1(^1, ^0). The strand we create will find only one answer to C1, C1(22, 22), so we wind up with an answer C2(22, 22).

Handling error answers

We introduced the idea of an "error answer"...how do we handle that? It's fairly simple. If a strand encounters an error answer, it simply fails. Done. The outer search however needs to treat an error answer as basically a no-op -- so e.g. the answer iterator should simply increment the error counter and move to the next answer.

Walk through: delayed trivial self cycle, variant 2

C1(A, B) :- C2(A, B), A = 22.
C2(A, B) :- C1(B, A).

• ensure_root_answer(C1(?A, ?B)) is invoked
  • We start solving C1(?A, ?B) with the ex-clause C1(?A, ?B) :- | C2(?A, ?B), ?A = 22
    • That starts solving C2(?A, ?B)
      • This gets an answer C2(?A, ?B) :- C1(?B, ?A) |
      • When answer is incorporated, we get C1(?A, ?B) :- | C1(?B, ?A), ?A = 22
    • C1(?B, ?A) is a non-trivial cycle, and so we get
      • C1(?A, ?B) :- C1(?B, ?A) | ?A = 22
    • Unification completes, leaving us with
      • C1(22, ?B) :- C1(?B, 22) |
    • This is a complete answer
  • ensure root answer attempts to refine this answer, creating a strand for C1(22, ?B) :- | C1(?B, 22)
    • This creates a table for C1(?B, 22) with ex-clause C1(?B, 22) :- | C2(?B, 22), ?B = 22
      • We start solving C2(?B, 22), which has ex-clause C2(?B, 22) :- C1(22, ?B)
        • This creates a table for C1(22, ?B), with ex-clause C1(22, ?B) :- C2(22, ?B), 22 = 22
          • This starts solving C2(22, ?B), which is a fresh table with ex-clause C2(22, ?B) :- C1(?B, 22)
            • This is a co-inductive cycle
            • So our answer is C2(22, ?B) :- C1(?B, 22) |
          • Incorporating this answer yields C1(22, ?B) :- 22 = 22, C1(?B, 22)
          • The unification constraint succeeds, leaving C1(22, ?B) :- C1(?B, 22)
          • Co-inductive cycle detected, so answer is
            • C1(22, ?B) :- C1(?B, 22) |
      • This answer is incorporated into C2, yielding the ex-clause
        • C2(?B, 22) :- C1(?B, 22)
      • Pursuing that sub-goal gives a co-inductive cycle, so our final answer is
        • C2(?B, 22) :- C1(?B, 22) |
    • This answer is incorporated, yielding ex-clause C1(?B, 22) :- | ?B = 22, C1(?B, 22)
    • Unification yields C1(22, 22) :- C1(22, 22)
    • Trivial self-cycle detected, so final answer is
      • C1(22, 22)
  • the answer for C1(?A, ?B) is thus updated to C1(22, 22)

Walk through: delayed trivial self cycle, variant 3

C1(A, B) :- C1(B, A).

This example is interesting because it shows that we have to incorporate non-trivial self cycles into an answer so they can recursively build on one another.

• we get an initial answer of
  • C1(?A, ?B) :- C1(?B, ?A) |
• if we attempt to refine this, we will get a strand C1(?X, ?Y) :- C1(?Y, ?X)
  • pursuing the first subgoal C1(?Y, ?X) leads us to our own table, but at answer 0
    • (the very answer we are refining)
    • the answer is C1(?Y, ?X) :- C1(?X, ?Y) |
  • this strand incorporates its own answer, yielding
    • C1(?X, ?Y) :- C1(?X, ?Y)
  • next subgoal is a trivial self-cycle, discard, yielding
    • C1(?X, ?Y) :-
• result: true

Walk through: non-trivial self cycle

Let's walk through one more case, the non-trivial self cycle.

C1(A) :- C1(B), B = 22, C2(A).
C2(44).

What happens here is that we get an initial answer from C1 that looks like:

C1(44) :- C1(22) |

Ensure root answer will thus try to refine by trying to solve C1(22). Interestingly, this is going to go to a distinct table, because the canonical form is not the same, but that table will just fail.

The On-Demand SLG solver

Given a set of program clauses (provided by our lowering rules) and a query, we need to return the result of the query and the value of any type variables we can determine. This is the job of the solver.

For example, exists<T> { Vec<T>: FromIterator<u32> } has one solution, so its result is Unique; substitution [?T := u32]. A solution also comes with a set of region constraints, which we'll ignore in this introduction.

Goals of the Solver

On demand

There are often many, or even infinitely many, solutions to a query. For example, say we want to prove that exists<T> { Vec<T>: Debug } for some type ?T. Our solver should be capable of yielding one answer at a time, say ?T = u32, then ?T = i32, and so on, rather than iterating over every type in the type system. If we need more answers, we can request more until we are done. This is similar to how Prolog works.

See also: The traditional, interactive Prolog query

Breadth-first

Vec<?T>: Debug is true if ?T: Debug. This leads to a cycle: [Vec<u32>, Vec<Vec<u32>>, Vec<Vec<Vec<u32>>>], and so on all implement Debug. Our solver ought to be breadth first and consider answers like [Vec<u32>: Debug, Vec<i32>: Debug, ...] before it recurses, or we may never find the answer we're looking for.

Cachable

To speed up compilation, we need to cache results, including partial results left over from past solver queries.

Description of how it works

The basis of the solver is the Forest type. A forest stores a collection of tables as well as a stack. Each table represents the stored results of a particular query that is being performed, as well as the various strands, which are basically suspended computations that may be used to find more answers. Tables are interdependent: solving one query may require solving others.

Walkthrough

Perhaps the easiest way to explain how the solver works is to walk through an example. Let's imagine that we have the following program:

trait Debug { }

struct u32 { }
impl Debug for u32 { }

struct Rc<T> { }
impl<T: Debug> Debug for Rc<T> { }

struct Vec<T> { }
impl<T: Debug> Debug for Vec<T> { }

Now imagine that we want to find answers for the query exists<T> { Rc<T>: Debug }. The first step would be to u-canonicalize this query; this is the act of giving canonical names to all the unbound inference variables based on the order of their left-most appearance, as well as canonicalizing the universes of any universally bound names (e.g., the T in forall<T> { ... }). In this case, there are no universally bound names, but the canonical form Q of the query might look something like:

Rc<?0>: Debug

where ?0 is a variable in the root universe U0. We would then go and look for a table with this canonical query as the key: since the forest is empty, this lookup will fail, and we will create a new table T0, corresponding to the u-canonical goal Q.

Ignoring negative reasoning and regions. To start, we'll ignore the possibility of negative goals like not { Foo }. We'll phase them in later, as they bring several complications.

Creating a table. When we first create a table, we also initialize it with a set of initial strands. A "strand" is kind of like a "thread" for the solver: it contains a particular way to produce an answer. The initial set of strands for a goal like Rc<?0>: Debug (i.e., a "domain goal") is determined by looking for clauses in the environment. In Rust, these clauses derive from impls, but also from where-clauses that are in scope. In the case of our example, there would be three clauses, each coming from the program. Using a Prolog-like notation, these look like:

(u32: Debug).
(Rc<T>: Debug) :- (T: Debug).
(Vec<T>: Debug) :- (T: Debug).

To create our initial strands, then, we will try to apply each of these clauses to our goal of Rc<?0>: Debug. The first and third clauses are inapplicable because u32 and Vec<?0> cannot be unified with Rc<?0>. The second clause, however, will work.

What is a strand? Let's talk a bit more about what a strand is. In the code, a strand is the combination of an inference table, an X-clause, and (possibly) a selected subgoal from that X-clause. But what is an X-clause (ExClause, in the code)? An X-clause pulls together a few things:

• The current state of the goal we are trying to prove;
• A set of subgoals that have yet to be proven;
• There are also a few things we're ignoring for now:
  • delayed literals, region constraints

The general form of an X-clause is written much like a Prolog clause, but with somewhat different semantics. Since we're ignoring delayed literals and region constraints, an X-clause just looks like this:

G :- L

where G is a goal and L is a set of subgoals that must be proven. (The L stands for literal -- when we address negative reasoning, a literal will be either a positive or negative subgoal.) The idea is that if we are able to prove L then the goal G can be considered true.

In the case of our example, we would wind up creating one strand, with an X-clause like so:

(Rc<?T>: Debug) :- (?T: Debug)

Here, the ?T refers to one of the inference variables created in the inference table that accompanies the strand. (I'll use named variables to refer to inference variables, and numbered variables like ?0 to refer to variables in a canonicalized goal; in the code, however, they are both represented with an index.)

For each strand, we also optionally store a selected subgoal. This is the subgoal after the turnstile (:-) that we are currently trying to prove in this strand. Initially, when a strand is first created, there is no selected subgoal.

Activating a strand. Now that we have created the table T0 and initialized it with strands, we have to actually try and produce an answer. We do this by invoking the ensure_root_answer operation on the table: specifically, we say ensure_root_answer(T0, A0), meaning "ensure that there is a 0th answer A0 to query T0".

Remember that tables store not only strands, but also a vector of cached answers. The first thing that ensure_root_answer does is to check whether answer A0 is in this vector. If so, we can just return immediately. In this case, the vector will be empty, and hence that does not apply (this becomes important for cyclic checks later on).

When there is no cached answer, ensure_root_answer will try to produce one. It does this by selecting a strand from the set of active strands -- the strands are stored in a VecDeque and hence processed in a round-robin fashion. Right now, we have only one strand, storing the following X-clause with no selected subgoal:

(Rc<?T>: Debug) :- (?T: Debug)

When we activate the strand, we see that we have no selected subgoal, and so we first pick one of the subgoals to process. Here, there is only one (?T: Debug), so that becomes the selected subgoal, changing the state of the strand to:

(Rc<?T>: Debug) :- selected(?T: Debug, A0)

Here, we write selected(L, An) to indicate that (a) the literal L is the selected subgoal and (b) which answer An we are looking for. We start out looking for A0.

Processing the selected subgoal. Next, we have to try and find an answer to this selected goal. To do that, we will u-canonicalize it and try to find an associated table. In this case, the u-canonical form of the subgoal is ?0: Debug: we don't have a table yet for that, so we can create a new one, T1. As before, we'll initialize T1 with strands. In this case, there will be three strands, because all the program clauses are potentially applicable. Those three strands will be:

• (u32: Debug) :-, derived from the program clause (u32: Debug)..
  • Note: This strand has no subgoals.
• (Vec<?U>: Debug) :- (?U: Debug), derived from the Vec impl.
• (Rc<?U>: Debug) :- (?U: Debug), derived from the Rc impl.

We can thus summarize the state of the whole forest at this point as follows:

Table T0 [Rc<?0>: Debug]
  Strands:
    (Rc<?T>: Debug) :- selected(?T: Debug, A0)

Table T1 [?0: Debug]
  Strands:
    (u32: Debug) :-
    (Vec<?U>: Debug) :- (?U: Debug)
    (Rc<?V>: Debug) :- (?V: Debug)

Delegation between tables. Now that the active strand from T0 has created the table T1, it can try to extract an answer. It does this via that same ensure_answer operation we saw before. In this case, the strand would invoke ensure_answer(T1, A0), since we will start with the first answer. This will cause T1 to activate its first strand, u32: Debug :-.

This strand is somewhat special: it has no subgoals at all. This means that the goal is proven. We can therefore add u32: Debug to the set of answers for our table, calling it answer A0 (it is the first answer). The strand is then removed from the list of strands.

The state of table T1 is therefore:

Table T1 [?0: Debug]
  Answers:
    A0 = [?0 = u32]
  Strand:
    (Vec<?U>: Debug) :- (?U: Debug)
    (Rc<?V>: Debug) :- (?V: Debug)

Note that I am writing out the answer A0 as a substitution that can be applied to the table goal; actually, in the code, the goals for each X-clause are also represented as substitutions, but in this exposition I've chosen to write them as full goals, following NFTD.

Since we now have an answer, ensure_answer(T1, A0) will return Ok to the table T0, indicating that answer A0 is available. T0 now has the job of incorporating that result into its active strand. It does this in two ways. First, it creates a new strand that is looking for the next possible answer of T1. Next, it incorporates the answer from A0 and removes the subgoal. The resulting state of table T0 is:

Table T0 [Rc<?0>: Debug]
  Strands:
    (Rc<?T>: Debug) :- selected(?T: Debug, A1)
    (Rc<u32>: Debug) :-

We then immediately activate the strand that incorporated the answer (the Rc<u32>: Debug one). In this case, that strand has no further subgoals, so it becomes an answer to the table T0. This answer can then be returned up to our caller, and the whole forest goes quiescent at this point (remember, we only do enough work to generate one answer). The ending state of the forest at this point will be:

Table T0 [Rc<?0>: Debug]
  Answer:
    A0 = [?0 = u32]
  Strands:
    (Rc<?T>: Debug) :- selected(?T: Debug, A1)

Table T1 [?0: Debug]
  Answers:
    A0 = [?0 = u32]
  Strand:
    (Vec<?U>: Debug) :- (?U: Debug)
    (Rc<?V>: Debug) :- (?V: Debug)

Here you can see how the forest captures both the answers we have created thus far and the strands that will let us try to produce more answers later on.

See also

• chalk_solve README, which contains links to papers used and acronyms referenced in the code
• This section is a lightly adapted version of the blog post An on-demand SLG solver for chalk
• Negative Reasoning in Chalk explains the need for negative reasoning, but not how the SLG solver does it

Chalk recursive solver

The recursive solver, as its name suggests, is a logic solver that works "recursively". In particular, its basic structure is a function like:

fn(Goal) -> Solution

where the Goal is some canonical goal and the Solution is a result like:

• Provable(S): meaning the goal is provable and it is provably exactly (and only) for the substitution S. S is a set of values for the inference variables that appear in the goal. So if we had a goal like Vec<?X>: Foo, and we returned Provable(?X = u32), it would mean that only Vec<u32>: Foo and not any other sort of vector (e.g., Vec<u64>: Foo does not hold).
• Ambiguous(S): meaning that we can't prove whether or not the goal is true. This can sometimes come with a substitution S, which offers suggested values for the inference variables that might make it provable.
• Error: the goal cannot be proven.

Recursion: pros and cons

The recursive solver is so-called because, in the process of solving one goal, it will "recurse" to solve another. Consider an example like this:

trait A { }
impl<T: A> A for Vec<T> { }
impl A for u32 { }
impl A for i32 { }

which results in program clauses like:

forall<T> { Implemented(Vec<T>: A) :- Implemented(T: A) }
Implemented(u32: A)
Implemented(i32: A)

First, suppose that we have a goal like Implemented(Vec<u64>: A). This would proceed like so:

• Solve(Implemented(Vec<u64>: A))
  • Solve(Implemented(u64: A))
    • returns Error
  • returns Error

In other words, the recursive solver would start by applying the first rule, which would cause us recursively try to solve Implemented(u64: A). This would yield an Error result, because there are no applicable rules, and that error would propagate back up, causing the entire attempt at proving things to fail.

Next, consider Implemented(Vec<u32>: A). This would proceed like so:

• Solve(Implemented(Vec<u32>: A))
  • Solve(Implemented(u32: A))
    • returns Provable with no substitution (no variables)
  • returns Provable

Finally, consider Implemented(Vec<?X>: A). This is more interesting because it has a variable:

• Solve(Implemented(Vec<?X>: A))
  • Solve(Implemented(?X: A))
    • finds two viable solutions, returns Ambiguous
  • returns Ambiguous

Recursion and completeness

One side-effect of the recursive solver's structure is that it cannot solve find solutions in some cases where a traditional Prolog solver would be successful. Consider this example:

#![allow(unused)]
fn main() {
trait A { }
trait B { }

impl<T: A + B> A for Vec<T> { }

impl A for u32 { }
impl B for u32 { }

impl A for i32 { }
impl B for i8 { }
}

In the recursive solver, with a goal of Implemented(Vec<?X>: A), we recursively try to prove Implemented(?X: A) and Implemented(?X: B), which are both ambiguous, and we get stuck there.

The SLG solver in contrast starts by exploring ?X = u32 and finds that it works, and then later tries to explore ?X = i32 and finds that it fails (because i32: B is not true).

The stack

The first "layer" of the recursive solver is the Stack. It is really just what it sounds like: a stack that stores each thing that the recursive solver is solving. Initially, it contains only one item, the root goal that was given by the user.

Each frame on the stack has an associated StackDepth, which is basically an index that increases (so 0 is the top of the stack, 1 is the next thing pushed, etc).

How the recursive solver works at the highest level

At the highest level, the recursive solver works like so.

• Push the initial goal G0 onto the stack.
• Find all the program clauses G1 :- G2...Gn that could apply to the goal G0.
• For each program clause, unify G1 and G0. If that succeeds, then recursively try to prove each goal Gi in the list G2..Gn:
  • If proving Gi yields an error, return an error.
  • If proving Gi yields an ambiguity, keep going, but remember that we got an ambiguous result.
  • If proving Gi succeeded, apply the resulting answer to our inference variables and keep going.
• At the end, if any result proved ambiguous, return ambiguous, otherwise construct the final answer and return success.

Example

#![allow(unused)]
fn main() {
trait A { }
trait B { }

impl<T: B> A for Vec<T> { }

impl B for u32 { }
}

Imagine we are trying to prove Implemented(Vec<?X>: A). There is one unbound inference variable here, ?X. We will ultimately get the result Provable(?X = u32). But how do we find it?

• Initially we are solving Implemented(Vec<?X>: A)
  • we find one applicable program clause, forall<T> { Implemented(Vec<T>: A) :- Implemented(T: B) }.
  • after unification, the list of subgoals is [Implemented(?X: B)].
  • we recursively try to solve Implemented(?X: B)
    • we find one applicable program clause, Implemented(u32: B).
    • after unification, ?X = u32, but there are no more subgoals.
    • we return the answer Provable(?X = u32).
  • we apply the substitution ?X = u32, and find there are no more subgoals.
  • we return the answer Provable(?X = u32).

Why do we need the stack?

You may have noticed that the description above never seemed to use the Stack, it only relied on the program stack. That's because I left out any discussion of cycles. In fact, the Stack data structure does mirror the program stack, it just adds some extra information we use in resolving cycles. We'll discuss cycles in the next chapter, when we discuss the search graph.

Figuring out if something is on the stack

The stack itself never stores the goal associated with a particular entry. That information is found in the search graph, which will be covered in detail in the next section. For now it suffices to say that the search graph maps from "some goal that we are currently solving" to "information about that goal", and one of the bits of information is the StackDepth of its entry on the stack (if any).

Therefore, when we are about to start solving some (canonical) goal G, we can detect a cycle by checking in the search graph to see whether G has an associated StackDepth. If so, it must be on the stack already (and we can set the cycle field to true...but I get ahead of myself, read the next chapters to learn more about that).

Inductive cycles

Recursive solving without cycles is easy. Solving with cycles is rather more complicated. Before we get into the details of the implementation, let's talk a bit about what behavior we actually expect in the face of possible cycles.

Inductive cycles

By default, Rust trait solving is inductive. What that means is that, roughly speaking, you have to prove something is true without any cycles (i.e., you can't say "it's true because it's true"!).

For our purpose, a "cycle" means that, in the course of proving some canonical goal G, we had to prove that same goal G again.

Consider this Rust program:

#![allow(unused)]
fn main() {
trait A { }
impl<T: A> A for Vec<T> { }
impl A for u32 { }
}

Whether or not we hit a cycle will depend on the goal we are trying to solve. If for example we are trying to prove Implemented(Vec<u32>: A), then we don't hit any cycle:

• Implemented(Vec<u32>: A) :- Implemented(u32: A) // from the first impl
  • Implemented(u32: A) // from the second impl

But what if we are trying to prove Implemented(?X: A)? This is a bit more interesting. Because we don't know what ?X is, both impls are actually potentially applicable, so we wind up with two ways to prove our goal. We will try them out one after the other.

One possible execution might be:

• Prove Implemented(?X: A)
  • we find the program clause forall<T> { Implemented(Vec<T>: A) :- Implemented(T: A) } from the first impl
    • we create the variable ?Y to represent T and unify ?X = Vec<?Y>.
    • after unification, we have the subgoal Implemented(?Y: A)
      • when we go to recursively prove this impl, however, we find that it is already on the stack
      • this is because the canonical form of Implemented(?X: A) and Implemented(?Y: A) is the same

What happens if we treat inductive cycles as errors?

So, what do we do when we hit an inductive cycle? Given that we told you that an inductive proof cannot contain cycles, you might imagine that we can just treat such a cycle as an error. But this won't give us the correct result.

Consider our previous example. If we just treat that cycle as an error, then we will conclude that the impl for Vec<T> doesn't apply to ?X: A, and we'll proceed to try the impl for u32. This will let us reason that ?X: A is provable if ?X = u32. This is, in fact, correct: ?X = u32 is a possible answer. The problem is, it's not the only one!

In fact, Implemented(?X: A) has an infinite number of answers. It is true for ?X = u32. It is true for ?X = Vec<u32>. It is also true for Vec<Vec<u32>> and Vec<Vec<Vec<u32>>> and so on.

Given this, the correct result for our query is actually "ambiguous" -- in particular, there is no unique substitution that we can give that would make the query provable.

How we solve cycles: loop and try again

The way we actually handle cycles is by iterating until we reach a fixed point (or ambiguity). We start out by assuming that all cycles are errors and we try to find some solution S. If we succeed, then we can do a loop and iterate again -- this time, for each cycle, we assume the result is S. This may yield some new solution, S1. The key point here is that we now have two possible solutions to the same goal, S and S1. This implies two possibilities:

• If S == S1, then in fact there is a unique solution, so we can return Provable(S).
• If S != S1, then we know there are two solutions, which means that there is not one unique solution, and hence the correct result is ambiguous, and in fact we can just stop and return right now.

This technique is very similar to the traditional Prolog technique of handling cycles, which is called tabling. The difference between our approach and tabling is that we are always looking for a unique solution, whereas Prolog (like the SLG solver) tries to enumerate all solutions (i.e., in Prolog, solving a goal is not a function but an iterator that yields solutions, and hence it would yield up S first, and then S1, and then any further answers we might get).

Intuitively, what is happening here is that we're building bigger and bigger "proof trees" (i.e., trees of impl applications). In the first iteration, where we assumed that all recursive calls were errors, we would find exactly one solution, u32: A -- this is the root tree. In the next iteration, we can use this result to build a tree for Vec<u32>: A and so forth.

Inductive cycles with no base case

It is interesting to look at what happens without the base case. Consider this program:

#![allow(unused)]
fn main() {
trait B { }
impl<T: B> B for Vec<T> { }
}

In this case, there is no base case -- this means that in fact there are no solutions at all to the query ?X: B. The reason is that the only type that could match would be a type of infinite size like Vec<Vec<Vec<...>>>: B, where the chain of Vec never terminates.

In our solver, this will work out just fine. We will wind up recursing and encountering a cycle. This will be treated as an error in the first iteration -- and then, at the end, we'll still have an error. This means that we've reached a fixed point, and we can stop.

Inductive cycles: when do we ever terminate

You might be wondering whether there are any examples of inductive cycles that actually terminate successfully and without ambiguity. In fact, there are very few, but you can construct an example like this:

#![allow(unused)]
fn main() {
trait C { }
impl<T: C + D> C for Vec<T> { }
impl C for u32 { }

trait D { }
}

In this case, the only valid result of Implemented(?X: C) is ?X = u32. It can't be Vec<u32> because Implemented(u32: D) is not true.

How does this work out with the recursive solver? In the first iteration, we wind up with ?X = u32, but we do encounter a cycle:

• proving Implemented(?X: C) has two possibilities...
  • ?X = Vec<?Y> and Implemented(?Y: C), which is a cycle (error, at least in this iteration)
  • ?X = u32, succeeds

So then we try the next iteration:

• proving Implemented(?X: C) has two possibilities...
  • ?X = Vec<?Y> and Implemented(?Y: C), which is a cycle, so we use our previous result of ?Y = u32
    • we then have to prove Implemented(u32: D), which fails
  • ?X = u32, succeeds

The search graph and caching

So now we have a good idea of what behavior we expect from cycles, or at least inductive cycles (we'll talk about coinduction later). But how do we actually implement this? That's where the SearchGraph comes into play.

The role of the SearchGraph is to store information about each goal that we are currently solving. Typically, these are goals on the stack -- but other times, they are goals that are no longer on the stack, but whose results (because of a cycle) were dependent on something that is still on the stack. We'll work through some examples to make it all clear.

Structure of the search graph

The search graph consists of nodes, each of which is assigned an index called a DepthFirstNumber. The name of this index alludes to the fact that, as we try to prove a given goal, we are implicitly performing a "depth-first search" over a graph of subgoals, and the index in the search graph is similar to a pre-order index on the resulting tree.

Example search graph

Consider this example trait plus impls:

#![allow(unused)]
fn main() {
trait A { }
impl<T: A, U: A> A for Result<T, U> { }
impl A for u32 { }
impl A for i32 { }
impl A for f32 { }
}

If we consider the full set of goals/subgoals that are involved in proving Implemented(Result<u32, i32>: A), it would look like this:

graph TD
  G1["Implemented(Result&lt;u32, i32&gt;: A)<br>Pre-order number: 0<br>DepthFirstNumber: 0"]
  G2["Implemented(u32: A)<br>Pre-order number: 1<br>DepthFirstNumber: 1"]
  G3["Implemented(i32: A)<br>Pre-order number: 2<br>DepthFirstNumber: 1"]
  G1 --> G2
  G1 --> G3

The graph also shows a possible set of pre-order numbers, as well as the DepthFirstNumber that would be used in the search graph. You can see that they start to diverge. Pre-order numbers uniquely identify each goal in the graph. In contrast, after we finish proving Implemented(u32: A), we remove that node the graph, and hence its DepthFirstNumber is re-used.

Goal lifecycle

Every goal that we prove in the recursive solver goes through the following states:

graph TD
  NewlyCreated["Newly created"]
  OnStack["On stack and in the search graph"]
  InGraph["Popped from stack but retained in search graph"]
  ProcessingComplete["Processing complete"]
  InCache["Stored in the cache"]
  NewlyCreated --> OnStack
  OnStack -- Explore all program clauses for the goal --> ProcessingComplete
  ProcessingComplete -- If node is a participant in a cycle --> InGraph
  InGraph -- On next iteration --> OnStack
  ProcessingComplete -- If not part of a cycle or when fixed-point is reached --> InCache

At first, we create the goal and push it onto the stack, and we also add it to the search graph. We then explore each of the relevant program clauses to try and find the solution(s) to the goal. Along the way we update the overall solution:

• If there are no valid solutions, then the result is an error.
• If there is exactly one solution, then we remember it as the unique solution.
• If there are multiple distinct solutions, the result is "ambiguous".

While we are doing this solving, we also track what other goals this goal winds up depending on. In particular, we are looking to see whether it winds up as a participant in a cycle -- that is, if it depends on any goals further up the goal stack.

If, when we're done with all program clauses, the goal never participated in any cycles, then we have reached our final solution. We can take that result and put it into the cache. The next time we look for a solution to this goal, we'll check that cache and return the result.

But otherwise, if the goal was a participant in a cycle, then we have to iterate, as described in the section on cycles. In that case, we keep the goal in the search graph, but we remove it from the stack. This allows the search graph to serve as a kind of "interim cache". If, as we continue to search through the other nodes that remain on the stack, we have to solve this same goal again, we will find it in the search cache and re-use the result.

For goals that are participants in a cycle, when the cycle reaches its fixed-point (i.e., the top-most node has stopped changing), we go through and take all the results for all the subgoals (which are still present in the search graph) and move them all into the "final cache".

In other words, any result that is present in the search graph can be considered an "interim cache", with a result that is still being determined and may be dependent on other goals on the stack. Once the goal is completely processed, it is moved to the cache field where others can use it.

Processing a single goal, a flow chart

Whenever we are asked to solve a goal, these are the steps we take:

graph TD
  GoalInGraph["Goal in search graph?"]
  FlagAsHead["If goal is on stack,<br>flag as head of cycle."]
  ReturnCurrentResult["Return result from<br>search graph."]
  PushOnStack["Push goal on stack,<br>add to the search graph with index `G`,<br>initial result is error"]
  ProcessEachClause["Process each program clause in turn,<br>computing result,<br>and tracking `Minimums`"]
  IsCycleParticipant["Is G dependent on<br>goal lower in stack?"]
  StoreInCache["Move results `G..` <br>from search graph to cache"]
  PopFromCacheNotGraph["Pop goal from stack<br>but leave in search graph"]
  CompareResult["Did result change from<br>what is stored in search graph?"]
  UpdateSearchGraph["Update stored result<br>in search graph"]
  ClearPreviousIteration["Clear search graph nodes `G+1..`<br>from previous iteration"]

  GoalInGraph -- Yes --> FlagAsHead
  FlagAsHead --> ReturnCurrentResult
  GoalInGraph -- No, not in the graph --> PushOnStack
  PushOnStack --> ProcessEachClause
  ProcessEachClause -- Is head of cycle --> CompareResult
  ProcessEachClause -- Not head of cycle --> IsCycleParticipant
  CompareResult -- No, fixed-point reached --> IsCycleParticipant
  CompareResult -- Yes, result changed --> UpdateSearchGraph
  UpdateSearchGraph --> ClearPreviousIteration
  ClearPreviousIteration --> ProcessEachClause
  IsCycleParticipant -- No --> StoreInCache
  IsCycleParticipant -- Yes --> PopFromCacheNotGraph

Starting to prove a goal

The first thing we do when proving some goal G is to check the search graph to see if there is already a node for this goal.

If there is a node for G

If there is a node for G, that indicates that there is some sort of cycle involved in the graph. For now, we will defer this case, and come back to it after we've explained what happens without cycles.

If there is no node for G: pushing a new goal onto the stack

If there is no node for G in the graph, then we have a new subgoal to add to the graph. We will first push a new entry onto the stack, yielding some new stack depth d. Then we create a new Node in the search graph. It will be assigned the next available DepthFirstNumber. The search graph node contains a field stack_depth that will be set to Some(d), where d is the depth of the node on the stack.

The search graph node also stores the "current solution" for the given goal. As described in the search on inductive cycles, this solution starts out as an error but may be gradually widened as we iterate, if we find solutions.

Tracking dependencies

The way that we track dependencies is through a structure called the Minimums. The name comes from the idea that it is tracking the minimum DepthFirstNumber of any goal whose result we depended on. The minimum for a goal G1 starts out as G1, since its result depends on itself, but if it winds up recursively processing some goal G2 that is on the stack, then the minimum will be adjusted to G2.

Along with the interim solution, the search graph node for a given goal also stores the Minimums that resulted from computing that interim solution (i.e., what goals did that solution depend on). If some goal G1 winds up recursively invoking some goal G2 that is in the search graph but not present on the stack, then we update the current Minimums with the values stored in the search graph.

Removing nodes from the graph

Once we complete the processing for a node, it needs to be removed from the processing stack. But we wish to leave it in the graph if it is dependent on something else that is already on the stack. We do that just by checking the Minimums value to see if it is less than the current goal.

Coinduction

This sub-chapter is meant to describe the current handling of coinductive goals in the recursive solver rather than providing an extensive overview over the theoretical backgrounds and ideas. It follows the description in this GitHub comment and the Zulip topic linked there. In general, coinductive cycles can arise for well-formedness checking and autotraits. Therefore, correctly handling coinductive cycles is necessary to model the Rust trait system in its entirety.

General Idea

Coinductive cycles can be handled the same way as inductive cycles described before. The only difference is the start value for coinductive goals. Whereas inductive goals start with a negative result and are iterated until a least fixed-point is found, coinductive goals start with a positive result (i.e. a unique solution with identity substitution). This negative result is then iterated until a greatest fixed-point is reached.

Mixed co-inductive and inductive Cycles

As described above, the handling of inductive and coindutive cycles differs only in the start value from which the computation begins. Thus, it might seem reasonable to have mixed inductive and coinductive cycles as all goals inside these cycles would be handled the same way anyway. Unfortunately, this is not possible for the kind of logic that Chalk is based on (i.e. essentially an extension of co-LP for Hereditary Harrop clauses, cf. this paper).

There is fundamental difference between results for inductive cycles and results for coinductive cycles of goals. An inductive goal is provable if and only if there exists a proof for it consisting of a finite chain of derivations from axioms that are members of the least-fixed point of the underlying logic program. On the other hand, coinductive goals are provable if there exists an at most infinite derivation starting from the axioms that proves it (this includes in particular all finite derivations). This infinite derivation is then part of the greatest fixed-point of the logic program. As infinite derivations are not feasible to compute, it is enough to show that such a derivation contains no contradiction.

A simple example X :- X. (with X a free variable) is thus not provable by inductive reasoning (the least solution/lfp for this is the empty solution, a failure) but it is provable by coinductive reasoning (the greatest solution/gfp is the universe, i.e. all values).

This difference between inductive and coinductive results becomes a problem when combined in a single cycle. Consider a coinductive goal CG and an inductive goal IG. Now consider the simplest possible mixed cycle:

CG :- IG
IG :- CG

It is apparent, that there can not exist a solution for IG as the cyclic dependency prevents a finite proof derivation. In contrast to that, CG could potentially be provable as the derivation CG if IG if CG if IG ... is infinite and based only on the two axioms. As a result, CG would hold whereas IG would not hold, creating a contradiction.

The simplest solution to this problem, proposed by Simon et al. in their paper about co-LP, is to disallow mixed inductive and coinductive cycles. This approach is also used by Chalk.

Prevention of Invalid Results

The problem of invalid results propagated outside of the coinductive cycle is also described in the Coinduction chapter for the SLG solver alongside the rather complex handling used with it. Whereas the SLG solver introduces special constructs to handle coinduction, it is sufficient for the recursive solver to use the same logic for inductive and coinductive cycles. The following is a description of how this works in more detail.

The Problem

The problem arises if a solution that is purely based on the positive starting value for the coinductive cycle is cached (or tabled in logic programming terms) and as such propagated to other goals that are possibly reliant on this. An example where all clause goals are assumedly coinductive may look like this (cf. the test case coinduction::coinductive_unsound1):

C :- C1.
C :- C2.
C1 :- C2, C3.
C2 :- C1.

The following is a computation to find out whether there exists a type that implements C. Here the implementation of C may be proved by either showing that the type implements C1 or C2.

• Start proving C by trying to prove C1:
  • For C1 try to prove C2 and C3:
    • Start with C2. For C2 we need to prove C1:
      • This is a (coinductive) cycle. Assume that C1 holds, i.e. use the positive start value.
    • Based on this C2 also holds. If this case is not handled specifically, the solution for C2 is cached without a reference to the solution for C1 on which it depends.
    • Now try to prove C3:
      • Find that there is no way do so from the given axioms.
    • Thus, there exists no solution for C3 and the computation fails. This valid result is cached and lifted back up.
  • Due to the failure of C3 there is also no solution for C1. This failure is also cached correctly and lifted back up. The cached solution for C2 has now become invalid as it depends on a positive result for C1.
• As a result of the failure for C1, C can not be proved from C1. Try proving C from C2 instead:
  • Find the cached result that C2 has a solution and lift it back up.
• Due to the solution for C2, C is also proved with the same solution.
• Stop with this positive but invalid result for C.

The Solution

The above example should make it evident that the caching of found solutions in coinductive cycles can lead to invalid results and should therefore be prevented. This can be achieved by delaying the caching of all results inside the coinductive cycle until it is clear whether the start of the cycle (i.e. C1 in the example above) is provable (cf. the handling of inductive cycles before). If the start of the cycle can be proven by the results of the cycle and related subgoals then the assumption about it was correct and thus all results for goals inside the cycle are also valid. If, however, the start of the cycle can not be proved, i.e. the initial assumption was false, then a subset of the found solutions for the coinductive cycle may be invalid (i.e. the solution for C2 in the example).

To remove such invalid results, the cycle is restarted with a negative result for the cycle start. With this approach, it is possible to remove all invalid result that would otherwise depend on the disproved cycle assumption. To allow for the cycle to be restarted correctly, all nodes in the search graph after the cycle start are deleted.

With this procedure, the example is handled as follows:

• Start proving C with C1:
  • For C1 prove C2 and C3:
    • For C2 prove C1:
      • This is a coinductive cycle. Assume that C1 holds.
    • Thus C2 also holds. Delay the caching of the result about C2.
    • There is no way to prove C3. Cache this result and lift the failure up.
  • Due to the failure of C3 there is also no solution for C1. Set C1 to a negative result and restart the cycle.
    • For C2 prove C1:
      • C1 has now a negative result.
    • Thus, C2 also has a negative result which is not yet cached.
    • Find the already cached negative result for C3.
  • Nothing changed regarding C1 (this would indicate a negative cycle which is currently not allowed) and the negative result for C1 and C2 are cached. Lift the negative result for C1 back up.
• Start proving C with C2:
  • Find negative cached result for C2. Lift the result back up.
• Neither C1 nor C2 have a positive result. Stop with the valid disproof of C.

Glossary and terminology

This is a glossary of terminology (possibly) used in the chalk crate.

Notation

Basic notation

Rules

• forall<T> { (Vec<T>: Clone) :- (T: Clone): for every T, Vec<T> implements Clone if T implements Clone

Queries

• Vec<i32>: Clone: does Vec<i32> implement Clone?
• exists<T> { Vec<T>: Clone }: does there exist a T such that Vec<T> implements Clone?

Binary connective

There are sixteen logical connectives on two boolean variables. The most interesting in this context are listed below. There is also a truth table given which encodes the possible results of the operations like this

f(false, false) f(false, true) f(true, false) f(true, true).

As a shorthand the resulting truth table is encoded with true = 1 and false = 0.

Binder

A binder is an expression that binds a literal to a certain expression. Examples for binders:

• The universal quantifier forall(a) states that a certain condition holds for all allowed values for a.
• A function definition f(x) = a * x is a binder for the variable x whereas a is a free variable.
• A sum \sum_n x_n binds the index variable n.

Canonical Form

A formula in canonical form has the property that its De Bruijn indices are minimized. For example when the formula forall<0, 1> { 0: A && 1: B } is processed, both "branches" 0: A and 1: B are processed individually. The first branch would be in canonical form, the second branch not since the occurring De Bruijn index 1 could be replaced with 0.

Clause

A clause is the disjunction of several expressions. For example the clause condition_1 || condition_2 || ... states that at least one of the conditions holds.

There are two notable special cases of clauses. A Horn clause has at most one positive literal. A Definite clause has exactly one positive literal.

Horn clauses can be written in the form A || !B || !C || ... with A being the optional positive literal. Due to the equivalence (P => Q) <=> (!P || Q) the clause can be expressed as B && C && ... => A which means that A is true if B, C, etc. are all true. All rules in chalk are in this form. For example

struct A<T> {}
impl<T> B for A<T> where T: C + D {}

is expressed as the Horn clause (T: C) && (T: D) => (A<T>: B). This formula has to hold for all values of T. The second example

struct A {}
impl B for A {}
impl C for A {}

is expressed as the Horn clause (A: B) && (A: C). Note the missing consequence.

De Bruijn Index

De Bruijn indices numerate literals that are bound in an unambiguous way. The literal is given the number of its binder. The indices start at zero from the innermost binder increasing from the inside out.

Given the example forall<T> { exists<U> { T: Foo<Item=U> } } the literal names U and T are replaced with 0 and 1 respectively and the names are erased from the binders: forall<_> { exists<_> { 1: Foo<Item=0> } }.

As another example, in forall<X, Y> { forall <Z> { X } }, X is represented as ^1.0. The 1 represents the De Bruijn index of the variable and the 0 represents the index in that scope: X is bound in the second scope counting from where it is referenced, and it is the first variable bound in that scope.

Formula

A formula is a logical expression consisting of literals and constants connected by logical operators.

Goal

With a set of type variables, given types, traits and impls, a goal specifies a problem which is solved by finding types for the type variables that satisfy the formula. For example the goal exists<T> { T: u32 } can be solved with T = u32.

Literal

A literal is an atomic element of a formula together with the constants true and false. It is equivalent to a variable in an algebraic expressions. Note that literals are not the same as the type variables used in specifying a goal.

Normal form

To say that a statement is in a certain normal form means that the pattern in which the subformulas are arranged fulfill certain rules. The individual patterns have different advantages for their manipulation.

Conjunctive normal form (CNF)

A formula in CNF is a conjunction of disjunctions. For example (x1 || x2 || x3) && (x4 || x5 || x6) is in CNF.

Disjunctive normal form (DNF)

A formula in DNF is a disjunction of conjunctions. For example (x1 && x2 && x3) || (x4 && x5 && x6) is in DNF.

Negation normal form (NNF)

A formula in NNF consists only of literals, the connectives && and || and true and false.

Prenex normal form (PNF)

All quantifiers are on the highest level of a formula and do not occur inside the subformulas of the expression.

• forall(x). exists(y). forall(z). P(x) && P(y) => P(z) is in PNF.
• (exists(x). P(x)) => exists(y). P(y) && forall(z). P(z) is not in PNF.

Normalization

Normalization is the process of converting an associated type to a concrete type. In the case of an iterator this would mean that the associated Item type is replaced with something more meaningful with respect to the individual context (e.g. u32).

Projection

Projection is the reference to a field or (in the context of Rust) to a type from another type.

Satisfiability

A formula is satisfiable iff there is a valuation for the atoms inside the formula that makes it true.

Unification

Unification is the process of solving a formula. That means unification finds values for all the free literals of the formula that satisfy it. In the context of chalk the values refer to types.

Universe

A universe sets the scope in which a particular variable name is bound. (See Binder.) A universe can encapsulate other universes. A universe can be contained by only one parent universe. Universes have therefore a tree-like structure. A universe can access the variable names of itself and the parent universes but not of the sibling universes.

Well-formed

A formula is well-formed if it is constructed according to a predefined set of syntactic rules.

In the context of the Rust type system this means that basic rules for type construction have to be met. Two examples: 1) Given a struct definition

struct HashSet<T: Hash>

then a type HashSet<i32> is well-formed since i32 implements Hash. A type HashSet<NoHash> with a type NoHash that does not implement the Hash trait is not well-formed.

2. If a trait demands by its definition the implementation of further traits for a certain type then these secondary traits have to be implemented as well. If a type Foo implements trait Eq: PartialEq then this type has to implement trait PartialEq as well. If it does not, then the type Foo: Eq is not well formed according to Rust type building rules.

Quantifier

Existential quantifier

A formula with the existential quantifier exists(x). P(x) is satisfiable if and only if there exists at least one value for all possible values of x which satisfies the subformula P(x).

In the context of chalk, the existential quantifier usually demands the existence of exactly one instance (i.e. type) that satisfies the formula (i.e. type constraints). More than one instance means that the result is ambiguous.

Universal quantifier

A formula with the universal quantifier forall(x). P(x) is satisfiable if and only if the subformula P(x) is true for all possible values for x.

Helpful equivalences

• not(forall(x). P(x)) <=> exists(x). not(P(x))
• not(exists(x). P(x)) <=> forall(x). not(P(x))

Skolemization

Skolemization is a technique of transferring a logical formula with existential quantifiers to a statement without them. The resulting statement is in general not equivalent to the original statement but equisatisfiable.

Validity

An argument (premise therefore conclusion) is valid iff there is no valuation which makes the premise true and the conclusion false.

Valid: A && B therefore A || B. Invalid: A || B therefore A && B because the valuation A = true, B = false makes the premise true and the conclusion false.

Valuation

A valuation is an assignment of values to all variables inside a logical formula.

Fixed-Points

A fixed-point of a function f is a value x for which f(x)=x. Similarly a pre-fixed-point is defined as x ≤ f(x), whereas for a post-fixed-point it holds that f(x) ≤ x.

A least fixed-point (lfp) of f is the fixed-point x of f for which all other fixed-points y are greater or equal (i.e. if f(y)=y then x ≤ y). Similarly, a greatest fixed-point (gfp) is greater or equal than all other fixed-points. If f is a function on sets, the least fixed-point is defined as the intersection of all pre-fixed-points, which are then defined as sets x for which x ⊆ f(x). The greatest fixed-point is in this case the union of all post-fixed-points, respectively.

This simple definition of lfp and gfp can also be lifted to general lattices. The results for Chalk goals form such a lattice and, thus, every solver for such goals tries to find such fixed-points.

Bibliography

If you'd like to read more background material, here are some recommended texts and papers:

Blog Posts

• Lowering Rust traits to logic
• Unification in Chalk, part 1
• Unification in Chalk, part 2
• Negative reasoning in Chalk
• Query structure in chalk
• Cyclic queries in chalk
• An on-demand SLG solver for chalk

Papers

"A proof procedure for the logic of Hereditary Harrop formulas", by Gopalan Nadathur. This paper covers the basics of universes, environments, and Lambda Prolog-style proof search. Quite readable.

"A new formulation of tabled resolution with delay", by Theresa Swift. This paper gives a kind of abstract treatment of the SLG formulation that is the basis for our on-demand solver.

Books

• "Introduction to Formal Logic", Peter Smith
• "Handbook of Practical Logic and Automated Reasoning", John Harrison
• "Types and Programming Languages", Benjamin C. Pierce
• Programming with Higher-order Logic, by Dale Miller and Gopalan Nadathur, covers the key concepts of Lambda prolog. Although it's a slim little volume, it's the kind of book where you learn something new every time you open it.

Incomplete chapters

Some topics yet to be written:

• Elaborate on the proof procedure
• SLG solving – introduce negative reasoning
• Go over how trait impls are selected and checked
• Add a section on higher-ranked trait bounds

Publishing Chalk

Note: this is mostly only useful for maintainers

The following crates get published to crates.io:

• chalk-derive
• chalk-engine
• chalk-ir
• chalk-recursive
• chalk-solve

The following crates get versioned without publishing:

• chalk-parse
• chalk-integration
• chalk (root directory)

Release Automation

Releases are fully automated. Once a week (Sunday at midnight UTC) a GitHub Actions job is executed which generates the changelog, bumps crate versions, and publishes the crates. If there have not been any changes since the last version, the release is skipped. However, if the job is manually triggered then the release will be published even if there are no changes.

The release pipeline is located in publish.yml.

Changelog Generation

The changelog is generated using auto-changelog and is stored in RELEASES.md. The template used for the changelog is in releases-template.hbs.