Broaden unification context

6 files changed, 478 insertions, 289 deletions

diff --git a/src/elab.sml b/src/elab.sml
index 7c3ec6b1..1b0e3ea1 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -36,7 +36,7 @@ datatype kind' =
        | KRecord of kind
 
        | KError
-       | KUnif of string * kind option ref
+       | KUnif of ErrorMsg.span * string * kind option ref
 
 withtype kind = kind' located
 
@@ -62,7 +62,7 @@ datatype con' =
        | CFold of kind * kind
 
        | CError
-       | CUnif of kind * string * con option ref
+       | CUnif of ErrorMsg.span * kind * string * con option ref
 
 withtype con = con' located
 
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 9158a6ae..8c51be11 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -50,8 +50,8 @@ fun p_kind' par (k, _) =
       | KRecord k => box [string "{", p_kind k, string "}"]
 
       | KError => string "<ERROR>"
-      | KUnif (_, ref (SOME k)) => p_kind' par k
-      | KUnif (s, _) => string ("<UNIF:" ^ s ^ ">")
+      | KUnif (_, _, ref (SOME k)) => p_kind' par k
+      | KUnif (_, s, _) => string ("<UNIF:" ^ s ^ ">")
 
 and p_kind k = p_kind' false k
 
@@ -156,10 +156,10 @@ fun p_con' par env (c, _) =
       | CFold _ => string "fold"
 
       | CError => string "<ERROR>"
-      | CUnif (_, _, ref (SOME c)) => p_con' par env c
-      | CUnif (k, s, _) => box [string ("<UNIF:" ^ s ^ "::"),
-                               p_kind k,
-                               string ">"]
+      | CUnif (_, _, _, ref (SOME c)) => p_con' par env c
+      | CUnif (_, k, s, _) => box [string ("<UNIF:" ^ s ^ "::"),
+                                   p_kind k,
+                                   string ">"]
         
 and p_con env = p_con' false env
 
diff --git a/src/elab_util.sig b/src/elab_util.sig
index d6d8acaa..1ecd6201 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -107,4 +107,48 @@ structure Sgn : sig
 
 end
 
+structure Decl : sig
+    datatype binder =
+             RelC of string * Elab.kind
+           | NamedC of string * Elab.kind
+           | RelE of string * Elab.con
+           | NamedE of string * Elab.con
+           | Str of string * Elab.sgn
+           | Sgn of string * Elab.sgn
+
+    val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
+                    con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
+                    exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB,
+                    sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB,
+                    sgn : ('context, Elab.sgn', 'state, 'abort) Search.mapfolderB,
+                    str : ('context, Elab.str', 'state, 'abort) Search.mapfolderB,
+                    decl : ('context, Elab.decl', 'state, 'abort) Search.mapfolderB,
+                    bind : 'context * binder -> 'context}
+                   -> ('context, Elab.decl, 'state, 'abort) Search.mapfolderB
+    val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
+                   con : (Elab.con', 'state, 'abort) Search.mapfolder,
+                   exp : (Elab.exp', 'state, 'abort) Search.mapfolder,
+                   sgn_item : (Elab.sgn_item', 'state, 'abort) Search.mapfolder,
+                   sgn : (Elab.sgn', 'state, 'abort) Search.mapfolder,
+                   str : (Elab.str', 'state, 'abort) Search.mapfolder,
+                   decl : (Elab.decl', 'state, 'abort) Search.mapfolder}
+                  -> (Elab.decl, 'state, 'abort) Search.mapfolder
+    val exists : {kind : Elab.kind' -> bool,
+                  con : Elab.con' -> bool,
+                  exp : Elab.exp' -> bool,
+                  sgn_item : Elab.sgn_item' -> bool,
+                  sgn : Elab.sgn' -> bool,
+                  str : Elab.str' -> bool,
+                  decl : Elab.decl' -> bool}
+                 -> Elab.decl -> bool
+    val search : {kind : Elab.kind' -> 'a option,
+                  con : Elab.con' -> 'a option,
+                  exp : Elab.exp' -> 'a option,
+                  sgn_item : Elab.sgn_item' -> 'a option,
+                  sgn : Elab.sgn' -> 'a option,
+                  str : Elab.str' -> 'a option,
+                  decl : Elab.decl' -> 'a option}
+                 -> Elab.decl -> 'a option
+end
+
 end
diff --git a/src/elab_util.sml b/src/elab_util.sml
index f764395d..45446a4e 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -58,7 +58,7 @@ fun mapfold f =
 
               | KError => S.return2 kAll
 
-              | KUnif (_, ref (SOME k)) => mfk' k
+              | KUnif (_, _, ref (SOME k)) => mfk' k
               | KUnif _ => S.return2 kAll
     in
         mfk
@@ -151,7 +151,7 @@ fun mapfoldB {kind = fk, con = fc, bind} =
                                        (CFold (k1', k2'), loc)))
 
               | CError => S.return2 cAll
-              | CUnif (_, _, ref (SOME c)) => mfc' ctx c
+              | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c
               | CUnif _ => S.return2 cAll
     in
         mfc
@@ -417,4 +417,219 @@ fun map {kind, con, sgn_item, sgn} s =
 
 end
 
+structure Decl = struct
+
+datatype binder =
+         RelC of string * Elab.kind
+       | NamedC of string * Elab.kind
+       | RelE of string * Elab.con
+       | NamedE of string * Elab.con
+       | Str of string * Elab.sgn
+       | Sgn of string * Elab.sgn
+
+fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = fst, decl = fd, bind} =
+    let
+        val mfk = Kind.mapfold fk
+
+        fun bind' (ctx, b) =
+            let
+                val b' = case b of
+                             Con.Rel x => RelC x
+                           | Con.Named x => NamedC x
+            in
+                bind (ctx, b')
+            end
+        val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
+
+        fun bind' (ctx, b) =
+            let
+                val b' = case b of
+                             Exp.RelC x => RelC x
+                           | Exp.NamedC x => NamedC x
+                           | Exp.RelE x => RelE x
+                           | Exp.NamedE x => NamedE x
+            in
+                bind (ctx, b')
+            end
+        val mfe = Exp.mapfoldB {kind = fk, con = fc, exp = fe, bind = bind'}
+
+        fun bind' (ctx, b) =
+            let
+                val b' = case b of
+                             Sgn.RelC x => RelC x
+                           | Sgn.NamedC x => NamedC x
+                           | Sgn.Sgn x => Sgn x
+                           | Sgn.Str x => Str x
+            in
+                bind (ctx, b')
+            end
+        val mfsg = Sgn.mapfoldB {kind = fk, con = fc, sgn_item = fsgi, sgn = fsg, bind = bind'}
+
+        fun mfst ctx str acc =
+            S.bindP (mfst' ctx str acc, fst ctx)
+
+        and mfst' ctx (strAll as (str, loc)) =
+            case str of
+                StrConst ds => 
+                S.map2 (ListUtil.mapfoldB (fn (ctx, d)  =>
+                                              (case #1 d of
+                                                   DCon (x, _, k, _) =>
+                                                   bind (ctx, NamedC (x, k))
+                                                 | DVal (x, _, c, _) =>
+                                                   bind (ctx, NamedE (x, c))
+                                                 | DSgn (x, _, sgn) =>
+                                                   bind (ctx, Sgn (x, sgn))
+                                                 | DStr (x, _, sgn, _) =>
+                                                   bind (ctx, Str (x, sgn))
+                                                 | DFfiStr (x, _, sgn) =>
+                                                   bind (ctx, Str (x, sgn)),
+                                               mfd ctx d)) ctx ds,
+                     fn ds' => (StrConst ds', loc))
+              | StrVar _ => S.return2 strAll
+              | StrProj (str, x) =>
+                S.map2 (mfst ctx str,
+                        fn str' =>
+                           (StrProj (str', x), loc))
+              | StrFun (x, n, sgn1, sgn2, str) =>
+                S.bind2 (mfsg ctx sgn1,
+                         fn sgn1' =>
+                            S.bind2 (mfsg ctx sgn2,
+                                     fn sgn2' =>
+                                        S.map2 (mfst ctx str,
+                                                fn str' =>
+                                                   (StrFun (x, n, sgn1', sgn2', str'), loc))))
+              | StrApp (str1, str2) =>
+                S.bind2 (mfst ctx str1,
+                         fn str1' =>
+                            S.map2 (mfst ctx str2,
+                                    fn str2' =>
+                                       (StrApp (str1', str2'), loc)))
+              | StrError => S.return2 strAll
+
+        and mfd ctx d acc =
+            S.bindP (mfd' ctx d acc, fd ctx)
+
+        and mfd' ctx (dAll as (d, loc)) =
+            case d of
+                DCon (x, n, k, c) =>
+                S.bind2 (mfk k,
+                         fn k' =>
+                            S.map2 (mfc ctx c,
+                                    fn c' =>
+                                       (DCon (x, n, k', c'), loc)))
+              | DVal (x, n, c, e) =>
+                S.bind2 (mfc ctx c,
+                         fn c' =>
+                            S.map2 (mfe ctx e,
+                                    fn e' =>
+                                       (DVal (x, n, c', e'), loc)))
+              | DSgn (x, n, sgn) =>
+                S.map2 (mfsg ctx sgn,
+                        fn sgn' =>
+                           (DSgn (x, n, sgn'), loc))
+              | DStr (x, n, sgn, str) =>
+                S.bind2 (mfsg ctx sgn,
+                         fn sgn' =>
+                            S.map2 (mfst ctx str,
+                                    fn str' =>
+                                       (DStr (x, n, sgn', str'), loc)))
+              | DFfiStr (x, n, sgn) =>
+                S.map2 (mfsg ctx sgn,
+                        fn sgn' =>
+                           (DFfiStr (x, n, sgn'), loc))
+    in
+        mfd
+    end
+
+fun mapfold {kind, con, exp, sgn_item, sgn, str, decl} =
+    mapfoldB {kind = kind,
+              con = fn () => con,
+              exp = fn () => exp,
+              sgn_item = fn () => sgn_item,
+              sgn = fn () => sgn,
+              str = fn () => str,
+              decl = fn () => decl,
+              bind = fn ((), _) => ()} ()
+
+fun exists {kind, con, exp, sgn_item, sgn, str, decl} k =
+    case mapfold {kind = fn k => fn () =>
+                                    if kind k then
+                                        S.Return ()
+                                    else
+                                        S.Continue (k, ()),
+                  con = fn c => fn () =>
+                                    if con c then
+                                        S.Return ()
+                                    else
+                                        S.Continue (c, ()),
+                  exp = fn e => fn () =>
+                                    if exp e then
+                                        S.Return ()
+                                    else
+                                        S.Continue (e, ()),
+                  sgn_item = fn sgi => fn () =>
+                                        if sgn_item sgi then
+                                            S.Return ()
+                                        else
+                                            S.Continue (sgi, ()),
+                  sgn = fn x => fn () =>
+                                   if sgn x then
+                                       S.Return ()
+                                   else
+                                       S.Continue (x, ()),
+                  str = fn x => fn () =>
+                                   if str x then
+                                       S.Return ()
+                                   else
+                                       S.Continue (x, ()),
+                  decl = fn x => fn () =>
+                                    if decl x then
+                                        S.Return ()
+                                    else
+                                        S.Continue (x, ())} k () of
+        S.Return _ => true
+      | S.Continue _ => false
+
+fun search {kind, con, exp, sgn_item, sgn, str, decl} k =
+    case mapfold {kind = fn x => fn () =>
+                                    case kind x of
+                                        NONE => S.Continue (x, ())
+                                      | SOME v => S.Return v,
+
+                  con = fn x => fn () =>
+                                   case con x of
+                                       NONE => S.Continue (x, ())
+                                     | SOME v => S.Return v,
+
+                  exp = fn x => fn () =>
+                                   case exp x of
+                                       NONE => S.Continue (x, ())
+                                     | SOME v => S.Return v,
+
+                  sgn_item = fn x => fn () =>
+                                        case sgn_item x of
+                                            NONE => S.Continue (x, ())
+                                          | SOME v => S.Return v,
+
+                  sgn = fn x => fn () =>
+                                   case sgn x of
+                                       NONE => S.Continue (x, ())
+                                     | SOME v => S.Return v,
+
+                  str = fn x => fn () =>
+                                   case str x of
+                                       NONE => S.Continue (x, ())
+                                     | SOME v => S.Return v,
+
+                  decl = fn x => fn () =>
+                                    case decl x of
+                                        NONE => S.Continue (x, ())
+                                      | SOME v => S.Return v
+
+                 } k () of
+        S.Return x => SOME x
+      | S.Continue _ => NONE
+
+end
+
 end
diff --git a/src/elaborate.sml b/src/elaborate.sml
index d8d29fa0..307af12e 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -47,7 +47,7 @@ fun elabExplicitness e =
       | L.Implicit => L'.Implicit
 
 fun occursKind r =
-    U.Kind.exists (fn L'.KUnif (_, r') => r = r'
+    U.Kind.exists (fn L'.KUnif (_, _, r') => r = r'
                     | _ => false)
 
 datatype kunify_error =
@@ -82,21 +82,21 @@ fun unifyKinds' (k1All as (k1, _)) (k2All as (k2, _)) =
           | (L'.KError, _) => ()
           | (_, L'.KError) => ()
 
-          | (L'.KUnif (_, ref (SOME k1All)), _) => unifyKinds' k1All k2All
-          | (_, L'.KUnif (_, ref (SOME k2All))) => unifyKinds' k1All k2All
+          | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' k1All k2All
+          | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' k1All k2All
 
-          | (L'.KUnif (_, r1), L'.KUnif (_, r2)) =>
+          | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) =>
             if r1 = r2 then
                 ()
             else
                 r1 := SOME k2All
 
-          | (L'.KUnif (_, r), _) =>
+          | (L'.KUnif (_, _, r), _) =>
             if occursKind r k2All then
                 err KOccursCheckFailed
             else
                 r := SOME k2All
-          | (_, L'.KUnif (_, r)) =>
+          | (_, L'.KUnif (_, _, r)) =>
             if occursKind r k1All then
                 err KOccursCheckFailed
             else
@@ -159,7 +159,7 @@ in
 
 fun resetKunif () = count := 0
 
-fun kunif () =
+fun kunif loc =
     let
         val n = !count
         val s = if n <= 26 then
@@ -168,7 +168,7 @@ fun kunif () =
                     "U" ^ Int.toString (n - 26)
     in
         count := n + 1;
-        (L'.KUnif (s, ref NONE), dummy)
+        (L'.KUnif (loc, s, ref NONE), dummy)
     end
 
 end
@@ -179,7 +179,7 @@ in
 
 fun resetCunif () = count := 0
 
-fun cunif k =
+fun cunif (loc, k) =
     let
         val n = !count
         val s = if n <= 26 then
@@ -188,7 +188,7 @@ fun cunif k =
                     "U" ^ Int.toString (n - 26)
     in
         count := n + 1;
-        (L'.CUnif (k, s, ref NONE), dummy)
+        (L'.CUnif (loc, k, s, ref NONE), dummy)
     end
 
 end
@@ -199,7 +199,7 @@ fun elabKind (k, loc) =
       | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc)
       | L.KName => (L'.KName, loc)
       | L.KRecord k => (L'.KRecord (elabKind k), loc)
-      | L.KWild => kunif ()
+      | L.KWild => kunif loc
 
 fun foldKind (dom, ran, loc)=
     (L'.KArrow ((L'.KArrow ((L'.KName, loc),
@@ -282,8 +282,8 @@ fun elabCon env (c, loc) =
         let
             val (c1', k1) = elabCon env c1
             val (c2', k2) = elabCon env c2
-            val dom = kunif ()
-            val ran = kunif ()
+            val dom = kunif loc
+            val ran = kunif loc
         in
             checkKind env c1' k1 (L'.KArrow (dom, ran), loc);
             checkKind env c2' k2 dom;
@@ -292,7 +292,7 @@ fun elabCon env (c, loc) =
       | L.CAbs (x, ko, t) =>
         let
             val k' = case ko of
-                         NONE => kunif ()
+                         NONE => kunif loc
                        | SOME k => elabKind k
             val env' = E.pushCRel env x k'
             val (t', tk) = elabCon env' t
@@ -306,7 +306,7 @@ fun elabCon env (c, loc) =
 
       | L.CRecord xcs =>
         let
-            val k = kunif ()
+            val k = kunif loc
 
             val xcs' = map (fn (x, c) =>
                                let
@@ -327,7 +327,7 @@ fun elabCon env (c, loc) =
         let
             val (c1', k1) = elabCon env c1
             val (c2', k2) = elabCon env c2
-            val ku = kunif ()
+            val ku = kunif loc
             val k = (L'.KRecord ku, loc)
         in
             checkKind env c1' k1 k;
@@ -336,8 +336,8 @@ fun elabCon env (c, loc) =
         end
       | L.CFold =>
         let
-            val dom = kunif ()
-            val ran = kunif ()
+            val dom = kunif loc
+            val ran = kunif loc
         in
             ((L'.CFold (dom, ran), loc),
              foldKind (dom, ran, loc))
@@ -347,34 +347,37 @@ fun elabCon env (c, loc) =
         let
             val k' = elabKind k
         in
-            (cunif k', k')
+            (cunif (loc, k'), k')
         end
 
 fun kunifsRemain k =
     case k of
-        L'.KUnif (_, ref NONE) => true
+        L'.KUnif (_, _, ref NONE) => true
       | _ => false
 fun cunifsRemain c =
     case c of
-        L'.CUnif (_, _, ref NONE) => true
-      | _ => false
-
-val kunifsInKind = U.Kind.exists kunifsRemain
-val kunifsInCon = U.Con.exists {kind = kunifsRemain,
-                                con = fn _ => false}
-val kunifsInExp = U.Exp.exists {kind = kunifsRemain,
-                                con = fn _ => false,
-                                exp = fn _ => false}
-
-val cunifsInCon = U.Con.exists {kind = fn _ => false,
-                                con = cunifsRemain}
-val cunifsInExp = U.Exp.exists {kind = fn _ => false,
-                                con = cunifsRemain,
-                                exp = fn _ => false}
+        L'.CUnif (loc, _, _, ref NONE) => SOME loc
+      | _ => NONE
+
+val kunifsInDecl = U.Decl.exists {kind = kunifsRemain,
+                                  con = fn _ => false,
+                                  exp = fn _ => false,
+                                  sgn_item = fn _ => false,
+                                  sgn = fn _ => false,
+                                  str = fn _ => false,
+                                  decl = fn _ => false}
+
+val cunifsInDecl = U.Decl.search {kind = fn _ => NONE,
+                                  con = cunifsRemain,
+                                  exp = fn _ => NONE,
+                                  sgn_item = fn _ => NONE,
+                                  sgn = fn _ => NONE,
+                                  str = fn _ => NONE,
+                                  decl = fn _ => NONE}
 
 fun occursCon r =
     U.Con.exists {kind = fn _ => false,
-                  con = fn L'.CUnif (_, _, r') => r = r'
+                  con = fn L'.CUnif (_, _, _, r') => r = r'
                          | _ => false}
 
 datatype cunify_error =
@@ -461,7 +464,7 @@ exception CUnify of L'.con * L'.con * cunify_error
 
 fun hnormKind (kAll as (k, _)) =
     case k of
-        L'.KUnif (_, ref (SOME k)) => hnormKind k
+        L'.KUnif (_, _, ref (SOME k)) => hnormKind k
       | _ => kAll
 
 fun kindof env (c, loc) =
@@ -500,7 +503,7 @@ fun kindof env (c, loc) =
       | L'.CFold (dom, ran) => foldKind (dom, ran, loc)
 
       | L'.CError => kerror
-      | L'.CUnif (k, _, _) => k
+      | L'.CUnif (_, k, _, _) => k
 
 fun unifyRecordCons env (c1, c2) =
     let
@@ -523,8 +526,8 @@ and recordSummary env c : record_summary =
              unifs = #unifs s1 @ #unifs s2,
              others = #others s1 @ #others s2}
         end
-      | (L'.CUnif (_, _, ref (SOME c)), _) => recordSummary env c
-      | c' as (L'.CUnif (_, _, r), _) => {fields = [], unifs = [(c', r)], others = []}
+      | (L'.CUnif (_, _, _, ref (SOME c)), _) => recordSummary env c
+      | c' as (L'.CUnif (_, _, _, r), _) => {fields = [], unifs = [(c', r)], others = []}
       | c' => {fields = [], unifs = [], others = [c']}
 
 and consEq env (c1, c2) =
@@ -577,7 +580,7 @@ and unifySummaries env (k, s1 : record_summary, s2 : record_summary) =
               | (_, _, (_, r) :: rest) =>
                 let
                     val r' = ref NONE
-                    val cr' = (L'.CUnif (k, "recd", r'), dummy)
+                    val cr' = (L'.CUnif (dummy, k, "recd", r'), dummy)
 
                     val prefix = case (fs, others) of
                                      ([], other :: others) =>
@@ -626,7 +629,7 @@ and unifySummaries env (k, s1 : record_summary, s2 : record_summary) =
 
 and hnormCon env (cAll as (c, loc)) =
     case c of
-        L'.CUnif (_, _, ref (SOME c)) => hnormCon env c
+        L'.CUnif (_, _, _, ref (SOME c)) => hnormCon env c
 
       | L'.CNamed xn =>
         (case E.lookupCNamed env xn of
@@ -758,22 +761,22 @@ and unifyCons'' env (c1All as (c1, _)) (c2All as (c2, _)) =
           | (L'.CError, _) => ()
           | (_, L'.CError) => ()
 
-          | (L'.CUnif (_, _, ref (SOME c1All)), _) => unifyCons' env c1All c2All
-          | (_, L'.CUnif (_, _, ref (SOME c2All))) => unifyCons' env c1All c2All
+          | (L'.CUnif (_, _, _, ref (SOME c1All)), _) => unifyCons' env c1All c2All
+          | (_, L'.CUnif (_, _, _, ref (SOME c2All))) => unifyCons' env c1All c2All
 
-          | (L'.CUnif (k1, _, r1), L'.CUnif (k2, _, r2)) =>
+          | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
             if r1 = r2 then
                 ()
             else
                 (unifyKinds k1 k2;
                  r1 := SOME c2All)
 
-          | (L'.CUnif (_, _, r), _) =>
+          | (L'.CUnif (_, _, _, r), _) =>
             if occursCon r c2All then
                 err COccursCheckFailed
             else
                 r := SOME c2All
-          | (_, L'.CUnif (_, _, r)) =>
+          | (_, L'.CUnif (_, _, _, r)) =>
             if occursCon r c1All then
                 err COccursCheckFailed
             else
@@ -898,7 +901,7 @@ fun elabHead env (e as (_, loc)) t =
             case hnormCon env t of
                 (L'.TCFun (L'.Implicit, x, k, t'), _) =>
                 let
-                    val u = cunif k
+                    val u = cunif (loc, k)
                 in
                     unravel (subConInCon (0, u) t',
                              (L'.ECApp (e, u), loc))
@@ -954,8 +957,8 @@ fun elabExp env (e, loc) =
             val (e1', t1) = elabHead env e1' t1
             val (e2', t2) = elabExp env e2
 
-            val dom = cunif ktype
-            val ran = cunif ktype
+            val dom = cunif (loc, ktype)
+            val ran = cunif (loc, ktype)
             val t = (L'.TFun (dom, ran), dummy)
         in
             checkCon env e1' t1 t;
@@ -965,7 +968,7 @@ fun elabExp env (e, loc) =
       | L.EAbs (x, to, e) =>
         let
             val t' = case to of
-                         NONE => cunif ktype
+                         NONE => cunif (loc, ktype)
                        | SOME t =>
                          let
                              val (t', tk) = elabCon env t
@@ -1034,8 +1037,8 @@ fun elabExp env (e, loc) =
             val (e', et) = elabExp env e
             val (c', ck) = elabCon env c
 
-            val ft = cunif ktype
-            val rest = cunif ktype_record
+            val ft = cunif (loc, ktype)
+            val rest = cunif (loc, ktype_record)
         in
             checkKind env c' ck kname;
             checkCon env e' et (L'.TRecord (L'.CConcat ((L'.CRecord (ktype, [(c', ft)]), loc), rest), loc), loc);
@@ -1044,36 +1047,22 @@ fun elabExp env (e, loc) =
 
       | L.EFold =>
         let
-            val dom = kunif ()
+            val dom = kunif loc
         in
             ((L'.EFold dom, loc), foldType (dom, loc))
         end
             
 
 datatype decl_error =
-         KunifsRemainKind of ErrorMsg.span * L'.kind
-       | KunifsRemainCon of ErrorMsg.span * L'.con
-       | KunifsRemainExp of ErrorMsg.span * L'.exp
-       | CunifsRemainCon of ErrorMsg.span * L'.con
-       | CunifsRemainExp of ErrorMsg.span * L'.exp
+         KunifsRemain of ErrorMsg.span
+       | CunifsRemain of ErrorMsg.span
 
 fun declError env err =
     case err of
-        KunifsRemainKind (loc, k) =>
-        (ErrorMsg.errorAt loc "Some kind unification variables are undetermined in kind";
-         eprefaces' [("Kind", p_kind k)])
-      | KunifsRemainCon (loc, c) =>
-        (ErrorMsg.errorAt loc "Some kind unification variables are undetermined in constructor";
-         eprefaces' [("Constructor", p_con env c)])
-      | KunifsRemainExp (loc, e) =>
-        (ErrorMsg.errorAt loc "Some kind unification variables are undetermined in expression";
-         eprefaces' [("Expression", p_exp env e)])
-      | CunifsRemainCon (loc, c) =>
-        (ErrorMsg.errorAt loc "Some constructor unification variables are undetermined in constructor";
-         eprefaces' [("Constructor", p_con env c)])
-      | CunifsRemainExp (loc, e) =>
-        (ErrorMsg.errorAt loc "Some constructor unification variables are undetermined in expression";
-         eprefaces' [("Expression", p_exp env e)])
+        KunifsRemain loc =>
+        ErrorMsg.errorAt loc "Some kind unification variables are undetermined in declaration"
+      | CunifsRemain loc =>
+        ErrorMsg.errorAt loc "Some constructor unification variables are undetermined in declaration"
 
 datatype sgn_error =
          UnboundSgn of ErrorMsg.span * string
@@ -1164,107 +1153,68 @@ fun strError env err =
 val hnormSgn = E.hnormSgn
 
 fun elabSgn_item ((sgi, loc), env) =
-    let
-        
-    in
-        resetKunif ();
-        resetCunif ();
-        case sgi of
-            L.SgiConAbs (x, k) =>
-            let
-                val k' = elabKind k
-
-                val (env', n) = E.pushCNamed env x k' NONE
-            in
-                if ErrorMsg.anyErrors () then
-                    ()
-                else (
-                    if kunifsInKind k' then
-                        declError env (KunifsRemainKind (loc, k'))
-                    else
-                        ()
-                    );
-
-                ([(L'.SgiConAbs (x, n, k'), loc)], env')
-            end
-
-          | L.SgiCon (x, ko, c) =>
-            let
-                val k' = case ko of
-                             NONE => kunif ()
-                           | SOME k => elabKind k
-
-                val (c', ck) = elabCon env c
-                val (env', n) = E.pushCNamed env x k' (SOME c')
-            in
-                checkKind env c' ck k';
-
-                if ErrorMsg.anyErrors () then
-                    ()
-                else (
-                    if kunifsInKind k' then
-                        declError env (KunifsRemainKind (loc, k'))
-                    else
-                        ();
+    case sgi of
+        L.SgiConAbs (x, k) =>
+        let
+            val k' = elabKind k
 
-                    if kunifsInCon c' then
-                        declError env (KunifsRemainCon (loc, c'))
-                    else
-                        ()
-                    );
+            val (env', n) = E.pushCNamed env x k' NONE
+        in
+            ([(L'.SgiConAbs (x, n, k'), loc)], env')
+        end
 
-                ([(L'.SgiCon (x, n, k', c'), loc)], env')
-            end
+      | L.SgiCon (x, ko, c) =>
+        let
+            val k' = case ko of
+                         NONE => kunif loc
+                       | SOME k => elabKind k
 
-          | L.SgiVal (x, c) =>
-            let
-                val (c', ck) = elabCon env c
+            val (c', ck) = elabCon env c
+            val (env', n) = E.pushCNamed env x k' (SOME c')
+        in
+            checkKind env c' ck k';
 
-                val (env', n) = E.pushENamed env x c'
-            in
-                (unifyKinds ck ktype
-                 handle KUnify ue => strError env (NotType (ck, ue)));
+            ([(L'.SgiCon (x, n, k', c'), loc)], env')
+        end
 
-                if ErrorMsg.anyErrors () then
-                    ()
-                else (
-                    if kunifsInCon c' then
-                        declError env (KunifsRemainCon (loc, c'))
-                    else
-                        ()
-                    );
+      | L.SgiVal (x, c) =>
+        let
+            val (c', ck) = elabCon env c
 
-                ([(L'.SgiVal (x, n, c'), loc)], env')
-            end
+            val (env', n) = E.pushENamed env x c'
+        in
+            (unifyKinds ck ktype
+             handle KUnify ue => strError env (NotType (ck, ue)));
 
-          | L.SgiStr (x, sgn) =>
-            let
-                val sgn' = elabSgn env sgn
-                val (env', n) = E.pushStrNamed env x sgn'
-            in
-                ([(L'.SgiStr (x, n, sgn'), loc)], env')
-            end
+            ([(L'.SgiVal (x, n, c'), loc)], env')
+        end
 
-          | L.SgiSgn (x, sgn) =>
-            let
-                val sgn' = elabSgn env sgn
-                val (env', n) = E.pushSgnNamed env x sgn'
-            in
-                ([(L'.SgiSgn (x, n, sgn'), loc)], env')
-            end
+      | L.SgiStr (x, sgn) =>
+        let
+            val sgn' = elabSgn env sgn
+            val (env', n) = E.pushStrNamed env x sgn'
+        in
+            ([(L'.SgiStr (x, n, sgn'), loc)], env')
+        end
 
-          | L.SgiInclude sgn =>
-            let
-                val sgn' = elabSgn env sgn
-            in
-                case #1 (hnormSgn env sgn') of
-                    L'.SgnConst sgis =>
-                    (sgis, foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis)
-                  | _ => (sgnError env (NotIncludable sgn');
-                          ([], env))
-            end
+      | L.SgiSgn (x, sgn) =>
+        let
+            val sgn' = elabSgn env sgn
+            val (env', n) = E.pushSgnNamed env x sgn'
+        in
+            ([(L'.SgiSgn (x, n, sgn'), loc)], env')
+        end
 
-    end
+      | L.SgiInclude sgn =>
+        let
+            val sgn' = elabSgn env sgn
+        in
+            case #1 (hnormSgn env sgn') of
+                L'.SgnConst sgis =>
+                (sgis, foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis)
+              | _ => (sgnError env (NotIncludable sgn');
+                      ([], env))
+        end
 
 and elabSgn env (sgn, loc) =
     case sgn of
@@ -1580,133 +1530,90 @@ fun subSgn env sgn1 (sgn2 as (_, loc2)) =
 
 
 fun elabDecl ((d, loc), env) =
-    let
-        
-    in
-        resetKunif ();
-        resetCunif ();
-        case d of
-            L.DCon (x, ko, c) =>
-            let
-                val k' = case ko of
-                             NONE => kunif ()
-                           | SOME k => elabKind k
-
-                val (c', ck) = elabCon env c
-                val (env', n) = E.pushCNamed env x k' (SOME c')
-            in
-                checkKind env c' ck k';
-
-                if ErrorMsg.anyErrors () then
-                    ()
-                else (
-                    if kunifsInKind k' then
-                        declError env (KunifsRemainKind (loc, k'))
-                    else
-                        ();
-
-                    if kunifsInCon c' then
-                        declError env (KunifsRemainCon (loc, c'))
-                    else
-                        ()
-                    );
+    case d of
+        L.DCon (x, ko, c) =>
+        let
+            val k' = case ko of
+                         NONE => kunif loc
+                       | SOME k => elabKind k
 
-                ([(L'.DCon (x, n, k', c'), loc)], env')
-            end
-          | L.DVal (x, co, e) =>
-            let
-                val (c', ck) = case co of
-                                   NONE => (cunif ktype, ktype)
-                                 | SOME c => elabCon env c
+            val (c', ck) = elabCon env c
+            val (env', n) = E.pushCNamed env x k' (SOME c')
+        in
+            checkKind env c' ck k';
 
-                val (e', et) = elabExp env e
-                val (env', n) = E.pushENamed env x c'
-            in
-                checkCon env e' et c';
+            ([(L'.DCon (x, n, k', c'), loc)], env')
+        end
+      | L.DVal (x, co, e) =>
+        let
+            val (c', ck) = case co of
+                               NONE => (cunif (loc, ktype), ktype)
+                             | SOME c => elabCon env c
 
-                if ErrorMsg.anyErrors () then
-                    ()
-                else (
-                    if kunifsInCon c' then
-                        declError env (KunifsRemainCon (loc, c'))
-                    else
-                        ();
+            val (e', et) = elabExp env e
+            val (env', n) = E.pushENamed env x c'
+        in
+            checkCon env e' et c';
 
-                    if cunifsInCon c' then
-                        declError env (CunifsRemainCon (loc, c'))
-                    else
-                        ();
+            ([(L'.DVal (x, n, c', e'), loc)], env')
+        end
 
-                    if kunifsInExp e' then
-                        declError env (KunifsRemainExp (loc, e'))
-                    else
-                        ();
+      | L.DSgn (x, sgn) =>
+        let
+            val sgn' = elabSgn env sgn
+            val (env', n) = E.pushSgnNamed env x sgn'
+        in
+            ([(L'.DSgn (x, n, sgn'), loc)], env')
+        end
 
-                    if cunifsInExp e' then
-                        declError env (CunifsRemainExp (loc, e'))
-                    else
-                        ());
+      | L.DStr (x, sgno, str) =>
+        let
+            val formal = Option.map (elabSgn env) sgno
+            val (str', actual) = elabStr env str
 
-                ([(L'.DVal (x, n, c', e'), loc)], env')
-            end
+            val sgn' = case formal of
+                           NONE => selfifyAt env {str = str', sgn = actual}
+                         | SOME formal =>
+                           (subSgn env actual formal;
+                            formal)
 
-          | L.DSgn (x, sgn) =>
-            let
-                val sgn' = elabSgn env sgn
-                val (env', n) = E.pushSgnNamed env x sgn'
-            in
-                ([(L'.DSgn (x, n, sgn'), loc)], env')
-            end
+            val (env', n) = E.pushStrNamed env x sgn'
+        in
+            case #1 (hnormSgn env sgn') of
+                L'.SgnFun _ =>
+                (case #1 str' of
+                     L'.StrFun _ => ()
+                   | _ => strError env (FunctorRebind loc))
+              | _ => ();
 
-          | L.DStr (x, sgno, str) =>
-            let
-                val formal = Option.map (elabSgn env) sgno
-                val (str', actual) = elabStr env str
+            ([(L'.DStr (x, n, sgn', str'), loc)], env')
+        end
 
-                val sgn' = case formal of
-                               NONE => selfifyAt env {str = str', sgn = actual}
-                             | SOME formal =>
-                               (subSgn env actual formal;
-                                formal)
+      | L.DFfiStr (x, sgn) =>
+        let
+            val sgn' = elabSgn env sgn
 
-                val (env', n) = E.pushStrNamed env x sgn'
-            in
-                case #1 (hnormSgn env sgn') of
-                    L'.SgnFun _ =>
-                    (case #1 str' of
-                         L'.StrFun _ => ()
-                       | _ => strError env (FunctorRebind loc))
-                  | _ => ();
-
-                ([(L'.DStr (x, n, sgn', str'), loc)], env')
-            end
+            val (env', n) = E.pushStrNamed env x sgn'
+        in
+            ([(L'.DFfiStr (x, n, sgn'), loc)], env')
+        end
 
-          | L.DFfiStr (x, sgn) =>
+      | L.DOpen (m, ms) =>
+        case E.lookupStr env m of
+            NONE => (strError env (UnboundStr (loc, m));
+                     ([], env))
+          | SOME (n, sgn) =>
             let
-                val sgn' = elabSgn env sgn
-
-                val (env', n) = E.pushStrNamed env x sgn'
+                val (_, sgn) = foldl (fn (m, (str, sgn)) =>
+                                         case E.projectStr env {str = str, sgn = sgn, field = m} of
+                                             NONE => (strError env (UnboundStr (loc, m));
+                                                      (strerror, sgnerror))
+                                           | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
+                                     ((L'.StrVar n, loc), sgn) ms
             in
-                ([(L'.DFfiStr (x, n, sgn'), loc)], env')
+                dopen env {str = n, strs = ms, sgn = sgn}
             end
 
-          | L.DOpen (m, ms) =>
-            (case E.lookupStr env m of
-                 NONE => (strError env (UnboundStr (loc, m));
-                          ([], env))
-               | SOME (n, sgn) =>
-                 let
-                     val (_, sgn) = foldl (fn (m, (str, sgn)) =>
-                                              case E.projectStr env {str = str, sgn = sgn, field = m} of
-                                                  NONE => (strError env (UnboundStr (loc, m));
-                                                           (strerror, sgnerror))
-                                                | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
-                                          ((L'.StrVar n, loc), sgn) ms
-                 in
-                     dopen env {str = n, strs = ms, sgn = sgn}
-                 end)
-    end
-
 and elabStr env (str, loc) =
     case str of
         L.StrConst ds =>
@@ -1844,7 +1751,30 @@ fun elabFile basis env file =
         val () = discoverC float "float"
         val () = discoverC string "string"
 
-        val (file, _) = ListUtil.foldlMapConcat elabDecl env' file
+        fun elabDecl' (d, env) =
+            let
+                val () = resetKunif ()
+                val () = resetCunif ()
+                val (ds, env) = elabDecl (d, env)
+            in
+                if ErrorMsg.anyErrors () then
+                    ()
+                else (
+                    if List.exists kunifsInDecl ds then
+                        declError env (KunifsRemain (#2 d))
+                    else
+                        ();
+                    
+                    case ListUtil.search cunifsInDecl ds of
+                        NONE => ()
+                      | SOME loc =>
+                        declError env (CunifsRemain loc)
+                    );
+
+                (ds, env)
+            end
+
+        val (file, _) = ListUtil.foldlMapConcat elabDecl' env' file
     in
         (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file
     end
diff --git a/src/explify.sml b/src/explify.sml
index 91accd81..0f416067 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -39,7 +39,7 @@ fun explifyKind (k, loc) =
       | L.KRecord k => (L'.KRecord (explifyKind k), loc)
 
       | L.KError => raise Fail ("explifyKind: KError at " ^ EM.spanToString loc)
-      | L.KUnif (_, ref (SOME k)) => explifyKind k
+      | L.KUnif (_, _, ref (SOME k)) => explifyKind k
       | L.KUnif _ => raise Fail ("explifyKind: KUnif at " ^ EM.spanToString loc)
 
 fun explifyCon (c, loc) =
@@ -62,7 +62,7 @@ fun explifyCon (c, loc) =
       | L.CFold (dom, ran) => (L'.CFold (explifyKind dom, explifyKind ran), loc)
 
       | L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc)
-      | L.CUnif (_, _, ref (SOME c)) => explifyCon c
+      | L.CUnif (_, _, _, ref (SOME c)) => explifyCon c
       | L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc)
 
 fun explifyExp (e, loc) =