Stream: wg-traits

Topic: nested quantification error


nikomatsakis (May 17 2019 at 17:49, on Zulip):

@Alexander Regueiro ok, I'm going to look a bit at that error, sorry for the delay.

nikomatsakis (May 17 2019 at 17:51, on Zulip):

You mentioned this test:

// compile-fail

#![feature(associated_type_bounds)]

use std::fmt::Debug;

trait Lam<Binder> { type App; }

fn nested_bounds<_0, _1, _2, D>()
where
    D: Clone + Iterator<Item: Send + for<'a> Iterator<Item: for<'b> Lam<&'a &'b u8, App = _0>>>,
    //~^ ERROR nested quantification of lifetimes [E0316]
    _0: Debug,
{}

fn nested_bounds_desugared<_0, _1, _2, D>()
where
    D: Clone + Iterator<Item = _2>,
    _2: Send + for<'a> Iterator,
    for<'a> <_2 as Iterator>::Item: for<'b> Lam<&'a &'b u8, App = _0>,
    //~^ ERROR nested quantification of lifetimes [E0316]
    _0: Debug,
{}

fn main() {}
nikomatsakis (May 17 2019 at 18:01, on Zulip):

But I'm not entirely sure that is the correct desugaring.

nikomatsakis (May 17 2019 at 18:02, on Zulip):

Well, I guess that one could write something like:

D: for<'a> Foo<'a, Bar: for<'b> Baz<'b>>

which ought to desugar to

for<'a, 'b> <X as Foo<'a>>::Bar: Baz<'b>
nikomatsakis (May 17 2019 at 18:02, on Zulip):

the "nested quantification error" comes about really because our grammar is... overly flexible, in some sense

nikomatsakis (May 17 2019 at 18:03, on Zulip):

we permit for<'a> T: Trait<'a> or T: for<'a> Trait<'a> but they are equivalent

nikomatsakis (May 17 2019 at 18:08, on Zulip):

anyway so I guess that means we have a few questions:

nikomatsakis (May 17 2019 at 18:08, on Zulip):

But my other question is sort of -- what is this desugaring to now. It reminds me that I was going to try to double-check the binding logic in that PR.

Alexander Regueiro (May 17 2019 at 18:13, on Zulip):

No worries. I appreciate you've been busy.

Alexander Regueiro (May 17 2019 at 18:13, on Zulip):

hmm

Alexander Regueiro (May 17 2019 at 18:14, on Zulip):

@nikomatsakis The desugaring now is basically what you see in nested_bounds_desugared, except it's at predicate-level, not HIR level...

Alexander Regueiro (May 17 2019 at 18:14, on Zulip):

@centril and I tended to think it was a reasonable desugaring

Alexander Regueiro (May 17 2019 at 18:15, on Zulip):

and that it would bee fine to error on both of the above cases for now (in a similar way), until nested lifetime bounds are supported (with Chalk?), in which case the errors can disappear in both cases.

nikomatsakis (May 17 2019 at 18:27, on Zulip):

I think though that the existing solver should be able to handle nested quantifications of this kind, too

nikomatsakis (May 17 2019 at 18:27, on Zulip):

still, maybe we can move these errors to HIR lowering or astconv or something

nikomatsakis (May 17 2019 at 18:27, on Zulip):

and then just have the resolve-lifetimes code .. ignore the situation

nikomatsakis (May 17 2019 at 18:28, on Zulip):

still, maybe we can move these errors to HIR lowering or astconv or something

not astconv, ideally hir lowering

nikomatsakis (May 17 2019 at 18:28, on Zulip):

I would think

Alexander Regueiro (May 17 2019 at 18:28, on Zulip):

hmm

Alexander Regueiro (May 17 2019 at 18:28, on Zulip):

the issue is, in HIR, the sugared form is still reprsented very differently

Alexander Regueiro (May 17 2019 at 18:29, on Zulip):

but maybe that's not a problem

nikomatsakis (May 17 2019 at 18:33, on Zulip):

nikomatsakis The desugaring now is basically what you see in nested_bounds_desugared, except it's at predicate-level, not HIR level...

I'm not really sure what you mean by "at predicate level", tbh -- well, I guess this desugaring is happening during astconv?

Alexander Regueiro (May 17 2019 at 18:36, on Zulip):

yes, astconv... I mean, it's generating extra predicates for the desugaring, rather than modifying HIR.

Alexander Regueiro (May 17 2019 at 18:36, on Zulip):

sorry, I didn't say that very well.

Alexander Regueiro (May 21 2019 at 00:16, on Zulip):

@nikomatsakis left you a note about nested lifetime bounds on Github... not sure of the original motivation for banning nested quantification.

Alexander Regueiro (May 21 2019 at 00:16, on Zulip):

I guess you're away this week though, so I'll wait for aan answer on that.

Alexander Regueiro (May 28 2019 at 16:04, on Zulip):

Hey @nikomatsakis. Now that you’re back can we try to get ATB wrapped up ASAP? :-) Mainly this issue.

nikomatsakis (May 31 2019 at 20:36, on Zulip):

Yep, sorry. So here's the thing -- as I wrote earlier, the "nested quantification error" is basically because Rust has this syntactic quirk

nikomatsakis (May 31 2019 at 20:36, on Zulip):

where we let you write the for<'a> binder in two (largely equivalent) places

nikomatsakis (May 31 2019 at 20:36, on Zulip):

and we didn't want people to write it in both

nikomatsakis (May 31 2019 at 20:36, on Zulip):

just because it's...misleading

nikomatsakis (May 31 2019 at 20:36, on Zulip):

i.e., you can have for<'a> T: Foo<'a> or T: for<'a> Foo<'a>

nikomatsakis (May 31 2019 at 20:37, on Zulip):

we didn't want people to write for<'a> T: for<'b> Foo<'a, 'b>

nikomatsakis (May 31 2019 at 20:37, on Zulip):

but not because it'd be invalid to do so per se -- presumably that'd be just equivalent to for<'a, 'b> T: Foo<'a, 'b>

nikomatsakis (May 31 2019 at 20:37, on Zulip):

it's not really obvious to me that this error has much or anything to do with this case

Alexander Regueiro (May 31 2019 at 21:09, on Zulip):

Oh I see

Alexander Regueiro (May 31 2019 at 21:10, on Zulip):

So we may not need any modification in this case eh.

Alexander Regueiro (May 31 2019 at 21:11, on Zulip):

@nikomatsakis In that case I’ll let you address those two WIP commits if you would, then LGTM. :-)

Last update: Nov 12 2019 at 16:35UTC