Well unreachable! and case! are not mutually exclusive, they serve different needs. Stuff like unreachable! and the benefits you found in it can and should wait. The pluggable type checker should come first. Though it’s also true that, as you said, unreachable! could complement the type checker if implemented in concert with it (i.e. issue warnings for places should [not] be unreachable, which is valuable when trying to catch non-exhaustiveness bugs).
Absolutely. I witnessed something very similar many years ago when people were very happliy doing catch (Exception e) { ... } in Java. And that achieved only one thing – it masked bugs. That made the code much harder to troubleshoot. We don’t need that in Elixir at runtime. We need something we can opt in to if we want to, and having (or lacking) stuff like case! should not be a compile-time error – so yeah, let’s not do overly defensive programming. We lose a core and very strong benefit of using a BEAM VM language.
Well if the new type checker can be instructed to exempt certain classes of warnings or just particular locations as Credo does, then that pokemon clause becomes completely unnecessary. You’ll get exactly the same behavior if you never write it + opt out of the exhaustiveness check on this one place where you don’t want to deal with it.
…Unless I keep misunderstanding the ever-expanding scope of this discussion 
.
EXACTLY. I believe you are the one who best summarized it so far, thank you!
IMO it should retain the current runtime behavior but issue a warning when ran against the new type checker. It should still compile and run as before and blow up if anything other except an :ok tuple is returned.
EXACTLY x2. IMO the goal is to try and introduce exhaustiveness check warnings for whoever wants to opt in to them and leave everything else the same for (a) those who will use Dialyzer and not the new type checker and (b) at runtime.
I remember because I quietly lol’d to myself at the time.