Next-gen trait solving - Rust Compiler Development Guide (original) (raw)
Rust Compiler Development Guide
Trait solving (new)
This chapter describes how trait solving works with the new WIP solver located inrustc_trait_selection/solve. Feel free to also look at the docs forthe current solver and the chalk solver.
Core concepts
The goal of the trait system is to check whether a given trait bound is satisfied. Most notably when typechecking the body of - potentially generic - functions. For example:
#![allow(unused)]
fn main() {
fn uses_vec_clone<T: Clone>(x: Vec<T>) -> (Vec<T>, Vec<T>) {
(x.clone(), x)
}
}
Here the call to x.clone()
requires us to prove that Vec<T>
implements Clone
given the assumption that T: Clone
is true. We can assume T: Clone
as that will be proven by callers of this function.
The concept of "prove the Vec<T>: Clone
with the assumption T: Clone
" is called a Goal. Both Vec<T>: Clone
and T: Clone
are represented using Predicate. There are other predicates, most notably equality bounds on associated items: <Vec<T> as IntoIterator>::Item == T
. See the PredicateKind
enum for an exhaustive list. A Goal
is represented as the predicate
we have to prove and the param_env
in which this predicate has to hold.
We prove goals by checking whether each possible Candidate applies for the given goal by recursively proving its nested goals. For a list of possible candidates with examples, look atCandidateSource. The most important candidates are Impl
candidates, i.e. trait implementations written by the user, and ParamEnv
candidates, i.e. assumptions in our current environment.
Looking at the above example, to prove Vec<T>: Clone
we first useimpl<T: Clone> Clone for Vec<T>
. To use this impl we have to prove the nested goal that T: Clone
holds. This can use the assumption T: Clone
from the ParamEnv
which does not have any nested goals. Therefore Vec<T>: Clone
holds.
The trait solver can either return success, ambiguity or an error as a CanonicalResponse. For success and ambiguity it also returns constraints inference and region constraints.