summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/elaborate.sml10
1 files changed, 9 insertions, 1 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 6ffb7716..c6825150 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -2577,7 +2577,14 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
let
val k' = case ko of
NONE => kunif env loc
- | SOME k => elabKind env k
+ | SOME k =>
+ case #1 k of
+ L.KWild => kunif env loc
+ (* Why duplicate this case of elabKind here?
+ * To avoid flagging a disallowed wildcard in
+ * a signature, since we are guaranteed to
+ * resolve this kind locally during elaboration. *)
+ | _ => elabKind env k
val (c', ck, gs') = elabCon (env, denv) c
val (env', n) = E.pushCNamed env x k' (SOME c')
@@ -4756,6 +4763,7 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file =
val () = mayDelay := true
val () = delayedUnifs := []
val () = delayedExhaustives := []
+ val () = inSignature := false
val d = (L.DFfiStr ("Basis", (L.SgnConst basis, ErrorMsg.dummySpan), SOME basis_tm), ErrorMsg.dummySpan)
val (basis_n, env', sgn) =