We may be speaking past each other somewhat. I certainly agree with you that losing let it crash semantics would be a Bad Thing. Where I either disagree or am misunderstanding you is in the bits that follow:
… by replacing it with lots of unnecessary checking code to keep the compiler happy throughout the code base and community libraries adopting bad defensive coding idioms and still have essentially the same runtime behaviour
How would the proposed ???/unreadable! make anything worse than the status quo? (Keeping in mind that the discussion here is on introducing a gradual type checker gradually, and these various proposals are just thought experiments on how best to support new capabilities that the type checker might give us while respecting existing code and idioms.)
Current behavior: I write a case that checks the things I expect. If something I don’t expect is passed in, it blows up.
Hypothetical type checking behavior: I write a case inside a function with a type signature that fully defines the set of inputs, so nothing changes and I only handle the things I expect. OR I write a case that is dealing with unbounded input of some kind (maybe dynamic()), and so I throw a _ -> ??? in there to indicate that I don’t expect that to happen, but if it does, just blow up.
What I’m missing is the way in which the above at all “encourages bad practices” or is “defensive programming.”
