src/doc/rustc-dev-guide/src/solve/trait-solving.md

   1 # Trait solving (new)
   2
   3 This chapter describes how trait solving works with the new WIP solver located in
   4 [`rustc_trait_selection/solve`][solve]. Feel free to also look at the docs for
   5 [the current solver](../traits/resolution.md) and [the chalk solver](../traits/chalk.md)
   6 can be found separately.
   7
   8 ## Core concepts
   9
  10 The goal of the trait system is to check whether a given trait bound is satisfied.
  11 Most notably when typechecking the body of - potentially generic - functions.
  12 For example:
  13
  14 ```rust
  15 fn uses_vec_clone<T: Clone>(x: Vec<T>) -> (Vec<T>, Vec<T>) {
  16     (x.clone(), x)
  17 }
  18 ```
  19 Here the call to `x.clone()` requires us to prove that `Vec<T>` implements `Clone` given
  20 the assumption that `T: Clone` is true. We can assume `T: Clone` as that will be proven by
  21 callers of this function.
  22
  23 The concept of "prove the `Vec<T>: Clone` with the assumption `T: Clone`" is called a [`Goal`].
  24 Both `Vec<T>: Clone` and `T: Clone` are represented using [`Predicate`]. There are other
  25 predicates, most notably equality bounds on associated items: `<Vec<T> as IntoIterator>::Item == T`.
  26 See the `PredicateKind` enum for an exhaustive list. A `Goal` is represented as the `predicate` we
  27 have to prove and the `param_env` in which this predicate has to hold.
  28
  29 We prove goals by checking whether each possible [`Candidate`] applies for the given goal by
  30 recursively proving its nested goals. For a list of possible candidates with examples, look at
  31 [`CandidateSource`]. The most important candidates are `Impl` candidates, i.e. trait implementations
  32 written by the user, and `ParamEnv` candidates, i.e. assumptions in our current environment.
  33
  34 Looking at the above example, to prove `Vec<T>: Clone` we first use
  35 `impl<T: Clone> Clone for Vec<T>`. To use this impl we have to prove the nested
  36 goal that `T: Clone` holds. This can use the assumption `T: Clone` from the `ParamEnv`
  37 which does not have any nested goals. Therefore `Vec<T>: Clone` holds.
  38
  39 The trait solver can either return success, ambiguity or an error as a [`CanonicalResponse`].
  40 For success and ambiguity it also returns constraints inference and region constraints.
  41
  42 ## Requirements
  43
  44 Before we dive into the new solver lets first take the time to go through all of our requirements
  45 on the trait system. We can then use these to guide our design later on.
  46
  47 TODO: elaborate on these rules and get more precise about their meaning.
  48 Also add issues where each of these rules have been broken in the past
  49 (or still are).
  50
  51 ### 1. The trait solver has to be *sound*
  52
  53 This means that we must never return *success* for goals for which no `impl` exists. That would
  54 simply be unsound by assuming a trait is implemented even though it is not. When using predicates
  55 from the `where`-bounds, the `impl` will be proved by the user of the item.
  56
  57 ### 2. If type checker solves generic goal concrete instantiations of that goal have the same result
  58
  59 Pretty much: If we successfully typecheck a generic function concrete instantiations
  60 of that function should also typeck. We should not get errors post-monomorphization.
  61 We can however get overflow as in the following snippet:
  62
  63 ```rust
  64 fn foo<T: Trait>(x: )
  65 ```
  66
  67 ### 3. Trait goals in empty environments are proven by a unique impl
  68
  69 If a trait goal holds with an empty environment, there is a unique `impl`,
  70 either user-defined or builtin, which is used to prove that goal.
  71
  72 This is necessary for codegen to select a unique method.
  73 An exception here are *marker traits* which are allowed to overlap.
  74
  75 ### 4. Normalization in empty environments results in a unique type
  76
  77 Normalization for alias types/consts has a unique result. Otherwise we can easily implement
  78 transmute in safe code. Given the following function, we have to make sure that the input and
  79 output types always get normalized to the same concrete type.
  80 ```rust
  81 fn foo<T: Trait>(
  82     x: <T as Trait>::Assoc
  83 ) -> <T as Trait>::Assoc {
  84     x
  85 }
  86 ```
  87
  88 ### 5. During coherence trait solving has to be complete
  89
  90 During coherence we never return *error* for goals which can be proven. This allows overlapping
  91 impls which would break rule 3.
  92
  93 ### 6. Trait solving must be (free) lifetime agnostic
  94
  95 Trait solving during codegen should have the same result as during typeck. As we erase
  96 all free regions during codegen we must not rely on them during typeck. A noteworthy example
  97 is special behavior for `'static`.
  98
  99 ### 7. Removing ambiguity makes strictly more things compile
 100
 101 We *should* not rely on ambiguity for things to compile.
 102 Not doing that will cause future improvements to be breaking changes.
 103
 104 ### 8. semantic equality implies structural equality
 105
 106 Two types being equal in the type system must mean that they have the same `TypeId`.
 107
 108
 109 [solve]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_trait_selection/solve/index.html
 110 [`Goal`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_trait_selection/solve/struct.Goal.html
 111 [`Predicate`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/struct.Predicate.html
 112 [`Candidate`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_trait_selection/solve/assembly/struct.Candidate.html
 113 [`CandidateSource`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_trait_selection/solve/assembly/enum.CandidateSource.html
 114 [`CanonicalResponse`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_trait_selection/solve/type.CanonicalResponse.html