Stream: t-compiler

Topic: issue #54401 - HRTB in impls unsoundness


Ariel Ben-Yehuda (Sep 25 2018 at 16:31, on Zulip):

Hi @nikomatsakis
So I read your comments about https://github.com/rust-lang/rust/issues/54302 and https://github.com/rust-lang/rust/issues/54302

Ariel Ben-Yehuda (Sep 25 2018 at 16:31, on Zulip):

I'm trying to think whether we should do a perf run

nikomatsakis (Sep 25 2018 at 16:33, on Zulip):

seems fine to do so

Ariel Ben-Yehuda (Sep 25 2018 at 16:34, on Zulip):

yea

Ariel Ben-Yehuda (Sep 25 2018 at 16:34, on Zulip):

I'm not sure how hard will be doing evaluation "correctly"

Ariel Ben-Yehuda (Sep 25 2018 at 16:35, on Zulip):

given that higher-ranked lifetimes can't come with where-clauses on them

nikomatsakis (Sep 25 2018 at 16:36, on Zulip):

I'm not sure how hard will be doing evaluation "correctly"

I'm not sure what you mean by correctly here

Ariel Ben-Yehuda (Sep 25 2018 at 16:36, on Zulip):

I mean, handling lifetimes in trait evaluations

Ariel Ben-Yehuda (Sep 25 2018 at 16:36, on Zulip):

because you only need to handle escaping regions

Ariel Ben-Yehuda (Sep 25 2018 at 16:36, on Zulip):

so you know that 'a: 'b can only hold if either 'a = 'b or 'a is an infer variable

nikomatsakis (Sep 25 2018 at 16:36, on Zulip):

(re: HR lifetimes, my assumption was that we would use an "implied bounds" sort of setup, for backwards compatibility)

nikomatsakis (Sep 25 2018 at 16:37, on Zulip):

(but that's a bit further down the line)

Ariel Ben-Yehuda (Sep 25 2018 at 16:37, on Zulip):

I don't think we do implied bounds today

Ariel Ben-Yehuda (Sep 25 2018 at 16:37, on Zulip):

but we also don't check WF today

Ariel Ben-Yehuda (Sep 25 2018 at 16:37, on Zulip):

so it equals out

nikomatsakis (Sep 25 2018 at 16:37, on Zulip):

right now we just ignore things involving HR regions until you actually instantiate them

nikomatsakis (Sep 25 2018 at 16:37, on Zulip):

right

Ariel Ben-Yehuda (Sep 25 2018 at 16:37, on Zulip):

I mean, of course you want implied bounds for WF

Ariel Ben-Yehuda (Sep 25 2018 at 16:37, on Zulip):

*for non-WF

Ariel Ben-Yehuda (Sep 25 2018 at 16:38, on Zulip):

I mean, you definitely want some sort of implied bounds for WF itself

Ariel Ben-Yehuda (Sep 25 2018 at 16:38, on Zulip):

but today a for<'a> Foo<'a>: Bar means forall<'a> Implemented(Foo<'a>: Bar) modulo bugs

Ariel Ben-Yehuda (Sep 25 2018 at 16:38, on Zulip):

with no extra predicates in the environment

Ariel Ben-Yehuda (Sep 25 2018 at 16:39, on Zulip):

(in a where clause)

nikomatsakis (Sep 25 2018 at 16:40, on Zulip):

I was just looking at roughly this topic in the context of the universe PR, realizing that we have to refactor how the region-obligations are being returned, in particular to handle the case where you are returning a relation to a placeholder region in some fresh universe

nikomatsakis (Sep 25 2018 at 16:40, on Zulip):

in the "older style", where the param-env carried the universe, I was capturing the param-env with the region obligations, and that was ok

nikomatsakis (Sep 25 2018 at 16:41, on Zulip):

but in the newer style, where the "current universe" lives in the inference context and we try to normalize, that doesn't work as well, you need to map to fresh universes

Ariel Ben-Yehuda (Sep 25 2018 at 16:41, on Zulip):

returning a relation?

nikomatsakis (Sep 25 2018 at 16:42, on Zulip):

i.e., when you do trait solving, you get back a series of region constraints you have to solve; these may involve placeholders in new universes, in the case of for<..> binders

nikomatsakis (Sep 25 2018 at 16:43, on Zulip):

placeholder being the term I am trying to adopt in lieu of 'skolemized', given that that term is confusing and used in different ways by different folks

Ariel Ben-Yehuda (Sep 25 2018 at 16:43, on Zulip):

don't you solve constraints from other universes eagerly?

nikomatsakis (Sep 25 2018 at 16:43, on Zulip):

not for regions, no

nikomatsakis (Sep 25 2018 at 16:44, on Zulip):

at least i'm hoping we can avoid it

nikomatsakis (Sep 25 2018 at 16:44, on Zulip):

though it might make some things easier, and might plausibly be needed for backwards compat

Ariel Ben-Yehuda (Sep 25 2018 at 16:45, on Zulip):

so that means that Eval(String: DeserializeOwned) is a compilation error rather than false?

nikomatsakis (Sep 25 2018 at 16:46, on Zulip):

if we avoided solving eagerly, then it would be a "ok" result but with region constraints that give an error when you try to solve them

nikomatsakis (Sep 25 2018 at 16:46, on Zulip):

this has a uniformity that appeals to me; I'm trying to think what my other reason was

Ariel Ben-Yehuda (Sep 25 2018 at 16:46, on Zulip):

yea, exactly what I'll call a "compilation error rather than false"

Ariel Ben-Yehuda (Sep 25 2018 at 16:46, on Zulip):

because I suppose it means that !(String: DeserializeOwned) is not Ok either?

Ariel Ben-Yehuda (Sep 25 2018 at 16:47, on Zulip):

in any modality?

nikomatsakis (Sep 25 2018 at 16:47, on Zulip):

sounds correct

Ariel Ben-Yehuda (Sep 25 2018 at 16:48, on Zulip):

btw, my RefFoo example was supposed to just have no regions in its problem predicate

Ariel Ben-Yehuda (Sep 25 2018 at 16:48, on Zulip):

so that you can't talk about any funkiness with that region

Ariel Ben-Yehuda (Sep 25 2018 at 16:49, on Zulip):

I just find that resolving a predicate with no inference variables returning things that do have inference variables to be confusing

nikomatsakis (Sep 25 2018 at 16:49, on Zulip):

I think one of my other concerns was that if we had to solve region constraints eagerly — well, that's complex, because you can have things like for<'a> { if ('a: 'b, 'b: 'a) { 'a = 'b } } and that should be true. So, at minimum, the setup that we use now for propagating universes wouldn't be right. (I'd like to try and implement a more careful solver for these kinds of scenarios, though, but I've not thought particularly hard about it.)

Ariel Ben-Yehuda (Sep 25 2018 at 16:49, on Zulip):

I remember that we didn't want to have negative reasoning on region equality

Ariel Ben-Yehuda (Sep 25 2018 at 16:49, on Zulip):

because of it being a back-compat/"stability" hazard

nikomatsakis (Sep 25 2018 at 16:50, on Zulip):

btw, my RefFoo example was supposed to just have no regions in its problem predicate

you mean this example?

trait RefFoo {
    fn ref_foo(&self) -> &'static u32;
}

impl<T> RefFoo for T where for<'a> &'a T: Foo {
    fn ref_foo(&self) -> &'static u32 {
        self.foo()
    }
}

how would the predicate be changed then?

Ariel Ben-Yehuda (Sep 25 2018 at 16:50, on Zulip):

I mean, in my example the "problem predicate" is <u32 as RefFoo>

Ariel Ben-Yehuda (Sep 25 2018 at 16:50, on Zulip):

which contains no lifetimes, but with "lazy outlives normalization" its normalization will suddenly contain inference variables

Ariel Ben-Yehuda (Sep 25 2018 at 16:51, on Zulip):

my mental model is that if your type is 'static, then you are in classical logic land and all trait questions have clear yes/no answers

nikomatsakis (Sep 25 2018 at 16:51, on Zulip):

I just find that resolving a predicate with no inference variables returning things that do have inference variables to be confusing

when you say "that do have inference variables", you are referring to the "placeholders" we have to create?

e.g., when we solve for<'a> 'a: 'static, this gets translated to a '!1: 'static sort of thing (where !1 is a placeholder) this was confused

nikomatsakis (Sep 25 2018 at 16:52, on Zulip):

oh maybe I see what you mean, sorry

nikomatsakis (Sep 25 2018 at 16:52, on Zulip):

you're saying, the impl that we apply?

Ariel Ben-Yehuda (Sep 25 2018 at 16:53, on Zulip):

when you say "that do have inference variables", you are referring to the "placeholders" we have to create?

can't you get constraints that have existentials in them?

nikomatsakis (Sep 25 2018 at 16:53, on Zulip):

I'm trying to think if you can

Ariel Ben-Yehuda (Sep 25 2018 at 16:53, on Zulip):

I think that RFC 447 won't let you

nikomatsakis (Sep 25 2018 at 16:53, on Zulip):

I think the answer is technically yes, but they would be constrained to be equal to placeholders

Ariel Ben-Yehuda (Sep 25 2018 at 16:54, on Zulip):

because it exactly forces things to equal to placeholders

Ariel Ben-Yehuda (Sep 25 2018 at 16:54, on Zulip):

*all inference variables

nikomatsakis (Sep 25 2018 at 16:54, on Zulip):

(and hence could conceivably be normalized)

nikomatsakis (Sep 25 2018 at 16:54, on Zulip):

chalk does handle unification on inference variables, in part to simplify the output

Ariel Ben-Yehuda (Sep 25 2018 at 16:55, on Zulip):

I think that in the current rustc, with no where-clauses on higher-universe placeholders

Ariel Ben-Yehuda (Sep 25 2018 at 16:55, on Zulip):

you never need to return placeholders

nikomatsakis (Sep 25 2018 at 16:55, on Zulip):

e.g. in this example, you would have for<'a> &'a T: Foo, this creates a placeholder !1 and then applies the impl. Applying the impl creates an existential ?0 that is equated with !1.

Ariel Ben-Yehuda (Sep 25 2018 at 16:55, on Zulip):

@nikomatsakis yea exactly, and then you equate ?0 = !1, and RFC 447 means you can always do it

nikomatsakis (Sep 25 2018 at 16:55, on Zulip):

you never need to return placeholders

well wouldn't that require us to eagerly solve the constriants?

Ariel Ben-Yehuda (Sep 25 2018 at 16:55, on Zulip):

yea, exactly

Ariel Ben-Yehuda (Sep 25 2018 at 16:56, on Zulip):

I don't think that with the current trait checker there are any obstructions to eagerly solving constraints

nikomatsakis (Sep 25 2018 at 16:56, on Zulip):

ok

Ariel Ben-Yehuda (Sep 25 2018 at 16:56, on Zulip):

because there are no where-clauses

nikomatsakis (Sep 25 2018 at 16:56, on Zulip):

sounds correct

nikomatsakis (Sep 25 2018 at 16:56, on Zulip):

(but we do want where clauses to close the soundness hole around contravariance)

Ariel Ben-Yehuda (Sep 25 2018 at 16:57, on Zulip):

will they be where clauses around HRTBs?

nikomatsakis (Sep 25 2018 at 16:57, on Zulip):

I guess those could be separated

nikomatsakis (Sep 25 2018 at 16:57, on Zulip):

I hadn't considered doing so

Ariel Ben-Yehuda (Sep 25 2018 at 16:57, on Zulip):

I mean, obviously we do have where clauses today, e.g. in trait impls

nikomatsakis (Sep 25 2018 at 16:58, on Zulip):

right but not on HRTB's

nikomatsakis (Sep 25 2018 at 16:58, on Zulip):

which I think is the relevant thing?

nikomatsakis (Sep 25 2018 at 16:58, on Zulip):

well

Ariel Ben-Yehuda (Sep 25 2018 at 16:59, on Zulip):

yea. I think that having HRTBs with where-clauses is a strictly "needs research" thing

nikomatsakis (Sep 25 2018 at 16:59, on Zulip):

(obviously the regions on impls can play a "placeholder" role, so there's a sort of asymmetry, I guess that's the point you were making?)

nikomatsakis (Sep 25 2018 at 16:59, on Zulip):

(e.g. when WF checking the impl or something)

Ariel Ben-Yehuda (Sep 25 2018 at 16:59, on Zulip):

I guess that's the point you were making?

Ariel Ben-Yehuda (Sep 25 2018 at 16:59, on Zulip):

when?

Ariel Ben-Yehuda (Sep 25 2018 at 17:00, on Zulip):

"higher-universe placeholders" - sure

Ariel Ben-Yehuda (Sep 25 2018 at 17:00, on Zulip):

only the "0 universe" can have where-clauses in it ATM

Ariel Ben-Yehuda (Sep 25 2018 at 17:03, on Zulip):

if you have eager unification universe code in a close-to-landing state, I'm for having #54401 use it

nikomatsakis (Sep 25 2018 at 17:05, on Zulip):

hmm, I might be able to make it resolve eagerly.

Ariel Ben-Yehuda (Sep 25 2018 at 17:05, on Zulip):

of course, if there is no perf impact, and there are no plans for having eager resolve ever, it might be ok to r+ this

Ariel Ben-Yehuda (Sep 25 2018 at 17:05, on Zulip):

but I remember that this cache was added to avoid severe perf issues with futures-based code, which definitely has lifetimes

Ariel Ben-Yehuda (Sep 25 2018 at 17:11, on Zulip):

I think the code even almost DTRT today

Ariel Ben-Yehuda (Sep 25 2018 at 17:11, on Zulip):

given that I get

Ariel Ben-Yehuda (Sep 25 2018 at 17:11, on Zulip):

EVAL(Binder(<&ReLateBound(DebruijnIndex(0), BrNamed(crate0:DefIndex(1:12), 'a)) u32 as Foo>))

Ariel Ben-Yehuda (Sep 25 2018 at 17:12, on Zulip):

so it's making the query with an HRTB

Ariel Ben-Yehuda (Sep 25 2018 at 17:16, on Zulip):

ah that because impl_or_trait_obligations does a plug_leaks

Ariel Ben-Yehuda (Sep 25 2018 at 17:17, on Zulip):

so maybe we just need to copy the fulfill HRTB obligation logic to select, and everything will work

Ariel Ben-Yehuda (Sep 25 2018 at 17:17, on Zulip):

(tm)

Ariel Ben-Yehuda (Sep 25 2018 at 17:17, on Zulip):

*the fulfill Outlives obligation logic

Ariel Ben-Yehuda (Sep 25 2018 at 21:22, on Zulip):

BTW, I actually think that evaluation is closer to being a Chalkifiable solver than selection, and that it just intentionally ignores region requirements to have better cacheability properties.

Ariel Ben-Yehuda (Sep 25 2018 at 21:23, on Zulip):

*closer to being a Chalkifiable solver than fulfillment

Ariel Ben-Yehuda (Sep 25 2018 at 21:23, on Zulip):

which is sort of a "perf hack" to handle incremental obligation resolution that goes in parallel with inference.

Ariel Ben-Yehuda (Sep 25 2018 at 21:25, on Zulip):

but sure, they are basically "independent" trait solving engines

Ariel Ben-Yehuda (Sep 25 2018 at 21:26, on Zulip):

(not quite independent, because fulfillment calls evaluation during winnowing)

nikomatsakis (Sep 26 2018 at 17:19, on Zulip):

@Ariel Ben-Yehuda so, that PR doesn't seem to regress perf in particular. I think i'd like to land it and then move on with "universe stuff" independently (I'm pushing on my branch some more, though I'm not (yet) doing eager errors — I want to get the lazy errors version working first, since that's the approach I was taking, and then see how I have to adapt it)

Ariel Ben-Yehuda (Sep 27 2018 at 19:19, on Zulip):

I am trying to investigate what it takes to make evaluation correct, and it seems to be as easy as I thought it is

Ariel Ben-Yehuda (Sep 27 2018 at 19:19, on Zulip):

I don't think it requires any universe stuff, because of how fulfillment works

nikomatsakis (Sep 27 2018 at 19:20, on Zulip):

what do you mean by correct?

Ariel Ben-Yehuda (Sep 27 2018 at 19:20, on Zulip):

to make it handle things the same way fulfillment does

nikomatsakis (Sep 27 2018 at 19:20, on Zulip):

are you planning to propagate back a set of region requirements?

Ariel Ben-Yehuda (Sep 27 2018 at 19:20, on Zulip):

you don't need to

Ariel Ben-Yehuda (Sep 27 2018 at 19:21, on Zulip):

it does most of the things for you anyway with plug_leaks

nikomatsakis (Sep 27 2018 at 19:21, on Zulip):

I guess you're saying: because we only care about this for global predicates?

Ariel Ben-Yehuda (Sep 27 2018 at 19:21, on Zulip):

for "staticized" predicates

Ariel Ben-Yehuda (Sep 27 2018 at 19:21, on Zulip):

yea

Ariel Ben-Yehuda (Sep 27 2018 at 19:21, on Zulip):

as in, where all "inference/free" regions are 'static

Ariel Ben-Yehuda (Sep 27 2018 at 19:21, on Zulip):

but evaluation always works staticized

Ariel Ben-Yehuda (Sep 27 2018 at 19:22, on Zulip):

and I think that "classical logic" queries will be staticized for quite some time

nikomatsakis (Sep 27 2018 at 19:22, on Zulip):

as in, where all "inference/free" regions are 'static

I believe this is the condition that is_global checks for, no?

Ariel Ben-Yehuda (Sep 27 2018 at 19:22, on Zulip):

@nikomatsakis

Ariel Ben-Yehuda (Sep 27 2018 at 19:22, on Zulip):

Well you can run evaluation even if your type contains 'a, it will just treat the 'a as though it was 'static

Ariel Ben-Yehuda (Sep 27 2018 at 19:22, on Zulip):

(and typeck does that quite a lot of times)

nikomatsakis (Sep 27 2018 at 19:23, on Zulip):

yes, I know, but we don't use that to skip fulfill cx work

nikomatsakis (Sep 27 2018 at 19:23, on Zulip):

put another way: I think it would still be a bug if we did, if I understand what you are saying

Ariel Ben-Yehuda (Sep 27 2018 at 19:23, on Zulip):

put another way: I think it would still be a bug if we did, if I understand what you are saying

sure, but trait matching etc. does use evaluation, so there's no reason for it to be semi-randomly incorrect

Ariel Ben-Yehuda (Sep 27 2018 at 19:24, on Zulip):

actually, thinking about it, we might want to return EvaluatedToOk in "intercrate context"

Ariel Ben-Yehuda (Sep 27 2018 at 19:24, on Zulip):

to not allow for extra coherence power

nikomatsakis (Sep 27 2018 at 19:24, on Zulip):

I don't see how it can be otherwise if you plan to ignore region obligations?

nikomatsakis (Sep 27 2018 at 19:24, on Zulip):

I still don't understand I guess what def'n of incorrect you are using

Ariel Ben-Yehuda (Sep 27 2018 at 19:25, on Zulip):

I mean, trait evaluation should return the correct answer for the staticized version of the query you ask it

Ariel Ben-Yehuda (Sep 27 2018 at 19:25, on Zulip):

if you ask it about &'a Foo: Bar, it should answer the correct answer for &'static Foo: Bar

Ariel Ben-Yehuda (Sep 27 2018 at 19:25, on Zulip):

for global types, staticize(T) = T, so you can just do evaluation

nikomatsakis (Sep 27 2018 at 19:26, on Zulip):

ok

nikomatsakis (Sep 27 2018 at 19:26, on Zulip):

seems reasonable

Ariel Ben-Yehuda (Sep 27 2018 at 19:29, on Zulip):

so I think I have it working

Ariel Ben-Yehuda (Sep 27 2018 at 19:29, on Zulip):

now I'll just try to check it a little to see it solves all the problems

Ariel Ben-Yehuda (Oct 01 2018 at 19:41, on Zulip):

Could you review this + https://github.com/rust-lang/rust/pull/54701 ? The latter is beta-nominated

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

@Ariel Ben-Yehuda yep

Ariel Ben-Yehuda (Oct 01 2018 at 21:46, on Zulip):

and what's the status of my PR for #54401? (#54624)?

Ariel Ben-Yehuda (Oct 01 2018 at 21:46, on Zulip):

is it waiting for something?

nikomatsakis (Oct 02 2018 at 13:43, on Zulip):

no, I think it's probably good to go, just didn't get to it when doing reviews yesterday I guess. I'll review latest status today

Last update: Nov 21 2019 at 13:35UTC