Michael Norrish wrote:

The attached causes the following error message, after doing a

poly < simple.sml

Poly/ML 5.3 Release candidate 1

...

# # # ... # # Error-Type error in function application.

Function: = : ''a * ''a -> bool Argument: (v, w) : ''a * hol_type Reason: Can't unify ''a to hol_type (Requires equality type) Found near exists_tyvar (fn v => v = w) ty Error-Type error in function application. Function: exists_tyvar : (hol_type -> bool) -> hol_type -> bool Argument: (fn v => v = w) : ''a -> bool Reason: Can't unify hol_type to ''a (Requires equality type) Found near exists_tyvar (fn v => v = w) ty Static Errors

Thanks. I've fixed it in SVN 903. The problem was to do with computing the equality status for datatypes in signatures whose constructors used types which had equality as a result of a type abbreviation. The simplest example I could come up with, and one I've put into my regression tests, was functor F(S: sig type t = int * int datatype s = X of t end) = struct fun f(x, y: S.s) = x = y end;

David