[MLton] Catching redundant pattern matches

[Matthew Fluet]

> > Also, is your redundant case inside the body of an (unused) functor?
> > It turns out that we perform match compilation (and discover
> > exhaustive/redundant matches) on the defunctorized program.
> ...
> > This is probably reason enough to move the match compilation into
> > the elaborator.
>
> One reason we do match compilation after defunctorization is because
> of exception aliasing.  I guess other implementations just assume
> exceptions aren't aliased, which generates redundant tests in some
> cases (not that this really matters for performance).
>
> Not warning about matches in unused functors is clearly a bug.
> Perhaps the right solution is to do match compilation in the
> elaborator just for the purposes of warnings, and then do match
> compilation after defunctorization to generate code.  It is
> duplication of work, but may not be too costly.

John Dias (@ Harvard) has been studying the Definition, and we were
discussing that the Definition's allowance of inconsistent specifications
can lead to truly bizzare situations.  For example:

signature SIG =
   sig
      datatype t = T
   end

functor F1 (Str : SIG where type t = int) =
   struct
      open Str

      fun isT (i : int) : bool =
	 case i of
	    T => true
	  | _ => false
   end

This would appear to be type correct with respect to the Definition,
although there is no way to construct a structure matching
SIG where type t = int.  T is a constructor, with type int.
It would appear that the following is also correct:

functor F2 (Str : SIG where type t = int) =
   struct
      open Str

      fun isT (i : int) : bool =
	 case i of
	    T => true
          | 42 => true
	  | _ => false
   end

Andreas Rossberg's "Bugs & Defects" mentions this problem, without giving
a clear solution.  When dealing with "int", MLton always assumes that the
matches are non-exhaustive, so demands a wild-card match.  A related
problem is the following:

datatype u = U of bool
functor F3 (Str : SIG where type t = u) =
   struct
      open Str

      fun isT (u : u) : bool =
	 case u of
	    T => true
          | U b => b
   end

Finally, I will note that MLton's -show-basis isn't always very
informative when forming inconsistent signatures.  If I add the signatures

signature SIG' =
  sig
    datatype v = V
  end where type v = int
signature SIG'' =
  sig
    type w
  end where type w = int

to the above declarations, then -show-basis yields:

datatype u = U of ?.bool
functor F1 (S: SIG
	       where datatype t = ?.int32)
   : sig
	datatype t = T
	val isT: ?.int32 -> ?.bool
     end
functor F2 (S: SIG
	       where datatype t = ?.int32)
   : sig
	datatype t = T
	val isT: ?.int32 -> ?.bool
     end
functor F3 (S: SIG
	       where datatype t = u)
   : sig
	datatype t = T
	val isT: u -> ?.bool
     end
signature SIG =
   sig
      datatype t = T
   end
signature SIG' =
   sig
      datatype v = V
   end
signature SIG'' =
   sig
      eqtype w = ?.int32
   end

which doesn't seem to describe SIG' correctly.