Stream: wg-traits

Topic: object safe for dispatch #57545


nikomatsakis (Apr 19 2019 at 17:58, on Zulip):

Hey @scalexm -- I am curious to get your thoughts on something. Have you seen RFC 2027? It proposes a change to the way that dyn Foo types work, summarized here. In short the idea is this:

Today, the type dyn Foo is only legal if the trait Foo is object-safe, and dyn Foo: Foo always holds.

Under this proposal, dyn Foo is always well-formed as a type, but dyn Foo: Foo only holds if Foo is object safe.

nikomatsakis (Apr 19 2019 at 17:58, on Zulip):

One of the things that we've been talking about is the interaction of dyn Foo and implied bounds, and I wanted to bring this to your attention.

scalexm (Apr 19 2019 at 18:00, on Zulip):

@nikomatsakis I’ve read it, and I think I concluded it was impossible to implement it soundly, but I can’t remember how I got to that conclusion

nikomatsakis (Apr 19 2019 at 18:00, on Zulip):

that sounds like a concern :)

nikomatsakis (Apr 19 2019 at 18:00, on Zulip):

I sort of have this nagging feeling too

scalexm (Apr 19 2019 at 18:00, on Zulip):

I think it was (as always) related with the dyn Animal<‘static> thing

nikomatsakis (Apr 19 2019 at 18:00, on Zulip):

Yes, presumably.

scalexm (Apr 19 2019 at 18:02, on Zulip):

I’m in a train right now, basically doing nothing, so I can try to recollect the details

scalexm (Apr 19 2019 at 18:09, on Zulip):

Ok so the setup was:

trait Animal<X>: 'static {}

and how to think about dyn Animal<&'a i32>

scalexm (Apr 19 2019 at 18:10, on Zulip):

If you have that those two things to hold:

Then this is unsound (because of the Projector trick)

scalexm (Apr 19 2019 at 18:11, on Zulip):

So under the RFC, the first point must be always true, so we must ensure that the second point does not hold

scalexm (Apr 19 2019 at 18:11, on Zulip):

And I don’t know how to do that

scalexm (Apr 19 2019 at 18:12, on Zulip):

So probably I did not actually get to a firm conclusion « this is impossible to implement it soundly », more like « I don’t know how to make it sound » :)

scalexm (Apr 19 2019 at 18:13, on Zulip):

Especially under the model I described for trait objects to fix the above soundness problem, the RFC could not work as dyn Animal<&'a i32> would not be considered well formed

nikomatsakis (Apr 19 2019 at 18:20, on Zulip):

This reminds me, @scalexm, that I think it'd be a good idea for us to try and do some "design presentations" on implied bounds. Basically spelling out how the current lowering works and what its effects are, to try and make sure people understand it. (And then, as a capstone, we could dive into the trait object questions.)

nikomatsakis (Apr 19 2019 at 18:20, on Zulip):

I would like to make a kind of list of "complex questions to tackle" around traits

nikomatsakis (Apr 19 2019 at 18:20, on Zulip):

So far we said that on monday we'll start digging into the built-in bounds problem, starting by explaining the SLG solve etc

nikomatsakis (Apr 19 2019 at 18:20, on Zulip):

Which seems good -- and I suspect we should just keep our focus there until we feel like we've worked out the things that arise

nikomatsakis (Apr 19 2019 at 18:20, on Zulip):

But maybe then we can turn to implied bounds a bit

nikomatsakis (Apr 19 2019 at 18:20, on Zulip):

So under the RFC, the first point must be always true, so we must ensure that the second point does not hold

it's not entirely clear to me that the first point must be true

nikomatsakis (Apr 19 2019 at 18:21, on Zulip):

i.e., that trait is presumably object safe anyway

nikomatsakis (Apr 19 2019 at 18:21, on Zulip):

(right?)

nikomatsakis (Apr 19 2019 at 18:21, on Zulip):

so it's not clear why this RFC even matters when it comes to this example

scalexm (Apr 19 2019 at 18:22, on Zulip):

I mean, the RFC states that dyn Trait must always be well-formed

scalexm (Apr 19 2019 at 18:23, on Zulip):

So if we want to fix the soundness issue under the RFC, we must ensure that we cannot prove dyn Animal<&'a i32>: Animal<&'a i32>

nikomatsakis (Apr 19 2019 at 18:24, on Zulip):

I mean, the RFC states that dyn Trait must always be well-formed

I'm not clear that it states this, or meant to state this

nikomatsakis (Apr 19 2019 at 18:24, on Zulip):

I'm also not clear on whether this RFC still makes sense

scalexm (Apr 19 2019 at 18:25, on Zulip):

yes maybe it does not say that after all indeed

scalexm (Apr 19 2019 at 18:26, on Zulip):

But at least it is definitely incompatible with the trait objects model I though about; as under that model you somehow had:
WellFormed(dyn Trait) iff dyn Trait: Trait && ObjectSafe(Trait)

scalexm (Apr 19 2019 at 18:27, on Zulip):

The iff was there to make implied bounds work correctly

scalexm (Apr 19 2019 at 18:35, on Zulip):

To put that model I thought of back in cache, the idea was the following:

scalexm (Apr 19 2019 at 18:36, on Zulip):

This all plays nicely with implied bounds (i.e. if you have dyn Trait as an input type you get all the bounds), but the constraint that you need to prove WellFormed(dyn Trait: Trait) to prove WellFormed(dyn Trait) fixes the Animal<&'a i32> issue

nikomatsakis (Apr 19 2019 at 18:37, on Zulip):

For some reason I'm having some trouble following this setup :)

scalexm (Apr 19 2019 at 18:38, on Zulip):

Because in that case proving WellFormed(dyn Animal<&'a i32>: Animal<&'a i32>) would eventually reduce to proving dyn Animal<&'a i32>: 'static which you cannot do

nikomatsakis (Apr 19 2019 at 18:39, on Zulip):

I think I have to remember what you mean by WellFormed(TraitRef) =)

nikomatsakis (Apr 19 2019 at 18:39, on Zulip):

That's..part of it

nikomatsakis (Apr 19 2019 at 18:39, on Zulip):

we never did settle on the best names for these things I think

scalexm (Apr 19 2019 at 18:40, on Zulip):

Yeah WellForme(TraitRef) still means « all the transitive super bounds hold »

scalexm (Apr 19 2019 at 18:40, on Zulip):

Including Implemented(TraitRef) itself

nikomatsakis (Apr 19 2019 at 18:40, on Zulip):

Right, ok. FullyImplemented or something like that

nikomatsakis (Apr 19 2019 at 18:41, on Zulip):

was another name we had kicked about

nikomatsakis (Apr 19 2019 at 18:41, on Zulip):

although I sort of recall thinking we should just call it Implemented and instead have ShallowImplemented for "I found an impl". Anyway.

scalexm (Apr 19 2019 at 18:41, on Zulip):

In the Animal case, the Implemented part is covered by the synthetic impl, however the 'static part is fully syntactic and cannot be proven

scalexm (Apr 19 2019 at 18:41, on Zulip):

Yeah right

nikomatsakis (Apr 19 2019 at 18:41, on Zulip):

I guess for full clarity we can just do FullyImplemented and ShallowImplemented

nikomatsakis (Apr 19 2019 at 18:42, on Zulip):

(or Deeply)

scalexm (Apr 19 2019 at 18:42, on Zulip):

Sounds good indeed

scalexm (Apr 19 2019 at 18:43, on Zulip):

I still have this issue in chalk with a lot of examples: https://github.com/rust-lang/chalk/issues/203

scalexm (Apr 19 2019 at 18:43, on Zulip):

(Regarding trait objects)

scalexm (Apr 19 2019 at 18:44, on Zulip):

To me, that setup is not that different from rustc’s current setup (we do have synthetic impls for all super traits of a trait objet)

nikomatsakis (Apr 19 2019 at 18:44, on Zulip):

In any case, the problem I guess is that where you had

WellFormed(dyn Trait<X>) :- DeeplyImplemented(dyn Trait<X>: Trait<X>) && ObjectSafe(Trait)

we would want to change this to remove the ObjectSafe part, but of course it is really just moving into the DeeplyImplemented(dyn Trait<X>: Trait<X>) predicate, so we would still have that WellFormed(dyn Trait<X>) does not hold.

scalexm (Apr 19 2019 at 18:44, on Zulip):

The new part is the well-formedness rule of a trait object

nikomatsakis (Apr 19 2019 at 18:44, on Zulip):

What we sort of want would be something like WellFormed(dyn Trait<X>) :- "predicates of Trait<X> apply"..maybe?

nikomatsakis (Apr 19 2019 at 18:44, on Zulip):

which might in turn give the error you are looked for?

scalexm (Apr 19 2019 at 18:44, on Zulip):

Yes but under the RFC, DeeplyImplemented(dyn Trait: Trait) would not hold if the trait isn’t object safe

scalexm (Apr 19 2019 at 18:45, on Zulip):

That the whole point of the RFC, I think

nikomatsakis (Apr 19 2019 at 18:45, on Zulip):

Right

nikomatsakis (Apr 19 2019 at 18:45, on Zulip):

But what I'm saying is

scalexm (Apr 19 2019 at 18:45, on Zulip):

Ah

nikomatsakis (Apr 19 2019 at 18:45, on Zulip):

DeeplyImplemented proves:

nikomatsakis (Apr 19 2019 at 18:45, on Zulip):

but in some sense we might just want the second part?

scalexm (Apr 19 2019 at 18:45, on Zulip):

Yes just strict super predicates

scalexm (Apr 19 2019 at 18:45, on Zulip):

Maybe that would work

scalexm (Apr 19 2019 at 18:49, on Zulip):

And in the FromEnv(dyn Trait) reverse rule you would only include the strict super predicates as well

nikomatsakis (Apr 19 2019 at 18:49, on Zulip):

Presumably, right

nikomatsakis (Apr 19 2019 at 18:49, on Zulip):

BTW, I wonder --

nikomatsakis (Apr 19 2019 at 18:50, on Zulip):

One of the challenges we've yet to discuss is extending to dyn (Trait1 + Trait2)

nikomatsakis (Apr 19 2019 at 18:50, on Zulip):

But I wonder if we could think instead about having a general T = T1 && T2 (I'm switching to intersection here, since the + is really "and", nor the "disjoint or" meaning it often has...)

nikomatsakis (Apr 19 2019 at 18:50, on Zulip):

And then have dyn Trait1 && dyn Trait2

nikomatsakis (Apr 19 2019 at 18:50, on Zulip):

Not sure how relevant that is, just occurred to me that it might be in some way easier

nikomatsakis (Apr 19 2019 at 18:51, on Zulip):

i.e., FromEnv(T1 && T2) :- FromEnv(T1); FromEnv(T2). and so forth

nikomatsakis (Apr 19 2019 at 18:51, on Zulip):

basically it wouldn't require us to quantify over "things within types"

scalexm (Apr 19 2019 at 18:51, on Zulip):

Ah I see

scalexm (Apr 19 2019 at 18:52, on Zulip):

Yes I think that would work indeed

scalexm (Apr 19 2019 at 18:55, on Zulip):

Ok so regarding the RFC, just including strict predicates in the rule probably works indeed + moving the ObjectSafe bound to the synthetic impl for the trait itself

scalexm (Apr 19 2019 at 19:09, on Zulip):

@nikomatsakis ok then you’re right the RFC seems doable

nikomatsakis (Apr 19 2019 at 19:11, on Zulip):

good, I guess

nikomatsakis (Apr 19 2019 at 19:11, on Zulip):

bad because it means I have to put more work into reviewing this PR :P

scalexm (Apr 19 2019 at 19:19, on Zulip):

@nikomatsakis lol

scalexm (Apr 19 2019 at 19:19, on Zulip):

I wasn’t expecting to have it implemented before we actually fix trait objects, but I think that shouldn’t hurt

scalexm (Apr 19 2019 at 19:20, on Zulip):

Also we probably won’t be able to stabilize until we do fix trait objects

scalexm (Apr 19 2019 at 19:20, on Zulip):

To be sure there are no bad interactions

nikomatsakis (Apr 19 2019 at 19:24, on Zulip):

So @scalexm, one other thing. For better or worse, this code compiles today:

trait Animal<X>: 'static { }

fn foo<'a>(x: &dyn Animal<&'a u32>) { }

fn main() {
}
scalexm (Apr 19 2019 at 19:25, on Zulip):

Yes that does not surprise me

nikomatsakis (Apr 19 2019 at 19:25, on Zulip):

So it seems like that type cannot be made to be not well-formed

nikomatsakis (Apr 19 2019 at 19:25, on Zulip):

(Unless maybe I didn't quite understand what you were proposing)

scalexm (Apr 19 2019 at 19:26, on Zulip):

Mmh you mean because it would break code?

nikomatsakis (Apr 19 2019 at 19:26, on Zulip):

Yes.

scalexm (Apr 19 2019 at 19:26, on Zulip):

I was expecting to break code anyway

nikomatsakis (Apr 19 2019 at 19:26, on Zulip):

I suppose it could be considered a bug fix

scalexm (Apr 19 2019 at 19:26, on Zulip):

Yes

nikomatsakis (Apr 19 2019 at 19:26, on Zulip):

But there's a real possibility we couldn't get away with that :)

scalexm (Apr 19 2019 at 19:26, on Zulip):

But we should evaluate how big the breakage would be indeed

nikomatsakis (Apr 19 2019 at 19:27, on Zulip):

That said, I'm also not very happy with the outlives rules on trait objects

nikomatsakis (Apr 19 2019 at 19:27, on Zulip):

Which seems related here

nikomatsakis (Apr 19 2019 at 19:27, on Zulip):

Changing them would probably also be a breaking change

nikomatsakis (Apr 19 2019 at 19:28, on Zulip):

(I wonder if it could be done with an edition, actually)

nikomatsakis (Apr 19 2019 at 19:28, on Zulip):

Presumably it could

nikomatsakis (Apr 19 2019 at 19:28, on Zulip):

Changing the outlives rules for fn types (which I would also like to do) cannot be done w/ an edition though

scalexm (Apr 19 2019 at 19:28, on Zulip):

Ah, you mean things like: dyn Trait<&'a i32> + 'static being WF but not actually outliving 'static?

nikomatsakis (Apr 19 2019 at 19:28, on Zulip):

right now they don't outlive 'static but they could

scalexm (Apr 19 2019 at 19:28, on Zulip):

Because that one is an annoying one which I did hit a few times in my code when multiple lifetimes and trait objects come to play

nikomatsakis (Apr 19 2019 at 19:29, on Zulip):

(in some universe)

nikomatsakis (Apr 19 2019 at 19:29, on Zulip):

it's more obvious to see with a type like fn(&'a u32) -- like, there is no region data in there, so in some sense it should be 'static

nikomatsakis (Apr 19 2019 at 19:29, on Zulip):

but the same applies to the X in dyn Trait<X> -- it doesn't necessarily represent closed over data

scalexm (Apr 19 2019 at 19:29, on Zulip):

Yes, but the Projector trick prevents it, unless you say that the arg type is not covered and you cannot implement generic impls for that fn type

scalexm (Apr 19 2019 at 19:29, on Zulip):

Yes I see

scalexm (Apr 19 2019 at 19:31, on Zulip):

It could make things simpler indeed, but this would break a lot of code for sure

scalexm (Apr 19 2019 at 19:32, on Zulip):

Whereas about making dyn Animal<&'a i32> not WF maybe not as much breakage, as this soundness bug has remained hidden for a long time so I don’t think a lot of people rely on it

scalexm (Apr 19 2019 at 19:32, on Zulip):

So yeah maybe for another edition

nikomatsakis (Apr 19 2019 at 19:37, on Zulip):

It could make things simpler indeed, but this would break a lot of code for sure

not entirely clear to me

nikomatsakis (Apr 19 2019 at 19:37, on Zulip):

but maybe :)

nikomatsakis (Apr 19 2019 at 19:38, on Zulip):

we could perhaps do a relatively...tailored rule

nikomatsakis (Apr 19 2019 at 19:38, on Zulip):

e.g., this impl would be legal

impl<T> Foo for fn(T) { }

but this one illegal

impl<T> Foo for fn(T) { type Output = T; }

i.e., a generic type parameter (here, T) cannot appear in the value of an associated type unless it appears in some input type in a suitably constrained position (and fn/trait parameters do not count).

nikomatsakis (Apr 19 2019 at 19:39, on Zulip):

I'm not sure how often that happens.

nikomatsakis (Apr 19 2019 at 19:39, on Zulip):

In the trait case, we could do it with an edition for sure.

nikomatsakis (Apr 19 2019 at 19:39, on Zulip):

Since we could use the older rules for older traits.

nikomatsakis (Apr 19 2019 at 19:39, on Zulip):

Whether we should I don't know, butI think the curent rules are limiting.

scalexm (Apr 19 2019 at 19:40, on Zulip):

Yes ok the assoc type value is the problematic one and is probably less used indeed

nikomatsakis (Apr 19 2019 at 19:40, on Zulip):

It's at least plausible

nikomatsakis (Apr 19 2019 at 19:40, on Zulip):

wish I had thought of that before

nikomatsakis (Apr 19 2019 at 19:40, on Zulip):

I was never very happy with that part of the RFC, but it never occurred to me to make it this tailored.

Last update: Nov 18 2019 at 01:55UTC