Trait bound on associated type not induced recursively

[milibopp]

Consider the following code:

trait TraitA {
    type AssocType;
    fn other(&self) -> Self::AssocType;
}

trait TraitB: TraitA
    where Self::AssocType: TraitB
{
    fn stuff(&self) {
        self.other().stuff()
    }
}

This does not compile, because the trait TraitB is not implemented for the type <<Self as TraitA>::AssocType as TraitA>::AssocType [E0277].

However, my reasoning from the above trait definition would be: when a type T implements TraitB then T::AssocType also implements TraitB. By replacing T with T::AssocType::... (n times) in this theorem, we can conclude that T::AssocType::... (n+1 times) implements TraitB, if its predecessor does so. Thus, by induction all T::AssocType::... (n times) should implement TraitB for all n.

Note, that this is not a problem for concrete implementations of TraitB. But abstract default methods cannot be implemented like that and users of TraitB also can't rely on the recursive trait bound.

Is there any way to make the compiler realize this? Or am I wrong?

[milibopp]

This might be related to #20671.

[soltanmm]

Note that translating the associated type to a type parameter allows the preceding example to compile:

trait TraitA<Type> {
    fn other(&self) -> Type;
}

trait TraitB<Type>: TraitA<Type>
    where Type: TraitB<Type>
{
    fn stuff(&self) {
        self.other().stuff()
    }
}

This seems inconsistent. Even though the 'home' of the parameter moved between the two examples (Type in TraitB lives in TraitB's type parameter list and AssocType in TraitB's where clause lives in TraitA), I believe they should be treated the same.

[arielb1]

This is another case of "non-supertrait predicates are not elaborated". closing.