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
Poly 5.2 compiles the same code fine. r902 also compiles it fine if the (redundant, in this stripped down example) KTypes signature is removed, and the KTypes structure loses its signature ascription.
mlton and Moscow ML also compile the code without complaint.
Michael