Safe code relied upon by unsafe is effectively unsafe

[ia0]

@RalfJung

This is indeed a well-known fact, that perhaps should be documented/communicated better: unsafe code can and does rely on the functional correctness of safe code that it explicitly depends on for soundness.

If anyone wants to read more about this in a semi-formal fashion, there's the unsafe mental model. The particular notion Ralf mentions is tracked by the robust keyword which is the dual of unsafe with respect to variance. This has currently no syntax or convention but still exists and is necessary to prove soundness.