It's also worth noting semantically what the type of `subtract` reads as. It says that for any two NonNegative typed values you can produce a new value in the type `Maybe NonNegative` which is the type of NonNegatives adjoined with one special "failure" value.

So this is a perfectly well-defined notion of subtraction on non-negative numbers. It reflects the obvious fact that NonNegatives are not closed under subtraction.