Stream: t-compiler/wg-nll

Topic: #55748, annotations and variance


pnkfelix (Dec 11 2018 at 13:00, on Zulip):

Hey @nikomatsakis

pnkfelix (Dec 11 2018 at 13:00, on Zulip):

there is an interesting issue that I've encountered while investigating #55748

pnkfelix (Dec 11 2018 at 13:01, on Zulip):

you can read the comments on the issue to see where some of my investigation has taken me

pnkfelix (Dec 11 2018 at 13:04, on Zulip):

but the latest thing is not relayed there (yet)

pnkfelix (Dec 11 2018 at 13:05, on Zulip):

namely, I tried putting in a change that makes the user-type-annotation in question use an Invariant relation rather than a Covariant one

pnkfelix (Dec 11 2018 at 13:06, on Zulip):

and it breaks one test (in NLL mode): run-pass/regions/regions-variance-covariant-use-covariant.rs

pnkfelix (Dec 11 2018 at 13:06, on Zulip):

but here's the interesting tidbit

pnkfelix (Dec 11 2018 at 13:09, on Zulip):

consider this: play

pnkfelix (Dec 11 2018 at 13:10, on Zulip):

namely, if we use type-ascription to attach the : Covariant<'static> annotation to the expression directly, rather than the local variable, the code gets rejected

pnkfelix (Dec 11 2018 at 13:11, on Zulip):

I at least have not managed to wrap my head around making a consistent user-oriented story for this behavior

pnkfelix (Dec 11 2018 at 13:17, on Zulip):

(Well, that’s not totally true; I can sort of explain it in terms of saying that the point where the co is assigned into the local is a spot where subtyping takes place )

pnkfelix (Dec 11 2018 at 13:56, on Zulip):

also, its worth pointing out a third case where I do expect to see subtyping applied that is not quite the same as either of the two I've presented

pnkfelix (Dec 11 2018 at 13:57, on Zulip):

Here's a new playground with all three cases and a summary of the behaviors I've observed

pnkfelix (Dec 11 2018 at 14:02, on Zulip):

Here: https://play.rust-lang.org/?version=nightly&mode=debug&edition=2018&gist=6565550a5b6d9243b449e719bd18ac3d

pnkfelix (Dec 11 2018 at 14:03, on Zulip):

(maybe I will open a fresh issue about this matter, since it really has gone far afield of the core question underlying #55748 )

pnkfelix (Dec 11 2018 at 14:04, on Zulip):

but the main point of the summary in the playground I linked above is that parameter passing still behaves as one expects (with respect to subtyping/variance)

pnkfelix (Dec 11 2018 at 14:07, on Zulip):

and it is only the question of how ascription should behave when attached to a let binding -- should it be consistent with ascription to an expression? Or consistent with parameter passing?

pnkfelix (Dec 11 2018 at 14:08, on Zulip):

OH! Even more interesting

pnkfelix (Dec 11 2018 at 14:08, on Zulip):

the test regions-variance-covariant-use-covariant.rs is using let _: Covariant<'static> = c;

pnkfelix (Dec 11 2018 at 14:08, on Zulip):

(which my change is then rejecting)

pnkfelix (Dec 11 2018 at 14:09, on Zulip):

but if you change it to let _c: Covariant<'static> = c;

pnkfelix (Dec 11 2018 at 14:09, on Zulip):

my change continues to accept

pnkfelix (Dec 11 2018 at 14:09, on Zulip):

I think this is a sign that the my change is an improvement over the status quo

pnkfelix (Dec 11 2018 at 14:10, on Zulip):

because ascriptions on let _: T = RHS bindings are IMO best interpreted as predicates directly on the RHS expression; no move is happening and thus it is not a predicate on any destination location for an assignment from RHS...

pnkfelix (Dec 11 2018 at 14:19, on Zulip):

here is a more complete playground covering the addition _c case I identified above: https://play.rust-lang.org/?version=nightly&mode=debug&edition=2015&gist=6cc57e52b8465dab69a477bd08b33ba2

pnkfelix (Dec 12 2018 at 13:34, on Zulip):

Also, just to be complete the record here, I have now filed an issue dedicated to the question immediately above: "should let _: T = RHS be synonymous with let _ = RHS: T?" #56715

nikomatsakis (Dec 12 2018 at 18:04, on Zulip):

@pnkfelix sorry failed to follow up, reading now

nikomatsakis (Dec 12 2018 at 18:08, on Zulip):

I at least have not managed to wrap my head around making a consistent user-oriented story for this behavior

I've been wondering about this. It seems also related to the meaning of : (type ascription) operator. Basically, if I follow you, it's often quite unclear whether exactly what the T in let pat: T = ... is constraining, right?

nikomatsakis (Dec 12 2018 at 18:09, on Zulip):

You are asserting that _: T should be understood as constraining the RHS -- it's hard to see what else it could do. But where exactly do we draw the line?

nikomatsakis (Dec 12 2018 at 18:10, on Zulip):

Or.. do we? I feel like perhaps the T has two effects?

One is to be a supertype of the RHS?

The other is to specify the types of the bindings (if any) as an "equality" constraint?

pnkfelix (Dec 12 2018 at 20:19, on Zulip):

hmm

pnkfelix (Dec 12 2018 at 20:19, on Zulip):

interesting, the idea of trying to divide it into two parts that way

pnkfelix (Dec 12 2018 at 20:20, on Zulip):

super-subtle. But also might be the only way we can hope to maintain backward compatibility while enforcing soundness

nikomatsakis (Dec 12 2018 at 20:22, on Zulip):

Yeah. I feel like I encountered this already

pnkfelix (Dec 19 2018 at 12:13, on Zulip):

@nikomatsakis so I'm continuing to poke at the demo on this issue, this time atop @davidtwco 's PR for #54943

pnkfelix (Dec 19 2018 at 12:13, on Zulip):

and I am still trying to puzzle through what the MIR does versus what it should do

pnkfelix (Dec 19 2018 at 12:14, on Zulip):

here is a gist of the MIR I am looking at (while looking in parallel at some RUST_LOG output)

pnkfelix (Dec 19 2018 at 12:15, on Zulip):

oh this is for the source code at this gist

pnkfelix (Dec 19 2018 at 12:16, on Zulip):

so the main thing I note here is that we enforce the user-type annotation via AscribeUserType(_6, +, UserTypeProjection { base: UserTypeAnnotation(2), projs: [] });

pnkfelix (Dec 19 2018 at 12:17, on Zulip):

which uses Variance::Covariant, as we've discussed ad nauseum on this thread.

pnkfelix (Dec 19 2018 at 12:17, on Zulip):

so my reading of that is that _6 represents a temporary for the RHS of let (mut y, mut _z): Pair<&u32> = (s, &local);

pnkfelix (Dec 19 2018 at 12:18, on Zulip):

and then we subsequently bind y in _4 = (_6.0: &'_#6r u32);

pnkfelix (Dec 19 2018 at 12:18, on Zulip):

but this means that we've failed to enforce any relationship between '_#6r and the user-type annotation

pnkfelix (Dec 19 2018 at 12:20, on Zulip):

well, I shouldn't say "failed to enforce any relationship"

pnkfelix (Dec 19 2018 at 12:21, on Zulip):

but if you look at the printout of the region relationships that is in the gist for the MIR

pnkfelix (Dec 19 2018 at 12:22, on Zulip):

in my idealized world, the relations there would end up implying that the regions attached to the references for _4 (y) and _5 (_z) are equal. But those regions ('_#13r and '_#14r respectively) are not equal.

pnkfelix (Dec 19 2018 at 12:24, on Zulip):

the MIR output there doesn't include this, but the RUST_LOG output includes lines like this:

DEBUG 2018-12-18T15:42:33Z: rustc_mir::borrow_check::nll::type_check: check_stmt: AscribeUserType(_6, +, UserTypeProjection { base: UserTypeAnnotation(2), projs: [] })
DEBUG 2018-12-18T15:42:33Z: rustc_mir::borrow_check::nll::type_check: relate_type_and_user_type(a=(&'_#15r u32, &'_#16r u32), v=+, user_ty=UserTypeProjection { base: UserTypeAnnotation(2), projs: [] }, locations=All(wildcard-tyvars.rs:1\
0:26: 10:36))
DEBUG 2018-12-18T15:42:33Z: rustc_mir::borrow_check::nll::type_check: user_ty base: UserTypeAnnotation(2) freshened: (&'_#22r u32, &'_#22r u32) projs: [] yields: Ok(Ty { ty: (&'_#22r u32, &'_#22r u32) })
DEBUG 2018-12-18T15:42:33Z: rustc_mir::borrow_check::nll::type_check::relate_tys: eq_types(a=(&'_#22r u32, &'_#22r u32), b=(&'_#15r u32, &'_#16r u32), locations=All(wildcard-tyvars.rs:10:26: 10:36))
DEBUG 2018-12-18T15:42:33Z: rustc_mir::borrow_check::nll::constraints: ConstraintSet::push('_#15r: '_#22r @ All(wildcard-tyvars.rs:10:26: 10:36)
DEBUG 2018-12-18T15:42:33Z: rustc_mir::borrow_check::nll::constraints: ConstraintSet::push('_#16r: '_#22r @ All(wildcard-tyvars.rs:10:26: 10:36)
pnkfelix (Dec 19 2018 at 12:24, on Zulip):

so to my eye, that is where I'm associating '_#22 with the region for the user-type annotation

pnkfelix (Dec 19 2018 at 12:29, on Zulip):

so in the end we end up with constraints that say (after some simplification): { '_#15r : '_#22r, '_#16r : '_#22r, '_#15r : '_#13r, '_#16r : '_#14r }

pnkfelix (Dec 19 2018 at 12:31, on Zulip):

and I guess I'm trying to figure out whether MIR code generation should be including assertions at the uses of local variables like y stating that its explicitly annotated type should be a subtype of the inferred type. In order to achieve (maybe?) the end effect of directly relating '_#22r and '_#13r

pnkfelix (Dec 19 2018 at 12:33, on Zulip):

or maybe the simpler way to go is to explore the two prong solution you proposed earlier (which I'll quote immediately below)

pnkfelix (Dec 19 2018 at 12:33, on Zulip):

Or.. do we? I feel like perhaps the T has two effects?

One is to be a supertype of the RHS?

The other is to specify the types of the bindings (if any) as an "equality" constraint?

this

pnkfelix (Dec 19 2018 at 12:38, on Zulip):

in fact, maybe I will try to do that now

nikomatsakis (Dec 19 2018 at 20:21, on Zulip):

in fact, maybe I will try to do that now

yes, I think we actually need two distinct type assertions. I'm not totally sure what we do now, I thought that was what we did but...

Last update: Nov 21 2019 at 23:25UTC