case expressions/transfers

[Matthew Fluet]

> > Easy enough to fix in removeUnused by doing a real exhaustiveness
> > check, but the numerical comparision would be cheaper.)
> 
> If we make exhaustive and irredundant invariants, then removeUnused
> won't have to check.

It still has to check something; if a datatype has one or more unused
variants, then we might be able to eliminate the default case (if the
existing cases are exhaustive for the used variants).

But, I agree that if the input to removeUnused satisfies the exhaustive
and irredundant invariants, then a comparision of the number of used cases
with the number of used datatype variants will be sufficient to determine
if the default case is needed.