Add a new scoping check for unification variables, to fix a type inference bug

10 files changed, 310 insertions, 181 deletions

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
 
diff --git a/src/elab_env.sml b/src/elab_env.sml
index e53c1538..ed96782e 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -484,7 +484,7 @@ fun class_name_in (c, _) =
     case c of
         CNamed n => SOME (ClNamed n)
       | CModProj x => SOME (ClProj x)
-      | CUnif (_, _, _, _, ref (SOME c)) => class_name_in c
+      | CUnif (_, _, _, _, ref (Known c)) => class_name_in c
       | _ => NONE
 
 fun isClass (env : env) c =
@@ -498,7 +498,7 @@ fun isClass (env : env) c =
 fun class_head_in c =
     case #1 c of
         CApp (f, _) => class_head_in f
-      | CUnif (_, _, _, _, ref (SOME c)) => class_head_in c
+      | CUnif (_, _, _, _, ref (Known c)) => class_head_in c
       | _ => class_name_in c
 
 exception Unify
@@ -512,16 +512,16 @@ fun unifyKinds (k1, k2) =
       | (KUnit, KUnit) => ()
       | (KTuple ks1, KTuple ks2) => (ListPair.appEq unifyKinds (ks1, ks2)
                                      handle ListPair.UnequalLengths => raise Unify)
-      | (KUnif (_, _, ref (SOME k1)), _) => unifyKinds (k1, k2)
-      | (_, KUnif (_, _, ref (SOME k2))) => unifyKinds (k1, k2)
+      | (KUnif (_, _, ref (KKnown k1)), _) => unifyKinds (k1, k2)
+      | (_, KUnif (_, _, ref (KKnown k2))) => unifyKinds (k1, k2)
       | (KRel n1, KRel n2) => if n1 = n2 then () else raise Unify
       | (KFun (_, k1), KFun (_, k2)) => unifyKinds (k1, k2)
       | _ => raise Unify
 
 fun eqCons (c1, c2) =
     case (#1 c1, #1 c2) of
-        (CUnif (nl, _, _, _, ref (SOME c1)), _) => eqCons (mliftConInCon nl c1, c2)
-      | (_, CUnif (nl, _, _, _, ref (SOME c2))) => eqCons (c1, mliftConInCon nl c2)
+        (CUnif (nl, _, _, _, ref (Known c1)), _) => eqCons (mliftConInCon nl c1, c2)
+      | (_, CUnif (nl, _, _, _, ref (Known c2))) => eqCons (c1, mliftConInCon nl c2)
 
       | (CRel n1, CRel n2) => if n1 = n2 then () else raise Unify
 
@@ -569,8 +569,8 @@ fun unifyCons (hnorm : con -> con) rs =
     let
         fun unify d (c1, c2) =
             case (#1 (hnorm c1), #1 (hnorm c2)) of
-                (CUnif (nl, _, _, _, ref (SOME c1)), _) => unify d (mliftConInCon nl c1, c2)
-              | (_, CUnif (nl, _, _, _, ref (SOME c2))) => unify d (c1, mliftConInCon nl c2)
+                (CUnif (nl, _, _, _, ref (Known c1)), _) => unify d (mliftConInCon nl c1, c2)
+              | (_, CUnif (nl, _, _, _, ref (Known c2))) => unify d (c1, mliftConInCon nl c2)
 
               | (CUnif _, _) => ()
 
@@ -663,7 +663,7 @@ fun unifySubst (rs : con list) =
 exception Bad of con * con
 
 val hasUnif = U.Con.exists {kind = fn _ => false,
-                            con = fn CUnif (_, _, _, _, ref NONE) => true
+                            con = fn CUnif (_, _, _, _, ref (Unknown _)) => true
                                    | _ => false}
 
 fun startsWithUnif c =
@@ -697,9 +697,9 @@ fun resolveClass (hnorm : con -> con) (consEq : con * con -> bool) (env : env) =
 
                                         fun isRecord () =
                                             let
-                                                val rk = ref NONE
+                                                val rk = ref (KUnknown (fn _ => true))
                                                 val k = (KUnif (loc, "k", rk), loc)
-                                                val r = ref NONE
+                                                val r = ref (Unknown (fn _ => true))
                                                 val rc = (CUnif (0, loc, k, "x", r), loc)
                                             in
                                                 ((CApp (f, rc), loc),
diff --git a/src/elab_err.sig b/src/elab_err.sig
index a66cf61f..14133d08 100644
--- a/src/elab_err.sig
+++ b/src/elab_err.sig
@@ -35,6 +35,7 @@ signature ELAB_ERR = sig
     datatype kunify_error =
              KOccursCheckFailed of Elab.kind * Elab.kind
            | KIncompatible of Elab.kind * Elab.kind
+           | KScope of Elab.kind * Elab.kind
 
     val kunifyError : ElabEnv.env -> kunify_error -> unit
 
@@ -59,6 +60,7 @@ signature ELAB_ERR = sig
            | TooLifty of ErrorMsg.span * ErrorMsg.span
            | TooUnify of Elab.con * Elab.con
            | TooDeep
+           | CScope of Elab.con * Elab.con
 
     val cunifyError : ElabEnv.env -> cunify_error -> unit
 
diff --git a/src/elab_err.sml b/src/elab_err.sml
index 84c8c61f..2bf059e6 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -63,6 +63,7 @@ fun kindError env err =
 datatype kunify_error =
          KOccursCheckFailed of kind * kind
        | KIncompatible of kind * kind
+       | KScope of kind * kind
 
 fun kunifyError env err =
     case err of
@@ -74,7 +75,10 @@ fun kunifyError env err =
         eprefaces "Incompatible kinds"
         [("Kind 1", p_kind env k1),
          ("Kind 2", p_kind env k2)]
-
+      | KScope (k1, k2) =>
+        eprefaces "Scoping prevents kind unification"
+        [("Kind 1", p_kind env k1),
+         ("Kind 2", p_kind env k2)]
 
 fun p_con env c = P.p_con env (simplCon env c)
 
@@ -122,6 +126,7 @@ datatype cunify_error =
        | TooLifty of ErrorMsg.span * ErrorMsg.span
        | TooUnify of con * con
        | TooDeep
+       | CScope of con * con
 
 fun cunifyError env err =
     case err of
@@ -167,6 +172,10 @@ fun cunifyError env err =
          eprefaces' [("Replacement", p_con env c1),
                      ("Body", p_con env c2)])
       | TooDeep => ErrorMsg.error "Can't reverse-engineer unification variable lifting"
+      | CScope (c1, c2) =>
+        eprefaces "Scoping prevents constructor unification"
+                  [("Have", p_con env c1),
+                   ("Need", p_con env c2)]
 
 datatype exp_error =
        UnboundExp of ErrorMsg.span * string
diff --git a/src/elab_ops.sml b/src/elab_ops.sml
index 0af2f4e7..dc9f69a4 100644
--- a/src/elab_ops.sml
+++ b/src/elab_ops.sml
@@ -156,7 +156,7 @@ fun reset () = (identity := 0;
 
 fun hnormCon env (cAll as (c, loc)) =
     case c of
-        CUnif (nl, _, _, _, ref (SOME c)) => (#1 (hnormCon env (E.mliftConInCon nl c)), loc)
+        CUnif (nl, _, _, _, ref (Known c)) => (#1 (hnormCon env (E.mliftConInCon nl c)), loc)
 
       | CNamed xn =>
         (case E.lookupCNamed env xn of
@@ -277,7 +277,7 @@ fun hnormCon env (cAll as (c, loc)) =
                                   let
                                       fun cunif () =
                                           let
-                                              val r = ref NONE
+                                              val r = ref (Unknown (fn _ => true))
                                           in
                                               (r, (CUnif (0, loc, (KType, loc), "_", r), loc))
                                           end
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 2b8dc5f4..d292d7c5 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -54,9 +54,9 @@ fun p_kind' par env (k, _) =
                           string ")"]
 
       | KError => string "<ERROR>"
-      | KUnif (_, _, ref (SOME k)) => p_kind' par env k
+      | KUnif (_, _, ref (KKnown k)) => p_kind' par env k
       | KUnif (_, s, _) => string ("<UNIF:" ^ s ^ ">")
-      | KTupleUnif (_, _, ref (SOME k)) => p_kind' par env k
+      | KTupleUnif (_, _, ref (KKnown k)) => p_kind' par env k
       | KTupleUnif (_, nks, _) => box [string "(",
                                        p_list_sep (box [space, string "*", space])
                                                   (fn (n, k) => box [string (Int.toString n ^ ":"),
@@ -202,7 +202,7 @@ fun p_con' par env (c, _) =
                              string (Int.toString n)]
 
       | CError => string "<ERROR>"
-      | CUnif (nl, _, _, _, ref (SOME c)) => p_con' par env (E.mliftConInCon nl c)
+      | CUnif (nl, _, _, _, ref (Known c)) => p_con' par env (E.mliftConInCon nl c)
       | CUnif (nl, _, k, s, _) => box [string ("<UNIF:" ^ s ^ "::"),
                                        p_kind env k,
                                        case nl of
diff --git a/src/elab_util.sig b/src/elab_util.sig
index 2998e7db..8a013554 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -64,6 +64,13 @@ structure Con : sig
     val map : {kind : Elab.kind' -> Elab.kind',
                con : Elab.con' -> Elab.con'}
               -> Elab.con -> Elab.con
+    val appB : {kind : 'context -> Elab.kind' -> unit,
+                con : 'context -> Elab.con' -> unit,
+                bind : 'context * binder -> 'context}
+               -> 'context -> (Elab.con -> unit)
+    val app : {kind : Elab.kind' -> unit,
+               con : Elab.con' -> unit}
+              -> Elab.con -> unit
     val existsB : {kind : 'context * Elab.kind' -> bool,
                   con : 'context * Elab.con' -> bool,
                    bind : 'context * binder -> 'context}
diff --git a/src/elab_util.sml b/src/elab_util.sml
index bf0185b1..df78616a 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -75,10 +75,10 @@ fun mapfoldB {kind, bind} =
 
               | KError => S.return2 kAll
 
-              | KUnif (_, _, ref (SOME k)) => mfk' ctx k
+              | KUnif (_, _, ref (KKnown k)) => mfk' ctx k
               | KUnif _ => S.return2 kAll
 
-              | KTupleUnif (_, _, ref (SOME k)) => mfk' ctx k
+              | KTupleUnif (_, _, ref (KKnown k)) => mfk' ctx k
               | KTupleUnif (loc, nks, r) =>
                 S.map2 (ListUtil.mapfold (fn (n, k) =>
                                              S.map2 (mfk ctx k,
@@ -217,7 +217,7 @@ fun mapfoldB {kind = fk, con = fc, bind} =
                            (CProj (c', n), loc))
 
               | CError => S.return2 cAll
-              | CUnif (nl, _, _, _, ref (SOME c)) => mfc' ctx (!mliftConInCon nl c)
+              | CUnif (nl, _, _, _, ref (Known c)) => mfc' ctx (!mliftConInCon nl c)
               | CUnif _ => S.return2 cAll
                         
               | CKAbs (x, c) =>
@@ -256,6 +256,19 @@ fun map {kind, con} s =
         S.Return () => raise Fail "ElabUtil.Con.map: Impossible"
       | S.Continue (s, ()) => s
 
+fun appB {kind, con, bind} ctx c =
+    case mapfoldB {kind = fn ctx => fn k => fn () => (kind ctx k; S.Continue (k, ())),
+                   con = fn ctx => fn c => fn () => (con ctx c; S.Continue (c, ())),
+                   bind = bind} ctx c () of
+        S.Continue _ => ()
+      | S.Return _ => raise Fail "ElabUtil.Con.appB: Impossible"
+
+fun app {kind, con} s =
+    case mapfold {kind = fn k => fn () => (kind k; S.Continue (k, ())),
+                  con = fn c => fn () => (con c; S.Continue (c, ()))} s () of
+        S.Return () => raise Fail "ElabUtil.Con.app: Impossible"
+      | S.Continue _ => ()
+
 fun existsB {kind, con, bind} ctx c =
     case mapfoldB {kind = fn ctx => fn k => fn () =>
                                                if kind (ctx, k) then
diff --git a/src/elaborate.sml b/src/elaborate.sml
index a1da9feb..34cb12b8 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -63,6 +63,29 @@
      U.Kind.exists (fn L'.KUnif (_, _, r') => r = r'
                      | _ => false)
 
+ fun validateCon env c =
+     (U.Con.appB {kind = fn env' => fn k => case k of
+                                                L'.KRel n => ignore (E.lookupKRel env' n)
+                                              | L'.KUnif (_, _, r as ref (L'.KUnknown f)) =>
+                                                r := L'.KUnknown (fn k => f k andalso validateKind env' k)
+                                              | _ => (),
+                  con = fn env' => fn c => case c of
+                                               L'.CRel n => ignore (E.lookupCRel env' n)
+                                             | L'.CNamed n => ignore (E.lookupCNamed env' n)
+                                             | L'.CModProj (n, _, _) => ignore (E.lookupStrNamed env' n)
+                                             | L'.CUnif (_, _, _, _, r as ref (L'.Unknown f)) =>
+                                               r := L'.Unknown (fn c => f c andalso validateCon env' c)
+                                             | _ => (),
+                  bind = fn (env', b) => case b of
+                                             U.Con.RelK x => E.pushKRel env' x
+                                           | U.Con.RelC (x, k) => E.pushCRel env' x k
+                                           | U.Con.NamedC (x, n, k, co) => E.pushCNamedAs env x n k co}
+                 env c;
+      true)
+     handle _ => false
+
+ and validateKind env k = validateCon env (L'.CRecord (k, []), ErrorMsg.dummySpan)
+
  exception KUnify' of kunify_error
 
  fun unifyKinds' env (k1All as (k1, _)) (k2All as (k2, _)) =
@@ -93,38 +116,49 @@
            | (L'.KError, _) => ()
            | (_, L'.KError) => ()
 
-           | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' env k1All k2All
-           | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' env k1All k2All
+           | (L'.KUnif (_, _, ref (L'.KKnown k1All)), _) => unifyKinds' env k1All k2All
+           | (_, L'.KUnif (_, _, ref (L'.KKnown k2All))) => unifyKinds' env k1All k2All
 
-           | (L'.KTupleUnif (_, _, ref (SOME k)), _) => unifyKinds' env k k2All
-           | (_, L'.KTupleUnif (_, _, ref (SOME k))) => unifyKinds' env k1All k
+           | (L'.KTupleUnif (_, _, ref (L'.KKnown k)), _) => unifyKinds' env k k2All
+           | (_, L'.KTupleUnif (_, _, ref (L'.KKnown k))) => unifyKinds' env k1All k
 
-           | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) =>
+           | (L'.KUnif (_, _, r1 as ref (L'.KUnknown f1)), L'.KUnif (_, _, r2 as ref (L'.KUnknown f2))) =>
              if r1 = r2 then
                  ()
              else
-                 r1 := SOME k2All
+                 (r1 := L'.KKnown k2All;
+                  r2 := L'.KUnknown (fn x => f1 x andalso f2 x))
 
-           | (L'.KUnif (_, _, r), _) =>
+           | (L'.KUnif (_, _, r as ref (L'.KUnknown f)), _) =>
              if occursKind r k2All then
                  err KOccursCheckFailed
+             else if not (f k2All) then
+                 err KScope
              else
-                 r := SOME k2All
-           | (_, L'.KUnif (_, _, r)) =>
+                 r := L'.KKnown k2All
+           | (_, L'.KUnif (_, _, r as ref (L'.KUnknown f))) =>
              if occursKind r k1All then
                  err KOccursCheckFailed
+             else if not (f k1All) then
+                 err KScope
+             else
+                 r := L'.KKnown k1All
+
+           | (L'.KTupleUnif (_, nks, r as ref (L'.KUnknown f)), L'.KTuple ks) =>
+             if not (f k2All) then
+                 err KScope
+             else
+                 ((app (fn (n, k) => unifyKinds' env k (List.nth (ks, n-1))) nks;
+                   r := L'.KKnown k2All)
+                  handle Subscript => err KIncompatible)
+           | (L'.KTuple ks, L'.KTupleUnif (_, nks, r as ref (L'.KUnknown f))) =>
+             if not (f k2All) then
+                 err KScope
              else
-                 r := SOME k1All
-
-           | (L'.KTupleUnif (_, nks, r), L'.KTuple ks) =>
-             ((app (fn (n, k) => unifyKinds' env k (List.nth (ks, n-1))) nks;
-               r := SOME k2All)
-              handle Subscript => err KIncompatible)
-           | (L'.KTuple ks, L'.KTupleUnif (_, nks, r)) =>
-             ((app (fn (n, k) => unifyKinds' env (List.nth (ks, n-1)) k) nks;
-               r := SOME k1All)
-              handle Subscript => err KIncompatible)
-           | (L'.KTupleUnif (loc, nks1, r1), L'.KTupleUnif (_, nks2, r2)) =>
+                 ((app (fn (n, k) => unifyKinds' env (List.nth (ks, n-1)) k) nks;
+                   r := L'.KKnown k1All)
+                  handle Subscript => err KIncompatible)
+           | (L'.KTupleUnif (loc, nks1, r1 as ref (L'.KUnknown f1)), L'.KTupleUnif (_, nks2, r2 as ref (L'.KUnknown f2))) =>
              let
                  val nks = foldl (fn (p as (n, k1), nks) =>
                                      case ListUtil.search (fn (n', k2) =>
@@ -136,10 +170,10 @@
                                        | SOME k2 => (unifyKinds' env k1 k2;
                                                      nks)) nks2 nks1
 
-                 val k = (L'.KTupleUnif (loc, nks, ref NONE), loc)
+                 val k = (L'.KTupleUnif (loc, nks, ref (L'.KUnknown (fn x => f1 x andalso f2 x))), loc)
              in
-                 r1 := SOME k;
-                 r2 := SOME k
+                 r1 := L'.KKnown k;
+                 r2 := L'.KKnown k
              end
 
            | _ => err KIncompatible
@@ -174,13 +208,14 @@
  val char = ref cerror
  val table = ref cerror
 
+
  local
      val count = ref 0
  in
 
  fun resetKunif () = count := 0
 
- fun kunif loc =
+ fun kunif' f loc =
      let
          val n = !count
          val s = if n <= 26 then
@@ -189,9 +224,11 @@
                      "U" ^ Int.toString (n - 26)
      in
          count := n + 1;
-         (L'.KUnif (loc, s, ref NONE), loc)
+         (L'.KUnif (loc, s, ref (L'.KUnknown f)), loc)
      end
 
+ fun kunif env = kunif' (validateKind env)
+
  end
 
  local
@@ -200,7 +237,7 @@
 
  fun resetCunif () = count := 0
 
- fun cunif (loc, k) =
+ fun cunif' f (loc, k) =
      let
          val n = !count
          val s = if n < 26 then
@@ -209,9 +246,11 @@
                      "U" ^ Int.toString (n - 26)
      in
          count := n + 1;
-         (L'.CUnif (0, loc, k, s, ref NONE), loc)
+         (L'.CUnif (0, loc, k, s, ref (L'.Unknown f)), loc)
      end
 
+ fun cunif env = cunif' (validateCon env)
+
  end
 
  fun elabKind env (k, loc) =
@@ -222,7 +261,7 @@
        | L.KRecord k => (L'.KRecord (elabKind env k), loc)
        | L.KUnit => (L'.KUnit, loc)
        | L.KTuple ks => (L'.KTuple (map (elabKind env) ks), loc)
-       | L.KWild => kunif loc
+       | L.KWild => kunif env loc
 
        | L.KVar s => (case E.lookupK env s of
                           NONE =>
@@ -238,18 +277,18 @@
 
  fun hnormKind (kAll as (k, _)) =
      case k of
-         L'.KUnif (_, _, ref (SOME k)) => hnormKind k
+         L'.KUnif (_, _, ref (L'.KKnown k)) => hnormKind k
        | _ => kAll
 
  open ElabOps
 
- fun elabConHead (c as (_, loc)) k =
+ fun elabConHead env (c as (_, loc)) k =
      let
          fun unravel (k, c) =
              case hnormKind k of
                  (L'.KFun (x, k'), _) =>
                  let
-                     val u = kunif loc
+                     val u = kunif env loc
                              
                      val k'' = subKindInKind (0, u) k'
                  in
@@ -303,8 +342,8 @@
              val (c1', k1, gs1) = elabCon (env, denv) c1
              val (c2', k2, gs2) = elabCon (env, denv) c2
 
-             val ku1 = kunif loc
-             val ku2 = kunif loc
+             val ku1 = kunif env loc
+             val ku2 = kunif env loc
 
              val denv' = D.assert env denv (c1', c2')
              val (c', k, gs4) = elabCon (env, denv') c
@@ -331,13 +370,13 @@
                (cerror, kerror, []))
             | E.Rel (n, k) =>
               let
-                  val (c, k) = elabConHead (L'.CRel n, loc) k
+                  val (c, k) = elabConHead env (L'.CRel n, loc) k
               in
                   (c, k, [])
               end
             | E.Named (n, k) =>
               let
-                  val (c, k) = elabConHead (L'.CNamed n, loc) k
+                  val (c, k) = elabConHead env (L'.CNamed n, loc) k
               in
                   (c, k, [])
               end)
@@ -358,7 +397,7 @@
                               NONE => (conError env (UnboundCon (loc, s));
                                        kerror)
                             | SOME (k, _) => k
-                 val (c, k) = elabConHead (L'.CModProj (n, ms, s), loc) k
+                 val (c, k) = elabConHead env (L'.CModProj (n, ms, s), loc) k
               in
                   (c, k, [])
               end)
@@ -367,8 +406,8 @@
          let
              val (c1', k1, gs1) = elabCon (env, denv) c1
              val (c2', k2, gs2) = elabCon (env, denv) c2
-             val dom = kunif loc
-             val ran = kunif loc
+             val dom = kunif env loc
+             val ran = kunif env loc
          in
              checkKind env c1' k1 (L'.KArrow (dom, ran), loc);
              checkKind env c2' k2 dom;
@@ -377,7 +416,7 @@
        | L.CAbs (x, ko, t) =>
          let
              val k' = case ko of
-                          NONE => kunif loc
+                          NONE => kunif env loc
                         | SOME k => elabKind env k
              val env' = E.pushCRel env x k'
              val (t', tk, gs) = elabCon (env', D.enter denv) t
@@ -401,7 +440,7 @@
 
        | L.CRecord xcs =>
          let
-             val k = kunif loc
+             val k = kunif env loc
 
              val (xcs', gs) = ListUtil.foldlMap (fn ((x, c), gs) =>
                                                     let
@@ -439,7 +478,7 @@
          let
              val (c1', k1, gs1) = elabCon (env, denv) c1
              val (c2', k2, gs2) = elabCon (env, denv) c2
-             val ku = kunif loc
+             val ku = kunif env loc
              val k = (L'.KRecord ku, loc)
          in
              checkKind env c1' k1 k;
@@ -449,8 +488,8 @@
          end
        | L.CMap =>
          let
-             val dom = kunif loc
-             val ran = kunif loc
+             val dom = kunif env loc
+             val ran = kunif env loc
          in
              ((L'.CMap (dom, ran), loc),
               mapKind (dom, ran, loc),
@@ -474,13 +513,13 @@
          let
              val (c', k, gs) = elabCon (env, denv) c
 
-             val k' = kunif loc
+             val k' = kunif env loc
          in
              if n <= 0 then
                  (conError env (ProjBounds (c', n));
                   (cerror, kerror, []))
              else
-                 (checkKind env c' k (L'.KTupleUnif (loc, [(n, k')], ref NONE), loc);
+                 (checkKind env c' k (L'.KTupleUnif (loc, [(n, k')], ref (L'.KUnknown (validateKind env))), loc);
                   ((L'.CProj (c', n), loc), k', gs))
          end
 
@@ -488,19 +527,19 @@
          let
              val k' = elabKind env k
          in
-             (cunif (loc, k'), k', [])
+             (cunif env (loc, k'), k', [])
          end
 
  fun kunifsRemain k =
      case k of
-         L'.KUnif (_, _, ref NONE) => true
-       | L'.KTupleUnif (_, _, ref NONE) => true
+         L'.KUnif (_, _, ref (L'.KUnknown _)) => true
+       | L'.KTupleUnif (_, _, ref (L'.KUnknown _)) => true
        | _ => false
  fun cunifsRemain c =
      case c of
-         L'.CUnif (_, loc, k, _, r as ref NONE) =>
+         L'.CUnif (_, loc, k, _, r as ref (L'.Unknown _)) =>
          (case #1 (hnormKind k) of
-              L'.KUnit => (r := SOME (L'.CUnit, loc); false)
+              L'.KUnit => (r := L'.Known (L'.CUnit, loc); false)
             | _ => true)
        | _ => false
 
@@ -529,7 +568,7 @@
 
  type record_summary = {
       fields : (L'.con * L'.con) list,
-      unifs : (L'.con * L'.con option ref) list,
+      unifs : (L'.con * L'.cunif ref) list,
       others : L'.con list
  }
 
@@ -598,10 +637,10 @@
               (L'.KTuple ks, _) => List.nth (ks, n - 1)
             | (L'.KUnif (_, _, r), _) =>
               let
-                  val ku = kunif loc
-                  val k = (L'.KTupleUnif (loc, [(n, ku)], ref NONE), loc)
+                  val ku = kunif env loc
+                  val k = (L'.KTupleUnif (loc, [(n, ku)], r), loc)
               in
-                  r := SOME k;
+                  r := L'.KKnown k;
                   k
               end
             | (L'.KTupleUnif (_, nks, r), _) =>
@@ -609,10 +648,10 @@
                    SOME k => k
                  | NONE =>
                    let
-                       val ku = kunif loc
-                       val k = (L'.KTupleUnif (loc, ((n, ku) :: nks), ref NONE), loc)
+                       val ku = kunif env loc
+                       val k = (L'.KTupleUnif (loc, ((n, ku) :: nks), r), loc)
                    in
-                       r := SOME k;
+                       r := L'.KKnown k;
                        k
                    end)
             | k => raise CUnify' (CKindof (k, c, "tuple")))
@@ -713,11 +752,11 @@
              case hnormKind (kindof env c) of
                  (L'.KRecord k, _) => k
                | (L'.KError, _) => kerror
-               | (L'.KUnif (_, _, r), _) =>
+               | (L'.KUnif (_, _, r as ref (L'.KUnknown f)), _) =>
                  let
-                     val k = kunif (#2 c)
+                     val k = kunif' f (#2 c)
                  in
-                     r := SOME (L'.KRecord k, #2 c);
+                     r := L'.KKnown (L'.KRecord k, #2 c);
                      k
                  end
                | k => raise CUnify' (CKindof (k, c, "record"))
@@ -751,7 +790,7 @@
                       unifs = #unifs s1 @ #unifs s2,
                       others = #others s1 @ #others s2}
                  end
-               | (L'.CUnif (nl, _, _, _, ref (SOME c)), _) => recordSummary env (E.mliftConInCon nl c)
+               | (L'.CUnif (nl, _, _, _, ref (L'.Known c)), _) => recordSummary env (E.mliftConInCon nl c)
                | c' as (L'.CUnif (0, _, _, _, r), _) => {fields = [], unifs = [(c', r)], others = []}
                | c' => {fields = [], unifs = [], others = [c']}
      in
@@ -845,35 +884,41 @@
 
          val (unifs1, fs1, others1, unifs2, fs2, others2) =
              case (unifs1, fs1, others1, unifs2, fs2, others2) of
-                 orig as ([(_, r)], [], [], _, _, _) =>
+                 orig as ([(_, r as ref (L'.Unknown f))], [], [], _, _, _) =>
                  let
                      val c = unsummarize {fields = fs2, others = others2, unifs = unifs2}
                  in
-                     if occursCon r c then
+                     if occursCon r c orelse not (f c) then
                          orig
                      else
-                         (r := SOME c;
+                         (r := L'.Known c;
                           empties)
                  end
-               | orig as (_, _, _, [(_, r)], [], []) =>
+               | orig as (_, _, _, [(_, r as ref (L'.Unknown f))], [], []) =>
                  let
                      val c = unsummarize {fields = fs1, others = others1, unifs = unifs1}
                  in
-                     if occursCon r c then
+                     if occursCon r c orelse not (f c) then
                          orig
                      else
-                         (r := SOME c;
+                         (r := L'.Known c;
                           empties)
                  end
-               | orig as ([(_, r1 as ref NONE)], _, [], [(_, r2 as ref NONE)], _, []) =>
+               | orig as ([(_, r1 as ref (L'.Unknown f1))], _, [], [(_, r2 as ref (L'.Unknown f2))], _, []) =>
                  if List.all (fn (x1, _) => List.all (fn (x2, _) => consNeq env (x1, x2)) fs2) fs1 then
                      let
                          val kr = (L'.KRecord k, loc)
-                         val u = cunif (loc, kr)
+                         val u = cunif env (loc, kr)
+
+                         val c1 = (L'.CConcat ((L'.CRecord (k, fs2), loc), u), loc)
+                         val c2 = (L'.CConcat ((L'.CRecord (k, fs1), loc), u), loc)
                      in
-                         r1 := SOME (L'.CConcat ((L'.CRecord (k, fs2), loc), u), loc);
-                         r2 := SOME (L'.CConcat ((L'.CRecord (k, fs1), loc), u), loc);
-                         empties
+                         if not (f1 c1) orelse not (f2 c2) then
+                             orig
+                         else
+                             (r1 := L'.Known c1;
+                              r2 := L'.Known c2;
+                              empties)
                      end
                  else
                      orig
@@ -950,10 +995,10 @@
      in
          (case (unifs1, fs1, others1, unifs2, fs2, others2) of
               (_, [], [], [], [], []) =>
-              app (fn (_, r) => r := SOME empty) unifs1
+              app (fn (_, r) => r := L'.Known empty) unifs1
             | ([], [], [], _, [], []) =>
-              app (fn (_, r) => r := SOME empty) unifs2
-            | (_, _, _, [], [], [cr as (L'.CUnif (nl, _, _, _, r), _)]) =>
+              app (fn (_, r) => r := L'.Known empty) unifs2
+            | (_, _, _, [], [], [cr as (L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f)), _)]) =>
               let
                   val c = summaryToCon {fields = fs1, unifs = unifs1, others = others1}
               in
@@ -961,10 +1006,17 @@
                       (reducedSummaries := NONE;
                        raise CUnify' (COccursCheckFailed (cr, c)))
                   else
-                      (r := SOME (squish nl c))
+                      let
+                          val sq = squish nl c
+                      in
+                          if not (f sq) then
+                              default ()
+                          else
+                              r := L'.Known sq
+                      end
                       handle CantSquish => default ()
               end
-            | ([], [], [cr as (L'.CUnif (nl, _, _, _, r), _)], _, _, _) =>
+            | ([], [], [cr as (L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f)), _)], _, _, _) =>
               let
                   val c = summaryToCon {fields = fs2, unifs = unifs2, others = others2}
               in
@@ -972,7 +1024,14 @@
                       (reducedSummaries := NONE;
                        raise CUnify' (COccursCheckFailed (cr, c)))
                   else
-                      (r := SOME (squish nl c))
+                      let
+                          val sq = squish nl c
+                      in
+                          if not (f sq) then
+                              default ()
+                          else
+                              r := L'.Known sq
+                      end
                       handle CantSquish => default ()
               end
             | _ => default ())
@@ -992,15 +1051,15 @@
                          let
                              val v' = case dom of
                                           (L'.KUnit, _) => (L'.CUnit, loc)
-                                        | _ => cunif (loc, dom)
+                                        | _ => cunif env (loc, dom)
                          in
                              unifyCons env loc v (L'.CApp (f, v'), loc);
                              unifyCons env loc r (L'.CRecord (dom, [(x, v')]), loc)
                          end
                        | L'.CRecord (_, (x, v) :: rest) =>
                          let
-                             val r1 = cunif (loc, (L'.KRecord dom, loc))
-                             val r2 = cunif (loc, (L'.KRecord dom, loc))
+                             val r1 = cunif env (loc, (L'.KRecord dom, loc))
+                             val r2 = cunif env (loc, (L'.KRecord dom, loc))
                          in
                              unfold (r1, (L'.CRecord (ran, [(x, v)]), loc));
                              unfold (r2, (L'.CRecord (ran, rest), loc));
@@ -1008,15 +1067,22 @@
                          end
                        | L'.CConcat (c1', c2') =>
                          let
-                             val r1 = cunif (loc, (L'.KRecord dom, loc))
-                             val r2 = cunif (loc, (L'.KRecord dom, loc))
+                             val r1 = cunif env (loc, (L'.KRecord dom, loc))
+                             val r2 = cunif env (loc, (L'.KRecord dom, loc))
                          in
                              unfold (r1, c1');
                              unfold (r2, c2');
                              unifyCons env loc r (L'.CConcat (r1, r2), loc)
                          end
-                       | L'.CUnif (0, _, _, _, ur) =>
-                         ur := SOME (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), loc), f), loc), r), loc)
+                       | L'.CUnif (0, _, _, _, ur as ref (L'.Unknown rf)) =>
+                         let
+                             val c' = (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), loc), f), loc), r), loc)
+                         in
+                             if not (rf c') then
+                                 cunifyError env (CScope (c, c'))
+                             else
+                                 ur := L'.Known c'
+                         end
                        | _ => raise ex
              in
                  unfold (r, c)
@@ -1063,14 +1129,14 @@
                                      onFail ()
                          in
                              case #1 (hnormCon env c2) of
-                                 L'.CUnif (0, _, k, _, r) =>
+                                 L'.CUnif (0, _, k, _, r as ref (L'.Unknown f)) =>
                                  (case #1 (hnormKind k) of
                                       L'.KTuple ks =>
                                       let
                                           val loc = #2 c2
-                                          val us = map (fn k => cunif (loc, k)) ks
+                                          val us = map (fn k => cunif' f (loc, k)) ks
                                       in
-                                          r := SOME (L'.CTuple us, loc);
+                                          r := L'.Known (L'.CTuple us, loc);
                                           unifyCons' env loc c1All (List.nth (us, n2 - 1))
                                       end
                                     | _ => tryNormal ())
@@ -1079,14 +1145,14 @@
                        | _ => onFail ()
              in
                  case #1 (hnormCon env c1) of
-                     L'.CUnif (0, _, k, _, r) =>
+                     L'.CUnif (0, _, k, _, r as ref (L'.Unknown f)) =>
                      (case #1 (hnormKind k) of
                           L'.KTuple ks =>
                           let
                               val loc = #2 c1
-                              val us = map (fn k => cunif (loc, k)) ks
+                              val us = map (fn k => cunif' f (loc, k)) ks
                           in
-                              r := SOME (L'.CTuple us, loc);
+                              r := L'.Known (L'.CTuple us, loc);
                               unifyCons' env loc (List.nth (us, n1 - 1)) c2All
                           end
                         | _ => trySnd ())
@@ -1095,14 +1161,14 @@
 
          fun projSpecial2 (c2, n2, onFail) =
              case #1 (hnormCon env c2) of
-                 L'.CUnif (0, _, k, _, r) =>
+                 L'.CUnif (0, _, k, _, r as ref (L'.Unknown f)) =>
                  (case #1 (hnormKind k) of
                       L'.KTuple ks =>
                       let
                           val loc = #2 c2
-                          val us = map (fn k => cunif (loc, k)) ks
+                          val us = map (fn k => cunif' f (loc, k)) ks
                       in
-                          r := SOME (L'.CTuple us, loc);
+                          r := L'.Known (L'.CTuple us, loc);
                           unifyCons' env loc c1All (List.nth (us, n2 - 1))
                       end
                     | _ => onFail ())
@@ -1123,40 +1189,64 @@
              (L'.CError, _) => ()
            | (_, L'.CError) => ()
 
-           | (L'.CUnif (nl1, loc1, k1, _, r1), L'.CUnif (nl2, loc2, k2, _, r2)) =>
+           | (L'.CUnif (nl1, loc1, k1, _, r1 as ref (L'.Unknown f1)), L'.CUnif (nl2, loc2, k2, _, r2 as ref (L'.Unknown f2))) =>
              if r1 = r2 andalso nl1 = nl2 then
                  ()
              else if nl1 = 0 then
                  (unifyKinds env k1 k2;
-                  r1 := SOME c2All)
+                  if f1 c2All then
+                      r1 := L'.Known c2All
+                  else
+                      err CScope)
              else if nl2 = 0 then
                  (unifyKinds env k1 k2;
-                  r2 := SOME c1All)
+                  if f2 c1All then
+                      r2 := L'.Known c1All
+                  else
+                      err CScope)
              else
                  err (fn _ => TooLifty (loc1, loc2))
 
-           | (L'.CUnif (0, _, _, _, r), _) =>
+           | (L'.CUnif (0, _, _, _, r as ref (L'.Unknown f)), _) =>
              if occursCon r c2All then
                  err COccursCheckFailed
+             else if f c2All then
+                 r := L'.Known c2All
              else
-                 r := SOME c2All
-           | (_, L'.CUnif (0, _, _, _, r)) =>
+                 err CScope
+           | (_, L'.CUnif (0, _, _, _, r as ref (L'.Unknown f))) =>
              if occursCon r c1All then
                  err COccursCheckFailed
+             else if f c1All then
+                 r := L'.Known c1All
              else
-                 r := SOME c1All
+                 err CScope
 
-           | (L'.CUnif (nl, _, _, _, r), _) =>
+           | (L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f)), _) =>
              if occursCon r c2All then
                  err COccursCheckFailed
              else
-                 (r := SOME (squish nl c2All)
+                 (let
+                      val sq = squish nl c2All
+                  in
+                      if f sq then
+                          r := L'.Known sq
+                      else
+                          err CScope
+                  end
                   handle CantSquish => err (fn _ => TooDeep))
-           | (_, L'.CUnif (nl, _, _, _, r)) =>
+           | (_, L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f))) =>
              if occursCon r c1All then
                  err COccursCheckFailed
              else
-                 (r := SOME (squish nl c1All)
+                 (let
+                      val sq = squish nl c1All
+                  in
+                      if f sq then
+                          r := L'.Known sq
+                      else
+                          err CScope
+                  end
                   handle CantSquish => err (fn _ => TooDeep))
 
            | (L'.CRecord _, _) => isRecord ()
@@ -1169,7 +1259,7 @@
 
            | (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
              (unifyCons' env loc d1 d2;
-             unifyCons' env loc r1 r2)
+              unifyCons' env loc r1 r2)
            | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) =>
              if expl1 <> expl2 then
                  err CExplicitness
@@ -1295,7 +1385,7 @@
              case hnormCon env t of
                  (L'.TKFun (x, t'), _) =>
                  let
-                     val u = kunif loc
+                     val u = kunif env loc
 
                      val t'' = subKindInCon (0, u) t'
                  in
@@ -1307,7 +1397,7 @@
              case hnormCon env t of
                  (L'.TKFun (x, t'), _) =>
                  let
-                     val u = kunif loc
+                     val u = kunif env loc
 
                      val t'' = subKindInCon (0, u) t'
                  in
@@ -1315,7 +1405,7 @@
                  end
                | (L'.TCFun (L'.Implicit, x, k, t'), _) =>
                  let
-                     val u = cunif (loc, k)
+                     val u = cunif env (loc, k)
 
                      val t'' = subConInCon env (0, u) t'
                  in
@@ -1393,7 +1483,7 @@ fun elabPat (pAll as (p, loc), (env, bound)) =
               | (NONE, NONE) =>
                 let
                     val k = (L'.KType, loc)
-                    val unifs = map (fn _ => cunif (loc, k)) xs
+                    val unifs = map (fn _ => cunif env (loc, k)) xs
                     val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs
                 in
                     (((L'.PCon (dk, pc, unifs, NONE), loc), dn),
@@ -1404,7 +1494,7 @@ fun elabPat (pAll as (p, loc), (env, bound)) =
                     val ((p', pt), (env, bound)) = elabPat (p, (env, bound))
 
                     val k = (L'.KType, loc)
-                    val unifs = map (fn _ => cunif (loc, k)) xs
+                    val unifs = map (fn _ => cunif env (loc, k)) xs
                     val nxs = length unifs - 1
                     val t = ListUtil.foldli (fn (i, u, t) => subConInCon env (nxs - i,
                                                                               E.mliftConInCon (nxs - i) u) t) t unifs
@@ -1416,7 +1506,7 @@ fun elabPat (pAll as (p, loc), (env, bound)) =
                 end
     in
         case p of
-            L.PWild => (((L'.PWild, loc), cunif (loc, (L'.KType, loc))),
+            L.PWild => (((L'.PWild, loc), cunif env (loc, (L'.KType, loc))),
                         (env, bound))
           | L.PVar x =>
             let
@@ -1424,7 +1514,7 @@ fun elabPat (pAll as (p, loc), (env, bound)) =
                             (expError env (DuplicatePatternVariable (loc, x));
                              terror)
                         else
-                            cunif (loc, (L'.KType, loc))
+                            cunif env (loc, (L'.KType, loc))
             in
                 (((L'.PVar (x, t), loc), t),
                  (E.pushERel env x t, SS.add (bound, x)))
@@ -1473,7 +1563,7 @@ fun elabPat (pAll as (p, loc), (env, bound)) =
                 val c = (L'.CRecord (k, map (fn (x, _, t) => ((L'.CName x, loc), t)) xpts), loc)
                 val c =
                     if flex then
-                        (L'.CConcat (c, cunif (loc, (L'.KRecord k, loc))), loc)
+                        (L'.CConcat (c, cunif env (loc, (L'.KRecord k, loc))), loc)
                     else
                         c
             in
@@ -1778,7 +1868,7 @@ fun normClassConstraint env (c, loc) =
             (L'.TFun (c1, c2), loc)
         end
       | L'.TCFun (expl, x, k, c1) => (L'.TCFun (expl, x, k, normClassConstraint env c1), loc)
-      | L'.CUnif (nl, _, _, _, ref (SOME c)) => normClassConstraint env (E.mliftConInCon nl c)
+      | L'.CUnif (nl, _, _, _, ref (L'.Known c)) => normClassConstraint env (E.mliftConInCon nl c)
       | _ => unmodCon env (c, loc)
 
 fun findHead e e' =
@@ -1887,7 +1977,7 @@ fun ndelVal (r : needed, k) =
 
 fun chaseUnifs c =
     case #1 c of
-        L'.CUnif (_, _, _, _, ref (SOME c)) => chaseUnifs c
+        L'.CUnif (_, _, _, _, ref (L'.Known c)) => chaseUnifs c
       | _ => c
 
 fun elabExp (env, denv) (eAll as (e, loc)) =
@@ -1937,7 +2027,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
           | L.EWild =>
             let
                 val r = ref NONE
-                val c = cunif (loc, (L'.KType, loc))
+                val c = cunif env (loc, (L'.KType, loc))
             in
                 ((L'.EUnif r, loc), c, [TypeClass (env, c, r, loc)])
             end
@@ -1948,8 +2038,8 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
 
                 val (e2', t2, gs2) = elabExp (env, denv) e2
 
-                val dom = cunif (loc, ktype)
-                val ran = cunif (loc, ktype)
+                val dom = cunif env (loc, ktype)
+                val ran = cunif env (loc, ktype)
                 val t = (L'.TFun (dom, ran), loc)
 
                 val () = checkCon env e1' t1 t
@@ -1966,7 +2056,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
           | L.EAbs (x, to, e) =>
             let
                 val (t', gs1) = case to of
-                                    NONE => (cunif (loc, ktype), [])
+                                    NONE => (cunif env (loc, ktype), [])
                                   | SOME t =>
                                     let
                                         val (t', tk, gs) = elabCon (env, denv) t
@@ -2042,8 +2132,8 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
                 val (c1', k1, gs1) = elabCon (env, denv) c1
                 val (c2', k2, gs2) = elabCon (env, denv) c2
 
-                val ku1 = kunif loc
-                val ku2 = kunif loc
+                val ku1 = kunif env loc
+                val ku2 = kunif env loc
 
                 val denv' = D.assert env denv (c1', c2')
                 val (e', t, gs3) = elabExp (env, denv') e
@@ -2057,11 +2147,11 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
             let
                 val (e', t, gs1) = elabExp (env, denv) e
 
-                val k1 = kunif loc
-                val c1 = cunif (loc, (L'.KRecord k1, loc))
-                val k2 = kunif loc
-                val c2 = cunif (loc, (L'.KRecord k2, loc))
-                val t' = cunif (loc, ktype)
+                val k1 = kunif env loc
+                val c1 = cunif env (loc, (L'.KRecord k1, loc))
+                val k2 = kunif env loc
+                val c2 = cunif env (loc, (L'.KRecord k2, loc))
+                val t' = cunif env (loc, ktype)
                 val () = checkCon env e' t (L'.TDisjoint (c1, c2, t'), loc)
                 val gs2 = D.prove env denv (c1, c2, loc)
             in
@@ -2115,8 +2205,8 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
                 val (e', et, gs1) = elabExp (env, denv) e
                 val (c', ck, gs2) = elabCon (env, denv) c
 
-                val ft = cunif (loc, ktype)
-                val rest = cunif (loc, ktype_record)
+                val ft = cunif env (loc, ktype)
+                val rest = cunif env (loc, ktype_record)
                 val first = (L'.CRecord (ktype, [(c', ft)]), loc)
                 val () = checkCon env e' et
                                   (L'.TRecord (L'.CConcat (first, rest), loc), loc);
@@ -2130,8 +2220,8 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
                 val (e1', e1t, gs1) = elabExp (env, denv) e1
                 val (e2', e2t, gs2) = elabExp (env, denv) e2
 
-                val r1 = cunif (loc, ktype_record)
-                val r2 = cunif (loc, ktype_record)
+                val r1 = cunif env (loc, ktype_record)
+                val r2 = cunif env (loc, ktype_record)
 
                 val () = checkCon env e1' e1t (L'.TRecord r1, loc)
                 val () = checkCon env e2' e2t (L'.TRecord r2, loc)
@@ -2147,8 +2237,8 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
                 val (e', et, gs1) = elabExp (env, denv) e
                 val (c', ck, gs2) = elabCon (env, denv) c
 
-                val ft = cunif (loc, ktype)
-                val rest = cunif (loc, ktype_record)
+                val ft = cunif env (loc, ktype)
+                val rest = cunif env (loc, ktype_record)
                 val first = (L'.CRecord (ktype, [(c', ft)]), loc)
 
                 val () = checkCon env e' et
@@ -2165,7 +2255,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
                 val (e', et, gs1) = elabExp (env, denv) e
                 val (c', ck, gs2) = elabCon (env, denv) c
 
-                val rest = cunif (loc, ktype_record)
+                val rest = cunif env (loc, ktype_record)
 
                 val () = checkCon env e' et
                                   (L'.TRecord (L'.CConcat (c', rest), loc), loc)
@@ -2180,7 +2270,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
           | L.ECase (e, pes) =>
             let
                 val (e', et, gs1) = elabExp (env, denv) e
-                val result = cunif (loc, (L'.KType, loc))
+                val result = cunif env (loc, (L'.KType, loc))
                 val (pes', gs) = ListUtil.foldlMap
                                  (fn ((p, e), gs) =>
                                      let
@@ -2255,7 +2345,7 @@ and elabEdecl denv (dAll as (d, loc), (env, gs)) =
                                         (fn ((x, co, e), gs) =>
                                             let
                                                 val (c', _, gs1) = case co of
-                                                                       NONE => (cunif (loc, ktype), ktype, [])
+                                                                       NONE => (cunif env (loc, ktype), ktype, [])
                                                                      | SOME c => elabCon (env, denv) c
                                             in
                                                 ((x, c', e), enD gs1 @ gs)
@@ -2339,7 +2429,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
        | L.SgiCon (x, ko, c) =>
          let
              val k' = case ko of
-                          NONE => kunif loc
+                          NONE => kunif env loc
                         | SOME k => elabKind env k
 
              val (c', ck, gs') = elabCon (env, denv) c
@@ -2479,8 +2569,8 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
              val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc)
 
              val (c', ck, gs') = elabCon (env, denv) c
-             val pkey = cunif (loc, cstK)
-             val visible = cunif (loc, cstK)
+             val pkey = cunif env (loc, cstK)
+             val visible = cunif env (loc, cstK)
              val (env', ds, uniques) =
                  case (#1 pe, #1 ce) of
                      (L.EVar (["Basis"], "no_primary_key", _), L.EVar (["Basis"], "no_constraint", _)) =>
@@ -2556,8 +2646,8 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
 
              val denv = D.assert env denv (c1', c2')
          in
-             checkKind env c1' k1 (L'.KRecord (kunif loc), loc);
-             checkKind env c2' k2 (L'.KRecord (kunif loc), loc);
+             checkKind env c1' k1 (L'.KRecord (kunif env loc), loc);
+             checkKind env c2' k2 (L'.KRecord (kunif env loc), loc);
 
              ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2))
          end
@@ -3421,9 +3511,9 @@ and wildifyStr env (str, sgn) =
                          end
 
                        | L'.KError => NONE
-                       | L'.KUnif (_, _, ref (SOME k)) => decompileKind k
+                       | L'.KUnif (_, _, ref (L'.KKnown k)) => decompileKind k
                        | L'.KUnif _ => NONE
-                       | L'.KTupleUnif (_, _, ref (SOME k)) => decompileKind k
+                       | L'.KTupleUnif (_, _, ref (L'.KKnown k)) => decompileKind k
                        | L'.KTupleUnif _ => NONE
 
                        | L'.KRel _ => NONE
@@ -3472,7 +3562,7 @@ and wildifyStr env (str, sgn) =
                               (SOME c1, SOME c2) => SOME (L.CConcat (c1, c2), loc)
                             | _ => NONE)
                        | L'.CUnit => SOME (L.CUnit, loc)
-                       | L'.CUnif (nl, _, _, _, ref (SOME c)) => decompileCon env (E.mliftConInCon nl c)
+                       | L'.CUnif (nl, _, _, _, ref (L'.Known c)) => decompileCon env (E.mliftConInCon nl c)
 
                        | L'.CApp (f, x) =>
                          (case (decompileCon env f, decompileCon env x) of
@@ -3599,7 +3689,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
                 L.DCon (x, ko, c) =>
                 let
                     val k' = case ko of
-                                 NONE => kunif loc
+                                 NONE => kunif env loc
                                | SOME k => elabKind env k
 
                     val (c', ck, gs') = elabCon (env, denv) c
@@ -3723,7 +3813,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
               | L.DVal (x, co, e) =>
                 let
                     val (c', _, gs1) = case co of
-                                           NONE => (cunif (loc, ktype), ktype, [])
+                                           NONE => (cunif env (loc, ktype), ktype, [])
                                          | SOME c => elabCon (env, denv) c
 
                     val (e', et, gs2) = elabExp (env, denv) e
@@ -3751,7 +3841,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
                                         (fn ((x, co, e), gs) =>
                                             let
                                                 val (c', _, gs1) = case co of
-                                                                       NONE => (cunif (loc, ktype), ktype, [])
+                                                                       NONE => (cunif env (loc, ktype), ktype, [])
                                                                      | SOME c => elabCon (env, denv) c
                                                 val c' = normClassConstraint env c'
                                             in
@@ -3868,8 +3958,8 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
 
                     val denv' = D.assert env denv (c1', c2')
                 in
-                    checkKind env c1' k1 (L'.KRecord (kunif loc), loc);
-                    checkKind env c2' k2 (L'.KRecord (kunif loc), loc);
+                    checkKind env c1' k1 (L'.KRecord (kunif env loc), loc);
+                    checkKind env c2' k2 (L'.KRecord (kunif env loc), loc);
 
                     ([(L'.DConstraint (c1', c2'), loc)], (env, denv', enD gs1 @ enD gs2 @ enD gs3 @ gs))
                 end
@@ -3959,8 +4049,8 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
                     val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc)
 
                     val (c', k, gs') = elabCon (env, denv) c
-                    val pkey = cunif (loc, cstK)
-                    val uniques = cunif (loc, cstK)
+                    val pkey = cunif env (loc, cstK)
+                    val uniques = cunif env (loc, cstK)
 
                     val ct = tableOf ()
                     val ct = (L'.CApp (ct, c'), loc)
@@ -3995,8 +4085,8 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
                     val (e', t, gs') = elabExp (env, denv) e
 
                     val k = (L'.KRecord (L'.KType, loc), loc)
-                    val fs = cunif (loc, k)
-                    val ts = cunif (loc, (L'.KRecord k, loc))
+                    val fs = cunif env (loc, k)
+                    val ts = cunif env (loc, (L'.KRecord k, loc))
                     val tf = (L'.CApp ((L'.CMap (k, k), loc),
                                        (L'.CAbs ("_", k, (L'.CRecord ((L'.KType, loc), []), loc)), loc)), loc)
                     val ts = (L'.CApp (tf, ts), loc)
@@ -4048,7 +4138,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
                     val (e1', t1, gs1) = elabExp (env, denv) e1
                     val (e2', t2, gs2) = elabExp (env, denv) e2
 
-                    val targ = cunif (loc, (L'.KType, loc))
+                    val targ = cunif env (loc, (L'.KType, loc))
 
                     val t1' = (L'.CModProj (!basis_r, [], "task_kind"), loc)
                     val t1' = (L'.CApp (t1', targ), loc)
diff --git a/src/explify.sml b/src/explify.sml
index 5081d33b..3c922a44 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -42,9 +42,9 @@ fun explifyKind (k, loc) =
       | L.KTuple ks => (L'.KTuple (map explifyKind ks), loc)
 
       | L.KError => raise Fail ("explifyKind: KError at " ^ EM.spanToString loc)
-      | L.KUnif (_, _, ref (SOME k)) => explifyKind k
+      | L.KUnif (_, _, ref (L.KKnown k)) => explifyKind k
       | L.KUnif _ => raise Fail ("explifyKind: KUnif at " ^ EM.spanToString loc)
-      | L.KTupleUnif (loc, _, ref (SOME k)) => explifyKind k
+      | L.KTupleUnif (loc, _, ref (L.KKnown k)) => explifyKind k
       | L.KTupleUnif _ => raise Fail ("explifyKind: KTupleUnif at " ^ EM.spanToString loc)
 
       | L.KRel n => (L'.KRel n, loc)
@@ -76,7 +76,7 @@ fun explifyCon (c, loc) =
       | L.CProj (c, n) => (L'.CProj (explifyCon c, n), loc)
 
       | L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc)
-      | L.CUnif (nl, _, _, _, ref (SOME c)) => explifyCon (ElabEnv.mliftConInCon nl c)
+      | L.CUnif (nl, _, _, _, ref (L.Known c)) => explifyCon (ElabEnv.mliftConInCon nl c)
       | L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc)
 
       | L.CKAbs (x, c) => (L'.CKAbs (x, explifyCon c), loc)