Check for leftover kind unifs

12 files changed, 174 insertions, 20 deletions

diff --git a/src/elab.sml b/src/elab.sml
index 89d25c26..89febb0b 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -60,7 +60,7 @@ datatype con' =
        | CConcat of con * con
 
        | CError
-       | CUnif of string * con option ref
+       | CUnif of kind * string * con option ref
 
 withtype con = con' located
 
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 58a342e2..2ac8f6fc 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -121,8 +121,10 @@ fun p_con' par env (c, _) =
                                               p_con env c2])
 
       | CError => string "<ERROR>"
-      | CUnif (_, ref (SOME c)) => p_con' par env c
-      | CUnif (s, _) => string ("<UNIF:" ^ s ^ ">")
+      | 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 da1a02f4..895f836c 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -28,11 +28,19 @@
 signature ELAB_UTIL = sig
 
 structure Kind : sig
-    val mapfold : (Elab.kind', 'state, 'abort) Search.mapfold_arg
+    val mapfold : (Elab.kind', 'state, 'abort) Search.mapfolder
                   -> (Elab.kind, 'state, 'abort) Search.mapfolder
     val exists : (Elab.kind' -> bool) -> Elab.kind -> bool
 end
 
+structure Con : sig
+    val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
+                      con : (Elab.con', 'state, 'abort) Search.mapfolder}
+                  -> (Elab.con, 'state, 'abort) Search.mapfolder
+    val exists : {kind : Elab.kind' -> bool,
+                  con : Elab.con' -> bool} -> Elab.con -> bool
+end
+
 val declBinds : ElabEnv.env -> Elab.decl -> ElabEnv.env
 
 end
diff --git a/src/elab_util.sml b/src/elab_util.sml
index f889db30..37d58fcc 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -33,7 +33,7 @@ structure S = Search
 
 structure Kind = struct
 
-fun mapfold (f : (Elab.kind', 'state, 'abort) S.mapfold_arg) : (Elab.kind, 'state, 'abort) S.mapfolder =
+fun mapfold f =
     let
         fun mfk k acc =
             S.bindP (mfk' k acc, f)
@@ -65,11 +65,98 @@ fun mapfold (f : (Elab.kind', 'state, 'abort) S.mapfold_arg) : (Elab.kind, 'stat
     end
 
 fun exists f k =
-    case mapfold (fn (k, ()) =>
-                     if f k then
-                         S.Return ()
-                     else
-                         S.Continue (k, ())) k () of
+    case mapfold (fn k => fn () =>
+                             if f k then
+                                 S.Return ()
+                             else
+                                 S.Continue (k, ())) k () of
+        S.Return _ => true
+      | S.Continue _ => false
+
+end
+
+structure Con = struct
+
+fun mapfold {kind = fk, con = fc} =
+    let
+        val mfk = Kind.mapfold fk
+
+        fun mfc c acc =
+            S.bindP (mfc' c acc, fc)
+
+        and mfc' (cAll as (c, loc)) =
+            case c of
+                TFun (c1, c2) =>
+                S.bind2 (mfc c1,
+                      fn c1' =>
+                         S.map2 (mfc c2,
+                              fn c2' =>
+                                 (TFun (c1', c2'), loc)))
+              | TCFun (e, x, k, c) =>
+                S.bind2 (mfk k,
+                      fn k' =>
+                         S.map2 (mfc c,
+                              fn c' =>
+                                 (TCFun (e, x, k', c'), loc)))
+              | TRecord c =>
+                S.map2 (mfc c,
+                        fn c' =>
+                           (TRecord c', loc))
+
+              | CRel _ => S.return2 cAll
+              | CNamed _ => S.return2 cAll
+              | CApp (c1, c2) =>
+                S.bind2 (mfc c1,
+                      fn c1' =>
+                         S.map2 (mfc c2,
+                              fn c2' =>
+                                 (CApp (c1', c2'), loc)))
+              | CAbs (e, x, k, c) =>
+                S.bind2 (mfk k,
+                      fn k' =>
+                         S.map2 (mfc c,
+                              fn c' =>
+                                 (CAbs (e, x, k', c'), loc)))
+
+              | CName _ => S.return2 cAll
+
+              | CRecord (k, xcs) =>
+                S.bind2 (mfk k,
+                      fn k' =>
+                         S.map2 (ListUtil.mapfold (fn (x, c) =>
+                                                      S.bind2 (mfc x,
+                                                            fn x' =>
+                                                               S.map2 (mfc c,
+                                                                    fn c' =>
+                                                                       (x', c'))))
+                                 xcs,
+                              fn xcs' =>
+                                 (CRecord (k', xcs'), loc)))
+              | CConcat (c1, c2) =>
+                S.bind2 (mfc c1,
+                      fn c1' =>
+                         S.map2 (mfc c2,
+                              fn c2' =>
+                                 (CConcat (c1', c2'), loc)))
+
+              | CError => S.return2 cAll
+              | CUnif (_, _, ref (SOME c)) => mfc' c
+              | CUnif _ => S.return2 cAll
+    in
+        mfc
+    end
+
+fun exists {kind, con} 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, ())} k () of
         S.Return _ => true
       | S.Continue _ => false
 
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 14fe47e1..b3250190 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -261,6 +261,28 @@ fun elabCon env (c, loc) =
             ((L'.CConcat (c1', c2'), loc), k)
         end
 
+fun kunifsRemain k =
+    case k of
+        L'.KUnif (_, ref NONE) => true
+      | _ => false
+
+val kunifsInKind = U.Kind.exists kunifsRemain
+val kunifsInCon = U.Con.exists {kind = kunifsRemain,
+                                con = fn _ => false}
+
+datatype decl_error =
+         KunifsRemainKind of ErrorMsg.span * L'.kind
+       | KunifsRemainCon of ErrorMsg.span * L'.con
+
+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)])
+
 fun elabDecl env (d, loc) =
     (resetKunif ();
      case d of
@@ -274,6 +296,17 @@ fun elabDecl env (d, loc) =
              val (env', n) = E.pushCNamed env x k'
          in
              checkKind env c' ck k';
+
+             if kunifsInKind k' then
+                 declError env (KunifsRemainKind (loc, k'))
+             else
+                 ();
+
+             if kunifsInCon c' then
+                 declError env (KunifsRemainCon (loc, c'))
+             else
+                 ();
+
              (env',
               (L'.DCon (x, n, k', c'), loc))
          end)
diff --git a/src/lacweb.grm b/src/lacweb.grm
index a6054494..7384dbf8 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -69,6 +69,7 @@ val s = ErrorMsg.spanOf
 
 %nonassoc DARROW
 %nonassoc COLON
+%nonassoc DCOLON TCOLON
 %right COMMA
 %right ARROW LARROW
 %right PLUSPLUS
@@ -102,6 +103,8 @@ cexp   : capps                          (capps)
 
        | FN SYMBOL kcolon kind DARROW cexp (CAbs (kcolon, SYMBOL, kind, cexp), s (FNleft, cexpright))
 
+       | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, RPARENright))
+
 kcolon : DCOLON                         (Explicit)
        | TCOLON                         (Implicit)
 
diff --git a/src/list_util.sig b/src/list_util.sig
index 4c4aa955..6ec109da 100644
--- a/src/list_util.sig
+++ b/src/list_util.sig
@@ -30,4 +30,7 @@ signature LIST_UTIL = sig
     val mapfoldl : ('data1 * 'state -> 'state * 'data2) -> 'state -> 'data1 list
                    -> 'state * 'data2 list
 
+    val mapfold : ('data, 'state, 'abort) Search.mapfolder
+                  -> ('data list, 'state, 'abort) Search.mapfolder
+
 end
diff --git a/src/list_util.sml b/src/list_util.sml
index fdc1ac55..eee8249b 100644
--- a/src/list_util.sml
+++ b/src/list_util.sml
@@ -42,4 +42,22 @@ fun mapfoldl f i =
         mf i []
     end
 
+structure S = Search
+
+fun mapfold f =
+    let
+        fun mf ls s =
+            case ls of
+                nil => S.Continue (nil, s)
+              | h :: t =>
+                case f h s of
+                    S.Return x => S.Return x
+                  | S.Continue (h', s) =>
+                    case mf t s of
+                        S.Return x => S.Return x
+                      | S.Continue (t', s) => S.Continue (h' :: t', s)
+    in
+        mf
+    end
+
 end
diff --git a/src/search.sig b/src/search.sig
index 65fc6aa6..102ef558 100644
--- a/src/search.sig
+++ b/src/search.sig
@@ -31,9 +31,6 @@ signature SEARCH = sig
              Return of 'abort
            | Continue of 'state
 
-    type ('data, 'state, 'abort) mapfold_arg =
-         'data * 'state -> ('data * 'state, 'abort) result
-
     type ('data, 'state, 'abort) mapfolder =
          'data -> 'state -> ('data * 'state, 'abort) result
 
@@ -52,11 +49,11 @@ signature SEARCH = sig
                -> ('state2, 'abort) result
 
     val bind2 : ('state2 -> ('state1 * 'state2, 'abort) result)
-               * ('state1 -> 'state2 -> ('state1 * 'state2, 'abort) result)
-               -> ('state2 -> ('state1 * 'state2, 'abort) result)
+               * ('state1 -> 'state2 -> ('state1' * 'state2, 'abort) result)
+               -> ('state2 -> ('state1' * 'state2, 'abort) result)
 
     val bindP : (('state11 * 'state12) * 'state2, 'abort) result
-                * ('state11 * 'state2 -> ('state11 * 'state2, 'abort) result)
+                * ('state11 -> 'state2 -> ('state11 * 'state2, 'abort) result)
                 -> (('state11 * 'state12) * 'state2, 'abort) result
 
 end
diff --git a/src/search.sml b/src/search.sml
index 50904bba..6b78e9b2 100644
--- a/src/search.sml
+++ b/src/search.sml
@@ -62,7 +62,7 @@ fun bind2 (r, f) acc =
 fun bindP (r, f) =
     case r of
         Continue ((x, pos), acc) =>
-        map (f (x, acc),
+        map (f x acc,
           fn (x', acc') =>
              ((x', pos), acc'))
       | Return x => Return x
diff --git a/src/sources b/src/sources
index 8cc24a1e..1c3ae6ff 100644
--- a/src/sources
+++ b/src/sources
@@ -1,3 +1,6 @@
+search.sig
+search.sml
+
 list_util.sig
 list_util.sml
 
@@ -17,9 +20,6 @@ source_print.sml
 
 elab.sml
 
-search.sig
-search.sml
-
 elab_util.sig
 elab_util.sml
 
diff --git a/tests/stuff.lac b/tests/stuff.lac
index c5d5852e..fe692eec 100644
--- a/tests/stuff.lac
+++ b/tests/stuff.lac
@@ -10,3 +10,6 @@ con c6 = {A : c1, name : c2}
 con c7 = [A = c1, name = c2]
 
 con c8 = fn t :: Type => t
+
+con c9 = {}
+con c10 = ([]) :: {Type}