Opting into totality

[Brian Goetz]

>> 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.")