diff options
-rw-r--r-- | src/elaborate.sml | 22 | ||||
-rw-r--r-- | tests/foldm.lac | 26 |
2 files changed, 45 insertions, 3 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml index e656d156..d8d29fa0 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -1082,6 +1082,7 @@ datatype sgn_error = | 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 @@ fun sgnError env err = (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 @@ datatype str_error = | 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 @@ fun strError env err = | 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 @@ fun elabSgn_item ((sgi, loc), env) = 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 @@ and elabSgn env (sgn, loc) = 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 --git a/tests/foldm.lac b/tests/foldm.lac new file mode 100644 index 00000000..64d30ba2 --- /dev/null +++ b/tests/foldm.lac @@ -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 |