Yes. When you say "sum type" and you're talking about, say, Ocaml or Standard ML or (mostly) Haskell or Rust, then what comes with that is also the infrastructu

Yes. When you say "sum type" and you're talking about, say, Ocaml or Standard ML or (mostly) Haskell or Rust, then what comes with that is also the infrastructure around sum types in those languages. They aren't really separable. That includes pattern matching and exhaustiveness checking (the latter is an opt-in warning in Haskell, and can be opted out of in Rust on a per-type basis). The discussion around "sum type" the concept is to disentangle it from the implementation strategy. Tagged unions are the implementation strategy, and they don't come with pattern matching or exhaustiveness checks. Of course, many of these terms are used interchangeably in common vernacular. But if you look at the comment that kicked off this annoying sub-thread: > so, um, unions? i have to say that in many years of programming, i have almost never needed to use such types. Then this is clearly trying to draw an equivalence between two different terms, but where no such equivalence exists. There's no acknowledgment here of the difference between what a "union" is (nevermind a tagged union) and the "sum types" being talked about in my original top level comment. And the last part, "i have almost never needed to use such types" is puzzling on multiple levels.