summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2020-02-07 10:34:21 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2020-02-07 10:34:21 -0500
commitef4e0c207abd0e41badf7bf0052b498eb6c01d43 (patch)
tree0c799af4d4680a9260c8b6209116b4f1d54b2f28
parentb0690cc786c858b4a41c7682937bebd53d318f6a (diff)
Fix signature matching of an imported datatype vs. a fresh datatype
-rw-r--r--src/elab_print.sml5
-rw-r--r--src/elaborate.sml12
2 files changed, 13 insertions, 4 deletions
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 8a6a651a..637164f4 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -546,7 +546,10 @@ fun p_datatype env (x, n, xs, cons) =
val env = E.pushCNamedAs env x n k NONE
val env = foldl (fn (x, env) => E.pushCRel env x k) env xs
in
- box [string x,
+ box [(if !debug then
+ string (x ^ "_" ^ Int.toString n)
+ else
+ string x),
p_list_sep (box []) (fn x => box [space, string x]) xs,
space,
string "=",
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 85234775..e975cabe 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -3325,8 +3325,14 @@ and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) =
| _ => env
val env = case #1 sgi1All of
L'.SgiDatatype dts1 => dt_pusher (dts1, dts2, env)
- | _ => env
-
+ | _ => foldl (fn ((x2, n2, xs2, _), env) =>
+ let
+ val k = (L'.KType, loc)
+ val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs2
+ in
+ E.pushCNamedAs env x2 n2 k' NONE
+ end) env dts2
+
val env = foldl (fn (x, env) => E.pushCRel env x k) env xs1
fun xncBad ((x1, _, t1), (x2, _, t2)) =
String.compare (x1, x2) <> EQUAL
@@ -4229,7 +4235,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
L'.StrFun _ => ()
| _ => strError env (FunctorRebind loc))
| _ => ();
- Option.map (fn tm => ModDb.insert (dNew,
+ Option.app (fn tm => ModDb.insert (dNew,
tm,
ErrorMsg.stopElabStructureAndGetErrored x
)) tmo;