Stream: t-compiler/wg-nll

Topic: #53873 type ascription bugs and semantics


pnkfelix (Sep 10 2018 at 13:36, on Zulip):

@nikomatsakis so we should talk here perhaps

pnkfelix (Sep 10 2018 at 13:37, on Zulip):

you ask a reasonable Q here, about when lifetimes in ascribed types should be meaningful

pnkfelix (Sep 10 2018 at 13:37, on Zulip):

to be honest, my intuition is that: if the programmer ascribed a type, at least to a variable (not sure yet about arbitrary expressions), then that type should be applied to the entire scope of that variable

pnkfelix (Sep 10 2018 at 13:38, on Zulip):

even over the course of assignments

pnkfelix (Sep 10 2018 at 13:38, on Zulip):

I realize that this might introduce borrowck errors (in the sense that sound code may start failing to compile, which might then be filed as an NLL-complete bug)

pnkfelix (Sep 10 2018 at 13:38, on Zulip):

but if someone is going to write out an explicit lifetime, I think we are probably better of err'ing on the side of respecting their request

pnkfelix (Sep 10 2018 at 13:39, on Zulip):

and also, I think that semantics will yield more intuitive user experience in terms of diagnostics

pnkfelix (Sep 10 2018 at 13:39, on Zulip):

namely avoiding cases like this: https://github.com/rust-lang/rust/pull/53873#issuecomment-419440395

nikomatsakis (Sep 10 2018 at 13:42, on Zulip):

ok so I wrote up a bunch of tests

nikomatsakis (Sep 10 2018 at 13:42, on Zulip):

I pushed them

nikomatsakis (Sep 10 2018 at 13:42, on Zulip):

there are two that worry me (both have a FIXME in the file)

pnkfelix (Sep 10 2018 at 13:43, on Zulip):

/me looks

nikomatsakis (Sep 10 2018 at 13:44, on Zulip):

one is the one I already showed

fn variable_no_initializer() {
    // FIXME: It is unclear to me whether this should be an error or not.

    let x = 22;
    let y: &'static u32;
    y = &x;
}
nikomatsakis (Sep 10 2018 at 13:44, on Zulip):

the other is this one

fn static_to_a_to_static_through_tuple<'a>(x: &'a u32) -> &'static u32 {
    // FIXME: The fact that this type-checks is perhaps surprising.
    // What happens is that the right-hand side is constrained to have
    // type `&'a u32`, which is possible, because it has type
    // `&'static u32`. The variable `y` is then forced to have type
    // `&'static u32`, but it is constrained only by the right-hand
    // side, not the ascribed type, and hence it passes.

    let (y, _z): (&'a u32, u32) = (&22, 44);
    y
}
nikomatsakis (Sep 10 2018 at 13:44, on Zulip):

it's probably worth me explaining a bit what I did in this PR

nikomatsakis (Sep 10 2018 at 13:44, on Zulip):

that last test exposes the "gap" — I think I've come to the conclusion that to enforce type constraints,

nikomatsakis (Sep 10 2018 at 13:45, on Zulip):

we have to do two things:

pnkfelix (Sep 10 2018 at 13:45, on Zulip):

and if you made the fn variable_no_initializer returns &'static u32

nikomatsakis (Sep 10 2018 at 13:45, on Zulip):
pnkfelix (Sep 10 2018 at 13:45, on Zulip):

and then have it return y

pnkfelix (Sep 10 2018 at 13:45, on Zulip):

I assume that would error

nikomatsakis (Sep 10 2018 at 13:45, on Zulip):

yes, one hopes :)

nikomatsakis (Sep 10 2018 at 13:45, on Zulip):

but yes, it will

nikomatsakis (Sep 10 2018 at 13:46, on Zulip):

the fact that we don't do this is why that second test passes

pnkfelix (Sep 10 2018 at 13:47, on Zulip):

can we discuss the first test a bit more before we move on to the second?

pnkfelix (Sep 10 2018 at 13:48, on Zulip):

... or do you see them as intrinsically linked?

nikomatsakis (Sep 10 2018 at 13:48, on Zulip):

yep

nikomatsakis (Sep 10 2018 at 13:49, on Zulip):

I don't think they are really linked

pnkfelix (Sep 10 2018 at 13:49, on Zulip):

poor timing on my followup Q

pnkfelix (Sep 10 2018 at 13:49, on Zulip):

okay

pnkfelix (Sep 10 2018 at 13:49, on Zulip):

that's what I thought

nikomatsakis (Sep 10 2018 at 13:49, on Zulip):

there is a link

nikomatsakis (Sep 10 2018 at 13:49, on Zulip):

but we could make the first test pass today by special-casing the simple pattern of x

nikomatsakis (Sep 10 2018 at 13:49, on Zulip):

but if we want let (x, y): (&'static u32, &'static u32); to propagate, we need to handle the pattern thing

nikomatsakis (Sep 10 2018 at 13:49, on Zulip):

so that is the link

nikomatsakis (Sep 10 2018 at 13:50, on Zulip):

so, I think I agree with your intution btw

nikomatsakis (Sep 10 2018 at 13:50, on Zulip):

that we do want an error here

nikomatsakis (Sep 10 2018 at 13:50, on Zulip):

that said, I don't know how to think about this in more complex cases, but actually the current solver isn't that smart anyway

pnkfelix (Sep 10 2018 at 13:50, on Zulip):

wait, "first test" is fn variable_no_initializer ?

nikomatsakis (Sep 10 2018 at 13:50, on Zulip):

polonius will bring this question more to the fore

nikomatsakis (Sep 10 2018 at 13:50, on Zulip):

wait, "first test" is fn variable_no_initializer ?

yes

pnkfelix (Sep 10 2018 at 13:50, on Zulip):

hmm. and you're saying the fix is some sort of special case on... the let x = ... ?

pnkfelix (Sep 10 2018 at 13:50, on Zulip):

not on our treatment of assignments?

nikomatsakis (Sep 10 2018 at 13:51, on Zulip):

that is correct

nikomatsakis (Sep 10 2018 at 13:51, on Zulip):

well

nikomatsakis (Sep 10 2018 at 13:51, on Zulip):

you could do various things

nikomatsakis (Sep 10 2018 at 13:52, on Zulip):

however, in the current solver, if we had let x: T; impose constraints on the regions in typeof(x)

nikomatsakis (Sep 10 2018 at 13:52, on Zulip):

those constraints would apply throughout the function

nikomatsakis (Sep 10 2018 at 13:52, on Zulip):

and in particular they would affect subsequent constraints

pnkfelix (Sep 10 2018 at 13:52, on Zulip):

wait wait

pnkfelix (Sep 10 2018 at 13:52, on Zulip):

I think

nikomatsakis (Sep 10 2018 at 13:52, on Zulip):

this is because our current solver is not (yet) location sensitive; this would not be true for polonius

pnkfelix (Sep 10 2018 at 13:52, on Zulip):

you are writing let x: T

pnkfelix (Sep 10 2018 at 13:52, on Zulip):

and the test says let x = ...

nikomatsakis (Sep 10 2018 at 13:52, on Zulip):

it does not

pnkfelix (Sep 10 2018 at 13:52, on Zulip):

so when you say "special case simple patterns"

pnkfelix (Sep 10 2018 at 13:53, on Zulip):

I am literally talking about the text

nikomatsakis (Sep 10 2018 at 13:53, on Zulip):

well

nikomatsakis (Sep 10 2018 at 13:53, on Zulip):

in the test, the variable is called y

pnkfelix (Sep 10 2018 at 13:53, on Zulip):

let x = ...; let y: &'static u32;

pnkfelix (Sep 10 2018 at 13:53, on Zulip):

this was in fact the source of my confusion

pnkfelix (Sep 10 2018 at 13:53, on Zulip):

as to why the "fix" would be to let x = ...;;

nikomatsakis (Sep 10 2018 at 13:53, on Zulip):

I see, I see

nikomatsakis (Sep 10 2018 at 13:53, on Zulip):

sorry, my bad

pnkfelix (Sep 10 2018 at 13:54, on Zulip):

okay now I think I am on a similar page to you, if not the same one

nikomatsakis (Sep 10 2018 at 13:54, on Zulip):

in any case, the point remains that if we had let y: &'static u32; impose a constraint on typeof(y) at that point

nikomatsakis (Sep 10 2018 at 13:54, on Zulip):

it would propagate down below

pnkfelix (Sep 10 2018 at 13:54, on Zulip):

We can special case let x: T; and also let x: T = ...

nikomatsakis (Sep 10 2018 at 13:54, on Zulip):

(in fact, maybe I'll handle that special case right now, just because ...)

pnkfelix (Sep 10 2018 at 13:54, on Zulip):

and have it constrain occurrences of x in the function body, including on the RHS of assignments

nikomatsakis (Sep 10 2018 at 13:54, on Zulip):

I sort of wish that let non-binding-pattern; were not even legal

nikomatsakis (Sep 10 2018 at 13:54, on Zulip):

but oh well :P

pnkfelix (Sep 10 2018 at 13:55, on Zulip):

Oh let non_binding_pattern; is so great though!

pnkfelix (Sep 10 2018 at 13:55, on Zulip):

:)

nikomatsakis (Sep 10 2018 at 13:55, on Zulip):

well

nikomatsakis (Sep 10 2018 at 13:55, on Zulip):

what I meant really is

nikomatsakis (Sep 10 2018 at 13:55, on Zulip):

I wish that it were only legal for variables and maybe tuples

pnkfelix (Sep 10 2018 at 13:55, on Zulip):

ah

nikomatsakis (Sep 10 2018 at 13:55, on Zulip):

stuff like

let Single { y }: Single<&'static u32>;
nikomatsakis (Sep 10 2018 at 13:55, on Zulip):

is just weird

pnkfelix (Sep 10 2018 at 13:55, on Zulip):

yes okay

nikomatsakis (Sep 10 2018 at 13:55, on Zulip):

but annoying for us to handle

nikomatsakis (Sep 10 2018 at 13:55, on Zulip):

I wonder if it is ever done

pnkfelix (Sep 10 2018 at 13:55, on Zulip):

that is goofy, I agree about that

pnkfelix (Sep 10 2018 at 13:56, on Zulip):

maybe we can kill it

nikomatsakis (Sep 10 2018 at 13:56, on Zulip):

that's what I am wondering :)

pnkfelix (Sep 10 2018 at 13:56, on Zulip):

in Rust 2021

nikomatsakis (Sep 10 2018 at 13:56, on Zulip):

or Rust 2018 :)

pnkfelix (Sep 10 2018 at 13:56, on Zulip):

you are optimistic

pnkfelix (Sep 10 2018 at 13:56, on Zulip):

but you are also the one in charge. :)

nikomatsakis (Sep 10 2018 at 13:56, on Zulip):

heh yes I know

pnkfelix (Sep 10 2018 at 13:56, on Zulip):

"All hands on deck!"

nikomatsakis (Sep 10 2018 at 13:56, on Zulip):

I would be curious if there is even a single crates.io crate that uses it

nikomatsakis (Sep 10 2018 at 13:56, on Zulip):

hard to grep for

nikomatsakis (Sep 10 2018 at 13:57, on Zulip):

anyway

nikomatsakis (Sep 10 2018 at 13:57, on Zulip):

we could make let x: T and even let (a, b, c): (T1, T2, T3) work with relative ease I think...

nikomatsakis (Sep 10 2018 at 13:57, on Zulip):

the rest is just sort of annoying to code, but not "undoable"

pnkfelix (Sep 10 2018 at 13:58, on Zulip):

fixing let x: T; and let x: T = ...; would make me pretty happy.

pnkfelix (Sep 10 2018 at 13:58, on Zulip):

the tuple cases probably do need to be done too

pnkfelix (Sep 10 2018 at 13:58, on Zulip):

the rest... eh, just emit a warning

pnkfelix (Sep 10 2018 at 13:58, on Zulip):

"Your lifetimes here are not respected."

nikomatsakis (Sep 10 2018 at 13:58, on Zulip):

I agree it's plausible

nikomatsakis (Sep 10 2018 at 13:58, on Zulip):

this is why I was wondering if we could even kill it somehow

nikomatsakis (Sep 10 2018 at 13:58, on Zulip):

anyway, let's solve the rest

nikomatsakis (Sep 10 2018 at 13:59, on Zulip):

let me see, I bet I can fix let x: T pretty easily

nikomatsakis (Sep 10 2018 at 13:59, on Zulip):

tuples I would prefer to defer to another PR

pnkfelix (Sep 10 2018 at 13:59, on Zulip):

so okay, that's the first case you described

pnkfelix (Sep 10 2018 at 13:59, on Zulip):

and I'm totally fine with deferring tuples

pnkfelix (Sep 10 2018 at 14:00, on Zulip):

since those are a case of the kind of propagation you describe for the "second case"

nikomatsakis (Sep 10 2018 at 14:00, on Zulip):

(I think that would also be something that could be readily mentored — tuples I mean)

nikomatsakis (Sep 10 2018 at 14:00, on Zulip):

so, the second case...

nikomatsakis (Sep 10 2018 at 14:00, on Zulip):

I guess plausibly the same treatment could be done

nikomatsakis (Sep 10 2018 at 14:00, on Zulip):

that is, we could probably solve the 80-20 for both cases by saying that we:

pnkfelix (Sep 10 2018 at 14:00, on Zulip):

so one thing I want to double check about the semantics here

nikomatsakis (Sep 10 2018 at 14:00, on Zulip):

"down-propagate" the ascribed type to the bindings for variables + tuples

nikomatsakis (Sep 10 2018 at 14:01, on Zulip):

(whether or not there is an initializer)

pnkfelix (Sep 10 2018 at 14:01, on Zulip):

let x = E: T; will now not be synonymous with let x: T = E;, right?

pnkfelix (Sep 10 2018 at 14:01, on Zulip):

(because the first case will not constraint all occurrences of x to have the type T)

nikomatsakis (Sep 10 2018 at 14:01, on Zulip):

not quite

nikomatsakis (Sep 10 2018 at 14:01, on Zulip):

it isn't today, either

nikomatsakis (Sep 10 2018 at 14:01, on Zulip):

I wouldn't think

pnkfelix (Sep 10 2018 at 14:01, on Zulip):

oh is that right?

pnkfelix (Sep 10 2018 at 14:02, on Zulip):

okay I shouldn't be surprised

nikomatsakis (Sep 10 2018 at 14:02, on Zulip):

e.g. with let mut

nikomatsakis (Sep 10 2018 at 14:02, on Zulip):

the type T in the first case only applies to E

pnkfelix (Sep 10 2018 at 14:02, on Zulip):

when you say "today"

pnkfelix (Sep 10 2018 at 14:03, on Zulip):

are you talking about AST-borrowck too?

pnkfelix (Sep 10 2018 at 14:03, on Zulip):

or just NLL?

nikomatsakis (Sep 10 2018 at 14:03, on Zulip):

I mean "as implemented, using AST borrowck"

pnkfelix (Sep 10 2018 at 14:03, on Zulip):

I guess I'm still surprised.

nikomatsakis (Sep 10 2018 at 14:03, on Zulip):

(iirc type ascription is usable with a feature gate?)

nikomatsakis (Sep 10 2018 at 14:03, on Zulip):

well e.g. I would expect:

let mut x: &'static u32 = &22;
let y = 44;
x = &y;

to error

pnkfelix (Sep 10 2018 at 14:03, on Zulip):

oh of course

pnkfelix (Sep 10 2018 at 14:04, on Zulip):

subtyping

pnkfelix (Sep 10 2018 at 14:04, on Zulip):

/me smacks head

nikomatsakis (Sep 10 2018 at 14:04, on Zulip):

but I don't expect

let mut x = &22: &'static u32;
let y = 44;
x = &y;

to error

nikomatsakis (Sep 10 2018 at 14:04, on Zulip):

you can probably write the same example with as...

nikomatsakis (Sep 10 2018 at 14:05, on Zulip):

ok so, I think now that if I do the "simple fix" for "down-propagating" pattern types into variable types

nikomatsakis (Sep 10 2018 at 14:05, on Zulip):

it will fix both my examples

nikomatsakis (Sep 10 2018 at 14:05, on Zulip):

it won't fix examples that use more complex patterns

nikomatsakis (Sep 10 2018 at 14:06, on Zulip):

e.g., structs etc

nikomatsakis (Sep 10 2018 at 14:06, on Zulip):

so in a way I guess my two examples -- today -- are the same problem

pnkfelix (Sep 10 2018 at 14:06, on Zulip):

okay so I think it sounds like we've resolved the questions you had, in terms of next steps. I'm happy to summarize this conversation on the PR if you like, as a way of answering the Q(s) you posed in your last comment there.

nikomatsakis (Sep 10 2018 at 14:06, on Zulip):

but I think that with polonius there is a distinct factor of where to enforce the subtyping constraint (this is indeed why I originally introduced Locations::All, but i'd like to remove that, but that's a problem for tomorrow)

nikomatsakis (Sep 10 2018 at 14:06, on Zulip):

sounds good

nikomatsakis (Sep 10 2018 at 14:07, on Zulip):

I think I can whip up that commit quickly

pnkfelix (Sep 10 2018 at 14:14, on Zulip):

so in a way I guess my two examples -- today -- are the same problem

I suppose they are "the same", although the first case is something where we want the type annotation to constrain all assignments to y, while the second case is something where we want the type-checker to continue using the (more constrained/conservative) declared type for y when checking the uses of y. Does that sound right?

pnkfelix (Sep 10 2018 at 14:15, on Zulip):

the words "constrained/conservative" are a bit goofy here

pnkfelix (Sep 10 2018 at 14:16, on Zulip):

its "constrained" in the sense that &'a u32 is a more limited type (when compared to &'static u32) for using y

nikomatsakis (Sep 10 2018 at 14:17, on Zulip):

(I actually have an idea how to implement the more complex patterns now, but I think it's best to leave for follow-up)

nikomatsakis (Sep 10 2018 at 14:18, on Zulip):

I suppose they are "the same", although the first case is something where we want the type annotation to constrain all assignments to y, while the second case is something where we want the type-checker to continue using the (more constrained/conservative) declared type for y when checking the uses of y. Does that sound right?

yes, I think that the second case has more to do with setting an upper bound on the type -- that is, in the example, it cannot go "up" to the super type &'static u32

nikomatsakis (Sep 10 2018 at 14:18, on Zulip):

note that I use == constraints when propagating the ascribed type down to the bindings

nikomatsakis (Sep 10 2018 at 14:23, on Zulip):

@pnkfelix hmm, a thought: given that we both agree that when the user ascribes a type to a variable, it should apply to all assignments/uses to that variable, maybe I should store the user_ty for variables in the LocalDefn

nikomatsakis (Sep 10 2018 at 14:24, on Zulip):

that is, I was modifying the code so that

let x: T;

would generate a statement, but instead I can store T in the local definition of x, and enforce it that way in the type checker

nikomatsakis (Sep 10 2018 at 14:24, on Zulip):

cool

nikomatsakis (Sep 10 2018 at 14:59, on Zulip):

@pnkfelix ok I made that change and pushed: indeed, things now work so long as you don't use more complex patterns

nikomatsakis (Sep 10 2018 at 14:59, on Zulip):

I realize incidentally that I think we are also not handling normalization correctly, but I want to address that in a follow-up too

nikomatsakis (Sep 10 2018 at 14:59, on Zulip):

er, I wonder what I meant by this " Fix the WF rule bug"

pnkfelix (Sep 10 2018 at 14:59, on Zulip):

heh. "Uh oh'

nikomatsakis (Sep 10 2018 at 15:00, on Zulip):

oh, I remember what I meant

nikomatsakis (Sep 10 2018 at 15:00, on Zulip):

hmm maybe I'll file a follow-up for that, too

nikomatsakis (Sep 10 2018 at 15:00, on Zulip):

it's sort of a corner case

nikomatsakis (Sep 10 2018 at 15:01, on Zulip):

we are vulnerable, I think, to #41677

nikomatsakis (Sep 10 2018 at 15:01, on Zulip):

but I'd like to make a test case

nikomatsakis (Sep 10 2018 at 15:01, on Zulip):

ok, well, my battery is out of power, so I will stop here for now :)

nikomatsakis (Sep 10 2018 at 15:01, on Zulip):

let me see if I have enough power to file a follow-up issue

nikomatsakis (Sep 10 2018 at 15:03, on Zulip):

@pnkfelix do you want to review the last few commits?

nikomatsakis (Sep 10 2018 at 15:03, on Zulip):

if so, the PR is ready

nikomatsakis (Sep 10 2018 at 15:03, on Zulip):

/me has to go, bbl

pnkfelix (Sep 10 2018 at 15:04, on Zulip):

great will do

nikomatsakis (Sep 10 2018 at 20:02, on Zulip):

@pnkfelix so I wrote up my idea for how to do the remaining bits without duplicating a ton of code; though we do still duplicate some, in that we have to work out the logic to map from patterns to places. Maybe though we can share that with MIR builder too.

nikomatsakis (Sep 10 2018 at 20:02, on Zulip):

This seems like something potentially mentorable

Keith Yeung (Sep 10 2018 at 20:15, on Zulip):

Hmm, I think I have an idea of what you just wrote

Keith Yeung (Sep 10 2018 at 20:15, on Zulip):

If this does become mentorable, I'd be happy to pick it up

nikomatsakis (Sep 10 2018 at 20:18, on Zulip):

I guess the existing PR has to land first

nikomatsakis (Sep 10 2018 at 20:18, on Zulip):

there are also a few other "unchecked boxes" to look into too

pnkfelix (Sep 11 2018 at 12:09, on Zulip):

oh wow the "series of projection elements -- basically, the path that leads from the type that was given to the type of the binding" actually sounds very much like something I was going to suggest

pnkfelix (Sep 11 2018 at 12:10, on Zulip):

namely, I kept thinking about the work I've read on Zippers and "The Derivative of a Type is the Type of its One-Hole Contexts"

pnkfelix (Sep 11 2018 at 12:13, on Zulip):

though now that I try to spell that out, a path from the given type down to the type of the binding isn't exactly the same as a One-Hole Context

pnkfelix (Sep 11 2018 at 12:14, on Zulip):

Still it definitely sounds like a promising direction

Last update: Nov 21 2019 at 13:15UTC