Is this only a problem if you have partial compilation/a shared library? Because, sure, at the call site you could assume that String: Magic is true, but as soon as that impl gets typechecked, that gets rejected, and thus, your program will too. So surely the bad example under heading The catch: how do we decide the impl is invalid can’t occur?

score 1 · canonical