Stream: wg-traits

Topic: regions and universes


nikomatsakis (Dec 17 2019 at 20:04, on Zulip):

Hey @Matthew Jasper

Matthew Jasper (Dec 17 2019 at 20:04, on Zulip):

Hi

nikomatsakis (Dec 17 2019 at 20:04, on Zulip):

I'm trying to decide where to start

nikomatsakis (Dec 17 2019 at 20:04, on Zulip):

I guess let me start with #65232

nikomatsakis (Dec 17 2019 at 20:05, on Zulip):

I'd like to land that PR but I have a few concerns

nikomatsakis (Dec 17 2019 at 20:05, on Zulip):
nikomatsakis (Dec 17 2019 at 20:05, on Zulip):

(e.g., maybe a warning period)

nikomatsakis (Dec 17 2019 at 20:05, on Zulip):

in my ideal world, we would have an RFC that kind of lays out "the plan" for how to handle this stuff

nikomatsakis (Dec 17 2019 at 20:06, on Zulip):

specifically I mean how to handle regions, higher-ranked subtyping, trait solving, and the interactions there

nikomatsakis (Dec 17 2019 at 20:06, on Zulip):

I think it would actually be plausible to do a warning period

nikomatsakis (Dec 17 2019 at 20:06, on Zulip):

or to preserve the existing region behavior

nikomatsakis (Dec 17 2019 at 20:06, on Zulip):

by adding a check to cherence

nikomatsakis (Dec 17 2019 at 20:06, on Zulip):

right now, the coherence test basially just ignores all the region constraints

nikomatsakis (Dec 17 2019 at 20:07, on Zulip):

but we could instead try to solve them, or at least look for "cross-universe" constraints that are not solveable

nikomatsakis (Dec 17 2019 at 20:07, on Zulip):

do you know the coherence interaction I am referring to?

Matthew Jasper (Dec 17 2019 at 20:08, on Zulip):

I know what the change in behaviour is. I don't really know how the coherence check works.

nikomatsakis (Dec 17 2019 at 20:08, on Zulip):

the test

nikomatsakis (Dec 17 2019 at 20:09, on Zulip):
trait TheTrait {
    fn foo(&self) { }
}

impl TheTrait for for<'a,'b> fn(&'a u8, &'b u8) -> &'a u8 {
}

impl TheTrait for for<'a> fn(&'a u8, &'a u8) -> &'a u8 {
}
nikomatsakis (Dec 17 2019 at 20:09, on Zulip):

I think the way to think about this is that

nikomatsakis (Dec 17 2019 at 20:09, on Zulip):

you have the operation TypeEqual(T1, T2) which, in the compiler anyway, returns a set of region constraints RC

nikomatsakis (Dec 17 2019 at 20:10, on Zulip):

(or errors)

nikomatsakis (Dec 17 2019 at 20:10, on Zulip):

i.e., the types are equal if RC are satisfiable

nikomatsakis (Dec 17 2019 at 20:10, on Zulip):

and the coherence code basically just ignores those constraints and considers things to potentially overlap, assuming RC is satisfiable

nikomatsakis (Dec 17 2019 at 20:11, on Zulip):

we could probalby just run the region inference code and it'd be ok, though most of the regions would wind up being inferred to 'empty or something

nikomatsakis (Dec 17 2019 at 20:11, on Zulip):

because there are no real constraints

nikomatsakis (Dec 17 2019 at 20:11, on Zulip):

that is, you have a bunch of variables, and they have to outlive one another, but there is nothing that forces them to be anything other than 'empty

nikomatsakis (Dec 17 2019 at 20:11, on Zulip):

except for universe placeholders, in this PR

nikomatsakis (Dec 17 2019 at 20:12, on Zulip):

so e.g. here I think you would find that we can't infer a single 'a that outlives '!a and '!b and yet is outlived by '!a

nikomatsakis (Dec 17 2019 at 20:12, on Zulip):

(does that make sense?)

Matthew Jasper (Dec 17 2019 at 20:13, on Zulip):

Yes.

nikomatsakis (Dec 17 2019 at 20:13, on Zulip):

I feel like .. 90% sure that this would be "more or less" equivalent to today's code, modulo those cases where today's code is wrong

Matthew Jasper (Dec 17 2019 at 20:13, on Zulip):

Where the types really are the same.

nikomatsakis (Dec 17 2019 at 20:14, on Zulip):

e.g., presumably

impl TheTrait for fn(&u8)

impl<'a> TheTrait for fn(&'a u8)

would probably overlap, because there is at least one lifetime ('empty) where those types are the same

nikomatsakis (Dec 17 2019 at 20:14, on Zulip):

similarly

impl TheTrait for for<'b> fn() -> &'b u8

impl<'a> TheTrait for fn() -> &'a u8

which is equivalent in the case where 'a is 'static

nikomatsakis (Dec 17 2019 at 20:16, on Zulip):

I could certainly try implementing that, it'd be easy enough

nikomatsakis (Dec 17 2019 at 20:16, on Zulip):

let me pivot slightly, to talk about the idea I had for how to handle regions in chalk

nikomatsakis (Dec 17 2019 at 20:16, on Zulip):

which is related to this in some sense

Matthew Jasper (Dec 17 2019 at 20:16, on Zulip):

but we could instead try to solve them, or at least look for "cross-universe" constraints that are not solveable

Implementing this?

nikomatsakis (Dec 17 2019 at 20:16, on Zulip):

right, I think I just have to add one or two lines of code

nikomatsakis (Dec 17 2019 at 20:16, on Zulip):

well, before I pivot, let me add one last thing --

nikomatsakis (Dec 17 2019 at 20:17, on Zulip):

I was debating at some point whether it would be possible to get away with the branch the way it is now (i.e., causing all those cases to overlap, even when the constraints are unsolveable)

nikomatsakis (Dec 17 2019 at 20:17, on Zulip):

in part because I was hoping that could make it so that the first round of type-checking could completely erase regons, even erasing their binding locations

nikomatsakis (Dec 17 2019 at 20:17, on Zulip):

this would basically change Rust's type system into a flat system w/o subtyping

nikomatsakis (Dec 17 2019 at 20:18, on Zulip):

(I think?)

nikomatsakis (Dec 17 2019 at 20:18, on Zulip):

which would be efficient

nikomatsakis (Dec 17 2019 at 20:18, on Zulip):

and most users I've talked (even sophisticated ones) are surprised to learn that an impl for fn(&u8) and an impl for fn(&'a u8) are both permitted, etc

nikomatsakis (Dec 17 2019 at 20:18, on Zulip):

(well, that specific example wouldn't be, but you know what I mean)

nikomatsakis (Dec 17 2019 at 20:19, on Zulip):

however I am not sure about that vision, and anyway I have to face the backwards compatibility facts -- i.e., I can't come up with a kind of compelling reason to justify rejecting some of these cases that are currently accepted

nikomatsakis (Dec 17 2019 at 20:20, on Zulip):

(except for the cases where there is legit overlap)

nikomatsakis (Dec 17 2019 at 20:20, on Zulip):

but I guess there'd always be room to move to a future compatibility warning later

nikomatsakis (Dec 17 2019 at 20:20, on Zulip):

after all, it's been literally this way since 1.0

nikomatsakis (Dec 17 2019 at 20:21, on Zulip):

(the truth is that even with my change, the branch will be rejecting all the impls I know of that take advantage of distinguishing binding locations)

nikomatsakis (Dec 17 2019 at 20:21, on Zulip):

(so I guess I need a warning anyway)

nikomatsakis (Dec 17 2019 at 20:21, on Zulip):

(or at least we might consider one)

nikomatsakis (Dec 17 2019 at 20:21, on Zulip):

anyway, let me spell out my idea for chalk I guess?

nikomatsakis (Dec 17 2019 at 20:21, on Zulip):

/me pauses

Matthew Jasper (Dec 17 2019 at 20:22, on Zulip):

Go ahead

nikomatsakis (Dec 17 2019 at 20:23, on Zulip):

ok so

nikomatsakis (Dec 17 2019 at 20:23, on Zulip):

the idea was roughly this

nikomatsakis (Dec 17 2019 at 20:23, on Zulip):

the idea was to consider Outlives('a: 'b) a predicate that must be "proven" like any other logical predicate

nikomatsakis (Dec 17 2019 at 20:24, on Zulip):

(whereas today, chalk just kind of "records" them as constraints and never tries to solve them)

nikomatsakis (Dec 17 2019 at 20:24, on Zulip):

there would be a few base rules that we supply for doing that

nikomatsakis (Dec 17 2019 at 20:24, on Zulip):
forall<'x> { Outlives('static: 'x) }
nikomatsakis (Dec 17 2019 at 20:24, on Zulip):
forall<'a, 'b, 'c> {
    Outlives('a: 'c) :-
      Outlives('a: 'b),
      Outlives('b: 'c)
}
nikomatsakis (Dec 17 2019 at 20:25, on Zulip):

and the last rule, which is important

nikomatsakis (Dec 17 2019 at 20:25, on Zulip):
Outlives('a: 'b) :- RecordOutlives('a: 'b)
nikomatsakis (Dec 17 2019 at 20:25, on Zulip):

so what is this "record outlives"?

nikomatsakis (Dec 17 2019 at 20:25, on Zulip):

this is kind of a built-in thing that "records" the constraint for NLL (or polonius...) to solve, but it can only be done if 'a and 'b are in the root universe

nikomatsakis (Dec 17 2019 at 20:26, on Zulip):

the intution here being that if I have a query to prove like

TypeEqual(&'a u8 = &'b u8)
nikomatsakis (Dec 17 2019 at 20:26, on Zulip):

where 'a and 'b are kind of "free" lifetimes, maybe I put them in the root universe (bear with me on that, I'm going to be hand-wavy for a second about the "root universe" I guess)

nikomatsakis (Dec 17 2019 at 20:26, on Zulip):

in that case I would be forced to prove Outlives('a: 'b) and Outlives('b: 'a), both of which I can prove by recording

nikomatsakis (Dec 17 2019 at 20:27, on Zulip):

so I get back those two things as region constraints that must be solved later

nikomatsakis (Dec 17 2019 at 20:27, on Zulip):

however, if I have something like

for<'a> fn(&'a u8) <: fn(&'b u8)
nikomatsakis (Dec 17 2019 at 20:27, on Zulip):

now I would wind up having to prove something like 'b: '!a for some placeholer '!a that is not in the root universe

nikomatsakis (Dec 17 2019 at 20:28, on Zulip):

I can't "record" that one, so I have to justify it some other way

nikomatsakis (Dec 17 2019 at 20:28, on Zulip):

for example, I could see that 'static: '!a (base rule) and that we could prove Outlives('b: 'static) by recording (both 'b and 'static are in root universe) and hence by transitivity we're done

nikomatsakis (Dec 17 2019 at 20:29, on Zulip):

i.e., we wind up recording that this is true if 'b: 'static

nikomatsakis (Dec 17 2019 at 20:29, on Zulip):

/me wonders if he got that right

nikomatsakis (Dec 17 2019 at 20:29, on Zulip):

I guess so :)

nikomatsakis (Dec 17 2019 at 20:29, on Zulip):

this is basically the same behavior that our region solver is doing in that PR, of course

Matthew Jasper (Dec 17 2019 at 20:29, on Zulip):

No, 'a becomes an inference variable.

nikomatsakis (Dec 17 2019 at 20:29, on Zulip):

yeah, ok, well, you get the idea :P

Matthew Jasper (Dec 17 2019 at 20:29, on Zulip):

:P

nikomatsakis (Dec 17 2019 at 20:29, on Zulip):

(maybe)

nikomatsakis (Dec 17 2019 at 20:30, on Zulip):

No, 'a becomes an inference variable.

glad you saw that, because it seemed like what I was saying made no sense when I ported it back to the original types

nikomatsakis (Dec 17 2019 at 20:30, on Zulip):

ok, change the example to

nikomatsakis (Dec 17 2019 at 20:30, on Zulip):
fn() -> &'b u8 <: for<'a> fn() -> &'a u8
nikomatsakis (Dec 17 2019 at 20:30, on Zulip):

(man that's hard to parse)

Matthew Jasper (Dec 17 2019 at 20:31, on Zulip):

That looks better...

nikomatsakis (Dec 17 2019 at 20:31, on Zulip):

but at least it makes sense that 'b = 'static is a solution :)

nikomatsakis (Dec 17 2019 at 20:31, on Zulip):

anyway what's neat about this is that (e.g.) polonius doesn't have to care about anything higher-ranked or higher-order or whatever

nikomatsakis (Dec 17 2019 at 20:31, on Zulip):

plus it fits with some other things I'd like to do

nikomatsakis (Dec 17 2019 at 20:31, on Zulip):

e.g., I'd like to be able to do

nikomatsakis (Dec 17 2019 at 20:31, on Zulip):
forall<'a, 'b> { if ('a: 'b, 'b: 'a) { &'a u8 = &'b u8 } }
nikomatsakis (Dec 17 2019 at 20:32, on Zulip):

this could plausibly be solved by chalk all by itself

nikomatsakis (Dec 17 2019 at 20:32, on Zulip):

more importantly, perhaps

nikomatsakis (Dec 17 2019 at 20:32, on Zulip):

consider a type like

for<'a, 'b> fn(Foo<'a, 'b>)
nikomatsakis (Dec 17 2019 at 20:32, on Zulip):

where struct Foo<'a, 'b: 'a>

nikomatsakis (Dec 17 2019 at 20:33, on Zulip):

here, although we don't yet know what 'a and 'b are, we do know that you should pick choices that make Foo<'a, 'b> WF

nikomatsakis (Dec 17 2019 at 20:33, on Zulip):

(the current compiler's handling of this is not sound, which is a longstanding bug, thoughh I can't find the issue number just now)

nikomatsakis (Dec 17 2019 at 20:34, on Zulip):

but also we sometimes hit cases where we are far too conservative today

Matthew Jasper (Dec 17 2019 at 20:34, on Zulip):

I've seen it

nikomatsakis (Dec 17 2019 at 20:34, on Zulip):

however, with this setup, we could do things like

forall<'a, 'b> {
    if (WF(Foo<'a, 'b>)) {
        ...
nikomatsakis (Dec 17 2019 at 20:34, on Zulip):

and use the implied bounds setup to figure out that this means that 'a: 'b

nikomatsakis (Dec 17 2019 at 20:34, on Zulip):

(I'm not sure how familiar you are with the chalk notation etc, so I'm assuming you'll ask me questions etc)

nikomatsakis (Dec 17 2019 at 20:35, on Zulip):

there is one "fly in the ointment", so to speak, but that's the basic idea

nikomatsakis (Dec 17 2019 at 20:35, on Zulip):

sorry, I should give a bit more context

nikomatsakis (Dec 17 2019 at 20:35, on Zulip):

I kind of wanted to "reinterpret" the WF rules on fn types

nikomatsakis (Dec 17 2019 at 20:35, on Zulip):

right now, we basically just don't validate the WF for things inside binders at all

nikomatsakis (Dec 17 2019 at 20:36, on Zulip):

and if you were just kind of naive then for<'a, 'b> fn(Foo<'a, 'b>) would not be WF because we don't have any constraints on 'a and 'b

nikomatsakis (Dec 17 2019 at 20:36, on Zulip):

but if we use an "implied bounds" setup, then we might say that there is an implied set of where clauses for fn types

nikomatsakis (Dec 17 2019 at 20:36, on Zulip):

that require all their argument types (and return type) to be WF

nikomatsakis (Dec 17 2019 at 20:36, on Zulip):

then you can extend fn subtyping to say that those bounds (now made explicit) must subsume one another

nikomatsakis (Dec 17 2019 at 20:37, on Zulip):

so e.g. for<'a> fn is really short (internally) for for<...> if(C) fn(...)

nikomatsakis (Dec 17 2019 at 20:37, on Zulip):

and hence when you have for<..> if(C) fn(...) <: for<...> if(D) fn(..)

nikomatsakis (Dec 17 2019 at 20:37, on Zulip):

there must be some relationship between C and D

nikomatsakis (Dec 17 2019 at 20:37, on Zulip):

i.e., assuming D, you can prove C, or maybe vice versa :P

nikomatsakis (Dec 17 2019 at 20:37, on Zulip):

/me thinks for a second :)

nikomatsakis (Dec 17 2019 at 20:38, on Zulip):

I thnk that's right... the caller will only have to prove D, so that should imply C

nikomatsakis (Dec 17 2019 at 20:38, on Zulip):

anyway, there is a fly in the ointment, as I said, but that's the big picture I was kind of shooting for

nikomatsakis (Dec 17 2019 at 20:38, on Zulip):

the fly is basically that the rules I gave will result in a lot of possible solutions

nikomatsakis (Dec 17 2019 at 20:39, on Zulip):

I'm not 100% sure how to handle that :)

nikomatsakis (Dec 17 2019 at 20:39, on Zulip):

i.e., left to its own devices, chalk would kind of try to enumerate way too many possibilities

nikomatsakis (Dec 17 2019 at 20:39, on Zulip):

I think though we can tweak the way we express the rules to be a bit less redundant --

nikomatsakis (Dec 17 2019 at 20:39, on Zulip):

and no matter what way you slice it, there is a separate thing, that we're going to have to add some notion of "or" into the cosntraints, so that you get back a variety of possible constraints

nikomatsakis (Dec 17 2019 at 20:40, on Zulip):

which we can then simplify, in some cases, though in the limit we might just have multiple possibilities we have to check

nikomatsakis (Dec 17 2019 at 20:40, on Zulip):

see e.g. https://github.com/rust-lang/rust/issues/21974

nikomatsakis (Dec 17 2019 at 20:40, on Zulip):

but I think that's an orthogonal problem

Matthew Jasper (Dec 17 2019 at 20:40, on Zulip):

Hopefully.

nikomatsakis (Dec 17 2019 at 20:40, on Zulip):

my plan for now was that chalk would produce C || D constraints, but that the solver would sort do something, e.g. maybe conver them to C && D at worst

nikomatsakis (Dec 17 2019 at 20:41, on Zulip):

it seems like step 1 would be producing the correct constraints

nikomatsakis (Dec 17 2019 at 20:41, on Zulip):

then we have to think about how to solve them...

Matthew Jasper (Dec 17 2019 at 20:41, on Zulip):

We do that for closures.

nikomatsakis (Dec 17 2019 at 20:41, on Zulip):

right

nikomatsakis (Dec 17 2019 at 20:41, on Zulip):

another interesting thought experiment: solve all possible sets of cosntraints, but use some kind of incremental dataflow to try and avoid redoing work :)

nikomatsakis (Dec 17 2019 at 20:41, on Zulip):

that is so far down the line it might as well be outer space

nikomatsakis (Dec 17 2019 at 20:41, on Zulip):

unfortunately, I have to run and go shovel the walk :)

nikomatsakis (Dec 17 2019 at 20:42, on Zulip):

but I'll come back in a bit, hopefully that made some sense to you, I'd be curious to know if you see any obvious flaws (either today or at some later point)

nikomatsakis (Dec 17 2019 at 20:42, on Zulip):

ah there was one last thing I didn't mention...

nikomatsakis (Dec 17 2019 at 20:42, on Zulip):

having to do how, in polonius, regions can really be "sets" of lifetimes

nikomatsakis (Dec 17 2019 at 20:43, on Zulip):

which I think is neat and useful but there is some interaction here for complex cases

nikomatsakis (Dec 17 2019 at 20:43, on Zulip):

e.g. if you had if ('a: 'b, 'a: 'c), and you had to prove exists<'x> { 'x: 'a and 'x: 'b }

nikomatsakis (Dec 17 2019 at 20:43, on Zulip):

I think that chalk would be forced to say 'x = 'a

nikomatsakis (Dec 17 2019 at 20:43, on Zulip):

but polonius might say 'x = union('a, 'b)

nikomatsakis (Dec 17 2019 at 20:44, on Zulip):

I don't actually know that this matters much in some sense

nikomatsakis (Dec 17 2019 at 20:44, on Zulip):

like I think the same set of constraints are solveable

nikomatsakis (Dec 17 2019 at 20:44, on Zulip):

it's just a matter of how "precise" the solutions are

nikomatsakis (Dec 17 2019 at 20:45, on Zulip):

having to do how, in polonius, regions can really be "sets" of lifetimes

I think this could be useful for impl Trait and capture clausees

nikomatsakis (Dec 17 2019 at 20:45, on Zulip):

ok, have to go now :snowflake:

Matthew Jasper (Dec 17 2019 at 20:45, on Zulip):

:wave:

Matthew Jasper (Dec 21 2019 at 19:54, on Zulip):

it's just a matter of how "precise" the solutions are

I was going to say that it matters for cases like this: https://play.rust-lang.org/?version=stable&mode=debug&edition=2018&gist=169cdb4aaa19abce2baa2b45e876f797. But that causes the compiler to ICE...

Matthew Jasper (Dec 21 2019 at 20:44, on Zulip):

In cases like the above I guess we could preemptively add another region for union('d, 'e) so that we have something for the region to be inferred to.

nikomatsakis (Dec 23 2019 at 11:20, on Zulip):

That case is hurting my head =)

nikomatsakis (Dec 23 2019 at 11:23, on Zulip):

(Note though that union in polonius terms is more like intersection in lifetimes, in case that's relevant)

nikomatsakis (Dec 23 2019 at 11:23, on Zulip):

Let me try to break that example into relations :)

nikomatsakis (Dec 23 2019 at 11:34, on Zulip):

So put that all together and you get

and we know from implied bounds that :

So yeah that's a case where we can't grow to d, e, or static -- not sure why I thought that couldn't arise, seems like exactly the sort of constraints that you would be looking for. =)

In any case, yes, I think the fallback would be to augment the solver either by introducing union or by making the value of a region equal to a set, but I'm not sure what that latter change would do precisely.

Last update: Jun 07 2020 at 10:15UTC