Compiler fails to recognise associated type bound

1

I encountered the following weird situation (example is highly simplified, playground: Rust Playground):

pub trait A {
    type X: B<T = Self>;
    type Y: A<X = Self::Z>;
    type Z: B;
}

pub trait B {
    type T;
    
    fn with_t(self, t: Self::T);
}

pub fn comp<S: A>(m: S::Y, s: <S::Y as A>::X) {
    s.with_t(m)
}

I would have hoped that the compiler understands that <<S::Y as A>::X as B>::T is the same type as S::Y due to the constraint on A::X, but it seems like it does not:

   Compiling playground v0.0.1 (/playground)
error[E0308]: mismatched types
  --> src/lib.rs:14:14
   |
14 |     s.with_t(m)
   |       ------ ^ expected `B::T`, found `A::Y`
   |       |
   |       arguments to this method are incorrect
   |
   = note: expected associated type `<<S as A>::Z as B>::T`
              found associated type `<S as A>::Y`
   = note: an associated type was expected, but a different one was found
note: method defined here
  --> src/lib.rs:10:8
   |
10 |     fn with_t(self, t: Self::T);
   |        ^^^^^^       -

For more information about this error, try `rustc --explain E0308`.
error: could not compile `playground` (lib) due to 1 previous error

The weird thing is that it works if I remove the <X = Self::Z> from A::Y which seems to bring the compiler on the wrong track. Any idea why this is happening and how I can fix this?

2

honestly i don't think i can follow it myself unless i take out a whiteboard to map all the relations and i doubt the compiler does that deep of a reasoning. in any case i strongly advise you to find a way to reduce the levels of indirection in the relationships between the types

3

Plus this code seems uncomfortably adjacent to unsoundness exploits which are, to this day, not fixed.

Does the next-gen trait solver help, by any chance?

4

In addition to what has been said above, which I second, here's my observation:

In comp you call s.with_t on m where s is required to be A::X. However, m is A::Y which in turn is A with X = Self::Z.
Since X: B<T = Self> and Z: B, it is not guaranteed, that <Z as B>::T is Self.
Hence, the bounds, as they are expressed, don't require the types of <m as B>::T and <s as B>::T to be the same.

Possible fix:

5

My guess is that the A<X = Self::Z> opens a path in the normalization recursion where _: B<T = Self> doesn't have to hold and no further reductions are possible; something like

<S as A>::Y =?= <<<S as A>::Y as A>::X as B>::T
// apply <<<S as A>::Y as A>::X as B>::T == <S as A>::Y
<S as A>::Y =?= <<S as A>::Y
// success

<S as A>::Y =?= <<<S as A>::Y as A>::X as B>::T
// apply <<S as A>::Y as A>::X == <S as A>::Z;
<S as A>::Y =?= <<S as A>::Z as B>::T
// can't reduce further on this path

If I understand your goal correctly, you can add the implication it is failing to prove as another associated type bound.

-    type Z;
+    type Z: B<T = Self::Y>;

I didn't try to follow your logic through, but the bounds you suggest reject some set of implementations which mine do not, as per the playground.

6

And in case it's useful, I got to my solution in part by mapping out some of the original implications:

    type X: B<T = Self>;
    type Y: A;
    type Z: B;

// Boxes are `Type: TraitItImplements`
// Paths `U:V` are following `<_ as U>::V`

         +-----+
  +----> | S:A |
  |      +-----+
  |         |_________ _________
  |         |         |         |
 B|T       A|X       A|Y       A|Z
  |         |         |         |
  |         V         V         V
  |      +-----+   +-----+   +-----+   B    +-----+
  +----- | C:B |   | D:A |   | E:B | -----> | J   |
         +-----+   +-----+   +-----+   T    +-----+
                    ^   |
                    |  A|X
                   B|T  |
                    |   V
                   +-----+
                   | G:B | ...
                   +-----+

And then when you add the requirement Y: A<X = Self::Z>, you end up combining boxes G:B and E:B, and thus also combing boxes J and D:A.

         +-----+
  +----> | S:A |
  |      +-----+
  |         |_________ ______________
  |         |         |              |
 B|T       A|X       A|Y            A|Z
  |         |         |              |
  |         V         V              V
  |      +-----+   +-----+  A     +-----+
  |      |     |   |     |------->| (G) |
  +----- | C:B |   | D:A |  X  B  | E:B |
         |     |   | (J) |<-------|     |
         +-----+   +-----+     T  +-----+
                     ...