Here is another example that propose a way to declare that several case methods are total using the keyword exclusive (if one case method is marked exclusive, all case methods must be marked exclusive).
The document alludes to this problem; certain sets of patterns are, in aggregate, total on a type. The poster child is `Optional.of` and `Optional.empty`. And yes, we want a way to express totality in the model (though, since we haven't even gotten to the mechanics of static/instance patterns yet, this is even further down the list). F# does it in the pattern declaration; somewhere there is a declaration like "pattern Foo = Bar | Baz", which captures the sum-ness of them.
Your `MyNumber` example induces a sum by saying "all the patterns in this class." This works in theory, but I think this particular approach runs out of gas pretty quickly, since (for example) a class could easily have patterns that are not part of the sum. (Further, patterns can overlap; I can have patterns for a, b, and a|b, and _any two_ of them are total.)
Again, I think this is a little farther down the road, but I think the winning intuition here is to synthesize exhaustiveness by constructively demonstrating adjunction to a known sealed domain. For example, Optional is adjoint to Boolean; if we project Optional down to Boolean, saying that the `Optional.of` pattern corresponds to true and the `Optional.empty` pattern corresponds to `false`, then we can derive both exhaustiveness _and more efficient dispatch_ from this information. Similarly, the Javac tree classes have `Kind` enums, and enums are sealed, so if we can project patterns down to (sets of) kinds, then the compiler can again derive both exhaustiveness and more efficient dispatch. (All this is to say that, while I don't have a 100% bulletproof answer yet, I've spent quite a bit of time on it, and already rejected the first six naive ideas here.)
What I take from your mail here is "exhaustiveness is important"; I agree (and said as much in the doc.) Is there more, that I've missed?
