Fergus Henderson <fjh@cs.mu.oz.au> writes: [...]

(2) Allow pattern matching on values of particular types, using `case'. [...] If we allow (2), then some programming mistakes that previously were type errors would instead become just inexhaustive pattern matches for which you get a run-time error.

For example:

foo :: Maybe a -> b -> Maybe b foo x y = case list of [] -> Nothing (x:xs) -> Just x where list = case x of Nothing -> 0 -- oops, meant [] instead of 0 Just foo -> [y]

If union types were allowed, with (2) above, this example would be legal, with `list' having the union type { [a], Integer }.

if you disallow undeclared union types, you'll catch easily this kind of errors.

But `foo Nothing 42' would evaluate to bottom, since the `case list' expression has no case with a pattern of type Integer.

So allowing union types in this way would reduce static type safety, at least unless we also forbid inexhaustive pattern matches.

well allowing inexhaustive pattern matching always leads to less type safetyness, no news :) And of course subtyping also reduce type safetyness. But it is the same for type classes. No one is more safe than using '+' for integers and '+.' for floats...

If instead you only allow (1), then probably union types would not be suitable for expressing the kinds of things that you want to express with them.

sure, you don't win anything.

...

Is there any reason for this restriction in the Haskell type system? Does this lead to losing the principal type property?

If you allow (2) above, there may be serious problems for principal types. For example, consider

f x = case x of Nothing -> False Just _ -> True

What's the most general type for `f'? The type `f :: Maybe a -> Bool' is less general than e.g. `f :: Union { Maybe a, ... } -> Bool', but you certainly don't want to infer the latter type.

not necessarily. If you disallow undeclared union types, the only occurence of Union { Maybe a, ... } will be Maybe a, unless one really wants to extend Maybe... cu Pixel.