> I said why does it even matter not why can't you do it

I've explained why it matters - the types are more precise in my version and if you start from that you can always throw away the extra precision if desired to get to your version. You can't go in the other direction, so starting from your version makes it impossible to safely recover an Int from the returned type of Optional[Int], even if you've already established the precondtion beforehand.

> There is 100% casting in your version

Creating an Optional[Int] from an Int is a conversion, not a cast. I thought it was obvious from the context but for the avoidance of any doubt, by 'casting' I mean an unsafe narrowing conversion. Optional[Int] is a larger type than Int, so it's trivial to create one from an Int:

    def pure(x: Int): Optional[Int] = Just(x)

you clearly can't safely go in the other direction, whether using pattern matching or otherwise. If you disagree, just complete the following definition:

    def fromOptional(o: Optional[Int]): Int =
        match o with
        | Some(i) => i
        | Nothing => ...

eventually you need to provide a default value for the case of no value.

> Imagine a map with RGB colors as keys.

Your example doesn't make sense, what would you expect (lookup Map.empty Red) to return? The optional return value is used to represent the key being missing in the map. Nonetheless the point I was making is that you wouldn't return Nothing from such a function in the event of a precondition failure e.g.

    def lookup(m: Map[K, V], v: K): Optional[V] =
        if m is None return Nothing
        ...

you would instead throw an exception if the input map is null and force the caller to handle it. The majority of static type systems are not powerful enough to encode arbitrary properties about values, so you have to decide which ones to check dynamically and which statically. Checking preconditions dynamically is reasonable if encodng them in the type system is too cumbersome.

> This prior point involves the creation of the type NonZero[Int] which involves: NonZero.fromInt

No, this is not necessarily the only way to create instances of NonZero. You could have a PosNat subtype with members one: PosNat and succ: PosNat -> PosNat. You could have a non-empty list type with a length member.

> Every other mathematical operation (+,-,x^y,/,) returns an Int not a NonZero[Int]

They don't return Optional[Int] either so I don't see how this is relevant. There's no reason the input has to come from some application of a different operator, it could come from configuration, user input, a property from some other type etc. The question is whether and how to model the constraints in the type. The constraint exists in the argument so it makes sense to constrain the input type, not widen the output.

> Notice how the above two sentences are the same?

Yes, if all you want to do is avoid establishing the property you care about and silently propagate some information-free 'failure' value to the top level, then you can do it either way. But the entire point of encoding properties in the types is to force you to establish them. These statements highlight the difference:

1. I've established the divisor is non-zero, called myDiv, received an Int and continue

2. I've established the divisor is non-zero, discarded that information to call yourDiv, recieved an Optional[Int] which cannot be empty, but which must be propagated. You could immediately unwrap the value but now you're just re-creating the dynamic behaviour of a function (Int, Int) -> Int which you've already rejected.