Sorry for the confusion, but regardless of whether you call it casting, conversion, or something else, it's still trivial to do safely in one directly and impossible to do safely in the other. Given your fixation on the terminology I assume you've now accepted this.

> But via an optional type you guarantee that it's handled

It's not 'handled', which is the point. There's no default value so you have no option but to propagate the missing value. Callers that establish the precondition still have to deal with an Optional value even though it can't be empty. Callers which establish the precondtion through the types receive a more precise type and don't have this problem. Callers that establish the precondition in the more simply-typed version (Int, Int) -> Int also receive an Int. Only your version imposes the imprecision on the return type.

> There is nothing wrong with using a Maybe monad here. There is zero reason why you need to throw an exception.

The Optional[Value] returned from a map lookup is used to incidicate the possibility of a missing key, which is an expected outcome of the operation itself. Passing a null map represents a structural error in the construction of the program at the point the call is made. If you represent both in the same type you can't distinguish these two cases.

> You now have a hole in subtraction as 3 - 3 would be a singularity.

There's no hole here, subtraction on NonZero just has to return Int instead.

> If it comes from IO anything goes, you have to be prepared for Anything

Yes, if it comes from user input you have to establish the property dynamically. Encoding the property in the argument type forces you to actually do it (whether statically or dynamically), and help you push the constraint to the highest level. Putting the optionality in the return type doesn't force you do do this, and imposes a cost on every call that actually does.