Re: [Sml-implementers] type-checking bug in several implementations

[Peter S. <se...@di...>]

On Fri, 9 Apr 2004, Stephen Weeks wrote:

> The following program is incorrectly handled by Hamlet, MLton, the ML
> Kit, and Moscow ML.  It should be rejected as type incorrect.  Hamlet
> and Moscow ML compile the program, but encounter a run time error (a
> seg fault in the case of Moscow ML).  MLton and the ML Kit report
> internal errors at compile time.

The CVS version of Moscow ML rejects the program as ill-typed (thanks
to Claudio Russo):

----------------------------------------------------------------------
Moscow ML version 2.01a (January 2004)
Enter `quit();' to quit.
[opening file "tyinfbug.sml"]
File "tyinfbug.sml", line 1-14, characters 11-251:
! ...........:
!    sig
!       val f: 'a option -> 'a option
!    end =
! ..........
! 	    fn z => (!r before (r := z))
! 	 end
!       val f = make ()
!    end
! Signature mismatch: the module does not match the signature ...
! Scheme mismatch: value identifier f
! is specified with type scheme
!   val 'a' f : 'a' option -> 'a' option
! in the signature
! but its declaration has the unrelated type scheme
!   val f : 'a option -> 'a option
! in the module
! The declared type scheme should be at least as general as the specified type scheme
[closing file "tyinfbug.sml"]
----------------------------------------------------------------------

Note that

  val 'a f : 'a option -> 'a option

is mosml's way of saying that 'a is universally quantified in the
type.

The only slightly unfortunate thing in the error message is that the
universally quantified type variable is called

     'a'

that is, type variable a prime.

Peter