The problem with union types for exceptions is that it becomes impossible to return an error as the correct case, or at least there is no way to discriminate an

The problem with union types for exceptions is that it becomes impossible to return an error as the correct case, or at least there is no way to discriminate any more. Functions that deal with errors also need to be able to have exceptional situations, and in many cases there are completely generic functions as well that can error out for generic reasons. A basic example is the elementary case of having a list of errors for some reason and indexing out of bounds producing an error, what if one have a list of values, which are all derived from itself accessing lists, each of which contains “Ok:Val+Err:OutOfBounds”, accessing that list itself now becomes indeterminate. The other issue is that the language needs to have support for union types rather than merely sum types. And there's a good reason almost no statically typed language has support for union types since it removes provability and it's not something that can in easily be statically decided, requiring dynamic type tags, but then again, that's what sum types effectively are as well. Typed Racket is statically typed and has union types, but it's an extra layer on top of a dynamically typed language, so the type tags where there already, but it's not easy to erase type data at run time not to implement. In your example of “String|Error”, it essentially requires that every String is now tagged at runtime with tag information about it in practice.