Explicit negative impls to fix `Pin` soundness hole

language design
8

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