# Notes on splitting unions in subtype checks

**URL:** <https://discuss.python.org/t/notes-on-splitting-unions-in-subtype-checks/109329>\
**Category:** Typing\
**Created:** [October 2, 2026, 10:30pm UTC](https://discuss.python.org/t/notes-on-splitting-unions-in-subtype-checks/109329 "2026-10-02T22:30:18Z")\
**Posts on this page:** 8\
**Page:** 1

<div class="post-metadata">

**Author:** ![grievejia](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/grievejia/32/18850_2.png) [@grievejia](https://discuss.python.org/u/grievejia)\
**Post date:** [October 2, 2026, 10:30pm UTC](https://discuss.python.org/t/notes-on-splitting-unions-in-subtype-checks/109329/1 "2026-10-02T22:30:19Z")

</div>

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](https://typing.python.org/en/latest/spec/concepts.html#subtype-supertype-and-type-equivalence)). A union `T1 | T2` is the union of the two sets ([union types](https://typing.python.org/en/latest/spec/concepts.html#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:

```python
┌──────────── 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 define `Color` as a three-value enum `RED`, `BLUE`, and `GREEN`.

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](https://typing.python.org/en/latest/spec/tuples.html#type-compatibility-rules), 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:

```python
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 & B` holds exactly when `X <: A` and `X <: B`.
- An intersection on the left is hard, because `A & B <: X` can hold when neither `A <: X` nor `B <: X` does. Each part can supply something `X` needs, without supplying everything. For example, take protocols `RequiresF` (requiring a method `f`), `RequiresG` (requiring `g`), and `RequiresFG` (requiring both). Then `RequiresF & RequiresG <: RequiresFG`, yet neither `RequiresF <: RequiresFG` nor `RequiresG <: 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.

---

<div class="post-metadata">

**Author:** ![dangotbanned](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/dangotbanned/32/25910_2.png) [@dangotbanned](https://discuss.python.org/u/dangotbanned)\
**Post date:** [October 2, 2026, 11:10pm UTC](https://discuss.python.org/t/notes-on-splitting-unions-in-subtype-checks/109329/2 "2026-10-02T23:10:32Z")

</div>

This could be a coincidence, but did I cause this rabbit hole? 😉

> <https://github.com/facebook/pyrefly/issues/4556>
>
> \### Describe the Bug
> 
> \`pyright\` and \`ty\` accept both versions, but \`pyrefly\` com…plains if there was an assignment before passing the argument to the function:
> 
> \`\`\`py
> from typing import Literal
> 
> def func(\_mapping: dict\[str, str | bool\]) -\> None:
> return
> 
> def example(a: Literal\[True\], b: Literal\[False\], c: str) -\> None:
> ok = func({"a": a, "b": b, "c": c})
> infer = {"a": a, "b": b, "c": c}
> nope = func(infer) # Argument \`dict\[str, Literal\[False, True\] | str\]\` is not assignable to parameter \`\_mapping\` with type \`dict\[str, bool | str\]\` in function \`func\` \[bad-argument-type\]
> \`\`\`
> 
> I took a look at the typing spec, and I didn't find anything specifying my expectation.
> The closest was here:
> \- https://typing.python.org/en/latest/spec/literal.html#interactions-with-enums-and-exhaustiveness-checks
> \- https://typing.python.org/en/latest/spec/literal.html#interactions-with-narrowing
> 
> 
> Essentially I'd expect \`Literal\[False, True\]\` to be assignable to \`bool\` - in the same way that \`Literal\[\<enum-members\>, ...\]\` is assignable to \`\<enum-class\>\`
> 
> 
> \### Sandbox Link
> 
> https://pyrefly.org/sandbox/?project=v2.pZTBDoIwDIZfZZEDmBB35wE8excOY0wkmo3A8GJ8d\_92EAUTovHWNO2frf36\_2CZo-u9Y5pgSewZmajgXnRojBFgLXHcxXL\_AalJwYRDTFQ2aR9pX0UqyldmrwAdUppveynoLpgKv-SebxRYESrFlEqKSoo0RfoBIPhI7Ml06FgvDrXWtbQYFue-7efGI3EICTEOD14HVOoBjgoEdrmNYKZGnL1v-0zKqd11tTRWVk73ctYhBcGtbqphn57LCceE9pD9B7U4kBavgRYTZ6jAlwfrG3811RcwPQE
> 
> \### Additional Info
> The repro is based on (https://github.com/dangotbanned/mosaic/blob/f24c14ed921794cb5db3712ab626d694c5501c00/packages/vgplot/spec-python/tools/codegen/typed\_dict.py#L51-L80).
> Where I tried out \`pyrefly\` on a new codebase and this error was reported twice

---

<div class="post-metadata">

**Author:** ![grievejia](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/grievejia/32/18850_2.png) [@grievejia](https://discuss.python.org/u/grievejia)\
**Post date:** [October 2, 2026, 11:18pm UTC](https://discuss.python.org/t/notes-on-splitting-unions-in-subtype-checks/109329/3 "2026-10-02T23:18:42Z")

</div>

Ha, partly! Issues like yours were part of what got me looking at this. Thanks for filing it!

---

<div class="post-metadata">

**Author:** ![AlexWaygood](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/alexwaygood/32/4722_2.png) [@AlexWaygood](https://discuss.python.org/u/AlexWaygood)\
**Post date:** [October 2, 2026, 11:23pm UTC](https://discuss.python.org/t/notes-on-splitting-unions-in-subtype-checks/109329/4 "2026-10-02T23:23:31Z")

</div>

This reminds me very much of [`AlwaysTruthy | bool` is equivalent to `AlwaysTruthy | Literal[False]` · Issue #216 · astral-sh/ty · GitHub](https://github.com/astral-sh/ty/issues/216), an issue I tried several times to fix (you can see the linked PRs), but found very hard to in practice. (`AlwaysTruthy` in ty is a structural type that represents “the set of all objects that are statically known to always evaluate to `True` in a boolean context”.)

---

<div class="post-metadata">

**Author:** ![AlexWaygood](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/alexwaygood/32/4722_2.png) [@AlexWaygood](https://discuss.python.org/u/AlexWaygood)\
**Post date:** [October 2, 2026, 11:26pm UTC](https://discuss.python.org/t/notes-on-splitting-unions-in-subtype-checks/109329/5 "2026-10-02T23:26:52Z")

</div>

> [@grievejia](#):
>
> The first two approaches amount to converting toward DNF or CNF, both of which risk exponential blowup in the worst case.

The approach ty takes is to always maintain DNF structure in our types: unions can contain intersections, but intersections can never contain unions at the top level in our representation. And yes, we’ve certainly encountered a fair few cases of exponential blowup! Though nothing so far that we’ve found impossible to mitigate.

---

<div class="post-metadata">

**Author:** ![grievejia](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/grievejia/32/18850_2.png) [@grievejia](https://discuss.python.org/u/grievejia)\
**Post date:** [October 2, 2026, 11:40pm UTC](https://discuss.python.org/t/notes-on-splitting-unions-in-subtype-checks/109329/6 "2026-10-02T23:40:11Z")

</div>

Thanks for the responses, Alex!

I hadn’t seen [#216](https://github.com/astral-sh/ty/issues/216) before, and it’s a great example of the problem: `bool <: AlwaysTruthy | Literal[False]` holds even though `bool` fits in neither branch on its own. The discussion on the linked PR was eye-opening too. I’d been thinking of these normalizations as sufficient guards, but it looks like there are some wrinkles I hadn’t appreciated earlier. This “decompose” operation mentioned there seems to overlap in concept with what I referred to as “non-join-primeness class type” in this post.

And it’s good to hear DNF is holding up in practice. Out of curiosity, where has the blowup actually shown up for you so far, and what do the mitigations look like? The example I could construct off the top of my head is

```python
def f(x: A1 | A2 | A3) -> None:
    if isinstance(x, (B1, B2, B3)):
        if isinstance(x, (C1, C2, C3)):
            reveal_type(x) # (A1 & B1 & C1) | (A1 & B1 & C2) | ... (27 terms)

```

but I’m not sure it’s something people would realistically write.

---

<div class="post-metadata">

**Author:** ![mikeshardmind](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/mikeshardmind/32/14381_2.png) [@mikeshardmind](https://discuss.python.org/u/mikeshardmind)\
**Post date:** [October 3, 2026, 4:55am UTC](https://discuss.python.org/t/notes-on-splitting-unions-in-subtype-checks/109329/7 "2026-10-03T04:55:17Z")

</div>

This came up during [intersection discussions](https://github.com/CarliJoy/intersection_examples/issues/22)

Quoting only a few choice points from it, but it’s worth reading in entirety.

> the formulas that define set-theoretic unions and intersections are as follows:  
> C⊆A∩B⟺(C⊆A∧C⊆B)  
> C⊇A∪B⟺(C⊇A∧C⊇B)

> The duality between intersection and union lies in reversing the subset relation, _not_ in replacing an “and” with an “or”. In fact it is a well understood idea that transitive relations play extremely poorly with “or”, and [extremely well with “and”](https://ncatlab.org/nlab/show/hom-functor+preserves+limits). Hence the above definitions both using “and”.

> I’ll also cut to the chase here: you want to reduce the left hand side to a _disjunctive_ normal form, and the right hand side to a _conjunctive_ normal form. The `|` on the left and the `&` on the right can then be taken apart. But the `&` on the left and the `|` on the right cannot.

---

<div class="post-metadata">

**Author:** ![grievejia](https://sea2.discourse-cdn.com/flex002/user_avatar/discuss.python.org/grievejia/32/18850_2.png) [@grievejia](https://discuss.python.org/u/grievejia)\
**Post date:** [October 3, 2026, 5:45am UTC](https://discuss.python.org/t/notes-on-splitting-unions-in-subtype-checks/109329/8 "2026-10-03T05:45:29Z")

</div>

Thanks for the pointer! I hadn’t seen that thread, and it’s a great read. The same core observation there, much earlier and more rigorously than I did, and “reverse the subset relation, not swap _and_ with _or_” is a clean way to put the duality.

I think my notes end up looking at the complementary question: given that `C <: A | B <=> C <: A ∨ C <: B` isn’t true in general, why do checkers get away with using it? For ordinary nominal classes, it turns out to be fine: once the left-hand side is in DNF and the right-hand side is in CNF, the remaining `&` on the left and `|` on the right can be taken apart as well. The cases in the post and the followup discussions (`bool` and enums, structural types like `AlwaysTruthy`, negations, etc.) are where that stops being sufficient.