Stream: t-compiler/wg-nll

Topic: #56715 meaning of type ascription


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

@pnkfelix so the complication with expr: T and the meaning there had to do with ref mut bindings and the potential unsoundness around them. Overall I would say that this effort to move to MIR is forcing us to take a good, hard look at what our : T ascriptions mean in general, and it feels like the answer is "it's complicated".

Anyway the bug we were worried about was something like

let ref mut x: T = y;

this had the semantics of making x be an &mut T that refers to y -- but if we have that the type T_y or y is some subtype of T, that's unsound, for the standard variance reasons.

nikomatsakis (Dec 17 2018 at 14:21, on Zulip):

same would presumably be true of let ref mut x = y: T

nikomatsakis (Dec 17 2018 at 14:21, on Zulip):

the current rule around the : T ascriptions is that "if the pattern includes a ref binding, then it forces strict equality", and we .. probably? .. need to do something similar around y: T expressions --

pnkfelix (Dec 17 2018 at 14:22, on Zulip):

I guess my Q is

nikomatsakis (Dec 17 2018 at 14:22, on Zulip):

that is, we could either (a) not consider them a place expression or (b) distinguish between the effect of a :T ascription in the context of a place (borrow) vs a use

pnkfelix (Dec 17 2018 at 14:22, on Zulip):

would it be so bad to use strict equality everywhere?

nikomatsakis (Dec 17 2018 at 14:22, on Zulip):

well

nikomatsakis (Dec 17 2018 at 14:22, on Zulip):

it'd be backwards incompatible

nikomatsakis (Dec 17 2018 at 14:22, on Zulip):

in a pretty major way

pnkfelix (Dec 17 2018 at 14:22, on Zulip):

(and rely on e.g. the moves/assignments to do the subtyping)

nikomatsakis (Dec 17 2018 at 14:23, on Zulip):

right now, let x: T = ... is more than subtyping -- it applies coercions

pnkfelix (Dec 17 2018 at 14:23, on Zulip):

sure, but we get to maybe couple it with NLL migration

nikomatsakis (Dec 17 2018 at 14:23, on Zulip):

I am not as worried about the subtyping thing as the coercions

nikomatsakis (Dec 17 2018 at 14:23, on Zulip):

e.g., something like this

let x: &[u32] = &[1, 2, 3];

coerces from the type &[u32; 3] to &[u32]

nikomatsakis (Dec 17 2018 at 14:24, on Zulip):

but maybe you mean something.. less than that

pnkfelix (Dec 17 2018 at 14:25, on Zulip):

the stuff I'm talking about, I think, is just about whether to use Variance::Covariant or Variance::Invariant at certain points

pnkfelix (Dec 17 2018 at 14:26, on Zulip):

I guess I'm not clear on how that effects coercions. I would have thought it only affects lifetime region inference/checking.

nikomatsakis (Dec 17 2018 at 14:26, on Zulip):

if we're only talking at the MIR locations

nikomatsakis (Dec 17 2018 at 14:26, on Zulip):

then I agree

nikomatsakis (Dec 17 2018 at 14:26, on Zulip):

but I guess I just want to fit it into my "overall view" of the type system

pnkfelix (Dec 17 2018 at 14:26, on Zulip):

Okay, yeah, when I said "everywhere", I guess I meant "everywhere in MIR"

pnkfelix (Dec 17 2018 at 14:27, on Zulip):

but not even that

pnkfelix (Dec 17 2018 at 14:27, on Zulip):

"on every type-ascription in the MIR"

nikomatsakis (Dec 17 2018 at 14:27, on Zulip):

I'm also not entirely clear on the motivation

pnkfelix (Dec 17 2018 at 14:27, on Zulip):

well right now

pnkfelix (Dec 17 2018 at 14:27, on Zulip):

when I write let x: T = RHS

pnkfelix (Dec 17 2018 at 14:28, on Zulip):

is that meant to be saying that x has some type T' that is a subtype of T

pnkfelix (Dec 17 2018 at 14:28, on Zulip):

or that x has type T exactly

pnkfelix (Dec 17 2018 at 14:28, on Zulip):

(I'm not even sure myself, right now...)

pnkfelix (Dec 17 2018 at 14:29, on Zulip):

but the whole thing behind #47184 was that we needed to respect user type annotations

nikomatsakis (Dec 17 2018 at 14:29, on Zulip):

or that x has type T exactly

there's another question too, right?

pnkfelix (Dec 17 2018 at 14:29, on Zulip):

and so I want to pin down what someone writing unsafe code can assume

nikomatsakis (Dec 17 2018 at 14:29, on Zulip):

"what is the type of the RHS"

pnkfelix (Dec 17 2018 at 14:30, on Zulip):

yep

nikomatsakis (Dec 17 2018 at 14:30, on Zulip):

i.e., what you are proposing seems to have nothing to do with the type of x

nikomatsakis (Dec 17 2018 at 14:30, on Zulip):

and everything to do with T_rhs

pnkfelix (Dec 17 2018 at 14:30, on Zulip):

well

pnkfelix (Dec 17 2018 at 14:30, on Zulip):

I was starting from my mental model

nikomatsakis (Dec 17 2018 at 14:30, on Zulip):

my "intuitive feeling" is that:

pnkfelix (Dec 17 2018 at 14:30, on Zulip):

of why we are even passing Variance::Covariant at the point in the code that I identified in #56715

nikomatsakis (Dec 17 2018 at 14:31, on Zulip):

but for more complex patterns, the first part gets tricky

pnkfelix (Dec 17 2018 at 14:31, on Zulip):

and that's why I was focusing on let x: T

nikomatsakis (Dec 17 2018 at 14:31, on Zulip):

and for ref bindings and "place expressions" on the right-hand-side, the second part is tricky (we actually forbid coercions here I think)

nikomatsakis (Dec 17 2018 at 14:32, on Zulip):

so my simple, "intuitive" formulation doesn't really capture all of it

nikomatsakis (Dec 17 2018 at 14:33, on Zulip):

of why we are even passing Variance::Covariant at the point in the code that I identified in #56715

let me go double check which code you are referring to )

nikomatsakis (Dec 17 2018 at 14:37, on Zulip):

ok, so, @pnkfelix if I'm not mistaken we are talking more about the relationship of T to T_rhs than the type of x

pnkfelix (Dec 17 2018 at 14:37, on Zulip):

It was introduced here; there wasn't much discussion at the time. :smile:

pnkfelix (Dec 17 2018 at 14:38, on Zulip):

Hmm maybe you are right, let me double check how ascribe_types is called.

nikomatsakis (Dec 17 2018 at 14:38, on Zulip):

It was introduced here; there wasn't much discussion at the time. :smile:

yeah, I mean, I wrote that code initially, I remember that

pnkfelix (Dec 17 2018 at 14:39, on Zulip):

so the calls to ascribe_types are asserting the candidate ascriptions for the relevant places

pnkfelix (Dec 17 2018 at 14:39, on Zulip):

as we descend the pattern

pnkfelix (Dec 17 2018 at 14:40, on Zulip):

Which ... I still would think would be asserting a statement about x

pnkfelix (Dec 17 2018 at 14:40, on Zulip):

and not a relationship between T and T_rhs ...

nikomatsakis (Dec 17 2018 at 14:40, on Zulip):

they are putting in match_pair.place

nikomatsakis (Dec 17 2018 at 14:40, on Zulip):

one sec

nikomatsakis (Dec 17 2018 at 14:41, on Zulip):

so I think this is where the ascriptions vector in Candidate is modified

nikomatsakis (Dec 17 2018 at 14:41, on Zulip):

by this code:

                candidate.ascriptions.push(Ascription {
                    span: user_ty_span,
                    user_ty: user_ty.clone(),
                    source: match_pair.place.clone(),
});
pnkfelix (Dec 17 2018 at 14:41, on Zulip):

okay now I agree with you

nikomatsakis (Dec 17 2018 at 14:41, on Zulip):

ok

pnkfelix (Dec 17 2018 at 14:42, on Zulip):

and I was miscasting the purpose of that code then

pnkfelix (Dec 17 2018 at 14:42, on Zulip):

which

pnkfelix (Dec 17 2018 at 14:42, on Zulip):

makes it all make more sense in terms of the behavior I was witnessing

pnkfelix (Dec 17 2018 at 14:42, on Zulip):

when I made the change I described (of sed -e s/Covariant/Invariant there)

pnkfelix (Dec 17 2018 at 14:42, on Zulip):

in terms of it only really affecting let _: T = RHS

nikomatsakis (Dec 17 2018 at 14:43, on Zulip):

yeah

nikomatsakis (Dec 17 2018 at 14:44, on Zulip):

I contend that it is a bit inconsistent to have permit coercions from T_rhs to T but not subtyping

pnkfelix (Dec 17 2018 at 14:44, on Zulip):

Okay yes

pnkfelix (Dec 17 2018 at 14:44, on Zulip):

I agree with that.

pnkfelix (Dec 17 2018 at 14:49, on Zulip):

just to double-check, your assertion is that let _: T = RHS can and will coerce when necessary, right?

pnkfelix (Dec 17 2018 at 14:49, on Zulip):

(i.e. I don't need to bind to an actual variable like _x in order to observe coercion occurring?)

pnkfelix (Dec 17 2018 at 14:50, on Zulip):

I guess I could/should test this readily enough.

nikomatsakis (Dec 17 2018 at 14:50, on Zulip):

just to double-check, your assertion is that let _: T = RHS can and will coerce when necessary, right?

yes I believe so

nikomatsakis (Dec 17 2018 at 14:51, on Zulip):

as there is no ref (syntactically) appearing in the LHS

pnkfelix (Dec 17 2018 at 14:52, on Zulip):

super-interesting

pnkfelix (Dec 17 2018 at 14:52, on Zulip):

since I sometimes think of _ as being "like" a ref

pnkfelix (Dec 17 2018 at 14:52, on Zulip):

in that it, on its own at least, will not cause a move

pnkfelix (Dec 17 2018 at 14:52, on Zulip):

but I believe I understand the basis for the design you present

pnkfelix (Dec 17 2018 at 14:53, on Zulip):

since the worrisome semantics would not be exposed by _; only by ref (or just ref mut maybe)

pnkfelix (Dec 17 2018 at 14:57, on Zulip):

(actually now I don't know how I'd observe coercion within the program itself without using a binding somewhere in the LHS...)

centril (Dec 17 2018 at 15:06, on Zulip):

/me reads backlog :P

centril (Dec 17 2018 at 15:27, on Zulip):

My mental model fits with @nikomatsakis's as well

pnkfelix (Dec 17 2018 at 15:27, on Zulip):

yeah at this point I've closed the issue

centril (Dec 17 2018 at 15:28, on Zulip):

@pnkfelix if my RFC is unclear and you think some fleshing out is needed I take PRs against my branch ;)

pnkfelix (Dec 17 2018 at 15:29, on Zulip):

We'll eventually need to deal with how type ascriptions on expressions behave

pnkfelix (Dec 17 2018 at 15:29, on Zulip):

(in terms of whether they need to be Covariant rather than Invariant in more cases)

pnkfelix (Dec 17 2018 at 15:29, on Zulip):

but for now all is fine with me.

centril (Dec 17 2018 at 15:29, on Zulip):

aight; we can do follow up RFCs

nikomatsakis (Dec 17 2018 at 17:26, on Zulip):

:+1:

Last update: Nov 21 2019 at 14:10UTC