[pattern-switch] Opting into totality

[Brian Goetz]

> I bring this up again not to defend the syntax, but to underscore a 
> more important point: that we thought at first that “sealing” switches 
> was about asserting totality and enlisting the compiler’s aid in 
> verifying same, but as we worked through the cases, and discovered 
> there were more cases of remainder than we initially thought, the main 
> value of sealing instead became restoring the switch to having no 
> unhandled remainder.  Whatever syntax we choose should try to evoke 
> that at least as much as evoking totality of the case labels. 

Taking this a little further: it is not that interesting to declare a 
switch `sealed` that has a default clause or other total pattern; such 
switches are "obviously" total and non-leaky.  It's nice, but we 
wouldn't add a language feature for it.

The interesting part of sealing a switch are cases like this. Assume 
Shape = Circ | Rect.

     switch (shape) {
         case Circ c:
         case Rect r:
     }

Here, sealing gives us two things: asserting we've covered all the cases 
(which is not going to be obvious except in the most trivial of sealed 
types) and handling of remainder (here, only null.) Similarly:

     switch (boxOfShape) {
         case Box(Circ c):
         case Box(Rect r):
     }

Same basic story -- not obvious that we've covered all boxes, the 
remainder is just slightly more complicated.

The compile-time checking for optimistic totality, and runtime checking 
for remainder, are two sides of the same coin; we are stating 
expectations that all possible inputs are covered, either by an explicit 
case or by an implicit remainder case.  We statically check the ones we 
can, and dynamically reject the "acceptable non-coverage."  
(Characterizing the acceptable non-coverage is the main bit of positive 
progress we've made recently.)

I think we may be skipping over a step by jumping to "throwing syntax at 
the problem."  The real question is, what do we want the users thinking 
about when they are coding, and what should we not be bothering them 
with?  We've already acknowledged that we _don't_ want them worrying 
about explicitly managing the remainder.

We've been approaching this as "I assert that this switch is 
sufficiently total", which included both strongly total and 
optimistically total switches (because that's what we already do for 
expression switches.)  But given that having a default case makes it 
obviously total (and obviates the need for remainder handling), perhaps 
we want to focus on the user asserting "I know I didn't write a default, 
but I am still covering all the cases."  Does that offer a different 
enough viewpoint that other options come into focus?