Type System 2 @BoxyUwU @WaffleLapkin

struct A;
struct B;
struct C;

trait Trait<'a, T> {
    type Assoc;
}

trait Bound {}

impl Bound for B {}
impl Bound for C {}

impl<'a> Trait<'a, B> for A {
    type Assoc = B;
}

impl<'a> Trait<'a, C> for A {
    type Assoc = C;
}

fn f<T>(_: T)
where
    for<'a> A: Trait<'a, T>,
    for<'a> <A as Trait<'a, T>>::Assoc: Bound,
{
}

fn main() {
    f(B);
}
Solution
error[E0277]: the trait bound `for<'a> <A as Trait<'a, _>>::Assoc: Bound` is not satisfied
  --> examples/trait_solver_2.rs:30:7
   |
30 |     f(B);
   |     - ^ the trait `for<'a> Bound` is not implemented for `<A as Trait<'a, _>>::Assoc`
   |     |
   |     required by a bound introduced by this call
   |
help: the following other types implement trait `Bound`
  --> examples/trait_solver_2.rs:11:1
   |
11 | impl Bound for B {}
   | ^^^^^^^^^^^^^^^^ `B`
12 | impl Bound for C {}
   | ^^^^^^^^^^^^^^^^ `C`
note: this is a known limitation of the trait solver that will be lifted in the future
  --> examples/trait_solver_2.rs:30:7
   |
30 |     f(B);
   |     --^-
   |     | |
   |     | the trait solver is unable to infer the generic types that should be inferred from this argument
   |     add turbofish arguments to this call to specify the types manually, even if it's redundant
note: required by a bound in `f`
  --> examples/trait_solver_2.rs:25:41
   |
22 | fn f<T>(_: T)
   |    - required by a bound in this function
...
25 |     for<'a> <A as Trait<'a, T>>::Assoc: Bound,
   |                                         ^^^^^ required by this bound in `f`

For more information about this error, try `rustc --explain E0277`.
error: could not compile `code` (example "trait_solver_2") due to 1 previous error

As the error message states this is actually a compiler bug! The trait bound for<'a> <A as Trait<'a, B>>::Assoc: Bound does actually hold.

Let's step through the process of type checking fn main to see where the compiler goes wrong.

Firstly, f(B); desugars to f::<_>(B). Let's give the inferred type argument of _ the name ?x for future reference.

Note that while as humans we can trivially tell that ?x should be inferred to B, the compiler has to actually figure this out which happens at a later step than where the bug in the compiler is.

When typechecking a function call, the compiler is responsible for checking all the where clauses of the function hold. This looks something like:

  1. Iterate over all the where clauses on the function
  2. For each where clause replace any generic parameters with the corresponding generic arguments provided by the caller
  3. Iterate over the list of where clauses with generic parameters replaced
  4. For each where clause have the trait solver try and prove the trait bound

In this question we have the function call f::<?x>(B), going through the above steps would look something like:

  1. Iterate over the where clauses
    • for<'a> A: Trait<'a, T>
    • for<'a> <A as Trait<'a, T>>::Assoc: Bound
  2. Replace the generic parameters with the generic arguments provided by the caller, in this case T should be replaced with ?x
    • for<'a> A: Trait<'a, ?x>
    • for<'a> <A as Trait<'a, ?x>>::Assoc: Bound
  3. Iterate over the where clauses with replaced generic parameters
    • See above list
  4. Have the trait solver check these trait bounds
    • for<'a> A: Trait<'a, ?x>. The trait solver handles this correct and returns ambiguity, meaning it doesn't yet know whether the trait bound holds or not.
    • for<'a> <A as Trait<'a, ?x>>::Assoc: Bound. The trait solver handles this incorrectly, and returns an error, meaning it thinks the trait bound doesn't hold.

The trait solver considers for<'a> <A as Trait<'a, ?x>>::Assoc: Bound to not hold due to a bug in how associated types are handled.

Let's start with going over a bit of context about how associated types are handled.

Currently the trait solver expects that all associated types have either been replaced with the aliased type, or the associated type is too generic and will never be possible to figure out what the aliased type is.

fn replaced_with_aliased_type() -> <std::vec::Iter<'_, u8> as Iterator>::Item {
    /* not important */
}

fn too_generic<I: Iterator>(i: I) -> <I as Iterator>::Item { 
    /* not important */
}

In this example we have two associated types:

  1. <std::vec::Iter<'_, u8> as Iterator>::Item
  2. <I as Iterator>::Item

The first associated type can be replaced with the aliased type, u8, by looking at the implementation of Iterator for std::vec::Iter and looking at the definition of the Item associated type.

The second associated type can't be replaced with the aliased type as there is no implementation corresponding to I: Iterator- only a trait bound.

Now, stepping back, if you remember the example trait bound that the trait solver doesn't handle correctly: for<'a> <A as Trait<'a, ?x>>::Assoc: Bound.

Part of this trait bound is the associated type <A as Trait<'a, ?x>>::Assoc. This associated type doesn't fit into either of the options we just discussed.

The compiler can't replace it with the aliased type because we dont't know which implementation to look at- it could be either Trait<'a, B> for A or Trait<'a, C> for A!

It's also not "too generic", there's no trait bound on main corresponding to A: Trait<'a, ?x>. This associated type should be able to be replaced with the aliased type, the compiler just can't do so yet at this point during type inference.

This associated type violates the expectation that all associated types fit neatly into one of these two categories.

When attempting to check the for<'a> <A as Trait<'a, ?x>>::Assoc: Bound trait bound holds, the trait solver assumes the associated type is this "too generic" kind of associated type.

Due to this assumption, it considers the types B and C to not be equal to <A as Trait<'a, ?x>>::Assoc. This in turn means that the impl's Bound for B and Bound for C are considered to not apply, as in order for these impls to be useable, the associated type must be equal to B or C (depending on which impl we're talking about).

Finally, as there are no impls that apply when trying to check the for<'a> <A as Trait<'a, ?x>>::Assoc: Bound trait bound, the trait solver considers the trait bound to not hold.

Note: This bug is fixed by the next-gen trait solver! Running this question's example with the unstable -Znext-solver flag results in compilation succeeding.