Explicit negative impls to fix `Pin` soundness hole

So, in the Unsoundness in `Pin` thread, we seem to have settled on the "best fix" being that we add the ability to explicitly declare that &T does not implement DerefMut. This might look something like this:

impl<T: ?Sized> !DerefMut for &T { }

As @withoutboats noted, the compiler today supports "negative impls" of this kind for use with auto traits. They are still unstable and some aspects of their implementation were never fully "worked out" -- for example, we currently (I believe) basically just ignore all where clauses on them and so forth.

I'm wondering "how much" we want to be specifying these features. There are a few "levels" to such a feature:

  • Something good enough to land on nightly that prevents the "evil" &T impl we are worried about.
  • Something we could stabilize, where !Trait impls are allowed but have no effect on anything else.
  • (Maybe) Something we could stabilize, where !Trait impls are allowed, and coherence takes them into account (e.g., so downstream crates can rely that the trait will never be implemented).
  • (Maybe) permitting T: !Trait declarations as where clauses.

I am not sure how far we will want to go, but I think at least the first three bullets. In particular, I would like for us to be able to do things like:

impl<T> !Copy for Box<T> { }

which in turn would mean you could do things like:

trait MyTrait { }
impl<T: Copy> MyTrait for T { }
impl<T> MyTrait for Box<T> { }

Supporting this will require defining, for the purpose of the coherence solver, what it means for things to not be implemented.

This then brings us to the 4th bullet (negative where clauses). In general, I do not think we want to introduce negative reasoning like T: !Trait where this simply means "there is no impl for T". This kind of negative reasoning is both fragile and also ups the complexity of our trait solver significantly (nested negative goals are bad). But if we have explicit negative impls, it is plausible that such a where clause could exist, where it has the meaning "there is an explicit negative impl that matches". In this case, the !MyTrait is almost a kind of "shadow trait" so to speak.

Still, it'll require some more thought to flesh out the proposal, and there are some design questions that arise. For example, I'd prefer I think to deprecate the ability to write impls that make negative assumptions about local types, in preference of having people writing explicit negative impls. Similarly, I'd want to spell out a bit more how things work with respect to auto traits.

I guess I don't want this thread to necessarily go too far down the design specifics -- at least not yet -- but I'd like to answer the question of "how much of this design we feel we need to do and when".

My inclination, I think, is that we should immediately prototype a way to bar the "evil" DerefMut impl with minimal implications for stable code. Then we can assess how far down the rest of the design path to go -- we don't necessarily have to do it now, though it'd be good to start sketching out what a coherent overall design looks like around traits. (I'd like to be doing that in the wg-traits repository, probably, though till now the focus there has been on implementation questions primarily.)

14 Likes

Thoughts on point 4:

I think that the idea of a Shadow Trait for where clauses would be more useful then negative reasoning, unless someone wants to be able to do for T: X + !Y and for T: !X + Y

Having where T: !Trait mean something other than "Trait is not implemented", even if it's "Trait is explicitly never going to be implemented", is dangerous for the obviousness of code.

Consider impl<T: Trait> A for T {} and impl<T: !Trait> A for T {}. This very much looks like it would be equivant to impl<T> A for T {}, but it isn't.


Another potential point to consider is if negative trait impls can (should?) be used for sealed traits. This would be a negative impl for all types except for some subset of known types.

On top of this, how does this interact with specialization? Can we default impl !Trait for T? Can we impl !Trait for a type with a default impl?

3 Likes

I think this is fine. The worst that can happen is some code doesn't compile, which is fine. This is the price to pay in order to make !Trait tractable.

Also, in Rust we like to make interfaces super explicit and making !Trait mean never implemented seems to fit that philosophy.

This is interesting, but I think sealed traits should be it's own thing (it may use the same machinery inside the compile, but that's an implementation detail).

!Trait wouldn't have any items, so specialization doesn't make sense. overlapping_marker_traits would give enough flexabliity, since !Trait is equivielent to a marker trait.

As I wrote before, I don't want to get too far into the details in this thread, at least not right now -- however, I don't think this would be very complicated to specify. The basic idea is that negative impls cannot overlap with positive impls. (I suppose you could allow negative impls to overlap with one another, although I think the code currently does not.)

This implies then that you cannot have a positive impl like impl<T> Trait for T get "specialized" by a negative impl impl !Trait for u32, that is simply an error. As for default impl !Trait, I think this has no particular sensible meaning and would not be allowed.

The way I think of it is that it's a question of what each impl fixes (that is, guarantees to be true in a way that cannot be changed by other impls):

  • default impl Foo for T fixes nothing, it just supplies default values.
  • impl Foo for T { ... } fixes that T: Foo is true
    • for each non-default item within, we fix that the value of that item for T: Foo is as specified
    • default items are not fixed, and can be specialized
  • impl !Foo for T { }, therefore, fixes that T: !Foo is true (or, similarly, that T: Foo is false)
1 Like

Initial prototype implementation PR posted

Some context: https://github.com/rust-lang/rfcs/pull/1148 (reading through this is a bit cringe for me lol)

I agree with Niko that we'd like to define up to point 3, and also that we can do this incrementally: start with point 1 today before troubling with points 2/3. Though I somewhat thing we'd want to tackle 2/3 together (that is, figure out the coherence changes before stabilizing the syntax).

For the 4th bullet, the main reason I think to have such a negative bound (with the meaning, as niko said, that there is an explicit negative impl) would be to declare explicitly mutually exclusive traits, as discussed in RFC proposal 1148. However, Niko and I have talked about some alternative syntax for this feature, like something more directly analogous to a product type. I think this can be treated as an extension beyond the 3rd bullet though and we don't have to work it out in detail today.

Recently, in Partial negative reasoning via a False trait I wondered about the benefits of having a False trait impossible of having an implementing type. It is easy to build such trait with negative impls:

trait False {}
impl<T:False> !False for T {}

This False trait can be used to build a positive version of !DerefMut. Instead of

impl<T: ?Sized> !DerefMut for &T { }

being possible to write

trait NotDerefMut {}
impl<T:DerefMut+NotDerefMut> False for T {}
impl<T: ?Sized> NotDerefMut for &T {}

Providing an immediate substitute for !DerefMut bounds:

impl<T:NotDerefMut> Thing for T {}

Thus, even without having explicit T:!Trait bounds, it is possible to make weak versions of them.

2 Likes

I agree that we should not stabilize until we've figured out the coherence changes. Procedurally, I think what I am happy with is:

  • To land #68004, we need to:
    • Document semantics of negative impls as they are today in a write-up
    • fcp merge
  • To stabilize, we need a proper RFC and a "well-rounded" semantics (in particular I would want to integrate with coherence, or come up with a strong reason not to). We do not have to permit T: !Trait explicitly in where-clause form.

What I'm not sure about yet is the urgency of doing this. In general, I am of the mind that I want to be "finishing things" and not starting things half-way. Although it wasn't on our radar, I think that having !Trait impls that coherence can trust would be genuinely useful, and I also suspect we could move fairly quickly on getting an RFC up and so forth.

I guess all I am saying is that -- if we can manage it -- I think it is worth considering trying to push negative impls all the way through to a stable feature. We've got clear motivation, after all (both to enable this sort of reasoning but also to ease some of the limitations of coherence, and as a small step towards finishing up the story on negative reasoning in coherence).

We'd have to figure out who is going to write up the RFC and help shepherd the effort, but I think it's reasonable in scale. I'm almost tempted to do it myself but I think it'd be better if I worked with someone else on it.

3 Likes

I think this just means that the trait solver cannot use excluded middle in the general case... I think that not believing in excluded middle is consistent with Rust's belief that new lemmas can be asserted by downstream crates we don't know about. I don't think this is any harder to reason about than the current coherence/orphan rules.

2 Likes

This is also perfectly consistent with Niko's older posts about using modalities to separate "things that can be relied on here" from "things that can be relied on in downstream crates". Such kind of "quantifying over the future"-style modalities are one of the most common examples of logics that fail to satisfy the excluded middle.

impl<T:False> !False for T {}

What is this? Logically speaking, this defines a predicate False: Type -> Prop satisfying forall T:Type, False(T) -> !False(T). This seems a pretty odd thing to say. This impl is exactly the kind of thing why we have to be careful with negative impls. :wink:

If you want a trait that is demonstrably not implemented for any type, the impl for that would be impl<T> !False for T {}. Coherence will ensure that we can never have both Trait and !Trait implemented for the same type.

3 Likes

Right, the T:False bound is not necessary there, not sure why I included it before. It is common to have something such as forall P, False -> P, which at P=!False becomes False->!False. I guess I have got used to "pretty odd things."

Regarding excluded middle. It seems extremely problematic. With excluded middle, to know if there are an assignment of traits to types becomes propositional satisfiability, with its complexity issues. Also, it could allow for a type to be inferred to "implement" a trait having not given actual implementation. It could have some sense with empty traits. Although even if having a general excluded middle should be avoided, it could be useful to have it for specific traits, but proceeding very carefully.

1 Like

One hopes that the following is illegal:

trait Foo = A + !B;
struct K<T> where T: !Foo { .. }

Or, in general, the lack of excluded middle makes !!Trait deeply questionable, unless we define !!Trait = Trait? I'm not sure I feel like that's the right thing, seeing as we don't have excluded middle?

I think @nakacristo was agreeing with us that having the trait system obey LEM (Law of Excluded Middle) would be a bad thing for many reasons. Though it was kind of hard to tell.

On the broader subject, I have no objections to niko's earlier comment, other than a vague unease at the huge pile of trait-related issues that only seems to keep growing. But maybe all of them are interdependent enough that it was always going to feel that way, and we were always going to have to work through some of this negative reasoning stuff.

Yes, I agree LEM is bad for many reasons. Sorry for being unclear.

Well, !!Trait is questionable both with LEM and without. With LEM some of !Trait or Trait should be true for a given type. Then if !!Trait is true, it means !Trait cannot be. Therefore Trait should be true. But then, if Trait has some method, how it is implemented for the type? Stating !!Trait without giving a normal impl Trait for Thing raises many questions. If we do not have LEM then !!Trait is rather meaningless.

This seems to be getting offtopic, since @nikomatsakis said

I would say that we do not have any hurry to get !!Trait or LEM.

1 Like

I am sympathetic to this, of course. That said, I feel fairly comfortable with this change -- certainly with the immediate step of accepting negative impls. As I said in our recent lang-team meeting, in terms of the code that's implemented today, this is a very small change -- basically just removing the line of code that restricted negative impls to auto traits.

In terms of going forward, e.g. creating interactions with coherence, I think it's important to base this work on Chalk -- in particular, on Chalk's definition of the trait system in terms of a "lowering" to logical predicates. I was thinking that it would be good to write-up the existing work we've done on handling coherence and then try to frame negative impls in that context.

(Chalk's does have a notion of negative goals, expressed not { G }, and we emulate a modal logic, which means you can express "not provable within this crate" and "not provable even in any downstream crate", but I'm not entirely convinced that the current setup is the one we actually want. Still, we need that already to express the coherence rules, since we need to be able to capture the limited negative reasoning that we support.)

2 Likes

(offtopic) I've been reading the thread, and been trying to understand the relationship between Trait, !Trait and ?Trait.
I'm pretty sure that this is not how it works, but is it a possibility that they could mean implements Trait, implements forbid-Trait, never-implements Trait, respectively?
If this were the case, then I think it should also be possible to express ?!Trait, which would mean never-implements forbid-Trait.

Then we wold have 3 possible cases:

  • A: When we impl Trait;
  • B: When we impl !Trait.
    • when we forbid-Trait;
  • Default: When we don't impl Trait nor impl !Trait.
    • when we never implemented Trait nor forbid it.

So we could use 5 different bound conditions to explore those cases:

  • T: Trait for A case.
    • when normal Trait was implemented.
  • T: !Trait for B case.
    • when Trait was forbidden.
  • T: ?Trait for both B and Default case.
    • when have never implemented Trait, so it's for when it was forbidden or when we actually never implemented Trait.
  • T: ?!Trait for both A and Default case.
    • when we have never forbidden Trait, so it's for when we normally implemented Trait or when we actually never forbid it.
  • T: ?Trait + ?!Trait for Default case.
    • when we never implemented a normal Trait, and also never forbid it.

Then, this would be the bound mutual exclusion relationship:

eg. !Trait bound and Trait bound are connected, 
so they must be mutually excluded.
That is, makes no sense to bound into a impl Trait
while also being bound into impl forbid-Trait.

              Default
                /\
               /  \
?!Trait       /    \       ?Trait
   \         /      \        /
    \       /        \      /
     \     /          \    /
     !Trait------------Trait

And this would be the opposite, the pair possibility bound relationship:

eg. !Trait bound and ?Trait bound are connected, 
because they both may relate to the B case, above.

      (B&Def)   (A&Def)    
      ?Trait    ?!Trait
       /  \       /  \
      /    \     /    \
 (B) /      \   /      \ (A)
!Trait     Default     Trait

Not really, because the meaning of T: ?Trait is already well-established: T may or may not implement Trait. This is only ever a meaningful thing to write in the case of T: ?Sized, because all type parameters are assumed by default to implement Sized / have a known compile-time size. The Reference even states that you may not do it for any other trait.

2 Likes

?Trait means we don't know if it implements that trait or not. That is, T: ?Sized means any T, regardless of its relationship to Sized. T: ?Trait is the set of all types.

1 Like

I would phrase it is:

  • T: Trait -- known to implement Trait; this is a semver guarantee
  • T: !Trait -- known to NOT implement Trait; this is a semver guarantee
  • T: ?Trait -- not known whether it implements Trait (the default status); this could change to either T: Trait or T: !Trait in a semver-compatible way

One way that your description is "reasonable" is that figuring out whether T: !Trait would be done in almost the same way as figuring out whether T: Trait -- basically, you look for an impl which applies to T and where the where clauses are satisfied. The different is that it is a negative impl like impl !Trait for T and not a positive impl.

3 Likes