So static type system are conservative. If variable v is supposed to have type T and the compiler cannot deduce that it for sure is then a type error is generat

So static type system are conservative. If variable v is supposed to have type T and the compiler cannot deduce that it for sure is then a type error is generated. Hence you need option types because static type systems are not powerful enough to deduce whether a given nullable variable actually can be null or not. In effect, the compiler throws its hands in the air and says "Nope too hard, you do it for me." So the programmer has to insert runtime checks in the form of pattern matching clauses for option types even when it is trivial for a human to prove that a reference won't ever be null. The compiler admits defeat and instead forces the programmer to use runtime type checking. It's mostly the same with nominative NonEmpty types. Any value the programmer has instantiated with one of NonEmpty's type constructors have type NonEmpty - everything else don't. For sure, you could create a NonEmpty class in Java too, but it would still be up to the programmer to enforce the type's semantic during program execution. If the variable L has type NonEmpty (list) then it's bloody obvious to a programmer that the expression pop(push(push(L, x), y)) also has type NonEmpty. To a compiler figuring that one out is mostly impossible.