Mercurial > urweb

diff src/elab.sml @ 1639:6c00d8af6239

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add a new scoping check for unification variables, to fix a type inference bug
author Adam Chlipala <adam@chlipala.net>
date Sun, 18 Dec 2011 11:29:13 -0500
parents 5337adf33a4a
children bb942416bf1c
line wrap: on
line diff
--- a/src/elab.sml	Sat Dec 17 20:42:39 2011 -0500
+++ b/src/elab.sml	Sun Dec 18 11:29:13 2011 -0500
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2010, Adam Chlipala
+(* Copyright (c) 2008-2011, Adam Chlipala
  * All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
@@ -38,12 +38,16 @@
        | KTuple of kind list
 
        | KError
-       | KUnif of ErrorMsg.span * string * kind option ref
-       | KTupleUnif of ErrorMsg.span * (int * kind) list * kind option ref
+       | KUnif of ErrorMsg.span * string * kunif ref
+       | KTupleUnif of ErrorMsg.span * (int * kind) list * kunif ref
 
        | KRel of int
        | KFun of string * kind
 
+and kunif =
+    KUnknown of kind -> bool (* Is the kind a valid unification? *)
+  | KKnown of kind
+
 withtype kind = kind' located
 
 datatype explicitness =
@@ -78,7 +82,11 @@
        | CProj of con * int
 
        | CError
-       | CUnif of int * ErrorMsg.span * kind * string * con option ref
+       | CUnif of int * ErrorMsg.span * kind * string * cunif ref
+
+and cunif =
+    Unknown of con -> bool (* Is the constructor a valid unification? *)
+  | Known of con
 
 withtype con = con' located