[MLton] Catching redundant pattern matches

[Stephen Weeks]

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

Amusing.

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

It's not clear that that's wrong in this case.  One could either read
the phrase "value (of the right type)" on page 28 the Definition as
meaning "{T} union Int", "{T} intersect Int", or "{T}" or "Int".  Hmmm
... one could even read it as requiring MLton's approach of waiting
until after defunctorization, since we don't yet know what the right
type is.  Anyways, my bet would be that if we tried to feed the above
to MLton's match compiler it would generate an internal bug, since the
match compiler assumes that datatypes and integers are disjoint.
Something else to worry about if we move match compilation forward.

My take on this whole inconsistent specification/unmatchable signature
thing is that the 97 Definition gets it much better than the 90
Definition.  I found the old rules, which tried to rule out
unmatchable signatures, worse because they ruled out some
unmatchables, but allowed others, and also ruled out some matchable
signatures (IIRC).  I would be happy with a system that ruled out
precisely the unmatchable signatures, but I don't know how to do it,
and in the absence of that, allowing most anything seems best.  Even
then, who's to say that it isn't useful to have unmatchable signatures
while developing a functor, and then later refine it to a matchable
signature in order to get a running program.

> 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
>       datatype v = V
>    end
...
> which doesn't seem to describe SIG' correctly.

Yeah, MLton doesn't display type identity information on datatypes, as
there was no good syntactic place to do so.  Consider 

signature SIG =
   sig
      structure T1:
	 sig
	    datatype t = T
	 end
      structure T2:
	 sig
	    datatype t = T
	 end
      sharing type T1.t = T2.t
   end

which displays as

signature SIG = 
   sig
      structure T1:
	 sig
	    datatype t = T
	 end
      structure T2:
	 sig
	    datatype t = T
	 end
   end

I.E. the type sharing isn't expressed.  If you think of a good place
to display type identity information on datatypes, the information is
certainly available.