Stream: wg-traits

Topic: desugaring projections in chalk


nikomatsakis (Oct 29 2019 at 14:27, on Zulip):

So I realized something this morning. While I still like the idea of desugaring projections, it's really equivalent to eager normalization -- and it has some of the same problems! In particular, it is straightforward to handle something like this:

Implemented(T: Foo< <T as Iterator>::Item >)

to

Implemented(T: Foo< U >) :- ProjectionEq(<T as Iterator>::Item  = U)

But we can't really normalize something like this that way:

Implemented(T: Foo< for<'a> fn(<&'a as Bar>::Item >)

The problem is that the result U might have to name 'a. This is of course a known bug in rustc. It works fine in chalk today, though, because we basically do the ProjectionEq desugaring, but quite "late", such that we create the ProjectionEq in a context where it is allowed to name 'a.

This doesn't really invalidate much of the work towards introducing type families etc -- that work is still needed to enable chalk to be shared between rustc and rust-analyzer, for example, and I still think it can be very useful for doing quality engineering later. But it does sort of mean that the "desugaring" plan doesn't make sense as I imagined it -- I'm not sure if there is some alternative formulation that does make sense, to be honest.

All of this fits well with our plan for next design meeting, since the stuff I had planned to talk about was exactly more details around how we handle cases like this (and how to help catch rustc up with chalk in some respects).

nikomatsakis (Oct 29 2019 at 14:29, on Zulip):

Interestingly, I had already written the code to do the transformation on a branch -- it included an unwrap call that would have failed for these higher-ranked constructs that I say we can't handle. That unwrap never failed. This suggests a hole in our test coverage we should probably fix. :)

nikomatsakis (Oct 29 2019 at 14:30, on Zulip):

I'm not sure if there is some alternative formulation that does make sense, to be honest.

I guess the alternative formulation might be to "lower" more of the equality rules, particularly those around higher-ranked types, into goals themselves. I'm not sure if there is real value there or not.

detrumi (Oct 29 2019 at 15:32, on Zulip):

I'm not sure I understand, isn't this possible?

Implemented(T: Foo< U >) :- ProjectionEq(for<'a> fn(<&'a as Bar>::Item) = U)
detrumi (Oct 29 2019 at 15:36, on Zulip):

Or is it the left U that might have to name 'a?

nikomatsakis (Oct 29 2019 at 19:16, on Zulip):

@detrumi what you wrote there is not directly possible just by the structure of our goals, but you could write something like

forall<T, U> { // let me make these explicit, I left them implicit before
    Implemented(T: Foo< fn(U) >) :-
        forall<'a> { ProjectionEq(<&'a as Bar>::Item = U) }
}

Unfortunately, as you noted, the problem here is that the U might have to name 'a -- ie., you could have

impl<T> Bar for T {
    type Item = T;
}

and (as you can see) 'a is not in scope at the point where U is declared.

Last update: Nov 12 2019 at 16:40UTC