As noted by masklinn, the compiler will complain about the non-exhaustive match. Stuff like this makes me want a dependently typed language for practical programming, in which I can express the concept of "this case ought to be impossible", and convince the compiler by supplying a proof. Also, this would eliminate the false dichotomy between "fast, unchecked, unsafe array indexing" and "slow, checked, safe array indexing", which would be a huge win for safe systems programming.