Expanding a bit on what niko and ralf said (thanks for the detailed description of the proof work, ralf), I think the best solution in the long term is to support explicit statements that a type does not and will not implement a trait, and then add the relevant statements for all the pointer types. This would allow ralf's coherence based reasoning without basing anything on coherence - for each type that doesn't implement DerefMut or Clone, they can point to the specific line of code that guarantees the type does not implement that trait.
There are reasons to support this feature unrelated to pin (in fact my first big RFC was proposing this back in 2015(!!)), but we don't have to go as far as changing coherence reasoning just yet.
Someone with more knowledge of coherence internals needs to review this, but I think we just need to make this change to the language: today, with the optin_builtin_traits feature turned on, you can add negative impls but only of auto traits. We need to remove the restriction to auto traits, and allow negative impls of all traits when that feature is turned on (so not on stable yet). Then, in std, we add these impls:
impl<'a, T: ?Sized> !DerefMut for &'a T { }
impl<'a, T: ?Sized> !Clone for &'a mut T { }
impl<T: ?Sized> !DerefMut for Rc<T> { }
impl<T: ?Sized> !DerefMut for Arc<T> { }
This would completely close the fundamental based hole and allow Ralf's team to prove the correctness of the pin APIs with no reliance on the orphan rules, without any change to the APIs themselves. Tada!
It also provides a path toward better supporting users who want to do the kind of coherence based reasoning that has run pin afoul. Users who want to reason about types not implementing traits will eventually have support for explicitly stating that the type does not implement that trait, which they are required to do if they want to create a provably safe abstraction based on that fact (which is resistant to any changes to the orphan rules).
This leaves only the problem with CoerceUnsized, which we didn't talk about today. tl;dr: I think we should just make coerceunsized an unsafe trait. There's a larger discussion about how its a distinct problem and justifies this different solution, but let's focus on the other problem for now.