That's cute, but no. There's a lot of code that only gets executed once in a blue moon and if my experience[1] is anything to go by, this is where types really shine. (Before you say "tests": The amount of code bases I've experienced in dynamically checked languages with no meaningful test coverage is shocking. That, and tests can only show the presence of bugs.)
Types are also hugely valuable as compiler-checked API documentation, especially if side effects can be document as in e.g. Haskell or Idris.
(I'm obviously assuming non-trivial type inference as in e.g. Haskell or O'Caml. If we're talking anemic type systems like Java or C#, then the trade-off becomes a lot harder to justify, at least for me. In these cases you can indeed remove a non-trivial amount of "ceremonial" code and the type systems indeed have very few useful guarantees like non-nullness and such.)
[1] We're all trading anecdotes here, let's be honest about that.
I wrote about this in another comment, in the context of writing tests.
Or the property 'this variable is never used after a free' in a language with manual memory management (Rust encodes this) or 'this program is free from data races' (also Rust)?
No one is arguing that strong static type systems make it impossible to write programs with bugs, but eliminating whole classes of bugs at compile time certainly makes it easier.
That's a big problem, indeed, if your goal is to ship code that was never executed.