Rust's next-generation trait solver

Rust's compiler team has been working on a long-term project to rewrite the trait solver — the part of the compiler that determines which concrete function should be called when a programmer uses a trait method that is implemented for multiple types. The rewrite is intended to simplify future changes to the trait system, fix a handful of tricky soundness bugs, and provide faster compile times. It's also nearly finished, with a relatively small number of remaining blocking bugs.

Trait solving

Traits in Rust are similar to typeclasses in Haskell or interfaces in Java: they are a set of associated functions that can be implemented for different types. Library code can use the functions from a trait on any type that implements the trait, even if that type is foreign to the library. When it comes time to generate code, however, the compiler needs to know which specific type is being used, and where its trait implementation lives, so that it can call the correct function. Trait implementations can be generic, and therefore apply to multiple concrete types. Figuring out which trait implementation is relevant to a particular type is the job of the compiler's trait solver.

Most of the time, this is straightforward: the compiler just needs to find a trait implementation of the form impl Trait for Type {...}. The problem grows more complex when considering generic types. For example, a Vec can be cloned if and only if the type of elements it contains can be cloned. In the standard library, there is a trait implementation block that is equivalent to the following (after expanding some syntactic sugar and disregarding the irrelevant A parameter):

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

This declaration can be viewed as an instruction for the trait solver: in order to find the Clone implementation for a Vec<Foo>, first find the Clone implementation for Foo. That implementation can be used to construct a working implementation for Vec<Foo>. The current trait solver follows these chains of instructions in a straightforward way. For each trait implementation that must be found, it determines whether it is best resolved through finding an impl statement or through using a where-bound (i.e. a where clause asserting that some generic type implements a trait). These can depend on other trait implementations existing, as in the Vec example, in which case the compiler adds them to a work list. In logic programming, these kinds of prerequisites that must be satisfied for another goal to be reached are called obligations; the compiler keeps taking obligations from the work list and processing them until they have all been eliminated. If they cannot be, an error is indicated.

This approach breaks down with more complicated types, however. It is possible to construct a situation where the obligations to be discharged form a loop. Doing so is a bit complicated, however, so even a minimal example is somewhat long:

    // Create a trait that has an associated generic type. Types that implement
    // Wrap correspond to a particular choice of Wrapper.
    trait Wrap {
        type Wrapper<T>;
    }

    // A singly linked list structure, with the payload omitted for brevity.
    // Each 'next' pointer goes to another list node wrapped in the Wrapper type
    // for some generic type W that must implement Wrap
    struct Link<W: Wrap> {
        next: Option<Box<W::Wrapper<Link<W>>>>
    }

    // Link structures can be formatted for debug print statements when their
    // contents can be — the omitted implementation calls the Debug
    // implementation for next's type, hence the second requirement.
    impl<W> Debug for Link<W>
    where W: Wrap,
          Option<Box<W::Wrapper<Link<W>>>>: Debug {
        ...      
    }

    // My Wrapper is a structure that wraps some other type T as its only field.
    struct MyWrapper<T = ()>(T);

    // And its associated wrapper type is just itself.
    impl Wrap for MyWrapper {
        type Wrapper<T> = MyWrapper<T>;
    }

    // Finally, wrappers can be formatted for debug print statements when the
    // wrapped value can be.
    impl<T> Debug for MyWrapper<T>
    where T: Debug { ... }

In order for the compiler to prove that Link<MyWrapper> implements Debug, it needs to show that a whole chain of requirements holds:

    Link<MyWrapper>: Debug ->
    Option<Box<MyWrapper::Wrapper<Link<MyWrapper>>>>: Debug ->
    Box<MyWrapper::Wrapper<Link<MyWrapper>>>: Debug ->
    MyWrapper::Wrapper<Link<MyWrapper>>: Debug ->
    Link<MyWrapper>: Debug

... but that chain eventually leads the compiler right back to where it started. Attempting to compile a Rust program that uses the Debug implementation of Link results in the error: "overflow evaluating the requirement `Link<MyWrapper>: Debug`".

In this case, however, it should be possible in theory for the compiler to generate an implementation of Debug for the same reason that assemblers can handle instructions that refer to their own address: the compiler can start generating the implementation, leaving a placeholder for the address, and then fill the address in once it knows it. At the stage where the trait solver runs, it isn't dealing with actual addresses, but the same idea applies; writing the Debug implementation for Link<MyWrapper> is a matter of "tying the knot" in a data structure representing the code to produce a structure that refers to itself.

The above example is contrived, but that's because this limitation of the language tends to come up in complex, highly generic code. Self-referential types are nothing new; it's only trying to abstract over them with traits that causes the problem. Code like that is not something that every programmer will need to write, but it is something that can make Rust libraries more flexible. Currently, crate authors need to work around this trait resolution problem by restructuring their interfaces to avoid creating loops in the trait solver.

A new approach

The trait solver's behavior isn't an inherent aspect of the problem, however. It's an implementation choice that was made essentially by default as the language's trait system slowly became more complex. The project to rewrite the trait solver began in 2015 with Chalk, an attempt to formalize Rust's type system. It compiles the rules of the type system — such as the mechanics of trait solving — into a Prolog-like system of logical inference rules that can then be solved generically with well-known logic-programming techniques. Chalk has two internal implementations of logical inference with their own strengths and weaknesses: the SLG solver (which uses an approach based on Prolog tabling) and the recursive solver, which more closely matches the operation of Rust's original trait solver. The SLG solver can handle some kinds of loops that the recursive solver cannot.

Rust developers determined that Chalk wasn't a good fit for the Rust compiler, however. One major concern was with maintaining the usefulness of error messages; the current implementation produces good error messages for simple mistakes, but Chalk's error messages have lagged behind. In 2023, the project decided to rewrite the trait solver within the compiler, using lessons from the first implementation and from Chalk.

The rewrite, called the next-generation trait solver, makes use of caching to both speed up trait solving and to defeat cycles. When called upon to start finding a trait implementation for a type, it starts by assuming that such an implementation will be found, and making a spot for it in the cache — it is marked as provisionally true, but cannot yet be fully relied on. Then the solver follows the chain of logical inferences in much the same manner as the current solver, with the exception that it looks results up in the cache when possible. When it derives a new piece of information, that is added to the cache; if deriving the new information relied on any provisional cache entries, the new entry is also marked as provisional.

If the trait solver ever reaches a point where the only remaining logical obligations refer to provisionally true cache entries, the entries are upgraded to actually true and can be referenced by other type-checking operations. On the other hand, if it doesn't reach such a point, the provisional cache entries are invalidated, and that branch of the computation is considered failed. It will either fail entirely (and show an error to the user), or continue trying some alternative potential solution.

In the case of the example above, when the new solver reached the state of needing to prove that Link<MyWrapper> implements Debug for the second time, it would see that the trait implementation had been cached as provisionally true by the previous exploration and (lacking other logical obligations) conclude that Link<MyWrapper> really does implement Debug.

Currently, the next-generation trait solver only extends this notion of provisional cache entries to a limited number of built-in traits, such as Send, but the plan is to eventually enable the behavior for all traits. The Rust developers are fairly sure that enabling this feature will just allow some code (like the above example) that doesn't currently compile to work, but since this is a logically intricate piece of code on which the correctness of the type system depends, they don't want to be too hasty. The next-generation trait solver itself is currently marked experimental for much the same reason.

One other interesting aspect of the next-generation trait solver is canonicalization. Since its design relies heavily on caching, the more types that can be cached, the faster compilation using the new trait solver will be. For that reason, logical obligations encountered in the course of trait solving are rewritten into a format that removes as many type variables and intermediate results as possible. This also has the nice effect of making it easy to reconstruct proof trees explaining how the compiler reached a particular answer. These are used to create more detailed error messages by explaining which options were tried and why they didn't work. Since the proof trees don't need to be generated unless an error message needs to be shown, being able to reconstruct them from the cache avoids the overhead of constructing them for code that does compile.

Trying it out

The next-generation trait solver is already used in stable Rust for coherence checking (that is, checking that trait implementations do not overlap), but is not yet used for general trait solving. In the nightly release of the compiler, the -Znext-solver=globally flag uses the next-generation trait solver for all trait-related type-system computations. The Rust developers have already used Crater to check that the flag does not cause compile errors for crates publicly released on crates.io, but would like to know if the flag causes problems for anyone's code prior to stabilization.

There are currently 76 open bugs related to the new trait solver, and 78 closed ones. The feature has made more progress than that suggests, however, since several of the closed bugs are rather large, and the remaining bugs are mostly internal compiler errors or performance problems that the Rust developers would like to see addressed. The new trait solver is intended to be both faster and more maintainable than the previous implementation, but whether that promise bears out remains to be seen. In either case, Rust developers may soon have the option to write more-complicated self-referential trait-based interfaces.