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.