Stream: t-compiler/wg-polonius

Topic: issue 58053 in polonius


Aaron Weiss (Feb 19 2020 at 16:40, on Zulip):

Hey folks,

Sorry if this isn't quite the right place to ask, but I've been going through the nll test suite and I'm curious about how issue 58053 would go through Polonius. Does this still error? It seems a bit odd to me that the type checker doesn't figure out that the origin of the result is the same as the origin of the argument.

I have a playground link here: https://play.rust-lang.org/?version=nightly&mode=debug&edition=2018&gist=8f967ccd6b534b992ea48ff9a4f451c2

lqd (Feb 19 2020 at 17:34, on Zulip):

I think it would error similarly, it was my impression that properly handling closures would require higher-rankedness via chalk, but Niko/Matthew would probably know better than me :)

lqd (Feb 19 2020 at 17:42, on Zulip):

(similarly, extracting f to a function would make it compile under today's NLL)

lqd (Feb 19 2020 at 18:06, on Zulip):

(and I believe this should be solved when higher-ranked lifetimes on closures are supported, like https://github.com/rust-lang/rust/issues/55526 or https://github.com/rust-lang/rust/issues/58052)

Aaron Weiss (Feb 19 2020 at 18:30, on Zulip):

@lqd so, if I'm understanding correctly, the issue is basically that f and g should have a type like fn<'a>(&'a i32) -> &'a i32, but are instead getting some type without the quantification?

Aaron Weiss (Feb 19 2020 at 18:31, on Zulip):

it's a little weird because I've encountered other scenarios like that, and in Oxide, annotating them with local (rather than polymorphic) provenances leads to the same behavior as Rust, but in this case, I get different behavior (Oxide seems to admit the program even with local provenances).

Aaron Weiss (Feb 19 2020 at 18:32, on Zulip):

If f and g are indeed getting not-quantified lifetimes/provenances/origins, then I'll have to figure out why I'm not producing the same error in that case.

lqd (Feb 19 2020 at 19:12, on Zulip):

Unfortunately I’m not sure of the specifics (there was also another case where quantification was short circuited as ‘static) but for the NLL case maybe @pnkfelix could help you there for instance

nikomatsakis (Feb 25 2020 at 20:15, on Zulip):

@Aaron Weiss the tl;dr is that this is outside of polonius

nikomatsakis (Feb 25 2020 at 20:16, on Zulip):

at least at present, the compiler determines the signatures of functions like that in its initial phases of type inference

nikomatsakis (Feb 25 2020 at 20:16, on Zulip):

and polonius (and NLL checker, etc) comes later and is just given that signature

nikomatsakis (Feb 25 2020 at 20:16, on Zulip):

now, it is true that we could probably do better

nikomatsakis (Feb 25 2020 at 20:17, on Zulip):

and I'm a bit surprised that that test case doesn't work, though I remember now that @pnkfelix and I were talking about this at some point and I had forgotten about it

nikomatsakis (Feb 25 2020 at 20:17, on Zulip):

we don't support a kind of "fully explicit" way of annotating the types on closures, which is kind of annoying

Aaron Weiss (Feb 25 2020 at 21:37, on Zulip):

@nikomatsakis I figured that it was related to inference, but I can't figure out an annotated version of the program that I can explain why it produces an error in terms of how Oxide works (or how Polonius seems to work).

Aaron Weiss (Feb 25 2020 at 21:37, on Zulip):

I tried to annotate it like so:

fn main() {
    let tmp: i32 = 3;
    let i: &'t0 i32 = &tmp;

    let f: fn(&'f1 i32) -> &'f2 i32 = |x: &'f1 i32| -> &'f2 i32 { x };
    //~^ ERROR lifetime may not live long enough
    let j: &'t0 i32 = f(i);

    let g: fn(&'x1 i32) -> &'x2 i32 = |x: &'x1 i32| { x };
    //~^ ERROR lifetime may not live long enough
    let k: &'t0 i32 = g(i);
}
Aaron Weiss (Feb 25 2020 at 21:38, on Zulip):

But from my perspective, since these lifetime variables are local to the scope we're in, it's fine to equate them (by flowing loans from e.g. 'f1 into 'f2).

Aaron Weiss (Feb 25 2020 at 21:39, on Zulip):

Is this because there's some other more syntactic check that actually happens here _before_ getting into the borrow checker (regardless of its implementation)?

Aaron Weiss (Feb 25 2020 at 21:39, on Zulip):

If so, what is that syntactic check doing exactly?

Aaron Weiss (Feb 25 2020 at 21:41, on Zulip):

(also, please forgive my abuse-of-notation that is using unboxed function types for closures)

nikomatsakis (Mar 03 2020 at 20:09, on Zulip):

yeah, a solid question @Aaron Weiss -- I have to go look -- I remember when I was last looking at this question that it seemed to be inferring a type like fn(&'a) -> &'b, which wouldn't really be legal to type even

Jake Goulding (Mar 05 2020 at 19:17, on Zulip):

we don't support a kind of "fully explicit" way of annotating the types on closures, which is kind of annoying

Can you use the trick of accepting and returning the closure?

fn restrict(f: F)
where
    F: Fn(/* All the specifics you need */)
{
    f
}

fn usage() {
    let f = restrict(|| /* ... */);
}
lqd (Mar 05 2020 at 22:08, on Zulip):

yeah that should work here

Last update: Apr 03 2020 at 17:45UTC