Trait solving (new-style)

🚧 This chapter describes "new-style" trait solving. This is still in the process of being implemented; this chapter serves as a kind of in-progress design document. If you would prefer to read about how the current trait solver works, check out this other chapter. 🚧

By the way, if you would like to help in hacking on the new solver, you will find instructions for getting involved in the Traits Working Group tracking issue!

The new-style trait solver is based on the work done in chalk. Chalk recasts Rust's trait system explicitly in terms of logic programming. It does this by "lowering" Rust code into a kind of logic program we can then execute queries against.

You can read more about chalk itself in the Overview of Chalk section.

Trait solving in rustc is based around a few key ideas:

  • Lowering to logic, which expresses Rust traits in terms of standard logical terms.
    • The goals and clauses chapter describes the precise form of rules we use, and lowering rules gives the complete set of lowering rules in a more reference-like form.
    • Lazy normalization, which is the technique we use to accommodate associated types when figuring out whether types are equal.
    • Region constraints, which are accumulated during trait solving but mostly ignored. This means that trait solving effectively ignores the precise regions involved, always – but we still remember the constraints on them so that those constraints can be checked by the type checker.
  • Canonical queries, which allow us to solve trait problems (like "is Foo implemented for the type Bar?") once, and then apply that same result independently in many different inference contexts.

This is not a complete list of topics. See the sidebar for more.

Ongoing work

The design of the new-style trait solving currently happens in two places:

chalk. The chalk repository is where we experiment with new ideas and designs for the trait system. It primarily consists of two parts:

  • a unit testing framework for the correctness and feasibility of the logical rules defining the new-style trait system.
  • the chalk_engine crate, which defines the new-style trait solver used both in the unit testing framework and in rustc.

rustc. Once we are happy with the logical rules, we proceed to implementing them in rustc. This mainly happens in librustc_traits.