How will you find such violations if opaque comes from so or some ffi, so compiler can't see through? you can't. It's heuristics. Sound type system is much stronger