I guess the case I'm referring to is:
switch (lunch) {
case Box(Soup s):
case Bag(Soup s):
}
Where Soup is the only know subtype of Lunch. This code is exhaustive,
but is Sandwich is added, it is no longer so.
Given Lunch is sealed to only permit Soup, and Container = Box|Bag, then
this switch is exhaustive on COntainer<Lunch>.
Later, when Lunch is extended to permit Sandwich, this switch becomes
not exhaustive on Container<Lunch>, and you get a compile error, as you
would want. Now you can totalize either by handling the
sandwich-related cases, OR by adding Box(Lunch)/Box(var) cases, OR by
adding Container(Soup) cases, OR by adding Container(Lunch) case, OR by
adding a default/var case.
That said, if an error is issued whenever a switch statement is not
exhaustive, that would alleviate my concerns - I think the error would
cover this case also.
Yes. Totality is compositional. We can treat `Box(Soup)` as Box(var
alpha) & alpha matches Soup. Then the switch is a big disjunction of
conjunctions, and we can rearrange with De Morgan's laws and related
boolean algebra tricks. So
Box(Soup) OR Box(Sandwich)
== (Box(var alpha) AND alpha matches Soup) OR (Box(var alpha) AND
alpha matches Sandwich)
== Box(var alpha) AND (alpha matches Soup OR alpha matches Sandwich)
== Box(var alpha) AND (alpha matches Lunch)
== Box(Lunch)
The think the I find mildly odd is that when Sandwich is added, it
might not be enough to add another `case`. If there was null-related
logic inside `case Box(Soup s):` that would have to be moved somewhere
else. So while in most cases it will be a straightforward refactoring,
I can see some puzzlers emerging here.
Can you pull on this string a big?
