Exactly. When we praise statically-typed languages like OCaml, Scala, and Haskell, I think people miss that we're not just talking about random type annotations

Exactly. When we praise statically-typed languages like OCaml, Scala, and Haskell, I think people miss that we're not just talking about random type annotations. It's exactly what you describe -- we're talking about being able to model domains using the type system, which goes far, far beyond simple type errors. Algebraic data types are the bedrock for this kind of modeling, and I can't for the life of me understand why more languages don't add them (particularly languages like Java and C#).