[rastrian]

I think we mostly agree for the nullable case in a sound-enough type system: if Foo | null is tracked precisely and the compiler forces a check before x.bar, then yes, you’re not “remembering” checks manually, the compiler is.

Two places where I still see tagged/discriminated unions win in practice:

1. Scaling beyond nullability. Once the union has multiple variants with overlapping structure, “untagged” narrowing becomes either ambiguous or ends up reintroducing an implicit tag anyway (some sentinel field / predicate ladder). An explicit tag gives stable, intention-revealing narrowing + exhaustiveness.

2. Boundary reality. In languages like TypeScript (even with strictNullChecks), unions are routinely weakened by any, assertions, JSON boundaries, or library types. Tagged unions make the “which case is this?” explicit at the value level, so the invariant survives serialization/deserialization and cross-module boundaries more reliably.

So I’d summarize it as: T | null is a great ergonomic tool for one axis (presence/absence) when the type system is enforced end-to-end. For domain states, I still prefer explicit tags because they keep exhaustiveness and intent robust as the system grows.

If you’re thinking Scala 3 / a sound type system end-to-end, your point is stronger; my caution is mostly from TS-in-the-wild + messy boundaries.

[cubefox]

I think the real promise of "set-theoretic type systems" comes when don't just have (untagged) unions, but also intersections (Foo & Bar) and complements/negations (!Foo). Currently there is no such language with negations, but once you have them, the type system is "functionally complete", and you can represent arbitrary Boolean combination of types. E.g. "Foo | (Bar & !Baz)". Which sounds pretty powerful, although the practical use is not yet quite clear.