Stream: t-compiler/wg-nll

Topic: impl Trait and union regions


nikomatsakis (Jun 05 2019 at 13:43, on Zulip):

So @pnkfelix (and others) I've been working on some extensions to the region solver to address some existing limitations of impl trait (these are particularly important for async await). (cc @Taylor Cramer)

nikomatsakis (Jun 05 2019 at 13:44, on Zulip):

This raises some interesting questions in the context of the NLL solver

pnkfelix (Jun 05 2019 at 13:44, on Zulip):

cc @WG-nll

nikomatsakis (Jun 05 2019 at 13:44, on Zulip):

I was debating about how to discuss them -- I can certainly outline some of it here

nikomatsakis (Jun 05 2019 at 13:44, on Zulip):

but maybe it's worth doing a call or something

nikomatsakis (Jun 05 2019 at 13:44, on Zulip):

as in general I feel like this is the sort of issue I would like to think about how to document etc (i.e., kind of a meta issue re: lang spec)

nikomatsakis (Jun 05 2019 at 13:44, on Zulip):

anyway let me outline the thing I'm looking at real fast

nikomatsakis (Jun 05 2019 at 13:46, on Zulip):

if you have impl trait today, we can get in this strange scenario:

fn foo<'a, 'b>(..) -> impl Trait<'a, 'b> { .. }

Here, the inferred return type can reference 'a and 'b but not other regions. The problem is that we have no way to express a cosntraint like that in our region solver.

nikomatsakis (Jun 05 2019 at 13:46, on Zulip):

The only sort of constraint our existing solvers know how to handle is 'r1: 'r2, but this would be what I'm calling a pick constraint.

nikomatsakis (Jun 05 2019 at 13:46, on Zulip):

I've been writing it:

pick 'r0 from ['r1...'rN]
nikomatsakis (Jun 05 2019 at 13:46, on Zulip):

i.e., it is satisfied if 'r0 == 'r[i] for some i > 0

nikomatsakis (Jun 05 2019 at 13:47, on Zulip):

(In today's code, that impl Trait I gave above is an error because there is no "least region" we can use as a bound; I am basically lifting this restriction)

nikomatsakis (Jun 05 2019 at 13:48, on Zulip):

(As a further aside, @Taylor Cramer and I realized that the existing inference scheme here was already a bit strange in that sometimes it has "room" to pick from a few sets of regions that would be sufficient; this is mostly unobservable, but not entirely, because of auto-trait leakage; i.e., you can have something like impl Send for Foo<'static> which can then observe if the region inferencer chose 'static or not)

nikomatsakis (Jun 05 2019 at 13:49, on Zulip):

The extension I'm doing is fairly conservative: it basically ignores pick constraints unless there is exactly one least choice it can use. I can give a bit more details but it's not the question that I am pondering. :)

nikomatsakis (Jun 05 2019 at 13:50, on Zulip):

The interesting case is this one:

trait Trait<'a, 'b> { }
impl<T> Trait<'_, '_> for T { }

fn foo<'a, 'b>(x: &'a u32, y: &'b u32) -> impl Trait<'a, 'b> {
    if condition() { x } else { y }
}
nikomatsakis (Jun 05 2019 at 13:50, on Zulip):

If you look carefully here, you will see that the return type is &'c u32 for some region 'c where 'a: 'c and 'b: 'c. You could imagine writing this region as 'a & 'b (an intersection), though I've been thinking of it as a union 'a | 'b because that fits the polonius model of regions as "loan sets"

pnkfelix (Jun 05 2019 at 13:51, on Zulip):

you expect the compiler to infer that type there?

pnkfelix (Jun 05 2019 at 13:51, on Zulip):

where its possible that 'c is ReEmpty ?

nikomatsakis (Jun 05 2019 at 13:51, on Zulip):

Anyway, my lexical solver rejects this example, but I believe it would be sound to accept it, in the sense that the caller can only use impl Trait<'a, 'b> when both 'a and 'b are live

nikomatsakis (Jun 05 2019 at 13:51, on Zulip):

where its possible that 'c is ReEmpty ?

that is not possible

pnkfelix (Jun 05 2019 at 13:51, on Zulip):

oh, hmm, you expect 'c will always exist (and be non-trivial)

nikomatsakis (Jun 05 2019 at 13:52, on Zulip):

it must be live at the return site, for example

nikomatsakis (Jun 05 2019 at 13:52, on Zulip):

the lexical solver probably can't accept this example ever

nikomatsakis (Jun 05 2019 at 13:52, on Zulip):

because it can't really express what is needed

nikomatsakis (Jun 05 2019 at 13:52, on Zulip):

it assigns the result the lifetime of the "Call site" (the outermost scope)

nikomatsakis (Jun 05 2019 at 13:52, on Zulip):

actually i'm not sure if the NLL solver can easily do so either, now that I think about it

nikomatsakis (Jun 05 2019 at 13:52, on Zulip):

(I think polonius could)

nikomatsakis (Jun 05 2019 at 13:53, on Zulip):

I was thinking about how the NLL solver represents regions as a union of elements, where some of those elements can be "free regions" (like 'a and 'b)

nikomatsakis (Jun 05 2019 at 13:54, on Zulip):

but that's actually not what we need here, as I noted above, you need the intersection (in NLL terms)

pnkfelix (Jun 05 2019 at 13:54, on Zulip):

right

nikomatsakis (Jun 05 2019 at 13:54, on Zulip):

(I think polonius could)

but I haven't thought about this much and don't care to (yet)

nikomatsakis (Jun 05 2019 at 13:54, on Zulip):

ok so maybe there's not so much of a question :)

pnkfelix (Jun 05 2019 at 13:54, on Zulip):

so maybe the representation could/should be a sum-of-products

pnkfelix (Jun 05 2019 at 13:54, on Zulip):

or rather, union-of-intersections (in NLL terms) ?

nikomatsakis (Jun 05 2019 at 13:55, on Zulip):

the reason I think polonius could handle this is that it is about tracking the origins, and basically you could imagine it saying something like "The origins of all regions in the hidden type cannot exceed a|b"

nikomatsakis (Jun 05 2019 at 13:55, on Zulip):

which is what we want

pnkfelix (Jun 05 2019 at 13:55, on Zulip):

or is that not going to have the right properties, in terms of lattices glb's or whatnot

nikomatsakis (Jun 05 2019 at 13:55, on Zulip):

anyway I don't know that this example is very important

nikomatsakis (Jun 05 2019 at 13:55, on Zulip):

I just found it interesting as I was writing test cases

nikomatsakis (Jun 05 2019 at 13:55, on Zulip):

so maybe the representation could/should be a sum-of-products

plausibly but I'm not inclined to do that without stronger motivation :)

nikomatsakis (Jun 05 2019 at 13:56, on Zulip):

that code is pretty perf sensitive, among other things

pnkfelix (Jun 05 2019 at 13:56, on Zulip):

anyway I don't know that this example is very important

can it arise meaningfully when you don't have such a wide blanket impl?

nikomatsakis (Jun 05 2019 at 13:56, on Zulip):

I'm not sure

pnkfelix (Jun 05 2019 at 13:56, on Zulip):

e.g. something that actually uses the region parameters

nikomatsakis (Jun 05 2019 at 13:56, on Zulip):

it's also a pure extension

nikomatsakis (Jun 05 2019 at 13:56, on Zulip):

i.e., we can do the thing I'm doing now, and see if people come up with good examples :)

pnkfelix (Jun 05 2019 at 13:57, on Zulip):

good examples to motivate adding a more expressive system, you mean, right?

nikomatsakis (Jun 05 2019 at 13:57, on Zulip):

regardless, even if we don't go in this direction, it still raises interesting questions about impl Trait -- the existing rules and support lack any sort of documentation to my knowledge

nikomatsakis (Jun 05 2019 at 13:57, on Zulip):

good examples to motivate adding a more expressive system, you mean, right?

correct

nikomatsakis (Jun 05 2019 at 13:57, on Zulip):

I would like to improve this situation (docs)

nikomatsakis (Jun 05 2019 at 13:57, on Zulip):

I guess I should be working on an amendment to the reference or something

pnkfelix (Jun 05 2019 at 13:57, on Zulip):

regardless, even if we don't go in this direction, it still raises interesting questions about impl Trait -- the existing rules and support lack any sort of documentation to my knowledge

I think there's some amount of active confusion w.r.t. the interaction between impl Trait and lifetimes

nikomatsakis (Jun 05 2019 at 13:57, on Zulip):

the rules are not very satisfying to me

pnkfelix (Jun 05 2019 at 13:57, on Zulip):

I was trying to find the dialogue I had with alexreg about the impl vs the spec on this front

pnkfelix (Jun 05 2019 at 13:58, on Zulip):

but I failed to find it quickly. I'll look again now

nikomatsakis (Jun 05 2019 at 13:58, on Zulip):

I think the existing solution (you can reference lifetimes that appear in bounds) is ungreat

nikomatsakis (Jun 05 2019 at 13:58, on Zulip):

or rather, it's a decent default, but I suspect we would do well to consider adding an explicit option

nikomatsakis (Jun 05 2019 at 13:58, on Zulip):

but that's kind of a separate story (only kind of)

pnkfelix (Jun 05 2019 at 13:59, on Zulip):

(this is the issue I was thinking of : #54184 )

pnkfelix (Jun 05 2019 at 13:59, on Zulip):

what is the explicit option you are thinking of?

pnkfelix (Jun 05 2019 at 13:59, on Zulip):

namely there are two directions , or maybe three, that I could imagine you going in...

nikomatsakis (Jun 05 2019 at 14:00, on Zulip):

we had discussed things like impl<'a> Debug

nikomatsakis (Jun 05 2019 at 14:00, on Zulip):

strongly related to #54184

nikomatsakis (Jun 05 2019 at 14:00, on Zulip):

it would basically desugar to a "unused" type parameter"

pnkfelix (Jun 05 2019 at 14:01, on Zulip):

Okay. So a way to add lifetimes that can be referenced by the impl Trait even if they do not (and perhaps cannot) appear in the Trait signature itself, right?

pnkfelix (Jun 05 2019 at 14:02, on Zulip):

hmm somehow I never noticed PR #57896

nikomatsakis (Jun 05 2019 at 14:10, on Zulip):

Okay. So a way to add lifetimes that can be referenced by the impl Trait even if they do not (and perhaps cannot) appear in the Trait signature itself, right?

yes. You can then imagine impl Trait as a default. The problem with this is the usual problem with defaults -- when you write impl<'a>, does that add to the default set?

nikomatsakis (Jun 05 2019 at 14:10, on Zulip):

Or does it "reset" the default set?

nikomatsakis (Jun 05 2019 at 14:10, on Zulip):

In particular, we default to capturing all type parameters -- what if you didn't want to?

pnkfelix (Jun 05 2019 at 14:11, on Zulip):

I'd say we should have a (different) way to mark lifetimes in the signature as not intended to be captured.

nikomatsakis (Jun 05 2019 at 14:11, on Zulip):

the expectation I think was that you would use an explicit abstract type (or type Foo = impl Trait, whatever) for this case

nikomatsakis (Jun 05 2019 at 14:11, on Zulip):

(which maybe is fine)

nikomatsakis (Jun 05 2019 at 14:11, on Zulip):

but I think is a big jump

nikomatsakis (Jun 05 2019 at 14:11, on Zulip):

I guess it depends how often

nikomatsakis (Jun 05 2019 at 14:11, on Zulip):

this comes up a lot in the compiler

nikomatsakis (Jun 05 2019 at 14:11, on Zulip):

often you want something like fn foo<'tcx, 'gcx>() -> impl Iterator<Item = Ty<'tcx>> that wants to capture 'gcx

nikomatsakis (Jun 05 2019 at 14:11, on Zulip):

anyway

centril (Jun 05 2019 at 16:19, on Zulip):

@nikomatsakis isn't this https://github.com/rust-lang/rust/issues/60670 ?

nikomatsakis (Jun 05 2019 at 16:19, on Zulip):

Related

nikomatsakis (Jun 05 2019 at 16:20, on Zulip):

Something like an existential lifetime is one way to solve it; impl<'gcx> is another.

centril (Jun 05 2019 at 16:22, on Zulip):

Notably we could say:

fn foo<'a, 'b>(x: &'a u32, y: &'b u32) -> impl exists<'c> { where 'a: 'c, 'b: 'c } Trait<'c, 'c> {
    if condition() { x } else { y }
}
nikomatsakis (Jun 06 2019 at 18:05, on Zulip):

plausible but not really the intended existential plan, which was more to make the type be exists<'c> { ... }

Last update: Nov 21 2019 at 13:05UTC