Comment by obastani

This breaks down because it's not easy to statically reason about when a variable is a NonZeroNumber. For example, what is the type signature for subtraction of two NonZeroNumbers? You can't guarantee that it isn't zero, so it has to be a Number. Thus, you can't divide by the difference. You could use a more powerful type system to reason about these kinds of constraints, but then type checking quickly becomes undecidable (or at least very, very expensive).