Opting into totality

[Brian Goetz]

The previous mail, on optimistic totality, only applied to switches that 
were already total.  Currently that includes only expression switches; 
we want a non-too-invasive way to mark a statement switch as total as well.

First, I'd like to rule out the variants of "automatically make XYZ 
statement switches total", such as, e.g., "statement switches over enums 
or sealed types" -- because partial switches are entirely _useful and 
reasonable_.  A partial switch is like an `if` without an `else`.  
Nothing wrong with that, regardless of whether the target is an enum or 
sealed type or some other known-enumerable type.  There's no reason to 
rule out partiality here.  Users won't thank us.


There are a number of syntactic options for opting in, such as:

  - A modified keyword (total-switch)
  - A modifier before or after `switch` (e.g., `switch enum`, as per 
Guy's #4, `sealed switch`, or `switch case` as per #8)
  - Turning the statement switch into a void expression switch (Guy's #5)
  - Giving `default` new jobs to do
  - A streamlined form of throw-on-residue default (e.g., `default: 
throw`, #6)
  - Using cast expressions to highlight the target type (#7)

There is something pretty attractive about saying only "this statement 
switch is total in exactly the same ways that all expression switches 
are", because then we have factored the interaction between the switch 
being total (or not) and the set of cases being optimistically total (or 
not), rather than introduced yet another mechanism whose only purpose is 
to plug a hole.

The idea of "turn it into an expression switch by casting to void" is 
cute, but will always be perceived by users as an "idiom" rather than an 
actual feature.  I would like to encourage developers to think more in 
terms of totality, because it contains hidden benefits for them.  (I am 
also vaguely fearful of an unexpected interaction when we try to turn 
`void` into a type in Valhalla, and would rather "avoid" creating new 
constraints on this.)

The idea of `default: throw` reads nicely, but the semantics feel too 
ad-hoc, in that we're inferring the behavior of `throw` in the context 
of a `default` in the context of an otherwise-optimistically-total 
switch.  I would expect that people would then expect `throw` to mean 
"throw the obvious thing" in other contexts, leading to disappointment.


Another option is to engage some notion of unreachability.  It has been 
requested a few times before to have a feature like an "unreachable" 
statement:

     void m(int x) {
         if (x == 0)
             throw new FooException();
         else
             return;

         unreachable;
     }

Which would be interpreted as an assertion that this statement is 
unreachable, that the compiler should issue an error if it can prove the 
statement _is_ reachable, and translate to throwing some sort of 
assertion error.  If we had such a notion, we could extend it to say:

     default: optimistically-unreachable

which would have the effect of (a) engaging reachability analysis and 
generating compiler errors if the case is known to be reachable, and (b) 
throwing the expected set of errors on residue at runtime.