Stream: wg-traits

Topic: design meeting 2019.11.04


nikomatsakis (Nov 04 2019 at 19:03, on Zulip):

Hi @WG-traits

nikomatsakis (Nov 04 2019 at 19:05, on Zulip):

So I think we were going to talk about regions, universes, etc

nikomatsakis (Nov 04 2019 at 19:05, on Zulip):

At least that's where we left it last time

nikomatsakis (Nov 04 2019 at 19:05, on Zulip):

I'm trying to decide the best "starting point"

nikomatsakis (Nov 04 2019 at 19:06, on Zulip):

So last time we were talking about normalization under binders

nikomatsakis (Nov 04 2019 at 19:07, on Zulip):

Meaning when you have something like for<'a> fn(<&'a () as Foo>::Bar)

nikomatsakis (Nov 04 2019 at 19:07, on Zulip):

Right now, rustc has some difficulty with this

nikomatsakis (Nov 04 2019 at 19:08, on Zulip):

let me back up :)

nikomatsakis (Nov 04 2019 at 19:09, on Zulip):

If we have a type like <T as Iterator>::Item

nikomatsakis (Nov 04 2019 at 19:09, on Zulip):

and we try to normalize it

Keith Yeung (Nov 04 2019 at 19:09, on Zulip):

what does "normalize" mean?

nikomatsakis (Nov 04 2019 at 19:09, on Zulip):

try to find an applicable impl and substitute the value from that impl

nikomatsakis (Nov 04 2019 at 19:09, on Zulip):

so e.g. if you have

nikomatsakis (Nov 04 2019 at 19:10, on Zulip):
impl<T> Iterator for vec::IntoIter<T> { type Item = T; }
nikomatsakis (Nov 04 2019 at 19:10, on Zulip):

and then we have <vec::IntoIter<Foo> as Iterator>::Item

nikomatsakis (Nov 04 2019 at 19:10, on Zulip):

we could normalize that to Foo

nikomatsakis (Nov 04 2019 at 19:11, on Zulip):

the way rustc works today, we have a phase where we look for associated type projections of this kind and we replace them --

nikomatsakis (Nov 04 2019 at 19:11, on Zulip):

this is called "normalizing"

nikomatsakis (Nov 04 2019 at 19:12, on Zulip):

to be clear, I am talking specifically about rustc right now

nikomatsakis (Nov 04 2019 at 19:12, on Zulip):

chalk has a slightly different approach, though it still involves a concept of normalizing

nikomatsakis (Nov 04 2019 at 19:13, on Zulip):

we call this "eager normalization" because, in rustc, we have to do it whenever we bring types "into scope" -- this context of "into scope" is not very clear, I realize, I'm not sure the best way to describe it.

nikomatsakis (Nov 04 2019 at 19:13, on Zulip):

An example would be: if you are type-checking, and you see an expression like foo.bar, where

struct Foo<T: Iterator> {
    bar: <T as Iterator>::Item
}
nikomatsakis (Nov 04 2019 at 19:13, on Zulip):

we would load the type for the field bar we will get <T as Iterator>::Item

nikomatsakis (Nov 04 2019 at 19:14, on Zulip):

this type is not "in scope", it is taken from the struct -- we have to do substitutions to bring it "into scope" in the sense I mean

nikomatsakis (Nov 04 2019 at 19:15, on Zulip):

so e.g. if the type of foo is Foo<vec::IntoIter<u32>>

nikomatsakis (Nov 04 2019 at 19:15, on Zulip):

we would substitute and get that the type of bar is <vec::IntoIter<u32> as Iterator>::Item --

nikomatsakis (Nov 04 2019 at 19:15, on Zulip):

and then we have to normalize

nikomatsakis (Nov 04 2019 at 19:15, on Zulip):

which would yield u32

nikomatsakis (Nov 04 2019 at 19:15, on Zulip):

the point of eager normalization is that we have to do that before we go and compare types

nikomatsakis (Nov 04 2019 at 19:16, on Zulip):

that simplifies the logic that compares types

detrumi (Nov 04 2019 at 19:16, on Zulip):

Right, so rustc normalizes as soon as it uses the type outside of the original context

nikomatsakis (Nov 04 2019 at 19:16, on Zulip):

yeah

nikomatsakis (Nov 04 2019 at 19:16, on Zulip):

but that can be tricky

nikomatsakis (Nov 04 2019 at 19:16, on Zulip):

for one thing, it's easy to forget

nikomatsakis (Nov 04 2019 at 19:16, on Zulip):

for another, sometimes there are times when you are kind of "mixing" things that are normalized and things that are not

nikomatsakis (Nov 04 2019 at 19:17, on Zulip):

that doesn't really matter, since normalizing twice doesn't hurt

nikomatsakis (Nov 04 2019 at 19:17, on Zulip):

but it can just make it hard to remember and it feels inefficient

nikomatsakis (Nov 04 2019 at 19:17, on Zulip):

even in our example above,

nikomatsakis (Nov 04 2019 at 19:17, on Zulip):

if the type of the local variable foo is "in scope", it must also be fully normalized

nikomatsakis (Nov 04 2019 at 19:17, on Zulip):

so the type vec::IntoIter<u32> that we substituted in is already normalized

nikomatsakis (Nov 04 2019 at 19:17, on Zulip):

and we then renormalize it, in a sense

nikomatsakis (Nov 04 2019 at 19:18, on Zulip):

but anyway the bigger problem is

nikomatsakis (Nov 04 2019 at 19:19, on Zulip):

when you have types like this one for<'a> fn(<&'a () as Foo>::Bar), we need to normalize "inside" the for binder

nikomatsakis (Nov 04 2019 at 19:19, on Zulip):

sometimes normalization doesn't complete right away, for example if there are inference variables

nikomatsakis (Nov 04 2019 at 19:19, on Zulip):

so e.g. in an extreme case if you have <?X as Iterator>::Item, we can't normalize it yet -- we don't know what impl it will be

nikomatsakis (Nov 04 2019 at 19:20, on Zulip):

the way we handle that today is that we create an inference variable to represent the result (?R) and then we add a pending obligation that says Normalize(<?X as Iterator>::Item -> ?R), essentially, to use a chalk-like notation

nikomatsakis (Nov 04 2019 at 19:20, on Zulip):

but if we get stuck in this position inside of the for<'a> binder, we are in a bad spot. We don't currently have a way to create inference variables that can "equal" a higher-ranked region like 'a

nikomatsakis (Nov 04 2019 at 19:21, on Zulip):

universes basically gives us a mechanism for doing this

nikomatsakis (Nov 04 2019 at 19:21, on Zulip):

(does this make sense so far?)

nikomatsakis (Nov 04 2019 at 19:21, on Zulip):

but if we get stuck in this position inside of the for<'a> binder, we are in a bad spot. We don't currently have a way to create inference variables that can "equal" a higher-ranked region like 'a

(I imagine it might not be clear why we can't do this yet...)

detrumi (Nov 04 2019 at 19:22, on Zulip):

You say "equal" a higher-ranked region, but isn't it like nesting scopes?

nikomatsakis (Nov 04 2019 at 19:22, on Zulip):

yeah, so that's part of it:

nikomatsakis (Nov 04 2019 at 19:22, on Zulip):

like if we are going to eagerly normalize

nikomatsakis (Nov 04 2019 at 19:22, on Zulip):

we have to be able to produce a result

nikomatsakis (Nov 04 2019 at 19:23, on Zulip):

so we might need to transform for<'a> fn(<vec::IntoIter<&'a u32> as Iterator>::Item)

nikomatsakis (Nov 04 2019 at 19:23, on Zulip):

to for<'a> fn(&'a u32)

nikomatsakis (Nov 04 2019 at 19:23, on Zulip):

anyway, the way lazy norm works is rather different

nikomatsakis (Nov 04 2019 at 19:24, on Zulip):

we wait until we are trying to equate two types (say, <vec::IntoIter<u32> as Iterator>::Item and u32)

nikomatsakis (Nov 04 2019 at 19:24, on Zulip):

and then we try to prove that this normalization works

nikomatsakis (Nov 04 2019 at 19:24, on Zulip):

so in some sense whereas before we had a function Normalize(T) -> U that (eagerly) normalized a type T to some type U, and that function had to recursively process everything

nikomatsakis (Nov 04 2019 at 19:25, on Zulip):

now our base operation is instead Equal(T, U) that proves two types are equal -- and it might do that by normalizing

nikomatsakis (Nov 04 2019 at 19:26, on Zulip):

this matters because it means that we enter new scopes

nikomatsakis (Nov 04 2019 at 19:26, on Zulip):

and we do operations in them

nikomatsakis (Nov 04 2019 at 19:26, on Zulip):

but we never try to return data out of them

nikomatsakis (Nov 04 2019 at 19:26, on Zulip):

You say "equal" a higher-ranked region, but isn't it like nesting scopes?

to circle back to this...

nikomatsakis (Nov 04 2019 at 19:27, on Zulip):

the idea of unvierses then is pretty simple, basically you have a counter that tracks the scopes you are in, and when you "enter" a for<'a> scope, you increment this counter -- that's called a new universe

nikomatsakis (Nov 04 2019 at 19:27, on Zulip):

it contains all the types from the previous univese, plus a placeholder

nikomatsakis (Nov 04 2019 at 19:27, on Zulip):

representing 'a

nikomatsakis (Nov 04 2019 at 19:29, on Zulip):

anyway I kind of feel like I'm re-covering stuff that I actually tried to write up in the rustc-guide, I'm trying to decide whihc points I want to emphasize...

nikomatsakis (Nov 04 2019 at 19:29, on Zulip):

...but if this is useful, I can kind of keep going :)

nikomatsakis (Nov 04 2019 at 19:31, on Zulip):

right, so in the new model, as you are going about, you sometimes enter a new scope -- this corresponds to kind of "entering" a forall. you are kind of tracking the innermost universe at this point in time

nikomatsakis (Nov 04 2019 at 19:32, on Zulip):

I'm trying to find where I wrote about this in the rustc-guid but I sort of can't :/

nikomatsakis (Nov 04 2019 at 19:33, on Zulip):

but I know I did somewhere...

nikomatsakis (Nov 04 2019 at 19:33, on Zulip):

ah yes, here is the chapter

nikomatsakis (Nov 04 2019 at 19:33, on Zulip):

the NLL checker in particular is based on this

nikomatsakis (Nov 04 2019 at 19:34, on Zulip):

sorry, my mind is elsewhere today :/ what I wanted to talk through a bit was the PR I've got open, and what I should do about it

nikomatsakis (Nov 04 2019 at 19:35, on Zulip):

let me back up a bit

tmandry (Nov 04 2019 at 19:35, on Zulip):

I was going to ask, I knew we used universes in rustc somewhere.. does that mean we primarily use them in NLL but not in type checking?

nikomatsakis (Nov 04 2019 at 19:35, on Zulip):

yeah, currently we use them in NLL, but not in the type-checker

nikomatsakis (Nov 04 2019 at 19:35, on Zulip):

er, not in the older region system

nikomatsakis (Nov 04 2019 at 19:35, on Zulip):

this is not 100% true

nikomatsakis (Nov 04 2019 at 19:35, on Zulip):

we are kind of in a hybrid state

nikomatsakis (Nov 04 2019 at 19:35, on Zulip):

we are actally tracking universes *everywhere

nikomatsakis (Nov 04 2019 at 19:36, on Zulip):

but we are ALSO simulating the older system of handling higher-ranked types / trait-bounds

nikomatsakis (Nov 04 2019 at 19:36, on Zulip):

which is called the 'leak check'

nikomatsakis (Nov 04 2019 at 19:36, on Zulip):

maybe I should explain how that worked

nikomatsakis (Nov 04 2019 at 19:36, on Zulip):

the idea was: imagine you have

for<'a> fn(&'a u32) = fn(?X)
nikomatsakis (Nov 04 2019 at 19:37, on Zulip):

this should not be true

nikomatsakis (Nov 04 2019 at 19:37, on Zulip):

after all, what can ?X be such that it is true?

nikomatsakis (Nov 04 2019 at 19:37, on Zulip):

the problem here is exactly scoping

nikomatsakis (Nov 04 2019 at 19:37, on Zulip):

if you expand out that equation, you get something like

nikomatsakis (Nov 04 2019 at 19:37, on Zulip):
exists<?X> {
    for<'a> fn(&'a u32) = fn(?X)
}
nikomatsakis (Nov 04 2019 at 19:38, on Zulip):

to put it in plain English, the fn(?X) type is "a function that takes some type ?X as argument"

nikomatsakis (Nov 04 2019 at 19:38, on Zulip):

and the for<'a> fn(&'a u32) is "a function that takes &'a u32 for any 'a as argument"

nikomatsakis (Nov 04 2019 at 19:38, on Zulip):

so there is a scoping problem here

nikomatsakis (Nov 04 2019 at 19:38, on Zulip):

the way that we used to detect this

nikomatsakis (Nov 04 2019 at 19:38, on Zulip):

is basically we would push onto the stack (here I mean the literal program stack, in a sense)

nikomatsakis (Nov 04 2019 at 19:38, on Zulip):

effectively a new universe

nikomatsakis (Nov 04 2019 at 19:38, on Zulip):

then we would recurisvely process the type equality

nikomatsakis (Nov 04 2019 at 19:39, on Zulip):

so if that new universe is U1, then we would replcae 'a with a placeholder region !1 (let's say)

nikomatsakis (Nov 04 2019 at 19:39, on Zulip):

and we would try to equate ?X with &'!1 u32

nikomatsakis (Nov 04 2019 at 19:40, on Zulip):

or I guess I made a more complicated example for myself

nikomatsakis (Nov 04 2019 at 19:40, on Zulip):

well, what this would do is replace ?X with &'?x u32, where '?x is an inference variable

nikomatsakis (Nov 04 2019 at 19:40, on Zulip):

so effectively you would get a constraint like '?x = '!1

nikomatsakis (Nov 04 2019 at 19:40, on Zulip):

so far so ok, the way to think about this in universes is:

nikomatsakis (Nov 04 2019 at 19:41, on Zulip):

the '!1 is in a universe 1 (say), but the ?x is in universe 0, and hence it can't name '!1, so you have an error

nikomatsakis (Nov 04 2019 at 19:41, on Zulip):

the question is more when this is detected

nikomatsakis (Nov 04 2019 at 19:41, on Zulip):

the non-nll code is doing this thing called the leak-check

nikomatsakis (Nov 04 2019 at 19:42, on Zulip):

basically during unification we check whether '!1 "leaks out" into any variables that can't name it

Alexander Regueiro (Nov 04 2019 at 19:42, on Zulip):

hi folks, around now

nikomatsakis (Nov 04 2019 at 19:42, on Zulip):

so we get an error

nikomatsakis (Nov 04 2019 at 19:42, on Zulip):

during the actual subtyping check

nikomatsakis (Nov 04 2019 at 19:43, on Zulip):

but this is different from how we handle regions most of the time

nikomatsakis (Nov 04 2019 at 19:43, on Zulip):

it's also a bit too strong

nikomatsakis (Nov 04 2019 at 19:43, on Zulip):

but this is different from how we handle regions most of the time

normally, the subtyping check just generates constraints that feed into region inference later

nikomatsakis (Nov 04 2019 at 19:44, on Zulip):

I guess I can explain that a bit too

nikomatsakis (Nov 04 2019 at 19:45, on Zulip):

currently when we do operations on types we divide into two phases: the first check compares the "skelton" of the type and generates "region constraints", and then the second phase processes those constraints (region inference)

nikomatsakis (Nov 04 2019 at 19:45, on Zulip):

so e.g. if you have &'0 u32 <: &'1 u32, where '0 and '1 are some regions, that would succeed, but generate a constraint '0: '1 -- meaning that we have to prove later that '0 outlives '1

nikomatsakis (Nov 04 2019 at 19:46, on Zulip):

this distinction is kind of important

nikomatsakis (Nov 04 2019 at 19:46, on Zulip):

because there are some parts of the compiler (e.g., coercions, coherence) that ignore those region constraints when deciding how to handle your program

Alexander Regueiro (Nov 04 2019 at 19:48, on Zulip):

BTW don't want to interrupt your current discussion, but ping me when you're okay to move onto trait upcasting briefly :-)

nikomatsakis (Nov 04 2019 at 19:48, on Zulip):

ok, I will stop here and see if any of this is making sense so far

tmandry (Nov 04 2019 at 19:52, on Zulip):

..so it sounds like you'd like to move the "leak check" out of the first phase (unification) and into the second (region inference)?

nikomatsakis (Nov 04 2019 at 19:52, on Zulip):

yes, more or less

nikomatsakis (Nov 04 2019 at 19:52, on Zulip):

and that's what my PR does

nikomatsakis (Nov 04 2019 at 19:53, on Zulip):

the problem with doing it in the first phase is two-fold

nikomatsakis (Nov 04 2019 at 19:53, on Zulip):

one, it's kind of surprising

nikomatsakis (Nov 04 2019 at 19:53, on Zulip):

in some cases

nikomatsakis (Nov 04 2019 at 19:53, on Zulip):

but more importantly, it assumes you have the full set of constraints available to you, so you can do the leak-check

nikomatsakis (Nov 04 2019 at 19:53, on Zulip):

basically what the code does is to walk the constraints that are propagating back, looking for constraints from a placeholder in some universe to a region that can't see that placeholder

nikomatsakis (Nov 04 2019 at 19:54, on Zulip):

it is also true that this code is too strong and gives the wrong result

nikomatsakis (Nov 04 2019 at 19:54, on Zulip):

so effectively you would get a constraint like '?x = '!1

so in my earlier example I mentioned this --

nikomatsakis (Nov 04 2019 at 19:54, on Zulip):

really this would be represented as two constraints

nikomatsakis (Nov 04 2019 at 19:55, on Zulip):
'!1: '?x
'?x: '!1
nikomatsakis (Nov 04 2019 at 19:55, on Zulip):

since if 'a: 'b and 'b: 'a then 'a = 'b

nikomatsakis (Nov 04 2019 at 19:55, on Zulip):

anyway so we would error out on those, because ?X is from an outer universe

nikomatsakis (Nov 04 2019 at 19:55, on Zulip):

but you can have examples like

'static: '!1

and this should not error

nikomatsakis (Nov 04 2019 at 19:56, on Zulip):

but the 'static may not always be visible

nikomatsakis (Nov 04 2019 at 19:56, on Zulip):

e.g. what if we had '?x: '!1, and ?x were later inferred to be equal to 'static?

nikomatsakis (Nov 04 2019 at 19:56, on Zulip):

right now, the leak-check rejects the constraint as unsatisfiable, but that's wrong

nikomatsakis (Nov 04 2019 at 19:56, on Zulip):

so the PR handles this in a more principled way

nikomatsakis (Nov 04 2019 at 19:56, on Zulip):

but this does have some effects on rust code

nikomatsakis (Nov 04 2019 at 19:57, on Zulip):

the biggest one has to do w/ coherence

nikomatsakis (Nov 04 2019 at 19:57, on Zulip):
impl Foo for for<'a> fn(&u8) { }
impl<'a> Foo for fn(&'a u8) { }
nikomatsakis (Nov 04 2019 at 19:57, on Zulip):

these two impls were previously permitted, but on the current branch, they are rejected

nikomatsakis (Nov 04 2019 at 19:58, on Zulip):

this falls out from coherence ignoring region constraints -- and the logic that causes them to get rejected has moved into the "solve the region constraints" part of the code

nikomatsakis (Nov 04 2019 at 19:58, on Zulip):

I'm not 100% sure if we can "get away" with this change -- it doesn't seem to affect many crates on crater, but we probably need a fresh crater run, and anyway we can't see all the crates.

nikomatsakis (Nov 04 2019 at 19:58, on Zulip):

I think though that we could restore the older behavior if needed by modifying coherence

nikomatsakis (Nov 04 2019 at 19:59, on Zulip):

That said, there are reasons to prefer the newer behavior

nikomatsakis (Nov 04 2019 at 20:00, on Zulip):

ok, I think I'm going to leave this dissertation here for the moment. I'd encourage people to check out the rustc-guide chapter -- I think it's a more organized presentation than the one I gave here. In any case, I didn't get to the tricky bits I had hope to talk about, but maybe I'll do some investigation and we can discuss next time.

nikomatsakis (Nov 04 2019 at 20:00, on Zulip):

(also feel free to ask me questions)

Matthew Jasper (Nov 04 2019 at 20:01, on Zulip):

so the PR handles this in a more principled way

This is already implemented, right? The PR removes the leak check and which allows the universe based check to produce errors.

nikomatsakis (Nov 04 2019 at 20:13, on Zulip):

yep

Last update: Nov 12 2019 at 17:00UTC