Stream: t-compiler/wg-nll

Topic: #54620 user type annot well-formed


nikomatsakis (Oct 04 2018 at 20:11, on Zulip):

cc @blitzerr — I didn't find a previous topic for this, so I created one

nikomatsakis (Oct 04 2018 at 20:11, on Zulip):

did the mentoring instructions I put on the issue make sense?

blitzerr (Oct 04 2018 at 20:13, on Zulip):

Kind of :smiley:.

blitzerr (Oct 04 2018 at 20:15, on Zulip):

I say that because I am going through the code in type_check/mod.rs and trying to figure out what's going on and what the terms such as well formed, prove_predicate, cannonical types and values mean

nikomatsakis (Oct 04 2018 at 20:16, on Zulip):

@blitzerr while the contents of this RFC aren't directly related, it may help with the general background (RFC 1214)

blitzerr (Oct 04 2018 at 20:16, on Zulip):

Cool thanks a lot @nikomatsakis

blitzerr (Oct 04 2018 at 20:18, on Zulip):

Also I will be away for a couple of weeks from Oct 8-23. So might not get it to PR approved state by then. Will that be an issue ?

nikomatsakis (Oct 04 2018 at 20:19, on Zulip):

Hmm, could be, yes

nikomatsakis (Oct 04 2018 at 20:19, on Zulip):

since we're trying to land this by Oct 25

blitzerr (Oct 05 2018 at 15:41, on Zulip):

@nikomatsakis
After the fix, we expect the error to be the same as it would be without NLL turned on right as it is here?
https://play.rust-lang.org/?gist=a6399e527836280d98889172fd919223&version=nightly&mode=debug&edition=2018

nikomatsakis (Oct 05 2018 at 16:05, on Zulip):

yes, more or less

nikomatsakis (Oct 05 2018 at 16:05, on Zulip):

at least in the same fns

blitzerr (Oct 07 2018 at 16:41, on Zulip):

Does someone know how to convert

b: CanonicalTy<'tcx>
into
var: CanonicalVar

So that it can be used by

canonical_var_values ```
blitzerr (Oct 07 2018 at 17:07, on Zulip):
pub(super) fn relate_type_and_user_type<'tcx>(
    infcx: &InferCtxt<'_, '_, 'tcx>,
    a: Ty<'tcx>,
    v: ty::Variance,
    b: CanonicalTy<'tcx>,
    locations: Locations,
    category: ConstraintCategory,
    borrowck_context: Option<&mut BorrowCheckContext<'_, 'tcx>>,
) -> Fallible<()> {
    debug!(
    ¦   "sub_type_and_user_type(a={:?}, b={:?}, locations={:?})",
    ¦   a, b, locations
    );
    let Canonical {
    ¦   variables: b_variables,
    ¦   value: b_value,
    } = b;

Here one could use b_variables instead of b.variables ?

blitzerr (Oct 07 2018 at 18:26, on Zulip):

@nikomatsakis
It does not look like I will be able to take the PR for #54620 to finish line by Oct 25 as I will be traveling. So it might be worthwhile to assign it to someone else. Sorry about that.

Matthew Jasper (Oct 07 2018 at 18:46, on Zulip):

I'm doing some things that are related, so I might pick it up with them.

blitzerr (Oct 08 2018 at 15:04, on Zulip):

Thanks a lot @Matthew Jasper

nikomatsakis (Oct 08 2018 at 15:30, on Zulip):

@blitzerr the question -- how to convert a canonical-ty into a canonical-var -- doesn't really make sense, I'm afraid

nikomatsakis (Oct 08 2018 at 15:30, on Zulip):

but maybe a moot point

blitzerr (Oct 08 2018 at 15:40, on Zulip):

@nikomatsakis
In
fn relate_type_and_user_type the argument is CanonicalTy<'tcx>
but the canonical_var_values: IndexVec<CanonicalVar, Option<Kind<'tcx>>>
is an index vector of CanonicalVar. So wouldn't it require a conversion ?

blitzerr (Oct 08 2018 at 15:45, on Zulip):

Because this is what my interpretation of the mentorship note was:
- Instantiate the canonical types with their canonical variables using (substitute function).
- Then create the well formed predicate for each.

blitzerr (Oct 08 2018 at 22:41, on Zulip):

@nikomatsakis

nikomatsakis (Oct 09 2018 at 16:09, on Zulip):

@Matthew Jasper so you are taking this issue?

nikomatsakis (Oct 09 2018 at 16:09, on Zulip):

(I was debating about fixing it, but I can do other things)

nikomatsakis (Oct 09 2018 at 16:09, on Zulip):

@blitzerr mainly because that type is not a key to that vector — you might want to read up on the rustc-guide chapter on canonicalization

Matthew Jasper (Oct 09 2018 at 16:10, on Zulip):

Yes, I should have a PR up later today.

nikomatsakis (Oct 09 2018 at 16:10, on Zulip):

@Matthew Jasper I was thinking of ripping out the code from relate_tys that tries to figure out the values for canonical values

nikomatsakis (Oct 09 2018 at 16:10, on Zulip):

and instead just instantiating with "fresh inference variables"

nikomatsakis (Oct 09 2018 at 16:10, on Zulip):

I think.. at this point... there is no reason not to do that? Ah, well, I guess it might mean I have to make relate_tys able to handle unbound type variables

nikomatsakis (Oct 09 2018 at 16:10, on Zulip):

but we have the generalization code

nikomatsakis (Oct 09 2018 at 16:11, on Zulip):

oh I guess we have the ability to "Substitute" into a canonical ty

nikomatsakis (Oct 09 2018 at 16:12, on Zulip):

I remember now that this was a decent alternative

nikomatsakis (Oct 09 2018 at 16:12, on Zulip):

@blitzerr to elaborate a bit more, the "canonical type" is basically a "type with holes in it" (missing bits) and the values in that vector are the values that go into those holes

Matthew Jasper (Oct 09 2018 at 16:13, on Zulip):

Ah, well, I guess it might mean I have to make relate_tys able to handle unbound type variables

How would that be different to now?

nikomatsakis (Oct 09 2018 at 16:45, on Zulip):

right now I think it panics

nikomatsakis (Oct 09 2018 at 16:45, on Zulip):

but the logic to handle an unbound type variable would not be particularly different from the logic we are using to handle canonical vars

nikomatsakis (Oct 09 2018 at 16:45, on Zulip):

instead, if we found a canonical var, we would panic

Matthew Jasper (Oct 09 2018 at 19:45, on Zulip):

So, unreachable type annotations get removed from the MIR before we get to borrowck.

Matthew Jasper (Oct 09 2018 at 19:48, on Zulip):

obvious solution 1: keep them around. problem: the RHS of let _: T = ...is a coercion site, so the type annotation applies to what looks like just a local variable only sometimes.

nikomatsakis (Oct 09 2018 at 19:49, on Zulip):

I am not sure if we really care

nikomatsakis (Oct 09 2018 at 19:49, on Zulip):

interesting question

Matthew Jasper (Oct 09 2018 at 19:49, on Zulip):

solution 2: only keep around the types and only check wf-ness of them. But this results in this:

instead, if we found a canonical var, we would panic

nikomatsakis (Oct 09 2018 at 19:49, on Zulip):

always hard to tell what to do with dead code for things like this

Matthew Jasper (Oct 09 2018 at 19:49, on Zulip):

solution 3: leave for another PR

Matthew Jasper (Oct 09 2018 at 19:51, on Zulip):

This could be a compiler tests only issue

nikomatsakis (Oct 09 2018 at 19:51, on Zulip):

i.e., something that won't arise in practice?

Matthew Jasper (Oct 09 2018 at 19:51, on Zulip):

yes

nikomatsakis (Oct 09 2018 at 19:51, on Zulip):

i'm thinking about it; in general, regions are now a "location-sensitive thing"

nikomatsakis (Oct 09 2018 at 19:52, on Zulip):

e.g., I think that if you have

let y = &foo;
if something {
    let x: &'a u32 = y;
    return;
}

// foo need not be borrowed here
nikomatsakis (Oct 09 2018 at 19:52, on Zulip):

this isn't really true today but hopefully will be with polonius

nikomatsakis (Oct 09 2018 at 19:53, on Zulip):

so in some sense if the code is dead, you can make a case that the region-oriented parts of the annotation don't "count" -- similar to how we don't really borrow check such code

Matthew Jasper (Oct 09 2018 at 19:59, on Zulip):

Link to the test that I'm try to get working (after enabling compare mode) https://github.com/rust-lang/rust/blob/master/src/test/ui/regions/regions-outlives-projection-container-wc.rs

nikomatsakis (Oct 09 2018 at 19:59, on Zulip):

yeah, so the code is not reachable...hmm.

nikomatsakis (Oct 09 2018 at 19:59, on Zulip):

so we do have a version of the type-checker

nikomatsakis (Oct 09 2018 at 19:59, on Zulip):

er, the MIR

nikomatsakis (Oct 09 2018 at 20:00, on Zulip):

before dead code is stripped

nikomatsakis (Oct 09 2018 at 20:00, on Zulip):

but I think running the borrowck on it would be maybe a big change

nikomatsakis (Oct 09 2018 at 20:00, on Zulip):

otoh there is something annoying about this being accepted

nikomatsakis (Oct 09 2018 at 20:01, on Zulip):

it doesn't feel like a "flow-sensitive" property

nikomatsakis (Oct 09 2018 at 20:01, on Zulip):

solution 2: only keep around the types and only check wf-ness of them. But this results in this:

instead, if we found a canonical var, we would panic

I don't understand what you meant here

Matthew Jasper (Oct 09 2018 at 20:02, on Zulip):

I mean that my attempt at solving this would panic if any types needed to be inferred.

nikomatsakis (Oct 09 2018 at 20:03, on Zulip):

hmm

nikomatsakis (Oct 09 2018 at 20:03, on Zulip):

so the user types could involve things like _

nikomatsakis (Oct 09 2018 at 20:03, on Zulip):

the main type-check will have inferred those — modulo regions —

nikomatsakis (Oct 09 2018 at 20:04, on Zulip):

I guess the question is what you mean by "keep the types around"

nikomatsakis (Oct 09 2018 at 20:04, on Zulip):

i.e., where would we do so

Matthew Jasper (Oct 09 2018 at 20:05, on Zulip):

So attempt 1 was to preserve the AscribeUserTypes in the simplify cfg pass: this results in surprising behaviour depending on whether the compiler coerces or not

Matthew Jasper (Oct 09 2018 at 20:06, on Zulip):

Attempt 2 was to just keep the canonical types, but then there's nothing to substitute

nikomatsakis (Oct 09 2018 at 20:07, on Zulip):

yeah, this is what I was pondering

nikomatsakis (Oct 09 2018 at 20:07, on Zulip):

neither of those really feel right

Matthew Jasper (Oct 09 2018 at 20:07, on Zulip):

Indeed

nikomatsakis (Oct 09 2018 at 20:07, on Zulip):

I guess in the end that it feels like the most consistent option might be to not strip dead code

nikomatsakis (Oct 09 2018 at 20:07, on Zulip):

until after borrow check

nikomatsakis (Oct 09 2018 at 20:08, on Zulip):

if we wanted to issue errors here

nikomatsakis (Oct 09 2018 at 20:08, on Zulip):

I'm a bit wary of accepting types that are so clearly not well-formed

nikomatsakis (Oct 09 2018 at 20:09, on Zulip):

I guess in the end that it feels like the most consistent option might be to not strip dead code

I wonder what would break if we tried to do that, feels like a big change

nikomatsakis (Oct 09 2018 at 20:09, on Zulip):

it sort of requires you to deal with a notion of control-flow graphs that have multiple entry points

nikomatsakis (Oct 09 2018 at 20:09, on Zulip):

e.g., ideally we would issue errors that are "local" to a dead region

nikomatsakis (Oct 09 2018 at 20:09, on Zulip):

so something like this:

return;

let mut x = 22;
let y = &x;
x += 1;
use(y);
nikomatsakis (Oct 09 2018 at 20:10, on Zulip):

seems clearly out of scope for this PR

Matthew Jasper (Oct 09 2018 at 20:10, on Zulip):

There are problems like

let x = 0;
return;
use(x); // unitialized
nikomatsakis (Oct 09 2018 at 20:11, on Zulip):

yep

nikomatsakis (Oct 09 2018 at 20:11, on Zulip):

it's a big ol' can of worms

nikomatsakis (Oct 09 2018 at 20:11, on Zulip):

and the same sort of applies to these WF rules, I think

Matthew Jasper (Oct 09 2018 at 20:11, on Zulip):

Fake edges on return/goto?

nikomatsakis (Oct 09 2018 at 20:11, on Zulip):

no, because that would make borrows extend too long

nikomatsakis (Oct 09 2018 at 20:12, on Zulip):

I don't really know what set of things you would need

nikomatsakis (Oct 09 2018 at 20:12, on Zulip):

we decided a while back to just not report borrow check errors in dead code for simplicity

nikomatsakis (Oct 09 2018 at 20:13, on Zulip):

rightly or wrongly, I feel like backing up on that decision is going to be a major shipping risk :)

nikomatsakis (Oct 09 2018 at 20:13, on Zulip):

and isn't really an option

nikomatsakis (Oct 09 2018 at 20:13, on Zulip):

so the question is whether to do something targeted to this WF case

Matthew Jasper (Oct 09 2018 at 20:13, on Zulip):

Yes

nikomatsakis (Oct 09 2018 at 20:13, on Zulip):

in general, the rules around unreachable code are a kind of "best effort" basis in any case

Matthew Jasper (Oct 09 2018 at 20:13, on Zulip):

(as in that's the question)

nikomatsakis (Oct 09 2018 at 20:14, on Zulip):

I guess the thing we are baking in here is the idea of things being "Well-formed modulo regions"

nikomatsakis (Oct 09 2018 at 20:15, on Zulip):

that is, we accept this code, but we wouldn't accept some other variations

nikomatsakis (Oct 09 2018 at 20:15, on Zulip):

(because the type-checker will catch them early on)

nikomatsakis (Oct 09 2018 at 20:15, on Zulip):

this is .. probably ok, it's a concept that applies elsewhere, it's just one of the bits of the traits story that I've been wanting to get a better handle on

nikomatsakis (Oct 09 2018 at 20:15, on Zulip):

I would say that for now you should file the PR without "fixing" this test as is, and file a follow-up issue

nikomatsakis (Oct 09 2018 at 20:16, on Zulip):

(the test can be modified to avoid loop { })

nikomatsakis (Oct 09 2018 at 20:16, on Zulip):

e.g., fn foo<T>() -> T

nikomatsakis (Oct 09 2018 at 20:16, on Zulip):

sound reasonable?

Matthew Jasper (Oct 09 2018 at 20:18, on Zulip):

Yes, and borrowck=migrate catches this.

nikomatsakis (Oct 09 2018 at 20:22, on Zulip):

what do you mean by it "catches this"?

Matthew Jasper (Oct 09 2018 at 20:34, on Zulip):

It gives an error for https://github.com/rust-lang/rust/blob/master/src/test/ui/regions/regions-outlives-projection-container-wc.rs

nikomatsakis (Oct 09 2018 at 20:36, on Zulip):

ah, because we re-enable region errors during migration?

nikomatsakis (Oct 09 2018 at 20:36, on Zulip):

well ok that gives a bit of breathing room I guess

nikomatsakis (Oct 09 2018 at 21:45, on Zulip):

@Matthew Jasper can I see your WIP branch too?

nikomatsakis (Oct 09 2018 at 21:45, on Zulip):

and/or do you expect to open a PR soon?

Matthew Jasper (Oct 09 2018 at 21:45, on Zulip):

I'll have a PR soon

Matthew Jasper (Oct 09 2018 at 22:04, on Zulip):

#54942

nikomatsakis (Oct 09 2018 at 22:16, on Zulip):

cool

nikomatsakis (Oct 09 2018 at 22:16, on Zulip):

gotta run now, took a quick look, pondering a bit

nikomatsakis (Oct 09 2018 at 22:20, on Zulip):

left a review

blitzerr (Oct 10 2018 at 06:54, on Zulip):

@nikomatsakis

@blitzerr to elaborate a bit more, the "canonical type" is basically a "type with holes in it" (missing bits) and the values in that vector are the values that go into those holes

that part I got. I will look at @Matthew Jasper 's PR to understand it better.

blitzerr (Oct 10 2018 at 06:54, on Zulip):

I guess the thing we are baking in here is the idea of things being "Well-formed modulo regions"

@nikomatsakis what did you mean by this ? Also when I tried to read up on regions, I found this https://rust-lang-nursery.github.io/rustc-guide/traits/regions.html. Is there some other doc that I can read to understand the concept and the discussion?

nikomatsakis (Oct 10 2018 at 12:55, on Zulip):

@blitzerr "region" is a synonym for "lifetime"

nikomatsakis (Oct 10 2018 at 12:56, on Zulip):

@Matthew Jasper did you ever open an issue re: enforcing WF conditions in dead code?

nikomatsakis (Oct 10 2018 at 12:57, on Zulip):

@blitzerr what I meant by "well-formed modulo regions": the goal is to eventually have a first type-check that basically "ignores" ("erases") all specific lifetime information. So we don't track if something is &'a u32 or &'b u32, just &u32. The results of that type-check are used to build the MIR. Then we run the borrow check. So I said "well-formed modulo regions" because you would get errors if your type is ill-formed in some way that is not dependent on the specific regions involved ('a vs 'b) but — if the code is dead code — you would not get errors even if the regions involved were incorrect.

Matthew Jasper (Oct 10 2018 at 14:06, on Zulip):

#54943

nikomatsakis (Oct 10 2018 at 14:11, on Zulip):

@Matthew Jasper great, I was thinking we should add a FIXME into the test case

blitzerr (Oct 10 2018 at 15:14, on Zulip):

Thanks a lot for explaining @nikomatsakis . Makes sense.

Last update: Nov 21 2019 at 13:20UTC