case expressions/transfers

[Matthew Fluet]

In preparation for the known-case optimization, I'm extending the
type-checker to verify that all SSA case transfers are non-redundant and
exhaustive.  (Well, at least with datatypes.  I'm going to set it up so
that Char/Int/Word8/Word cases must have a default.  It's only possible to
have an exhaustive case for Char and Word8, but I don't think it's worth
checking.)  I'm adding this to the checkScopes portion of the
type-checker, because it doesn't seem worth trying to extend anayze to
handle this.

Anyways, I was working a test case to see what SSA programs might actually
show up and came up with this:

datatype t = A | B | C | D

val toString1
  = fn A => "A"
     | B => "B"
     | C => "C"
     | D => "D"
     | A => "AA"
     | B => "BB"
     | _ => "Z"

val toString2
  = fn A => "A"

val rand = _ffi "rand": unit -> int;

val x = case rand ()
	  of 0 => A
	   | 1 => B
	   | 2 => C
	   | 3 => D
	   | 0 => D
	   | 1 => C

val _ = print (concat [toString1 x, " ", toString2 x, "\n"])


Technically, I think this is an invalid input program because of the
redundant cases in the definitions of toString1 and x, but MLton accepts
it.  It does, however, raise a shrinker error after removeUnused1 which is
arguably a bug in removeUnused.  (removeUnused decides whether or not to
keep the default case of a Case.Con by comparing the number of variants in
the datatype to the number of cases; in toString1 the number of cases is
always equal to 6, so it keeps the default branch; but the way used is
computed, the block corresponding to the default label is marked unused so
doesn't appear in the program handed to the shrinker.  Conversely, this
means that if I defined
val toString1
  = fn A => "A"
     | A => "AA"
     | A => "AAA"
     | A => "AAAA"
     | _ => "Z"
then I would eliminate the default case and we would get a program that
used the first A case for any non-A variant, because in the translation
from MACHINE the first branch in a case without a default is always
promoted to the default.   Easy enough to fix in removeUnused by doing a
real exhaustiveness check, but the numerical comparision would be
cheaper.)

But, that's not my main point.  Something before closure conversion
simplifies the definition of x to remove the redundant branches (and
inserts the default branch to raise a Match exception), but the
corresponding simplification is not performed on the definition of
toString1.  Is there a reason why?  A reason not to?