From 4eb93836d04d18f43d8c4360f290a7977d96c468 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sun, 18 Dec 2011 11:29:13 -0500
Subject: Add a new scoping check for unification variables, to fix a type
 inference bug

---
 src/elab.sml | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

(limited to 'src/elab.sml')

diff --git a/src/elab.sml b/src/elab.sml
index c042d916..15365951 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -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 @@ datatype kind' =
        | 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 @@ datatype con' =
        | 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
 
-- 
cgit v1.2.3