From ef4e0c207abd0e41badf7bf0052b498eb6c01d43 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Fri, 7 Feb 2020 10:34:21 -0500 Subject: Fix signature matching of an imported datatype vs. a fresh datatype --- src/elab_print.sml | 5 ++++- src/elaborate.sml | 12 +++++++++--- 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; -- cgit v1.2.3