Proper union types are really hard if you want to do anything more than check. Once you're into inference territory, this gets really hard. Look at Haskell's f

Proper union types are really hard if you want to do anything more than check. Once you're into inference territory, this gets really hard. Look at Haskell's faux union Either. It should be true that Either a a = a but of course, it isn't and you always have to destructure this. In inference it's easier to just infer one most general type instead of a (possibly infinite) number of sets of types. Basicaly wherever types are ambiguous, you'd need to try all alternatives and possibly compile all of them. Faux unions are also underused but we do find them from time to time.