Why 'externalized' proofs of cyclic trait impls does not work

This explains two approaches to handling supertraits in a Rust-like type system: modular proofs, where each impl must itself establish any declared supertraits, versus external proofs, where users of an impl must re-verify those supertrait obligations. Using trait Magic: Copy as an example, a modular regime would reject impl Magic for String because String does not implement Copy, and would allow the rest of the program to rely on impls to infer Copy from Magic. An external scheme would only permit a shallow claim (e.g., Shallow(Magic: String)) that forces callers to re-prove the supertraits and is analogous to requiring every caller to inspect a callee’s body instead of trusting its signature.

External proofs are incompatible with how unsafe traits are handled, because unsafe impls are precisely the places where the impl is trusted to discharge safety obligations. An invalid unsafe impl, such as asserting Nullable for Box when that’s false, would produce unsoundness if callers could coerce values based on an external-only guarantee. That inconsistency shows impls must be responsible for both ordinary supertrait obligations and unsafe conditions. The clear consequence is to adopt modular (coinductive) proofs for cyclic trait impls so impls themselves validate the full set of obligations; a concrete coinductive approach is proposed to follow.