One question I have is that optimistic totality can apply in switches that are not on sealed types, or where sealed types show up in nested contexts. For example: switch (box) { case Box(var x): ... } Here, I think we want to say that Box(var x) is o.t. on Box, but it doesn't match null. So how does the programmer indicate that they want to get totality checking and residue rejection?I believe that “switch case” can handle this: switch case (box) { case Box(var x): ... } This says, among other things, that it is a static error if the (singleton) set of case patterns { Box(var x) } is not o.t. on the type of “box”, and it says we want residue checking, so it’s as if the compiler rewrote it to: switch case (box) { case null: throw <null residue error, which could be NPE or something else> case Box(var x): ... } Alternatively, we could write switch (box) { default Box(var x): ... } which says that it is a static error if the pattern Box(var x) is not total on the type of “box”. It’s not, because it doesn’t match null, so we get a static error, as desired. Perhaps we should have written switch (box) { case Box(var x): … default Box z: ... } But I’m thinking the “switch case” solution is preferable for this specific example.
OK, so (taking this example with the next) the mental model for `switch case` is not as I suggested -- "switch by covering parts" -- as much as "a switch that is optimistically total, and which gets built-in residue rejection." Because there are multiple categories of o.t. that don't involve enum/sealed types at all, or that get their optimism only indirectly through enum/sealed types.
Let me probe at another aspect; that it is an error for a `switch case` to have a default clause. This seems a tad on the pedantic side, in that surely if you add a `default` clause to an already o.t. switch with non-empty residue, it is (a) still total and (b) might afford you the opportunity to customize the residue rejection. But I think your response would be "that's fine, it's not a switch case, it's an ordinary total switch with a default clause.
Which says to me that you are motivated to highlight the negative space between "optimistically total" and "total"; what a `switch case` asserts is _both_ that the set of cases is optimistically total, _and_ that there's a non-empty residue for which which we cede responsibility to the switch. (Secondarily, I think you're saying that a `default` at the end of the switch is enough to say "obviously, it's total.")
