Splitting unions in subtype checks

I’ve been looking at how type checkers solve subtype constraints lately. This post describes an interesting case that does not seem to be widely discussed, and may be useful to other type checker authors. Throughout the post I’ll write X <: Y to denote “X is a subtype of Y”, and I’ll only be talking about fully static types. The problem The typing spec currently takes a set-theoretic interpretation of types: it treats a type as a set of values, and subtyping as the subset relation (concepts). ...