Is this a lifetime BUG in compiler?

help
1

For the following code:

trait L1<'a> {
    type A1;
    type B1;
}

trait L2<'a>: L1<'a, A1 = Self::A2, B1 = Self::B2> {
    type A2;
    type B2;
}

impl<'a, T, A, B> L2<'a> for T
where
    T: L1<'a, A1 = A, B1 = B>,
{
    type A2 = A;
    type B2 = B;
}

trait L3: for<'a> L2<'a, A2 = Self::A3<'a>, B2 = Self::B3> {
    type A3<'a>;
    type B3;
}

impl<T, B> L3 for T
where
    T: for<'a> L2<'a, B2 = B>,
{
    type A3<'a> = <T as L2<'a>>::A2;
    type B3 = B;
}

When it is compiled, an error will be reported:

error[E0275]: overflow evaluating the requirement `for<'a> Self: L2<'a>`
  --> src/lib.rs:34:5
   |
34 |     trait L3: for<'a> L2<'a, A2 = Self::A3<'a>, B2 = Self::B3> {
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = help: consider increasing the recursion limit by adding a `#![recursion_limit = "256"]` attribute to your crate (`playground`)
note: required for `Self` to implement `L3`
  --> src/lib.rs:38:16
   |
38 |     impl<T, B> L3 for T
   |                ^^     ^
39 |     where
40 |         T: for<'a> L2<'a, B2 = B>,
   |            ---------------------- unsatisfied trait bound introduced here
note: required for `Self` to implement `for<'a> L2<'a>`
  --> src/lib.rs:26:23
   |
26 |     impl<'a, T, A, B> L2<'a> for T
   |                       ^^^^^^     ^
27 |     where
28 |         T: L1<'a, A1 = A, B1 = B>,
   |                   ------ unsatisfied trait bound introduced here
   = note: 61 redundant requirements hidden
   = note: required for `Self` to implement `L3`

For more information about this error, try `rustc --explain E0275`.

And when the last implementation condition is changed from L2 to L1:

impl<T, B> L3 for T
where
    T: for<'a> L1<'a, B1 = B>,
{
    type A3<'a> = <T as L1<'a>>::A1;
    type B3 = B;
}

An error will be reported as:

error[E0308]: mismatched types
  --> src/lib.rs:38:23
   |
38 |     impl<T, B> L3 for T
   |                       ^ lifetime mismatch
   |
   = note: expected associated type `<T as L1<'a>>::A1`
              found associated type `<T as L1<'_>>::A1`
   = note: an associated type was expected, but a different one was found
note: the lifetime requirement is introduced here
  --> src/lib.rs:34:15
   |
34 |     trait L3: for<'a> L2<'a, A2 = Self::A3<'a>, B2 = Self::B3> {
   |               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

For more information about this error, try `rustc --explain E0308`.

for<'a> currently works like "for any 'a" and "∀'a". It seems that the type system has some BUGs for the lifetime in for<'a>.

2

Without looking too closely, this looks like a known limitation in the trait solver — not a bug, but less than ideal.

The trait solver’s general job — given a list of assumptions, prove that certain bounds hold — is Turing-complete, so it’s inevitable that there will be limits somewhere.

See in particular, relevant for where-bounds and associated types: Tracking issue for where-bounds shadowing trait implementations · Issue #152409 · rust-lang/rust · GitHub
(This is a “technical limitation of the current implementation”. Again, though, we can push the trait solver implementation further and hopefully cover more use cases, but there will still be limits in any concrete implementation.)

About trait bounds that differ only by a lifetime: Treatment of regions in trait matching is perhaps too simplistic · Issue #21974 · rust-lang/rust · GitHub

3

I don't think so. I've read the issues in your reply, but the problem is a little different.

The problem is caused by for<'a>, the relationship of supertraits, and the relationship of blanket implementations. If one of them breaks, the problem will not happen.

It seems that the checker cannot parse for<'a> correctly as "for any 'a", and creates distinct lifetimes respectively in the implementaion chain and in the supertrait chain. So, when the trait bound is checked, the equivalent cannot hold.

4

I have a solution like this:

trait L1<'a> {
    type A1;
    type B1;
}

trait L2<'a>: L1<'a, A1 = Self::A2, B1 = Self::B2> {
    type A2;
    type B2;
}

impl<'a, T, A, B> L2<'a> for T
where
    T: L1<'a, A1 = A, B1 = B>,
{
    type A2 = A;
    type B2 = B;
}

trait L3TypeA {
    type A3<'a>;
}

impl<T> L3TypeA for T
where
    T: for<'a> L2<'a>,
{
    type A3<'a> = <T as L2<'a>>::A2;
}
  
trait L3:
    for<'a> L3TypeA<A3<'a> = <Self as L2<'a>>::A2>
    + for<'a> L2<'a, B2 = Self::B3>
{
    type B3;
}

impl<T, B> L3 for T
where
    T: for<'a> L2<'a, B2 = B>,
{
    type B3 = B;
}
5

The OP currently compiles with the next trait solver.

trait L3: for<'a> L2<'a, A2 = Self::A3<'a>, B2 = Self::B3> {
    type A3<'a>;

Why have a lifetime parameter on A3? The bound means it can't be used in the fully resolved type. Edit: Nevermind, I misread the bound.

6

Because A2 may change with 'a, A3 needs a lifetime to be general enough.

What is the fully resolved type?

7

I just looked up the meaning, but I don't understand "it can't be used in the fully resolved type".

What does "be used in the fully resolved type" mean? Can you give me an example?

8

My bad, I misread A2 in the bound as type variable and not an associated type. The lifetime parameter on A3 may appear in the fully resolved type.

9

OK, I think I get it. You mean if Self::A3<'a> = X is in the bound, then the implementation type A3<'a> = *type* cannot use 'a in the *type*. And you previously thought A2 is the X. Is that right?

10

I mean when you have something like

impl<TypeVariable, T> ...
where
    for<'a> T: Trait<GenericAssociatedType<'a> = TypeVariable>,

then <T as Trait>::GenericAssociatedType<'a> has to be the same type for all 'a. Or similarly for

impl<TypeVariable, T> ...
where
    for<'a> T: Trait<'a, AssociatedType = TypeVariable>,

and <T as Trait<'a>>::AssociatedType. I thought something like that was present (but it isn't).

11

Oh, yes, I get what you mean. Thank you very much! :bouquet: :corro: