# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1214498126 14400
# Node ID 88ffb3d618174246894aca1666ae27e42826f504
# Parent  144d082b47ae2db4a49fc8915599bb11444e6856
Folding through a functor

diff -r 144d082b47ae -r 88ffb3d61817 src/elaborate.sml
--- a/src/elaborate.sml	Thu Jun 26 12:12:06 2008 -0400
+++ b/src/elaborate.sml	Thu Jun 26 12:35:26 2008 -0400
@@ -1082,6 +1082,7 @@
        | SgiWrongCon of L'.sgn_item * L'.con * L'.sgn_item * L'.con * cunify_error
        | SgnWrongForm of L'.sgn * L'.sgn
        | UnWhereable of L'.sgn * string
+       | WhereWrongKind of L'.kind * L'.kind * kunify_error
        | NotIncludable of L'.sgn
        | DuplicateCon of ErrorMsg.span * string
        | DuplicateVal of ErrorMsg.span * string
@@ -1117,6 +1118,11 @@
         (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'";
          eprefaces' [("Signature", p_sgn env sgn),
                      ("Field", PD.string x)])
+      | WhereWrongKind (k1, k2, kerr) =>
+        (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'";
+         eprefaces' [("Have", p_kind k1),
+                     ("Need", p_kind k2)];
+         kunifyError kerr)
       | NotIncludable sgn =>
         (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'";
          eprefaces' [("Signature", p_sgn env sgn)])
@@ -1134,6 +1140,7 @@
        | NotFunctor of L'.sgn
        | FunctorRebind of ErrorMsg.span
        | UnOpenable of L'.sgn
+       | NotType of L'.kind * (L'.kind * L'.kind * kunify_error)
 
 fun strError env err =
     case err of
@@ -1147,6 +1154,12 @@
       | UnOpenable sgn =>
         (ErrorMsg.errorAt (#2 sgn) "Un-openable structure";
          eprefaces' [("Signature", p_sgn env sgn)])
+      | NotType (k, (k1, k2, ue)) =>
+        (ErrorMsg.errorAt (#2 k) "'val' type kind is not 'Type'";
+         eprefaces' [("Kind", p_kind k),
+                     ("Subkind 1", p_kind k1),
+                     ("Subkind 2", p_kind k2)];
+         kunifyError ue)
 
 val hnormSgn = E.hnormSgn
 
@@ -1209,7 +1222,8 @@
 
                 val (env', n) = E.pushENamed env x c'
             in
-                unifyKinds ck ktype;
+                (unifyKinds ck ktype
+                 handle KUnify ue => strError env (NotType (ck, ue)));
 
                 if ErrorMsg.anyErrors () then
                     ()
@@ -1316,8 +1330,10 @@
             case #1 (hnormSgn env sgn') of
                 L'.SgnError => sgnerror
               | L'.SgnConst sgis =>
-                if List.exists (fn (L'.SgiConAbs (x, _, k), _) =>
-                                   (unifyKinds k ck;
+                if List.exists (fn (L'.SgiConAbs (x', _, k), _) =>
+                                   x' = x andalso
+                                   (unifyKinds k ck
+                                    handle KUnify x => sgnError env (WhereWrongKind x);
                                     true)
                                  | _ => false) sgis then
                     (L'.SgnWhere (sgn', x, c'), loc)
diff -r 144d082b47ae -r 88ffb3d61817 tests/foldm.lac
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/foldm.lac	Thu Jun 26 12:35:26 2008 -0400
@@ -0,0 +1,26 @@
+con currier = fold (fn nm => fn t => fn acc => t -> acc) {}
+
+signature S = sig
+        type t
+        val x : t
+
+        con rs :: {Type}
+        val create : currier rs -> t
+end
+
+functor Currier (M : sig con rs :: {Type} end) : S where con rs = M.rs = struct
+        val currier : rs :: {Type} -> currier rs =
+                fold [currier] (fn nm :: Name => fn t :: Type => fn rest :: {Type} => fn acc => fn x : t => acc) {}
+
+        type t = currier M.rs
+        val x = currier [M.rs]
+
+        con rs = M.rs
+        val create : t -> t = fn x => x
+end
+
+structure ChefsSpecial = Currier(struct
+        con rs = [A = int, B = float]
+end)
+
+val main = ChefsSpecial.x