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"
&Timpl we are worried about. - Something we could stabilize, where
!Traitimpls are allowed but have no effect on anything else. - (Maybe) Something we could stabilize, where
!Traitimpls 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: !Traitdeclarations 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.)
