[ufo]

While this is technically correct (the best kind of correct) it also trivializes the argument and somewhat misses the point. For example, in a dynamic language all the values are belong to a single type and carry a tag at runtime to identify their category. Static languages also do that but on more restricted scope - you aren't allowed to accidentally mix strings and integers in Haskell but you can accidentally mix empty/non-empty lists (getting a runtime exception on `head`) or zero/nonzero numbers (breaking division). You can sort of fix this if you go up to dependent types but then the type system gets much more complicated and its not always easy to statically create the proofs for everything so you start to see the appeal of dynamically checking some of the stuff.

[chongli]

Haskell but you can accidentally mix empty/non-empty lists (getting a runtime exception on `head`) or zero/nonzero numbers (breaking division).

This is due to Haskell's support for partial functions. It does induce some weakness in the type system but it brings the benefit of making the language Turing-complete. As for these specific examples, they would be solved if the libraries in question were rewritten.

[ufo]

The problem is that you might be forced to add dependent types to the language to be able to safely define some of those partial functions. This is not a trivial matter since dependent type systems are even more complicated and might demand extra work (proofs) from the programmer.

IMO, there are situations where you are better off doing trivial runtime checks instead of trying to write complex proofs that might themselves contain bugs and that are tightly coupled to your current implementation and choice of datastructures.