You can really make that type do a compile-time check on runtime values?

It would be better to have some way of getting the compiler to optimize constraints, perhaps by proving at compile time that the error is impossible.