Permit higher-ranked qualifiers to enclose the self type

[nikomatsakis]

There is a need to permit for qualifiers that appear in more places. In particular, I'd like to be able to write something like this:

where for<'a, 'b> &'a T : Foo<&'b T>

but today the parser only accepts for after the :. the rest of the code already considers 'a and 'b to be in scope for the self-type of the trait, so it's just the parser that has to be changed. I imagine that the for, in that case, would distribute over all the attached where clauses, so:

where for<'a> T : Foo<&'a T> + Bar<&'a T>

would be equivalent to:

where T : for<'a> Foo<&'a T> + for<'a> Bar<&'a T>

Nested for qualifiers would be illegal, I think:

where for<'a> T : for<'b> Foo<&'a &'b T> // ERROR

[jroesch]

@nikomatsakis you mentioned filling an RFC for this behavior + impossible impls, should we follow up on that or hold off until we close the rest of the issues. It seems like a relatively succinct set of changes.

[nikomatsakis]

I am placing this on the beta milestone due to the importance for working with bigints and the like.

cc @aturon

[nikomatsakis]

There are some minor syntactic issues to work out. My preference would be to accept only the simplest possible form:

• for<'a> Type : Trait<...>

We would not accept any of the following:

• for<'a> Type : Trait<...> + Trait2<..> -- what is the scope of the for here?
• for<'a> Type : for<'b> Trait<..> -- are these union'd or what?

[nrc]

Fixing this is exposing quite a lot of sadness, mostly around the representation of trait refs. I am currently trying to resist the temptation to fix it properly because that seems like a lot of work and touches a lot of complex parts of the compiler.

So, currently part of a where clause such as T: for<'a> U is represented as Binder, where T is encoded inside the trait ref as part of the substs on U. This is cute, but ultimately annoying because it glosses over the scope of the for quantifier - it should be inside the constraint, but outside the trait ref, but such a placing doesn't exist since the trait ref includes the constraint and the only binding scope is outside the trait ref.

This is probably OK for most of the compiler - it is fine to extend the scope of the quantifier. But lifetime resolution needs the precise scope. There doesn't seem to be a nice way to coelesce the lifetimes bound in the two places (T: for<'a> U vs for<'a> T: U) during lifetime resolution, but that seems to be the nicest solution here (or at least the one which changes the least amount of code).

[nikomatsakis]

On Wed, Feb 04, 2015 at 06:43:56PM -0800, Nick Cameron wrote:

So, currently part of a where clause such as T: for<'a> U is represented as Binder, where T is encoded inside the trait ref as part of the substs on U. This is cute, but ultimately annoying because it glosses over the scope of the for quantifier - it should be inside the constraint, but outside the trait ref, but such a placing doesn't exist since the trait ref includes the constraint and the only binding scope is outside the trait ref.

This is by design, yes, in anticipation of wanting to support precisely this feature.

This is probably OK for most of the compiler - it is fine to extend the scope of the quantifier. But lifetime resolution needs the precise scope. There doesn't seem to be a nice way to coelesce the lifetimes bound in the two places (T: for<'a> U vs for<'a> T: U) during lifetime resolution, but that seems to be the nicest solution here (or at least the one which changes the least amount of code).

Perhaps we should chat about this live, probably easier. Lifetime
resolution is driven by the AST, which can be structured
differently. It is certainly possible to collapse multiple binders but
I think we should probably just avoid having to, which is what I was
getting at with this comment

[nikomatsakis]

Oh, I see your PR now, guess it's a moot point.