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