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). A union T1 | T2 is the union of the two sets (union types).
With those definitions, a constraint of the form A | B <: X is equivalent to the conjunction (A <: X) && (B <: X).
It is tempting to think the symmetric rule holds when the union is on the other side: surely X <: A | B should be equivalent to (X <: A) || (X <: B)? But on closer look, this doesn’t hold in general set theory: it fails when X has one part inside A and another part inside B. Here, X fits inside A | B as a whole, but inside neither member alone, as depicted below:
┌──────────── A ────────────┐┌──────────── B ────────────┐
│ ││ │
│ ┌──────────────────┼┼───────────────┐ │
│ │ part of X ││ part of X │ │
│ │ inside A ││ inside B │ │
│ └──────────────────┼┼───────────────┘ │
│ ││ │
└───────────────────────────┘└───────────────────────────┘
A realistic example exists in today’s type system: bool <: Literal[True] | Literal[False]. This subtyping relation obviously holds, but bool is neither a subtype of Literal[True] nor a subtype of Literal[False].
However, all mainstream checkers I examined (mypy, pyright, pyrefly, and ty) use the rule that X <: A | B implies X <: A || X <: B by default. mypy’s subtypes.py says it directly:
Normally, when ‘left’ is not itself a union, the only way ‘left’ can be a subtype of the union ‘right’ is if it is a subtype of one of the items making up the union.
Why does this simplification remain OK in practice?
Why the split usually works
If we are only talking about ordinary nominal class types, which constitute the vast majority of types in the type system, C <: A | B does imply C <: A or C <: B. This is because subtyping between classes is just subclassing, and subclassing is all-or-nothing on sets of values: if C is a subtype of A, then every C value is an A value, with no exceptions.
So suppose C <: A | B, and suppose C has an instance whose exact runtime class is C. That instance must be either an A or a B. If it is an A, nominal membership means that C subclasses A, so C <: A. Symmetrically, if it is a B, then C <: B. Either way, one of the two holds.
In lattice theory, this property of X <: A | B => (X <: A) || (X <: B) is called being join-prime. In the current Python type system, ordinary classes are join-prime in the common case.
Where it breaks today
This section lists cases where join-primeness can fail, and how type checkers typically account for them.
Union types themselves. When X is itself a union type, join-primeness breaks. For example, A | B <: (A | C) | (B | D) holds, but A | B is not a subtype of either side for unrelated A, B, C, and D.
Type checkers usually address this problem by breaking down the union on the left before splitting the one on the right. In the example above, we would first get two smaller constraints A <: (A | C) | (B | D) and B <: (A | C) | (B | D). Each left-hand side is now an ordinary class, so join-prime reasoning applies safely. Nested unions on the right are harmless: checkers often flatten them (e.g. to A | B | C | D) for convenience, but that isn’t needed for correctness.
Enum and literal types. If a class type can be broken down into finite “smaller” pieces, we’ll lose join-primeness. For example,
bool <: Literal[True] | Literal[False]Color <: Literal[Color.RED] | Literal[Color.BLUE] | Literal[Color.GREEN], if we defineColoras a three-value enumRED,BLUE, andGREEN.
Type checkers usually handle this via rewrite: a union that contains every literal member of bool or an enum is collapsed back into bool or the enum itself, either when the union is constructed or as a fallback during the subtype check. The check then reduces to bool <: bool or Color <: Color, and the usual branch split never sees the hidden union.
Metatypes. The spec says type[A | B] <: type[A] | type[B] (for unrelated A and B). But type[A | B] is a subtype of neither on the right-hand side. As with the previous example, type checkers can typically avoid this case via normalization.
Fixed-length tuple types. Under set-theoretical interpretation, tuple types exhibit some interesting behaviors:
tuple[A | B] <: tuple[A] | tuple[B]tuple[A | B, C | D] <: tuple[A, C] | tuple[A, D] | tuple[B, C] | tuple[B, D]- etc.
Again, we can observe that the left-hand side “tuple of union” type need not be a subtype of any union branch in the “union of tuple” types on the right-hand side.
These equivalences are included in the typing spec, but the conformance suite does not directly test them as assignment or subtyping relations. Support for these rules is not universally implemented. In theory, this case can be handled in the same way as before via aggressive normalization: we could break the tuple of union apart (or, when the right-hand side covers every combination, combine it back into a tuple of union). But doing this for tuples would cause a combinatorial explosion as the number of union-bearing positions and alternatives grows, which may explain why type checkers are generally reluctant to do it.
Beyond today’s type system
Python doesn’t have sealed classes or first-class intersection and negation types at the moment. This section looks at what adding them would change.
Sealed classes
A sealed class declares that all of its subclasses are known, which lets a checker reason about that one hierarchy under a closed-world assumption. Consider the following example, using a hypothetical @sealed decorator:
class A: ...
class B: ...
@sealed
class C(ABC):
@abstractmethod
def f(self): ...
class D(C, A): # a C that is also an A
def f(self): ...
class E(C, B): # a C that is also a B
def f(self): ...
Because C is sealed and abstract, every C instance is either a D or an E, so a checker could treat C as D | E. That gives C <: A | B. But C <: A fails because E instances are not A instances; symmetrically, D shows that C <: B fails. As with enums, a checker would need to expand C into its subclasses before applying the usual branch split.
Intersections
An intersection type would bring the mirror image of the union problem:
- An intersection on the right is easy, since
X <: A & Bholds exactly whenX <: AandX <: B. - An intersection on the left is hard, because
A & B <: Xcan hold when neitherA <: XnorB <: Xdoes. Each part can supply somethingXneeds, without supplying everything. For example, take protocolsRequiresF(requiring a methodf),RequiresG(requiringg), andRequiresFG(requiring both). ThenRequiresF & RequiresG <: RequiresFG, yet neitherRequiresF <: RequiresFGnorRequiresG <: RequiresFG.
Intersections would also give X more ways to hide a union, because intersection distributes over union. For example, (A | B) & C is equivalent to (A & C) | (B & C), so it can fit inside that union even when it fits inside neither branch alone. A checker cannot apply the usual branch split here without losing completeness unless it first accounts for this hidden union structure. It could expand the left-hand side into a union of intersections, factor the right-hand side in the opposite direction, or use a solver that reasons about the Boolean structure directly. The first two approaches amount to converting toward DNF or CNF, both of which risk exponential blowup in the worst case.
Negations
A negation type would break join-primeness further, because it would make the “part of A, part of B” situation easier to construct.
For example, take A and C to be two unrelated nominal classes that could share a common subclass. The subtyping relation C <: A | ~A always holds, because the right-hand side is equivalent to object. But obviously C is a subtype of neither A (they don’t declare an inheritance relation) nor ~A (one could always define another class that subclasses both C and A, so some C objects can be A objects).
One may think that we only need another form of normalization to handle this: e.g. to combine A | ~A into object or A & ~A to Never. But this is incomplete: Take C <: (A & B) | ~A | ~B with unrelated nominal non-final classes A, B, and C. The right-hand side is already in DNF, and in fact it’s equivalent to object, but that can’t be derived without further boolean operations beyond local complement merge. In general, deciding such hidden tautologies is at least as hard as propositional tautology, which is co-NP-hard, so it’s unlikely that one would find a complete decision procedure with worst-case polynomial complexity.
Wrapping up
The split works well today because relatively few supported type forms can hide a union. Checkers normalize or special-case important cases such as enums and metatypes, while accepting some incompleteness elsewhere, such as fixed-length tuple expansion. Sealed classes would add another hidden union to expand, much like enums. Intersection types would create the corresponding problem for A & B <: X, while negation types would make even ordinary nominal classes non-join-prime.
I used to think that these normalization rewrites within type checkers were purely for simplification and performance, but from this investigation I now realize that these rewrites are actually load-bearing for completeness as well.
Once X <: A | B gets converted into X <: A || X <: B, checkers then have to deal with the resulting disjunctive constraints. This is another fascinating topic, and major type checkers are extremely creative in how they avoid solving it in full generality for better performance. But that’s a separate rabbit hole, so I’ll leave it for another day.
