[pattern-switch] Totality

[Brian Goetz]

>>
>>  - Let S be a sealed abstract type or interface, with permitted 
>> direct subtypes C*, and P* be a set of patterns applicable to S.  If 
>> for each C in C*, there exists a subset Pc of P* that is total on C 
>> with remainder Rc, then P* is total on S with remainder { null } 
>> union \forall{c \in C}{ Rc }.
>

Guy's example implicitly points out that this rule is missing a case.  
It should be { null, S s } union { Rc : c in C }.  The `S s` entry is 
the analogue of `E e` for sealed types.

The analogue of this rule, when S is concrete, is:

  - Let S be a sealed concrete class, with permitted direct subtypes C*, 
and P* be a set of patterns applicable to S.  If for each C in C* union 
{ S }, there exists a subset Pc of P* that is total on C with remainder 
Rc, then P* is total on S with remainder { null } union { Rc : c in C }.

That is, we have to consider `S` one of its own subtypes when S is 
concrete, and then we don't need it in the remainder.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.java.net/pipermail/amber-spec-experts/attachments/20200826/77e4e32b/attachment.htm>