[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.