# trait solver explore session doc from https://www.youtube.com/watch?v=4E5x2PzEKhg - projection: `fn foo<T: Trait<Assoc = u32>>()` as caller have to prove `<T as Trait>::Assoc == u32` - `Vec<<u32 as Trait>::Output>` normalize that to `Vec<String>` auto trait impl: ```rust struct Foo { field: String, other_field: Vec<u32>, } ``` `Foo: Send` goal constituent types are: - `[String, Vec<u32>]` - check: `String: Send` - `Vec<u32>: Send` ```rust! trait Foo<T> {} impl Foo<u32> for i32 {} fn impls_foo<T: Foo<U>, U>() {} fn main() { impls_foo::<i32, _>(); } ``` can inherit associated types ```rust trait Trait { type Assoc = u32; } impl Trait for () {} ``` ```rust enum List<T> { Nil, Cons(T, Box<List<T>>), } ``` - `List<u32>: Send` - `u32: Send` - `Box<List<u32>>: Send` - `List<u32>: Send` for coinduction: https://github.com/rust-lang/rustc-dev-guide/pull/1551 - `u32: Trait<?0>` - `u32: Trait<?3>` instead prove - `exists<T> u32: Trait<T>` - yes: but `T` has to be `u32` > What happens if there are multiple types that ` T` can be? i.e. `u32` impls both `Trait<A>` and `Trait<B>` and we are proving `u32: Trait<?0>` ```rust! impl Trait<A> for u32 {} // impl a impl Trait<B> for u32 {} // impl b ``` `assemble_and_evaluate_candidates` return `[Candidate { source: impl a, result: Yes, ?0 == A }, Candidate { source: impl b, result: Yes, ?0 == B }]` `merge_trait_candidates_discard_reservation_impls` returns `Ambiguity` with no constraints. ```rust! impl Trait<Vec<A>> for u32 {} // impl a impl Trait<Vec<B>> for u32 {} // impl b ``` `assemble_and_evaluate_candidates` return `[Candidate { source: impl a, result: Yes, ?0 == Vec<A> }, Candidate { source: impl b, result: Yes, ?0 == Vec<B> }]` `Ambiguous` but we know `?0 = Vec<?1>` ### canonicalization: rustc-dev-guide sections: new solver section is XXX (still PR) chalk section about it: https://rust-lang.github.io/chalk/book/canonical_queries/canonicalization.html ---- A step by step walkthrough: Example goal: `Vec<?x>: Trait<?y, Vec<?y>>` - replace infer vars and placeholders with canonical variables bound by the `Canonical`, putting the original values (and universes) into an `OriginalQueryValues` map. - `Canonical`:`exists<T0, T1> Vec<T0>: Trait<T1, Vec<T1>>` - `OriginalQueryValues`: `[?x, ?y]` - call the query with only the `Canonical` - instantiate the `Canonical`, instantiating the bound vars not only in the `goal`, but also for `CanonicalVarValues` - `goal`: `Vec<?0>: Trait<?1, Vec<?1>>` - `CanonicalVarValues`: `[?0, ?1]` - compute the query - e.g. it holds for `Vec<u32>: Trait<Box<?2>, Vec<Box<?2>>>` - `goal`: `Vec<u32>: Trait<Box<?2>, Vec<Box<?2>>>` - `CanonicalVarValues`: `[u32, Box<?2>]` (if we were to resolve the vars eagerly) - as a response we only need the `CanonicalVarValues` - result: `OK` - `CanonicalVarValues`: `exists<T0> [u32, Box<T0>]` - the caller instantiates the var values again with the universe info from the `OriginalQueryValues` map - `CanonicalVarValues`: `[u32, Box<?z>]` - finally, equate the `OrginalQueryValues` with the `CanonicalVarValues` - `?x == u32`, `?y == Box<?z>` - final (non-canonical) result - OK `Vec<u32>: Trait<Box<?z>, Vec<Box<?z>>>` holds :tada: --- `exists<T> forall<U> { T == U }` this doesn't hold `forall<U> exists<T> { T == U }` this holds `exists<T> for<'a> u32: Trait<'a, T>` - `u32: Trait<'!a.1, ?t.0>` - `<() as Foo<'!a.1, ?t.0>::Assoc: OtherTrait` - `Projection<<() as Foo<'!a.1, ?t.0>>::Assoc, ?0.1)` - `exists<T> for<'a> exists<U> Projection<<() as Foo<'a, T>>::Assoc, U)`