This is a local violation of the invariants. It is not something that happens due to the code in another trait as I had shown in my proof of unsafety.
In my category of delineating the boundary of safety, I want to be able to say that if I violate the invariants locally, then that is unsafe because it is a human observable bug.
Whereas, the proof example I showed upthread, the trait NatPos did not violate its invariants. It required coercion to a Nat with a shared mutable reference in order to violate the invariants of `Pos'. That was a non-local unsafety, thus although a bug, I'd like to have the compiler make it impossible. And so I described the optional rule for making it impossible. Whether that optional rule has any practical implementation is a separate question.