Stream: t-compiler/wg-nll

Topic: #67681 and region solving


Matthew Jasper (Jan 06 2020 at 19:29, on Zulip):

@nikomatsakis can we schedule a time to discuss #67681 and further plans in that direction? I'm available from about this time (19:30 UTC) onwards on weekdays.

Matthew Jasper (Jan 07 2020 at 17:58, on Zulip):

ping @nikomatsakis ^

nikomatsakis (Jan 14 2020 at 17:59, on Zulip):

ugh I missed this, sorry @Matthew Jasper

nikomatsakis (Jan 14 2020 at 17:59, on Zulip):

yes, let's do that

nikomatsakis (Jan 14 2020 at 18:00, on Zulip):

are you still available with those times?

Matthew Jasper (Jan 14 2020 at 19:00, on Zulip):

Yes

Matthew Jasper (Jan 15 2020 at 19:36, on Zulip):

@nikomatsakis :wave:

nikomatsakis (Jan 15 2020 at 19:38, on Zulip):

Hi:)

nikomatsakis (Jan 15 2020 at 19:38, on Zulip):

Gimme one or two minutes

nikomatsakis (Jan 15 2020 at 19:43, on Zulip):

ok ok

nikomatsakis (Jan 15 2020 at 19:43, on Zulip):

So yeah @Matthew Jasper not sure if we had a precise agenda

nikomatsakis (Jan 15 2020 at 19:43, on Zulip):

I guess the bigger question is "how to remove lexical checker"

nikomatsakis (Jan 15 2020 at 19:43, on Zulip):

well I'm not sure if that's the right framing, so maybe we should start with that question

nikomatsakis (Jan 15 2020 at 19:43, on Zulip):

is the goal to remove lexical checker or to move typeck to not compute regions

Matthew Jasper (Jan 15 2020 at 19:44, on Zulip):

Well, I have a list of things that move towards _move typeck to not compute regions_

Matthew Jasper (Jan 15 2020 at 19:45, on Zulip):

I'm not sure if getting the NLL solver to handle region solving in, say item wf checking would be that beneficial.

nikomatsakis (Jan 15 2020 at 19:46, on Zulip):

Yes

nikomatsakis (Jan 15 2020 at 19:46, on Zulip):

Well, yes and no

nikomatsakis (Jan 15 2020 at 19:46, on Zulip):

I mean the advantage would obviously be that we have only one region checker, whereas now we have 2

nikomatsakis (Jan 15 2020 at 19:46, on Zulip):

but I think I"ve basically come around to thinking "that is a waste of time"

nikomatsakis (Jan 15 2020 at 19:46, on Zulip):

that is, we should focus more on liberating typeck

nikomatsakis (Jan 15 2020 at 19:47, on Zulip):

and things like "item wf checking" can wait

Matthew Jasper (Jan 15 2020 at 19:47, on Zulip):

It's much lower priority at least.

nikomatsakis (Jan 15 2020 at 19:47, on Zulip):

so what is your list?

nikomatsakis (Jan 15 2020 at 19:48, on Zulip):

(also, I'm trying to remember what the PR you had was...)

nikomatsakis (Jan 15 2020 at 19:49, on Zulip):

also, I rebased the "no leak check" branch btw

nikomatsakis (Jan 15 2020 at 19:49, on Zulip):

we could talk a bit about that too :)

nikomatsakis (Jan 15 2020 at 19:49, on Zulip):

I haven't yet tried to keep the leak check and issue warnings, I was going to tinker with that, prob not too hard to do

Matthew Jasper (Jan 15 2020 at 19:50, on Zulip):
Matthew Jasper (Jan 15 2020 at 19:51, on Zulip):

If we keep the leak check and emit warnings, does selection also need the leak check to avoid ambiguity errors?

nikomatsakis (Jan 15 2020 at 19:51, on Zulip):

Yes, I think it does

nikomatsakis (Jan 15 2020 at 19:51, on Zulip):

Which is why I think if we issue warnings

nikomatsakis (Jan 15 2020 at 19:51, on Zulip):

We probably want to keep leak check .. all the time?

nikomatsakis (Jan 15 2020 at 19:51, on Zulip):

it just feels like things will be too inconsistent otherwise

nikomatsakis (Jan 15 2020 at 19:51, on Zulip):

ok so

nikomatsakis (Jan 15 2020 at 19:51, on Zulip):

looking at the list

nikomatsakis (Jan 15 2020 at 19:52, on Zulip):

I guess the idea of the first step is

nikomatsakis (Jan 15 2020 at 19:52, on Zulip):

start by erasing all the regions coming out from typeck--

Matthew Jasper (Jan 15 2020 at 19:52, on Zulip):

That list gets us about half way. I guess that the long term goal is to not even create ReVars?

nikomatsakis (Jan 15 2020 at 19:52, on Zulip):

thus proving the current "hypothesis" that NLL doesn't depend at all on the regionck from typeck

nikomatsakis (Jan 15 2020 at 19:53, on Zulip):

this is interesting

nikomatsakis (Jan 15 2020 at 19:53, on Zulip):

if I'm reading your list correctly, at no point do we stop running lexical_region_resolve on regular functions...? oh, I see, that was the second bullet

nikomatsakis (Jan 15 2020 at 19:54, on Zulip):

I misunderstood it at first

Matthew Jasper (Jan 15 2020 at 19:56, on Zulip):

(also, I'm trying to remember what the PR you had was...)

It moves opaque type region inference to borrow checking.

nikomatsakis (Jan 15 2020 at 19:56, on Zulip):

ah right right

nikomatsakis (Jan 15 2020 at 19:56, on Zulip):

so as far as visiting expressions in regionck

nikomatsakis (Jan 15 2020 at 19:57, on Zulip):

I think maybe some aspects of WF checking were triggered by that?

nikomatsakis (Jan 15 2020 at 19:57, on Zulip):

trying to remember, there is something "special" about a type outliving the empty region

nikomatsakis (Jan 15 2020 at 19:57, on Zulip):

re: my PR, I was hoping that we land it with the leak-check on "life support"

nikomatsakis (Jan 15 2020 at 19:57, on Zulip):

and then at next release maybe rip it out, hopefully that gives a bit of transition? I'd hope it's short

nikomatsakis (Jan 15 2020 at 19:57, on Zulip):

I still feel a bit uncomfortable, like how best to explain what we are doing and "why"

nikomatsakis (Jan 15 2020 at 19:58, on Zulip):

but I also like that this gives some time to write the code in NLL checker that I didn't get to

nikomatsakis (Jan 15 2020 at 19:58, on Zulip):

I still feel a bit uncomfortable, like how best to explain what we are doing and "why"

I think it probably suffices to say:

We are pursuing a model of region checking that is maximally conservative in some sense, and fixing lots of existing bugs in the current code.

nikomatsakis (Jan 15 2020 at 19:59, on Zulip):

the maximally conservative part refers to this balance of "how much checking takes place eagerly, and hence effects subtyping" and "how much takes place in region checking" -- or just kind of -- where do region constraints get evaluated

nikomatsakis (Jan 15 2020 at 20:00, on Zulip):

I feel I can write up an explanation around this, maybe make a tracking issue, though I think ideally I would want to have an RFC (though it would be the sort of RFC that nobody reads but Ariel Ben-Yehuda, no doubt =)

nikomatsakis (Jan 15 2020 at 20:01, on Zulip):

but I think an RFC would be better for when we sort of know the "full answer", and/or part of describing chalk/polonius

nikomatsakis (Jan 15 2020 at 20:01, on Zulip):

anyway I think your plan for moving regions makes sense

nikomatsakis (Jan 15 2020 at 20:01, on Zulip):

do we have a tracking issue for this?

Matthew Jasper (Jan 15 2020 at 20:02, on Zulip):

No. I was going to create one after this and I had a bit more clarity on the goal.

nikomatsakis (Jan 15 2020 at 20:02, on Zulip):

I'm pondering the part about

nikomatsakis (Jan 15 2020 at 20:02, on Zulip):

well first off

nikomatsakis (Jan 15 2020 at 20:02, on Zulip):

That list gets us about half way. I guess that the long term goal is to not even create ReVars?

to come back to this

nikomatsakis (Jan 15 2020 at 20:02, on Zulip):

yeah I mean in my ideal world

nikomatsakis (Jan 15 2020 at 20:02, on Zulip):

we'd be erasing regions as we bring things "into scope" of the type checker

nikomatsakis (Jan 15 2020 at 20:03, on Zulip):

this would also improve caching, presumably, between functions

Matthew Jasper (Jan 15 2020 at 20:04, on Zulip):

Indeed. And maybe reduce the number of types we're interning.

nikomatsakis (Jan 15 2020 at 20:04, on Zulip):

right

nikomatsakis (Jan 15 2020 at 20:04, on Zulip):

so I guess that is my goal :)

nikomatsakis (Jan 15 2020 at 20:04, on Zulip):

I'm still pondering the part about:

keep running regionck without running the region solver

nikomatsakis (Jan 15 2020 at 20:05, on Zulip):

are there checks that it does that we would have to do elsewhere?

nikomatsakis (Jan 15 2020 at 20:05, on Zulip):

is it just a matter of bad error messages or something?

nikomatsakis (Jan 15 2020 at 20:05, on Zulip):

I remember being not very happy about the hacks around "outlives 'empty"

nikomatsakis (Jan 15 2020 at 20:05, on Zulip):

and in particular the checks that say "is this 'empty? if so, return" that we use to avoid ICEs

nikomatsakis (Jan 15 2020 at 20:05, on Zulip):

but I sort of forget if I had a different sol'n in mind

Matthew Jasper (Jan 15 2020 at 20:06, on Zulip):

It can also cause dropck_outlives to run which hides the hang that https://github.com/rust-lang/rust/pull/67731 fixes.

nikomatsakis (Jan 15 2020 at 20:07, on Zulip):

but NLL subsumes that check, right?

Matthew Jasper (Jan 15 2020 at 20:08, on Zulip):

I think NLL skips it for types with no free lifetimes (in fact, no free lifetimes that don't contain a universal region atm)

nikomatsakis (Jan 15 2020 at 20:09, on Zulip):

is that a problem?

Matthew Jasper (Jan 15 2020 at 20:09, on Zulip):

Not with that PR.

nikomatsakis (Jan 15 2020 at 20:09, on Zulip):

ok =)

nikomatsakis (Jan 15 2020 at 20:12, on Zulip):

well, ok, then I'll get to work on those modifications to leak check PR ;)

nikomatsakis (Jan 15 2020 at 20:12, on Zulip):

and you create tracking issue :)

nikomatsakis (Jan 15 2020 at 20:12, on Zulip):

we'll figure out the next steps after that

Matthew Jasper (Jan 15 2020 at 20:13, on Zulip):

:+1:

Matthew Jasper (Jan 15 2020 at 20:14, on Zulip):

This issue title is something like "Don't infer regions in type checking"?

nikomatsakis (Jan 15 2020 at 20:14, on Zulip):

Did you see https://github.com/rust-lang/rust/pull/67911 ?

nikomatsakis (Jan 15 2020 at 20:14, on Zulip):

you are assigned to it, I guess

nikomatsakis (Jan 15 2020 at 20:15, on Zulip):

are my concerns correct, that this approach won't work?

nikomatsakis (Jan 15 2020 at 20:15, on Zulip):

or am I missing something :)

Matthew Jasper (Jan 15 2020 at 20:15, on Zulip):

I agree that this doesn't currently work. I haven't had time to think about how best to go about fixing it.

nikomatsakis (Jan 15 2020 at 20:17, on Zulip):

OK, me neither

Matthew Jasper (Jan 15 2020 at 20:25, on Zulip):

Opened #68261

Last update: Jan 21 2020 at 08:20UTC