Associated type projections don't play well with HRTBs and normalization

[soltanmm]

trait MyFrom<T> {}
impl<T> MyFrom<T> for T {}

trait MyInto<T> {}
impl<T, U> MyInto<U> for T where U: MyFrom<T> {}


trait A<'self_> {
    type T;
}
trait B: for<'self_> A<'self_> {
    //type U: for<'self_> MyFrom<<Self as A<'self_>>::T>;  // <-- this won't compile
    type U: for<'self_> MyInto<<Self as A<'self_>>::T>;  // <-- but this will
}


struct M;
impl<'self_> A<'self_> for M {
    type T = usize;
}
impl B for M {
    type U = usize;
}


fn main() {}

playpen link

This could've been written with MyInto written as Into and similarly for MyFrom/From. It was written this way only to make explicit the necessity of one blanket impl for satisfying the other.

I'm guessing that extensional equality is not judged, even though it is possible to make such a judgment and such a judgment must be made to compile code that compiles today. <Self as A<'self_>>::T on line 12 ought to be equated to usize (which must be detected at some other point in time else line 13 wouldn't be able to compile).

EDIT: Playing around a bit, it looks more and more like it's all about the HKL bounds...

[soltanmm]

HRTBs (I've been using the wrong nomenclature the whole time!) make projections sad.

///////////////
// HRTB setup
//
trait A {
    type S;
}
trait B<'self_> {
    type T;
}
trait C: for<'self_> B<'self_> {
    type U: for<'self_> A<S=<Self as B<'self_>>::T>;  // requires normalizing through an HRTB
}

//////////////////////
// Problematic impls
//
impl A for usize {
    type S = usize;
}
impl<'self_> B<'self_> for usize {
    type T = usize;
}
impl C for usize {
    type U = usize;
}


fn main() {}

<anon>:23:1: 25:2 error: type mismatch resolving `for<'self_> <usize as A>::S == <usize as B<'self_>>::T`:
 expected usize,
    found associated type [E0271]
<anon>:23 impl C for usize {
<anon>:24     type U = usize;
<anon>:25 }
<anon>:23:1: 25:2 help: see the detailed explanation for E0271
<anon>:23:1: 25:2 note: required by `C`
error: aborting due to previous error
playpen: application terminated with error code 101

Very likely a dupe of #28994.

[eddyb]

cc @nikomatsakis

[arielb1]

Known issue.

[soltanmm]

@arielb1 (or @nikomatsakis? Still a bit unclear on y'all's role separation)
What's the expected overall approach to fixing this issue? Even if you don't expect a newcomer to handle it, I'd like to know anyway. :-D

[nikomatsakis]

@soltanmm actually, I'm not entirely sure. There are a serious of refactorings that I have in mind for the type system / trait resolver, and I've been figuring that after those are done, I would come back to revisit some of these issues, if they still occur, but it may be worth digging into this example (or #28994) in detail. Honestly it's not all fresh in my mind.

The refactorings I am thinking of are, first, lazy normalization (as described in this discuss thread), which may indeed help here, though I've not thought it through very deeply. Second, I'd like to generally rework how the trait checker is working to make it easier to extend the environment as you go -- the current setup, where the set of assumptions etc is semi-fixed when the inference context is created -- makes it hard to "descend through" a binder like for and then do trait resolutions and normalizations within that context.

[soltanmm]

So, potentially w.r.t. lazy normalization, I've been playing with another bit of code (trying to shrink it a bit):

trait Hkt<'a> { type Output; }
trait A where for<'s> <Self::B as Hkt<'s>>::Output: Clone {
    type B: for<'s> Hkt<'s>;
}
trait C: A
    where for<'s> <Self::B as Hkt<'s>>::Output: Clone
{}

impl<'a> Hkt<'a> for usize { type Output = usize; }

struct S;
impl A for S {
    type B = usize;
}

From reading the debug logs, it seems that when checking the well-formed-ness of impl A for S, upon normalizing S::B to usize, and registering and selecting on the implied <usize as Hkt<'a>>::Output: Clone, the compiler has no idea that <usize as Hkt<'a>>::Output == usize and never normalizes to it either. Is this a situation in which the compiler might have assumed that everything was already normalized the best it could be and thus gave up?

An aside: does lazy normalization have something to do with this asterisk in project.rs?