From 2a7c54badfcd4e30105a0127b25975000ff09bbb Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Wed, 18 Sep 2019 13:51:13 -0400
Subject: Disallow wildcards in signatures (should help with #174)

---
 src/elab_err.sig  |  2 ++
 src/elab_err.sml  |  6 ++++++
 src/elaborate.sml | 35 ++++++++++++++++++++++++++---------
 tests/wildsig.ur  |  7 +++++++
 4 files changed, 41 insertions(+), 9 deletions(-)
 create mode 100644 tests/wildsig.ur

diff --git a/src/elab_err.sig b/src/elab_err.sig
index acf137df..fc80fcac 100644
--- a/src/elab_err.sig
+++ b/src/elab_err.sig
@@ -29,6 +29,7 @@ signature ELAB_ERR = sig
 
     datatype kind_error =
              UnboundKind of ErrorMsg.span * string
+           | KDisallowedWildcard of ErrorMsg.span
 
     val kindError : ElabEnv.env -> kind_error -> unit
 
@@ -47,6 +48,7 @@ signature ELAB_ERR = sig
            | DuplicateField of ErrorMsg.span * string
            | ProjBounds of Elab.con * int
            | ProjMismatch of Elab.con * Elab.kind
+           | CDisallowedWildcard of ErrorMsg.span
 
     val conError : ElabEnv.env -> con_error -> unit
 
diff --git a/src/elab_err.sml b/src/elab_err.sml
index 385caca3..bbe1c160 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -40,11 +40,14 @@ val p_kind = P.p_kind
              
 datatype kind_error =
          UnboundKind of ErrorMsg.span * string
+       | KDisallowedWildcard of ErrorMsg.span
 
 fun kindError env err =
     case err of
         UnboundKind (loc, s) =>
         ErrorMsg.errorAt loc ("Unbound kind variable " ^ s)
+      | KDisallowedWildcard loc =>
+        ErrorMsg.errorAt loc "Wildcard not allowed in signature"
 
 datatype kunify_error =
          KOccursCheckFailed of kind * kind
@@ -76,6 +79,7 @@ datatype con_error =
        | DuplicateField of ErrorMsg.span * string
        | ProjBounds of con * int
        | ProjMismatch of con * kind
+       | CDisallowedWildcard of ErrorMsg.span
 
 fun conError env err =
     case err of
@@ -101,6 +105,8 @@ fun conError env err =
         (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor";
          eprefaces' [("Constructor", p_con env c),
                      ("Kind", p_kind env k)])
+      | CDisallowedWildcard loc =>
+        ErrorMsg.errorAt loc "Wildcard not allowed in signature"
 
 datatype cunify_error =
          CKind of kind * kind * E.env * kunify_error
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 97b36a0b..6ffb7716 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -260,6 +260,19 @@
 
  end
 
+ (* Wildcards are disallowed inside signatures.
+  * We use a flag to indicate when we are in a signature,
+  * with a helper function for entering this mode and properly backing out afterward. *)
+ val inSignature = ref false
+ fun enterSignature f =
+     let
+         val inS = !inSignature
+     in
+         inSignature := true;
+         (f () handle ex => (inSignature := inS; raise ex))
+         before inSignature := inS
+     end
+ 
  fun elabKind env (k, loc) =
      case k of
          L.KType => (L'.KType, loc)
@@ -268,7 +281,7 @@
        | L.KRecord k => (L'.KRecord (elabKind env k), loc)
        | L.KUnit => (L'.KUnit, loc)
        | L.KTuple ks => (L'.KTuple (map (elabKind env) ks), loc)
-       | L.KWild => kunif env loc
+       | L.KWild => if !inSignature then (kindError env (KDisallowedWildcard loc); kerror) else kunif env loc
 
        | L.KVar s => (case E.lookupK env s of
                           NONE =>
@@ -531,11 +544,15 @@
          end
 
        | L.CWild k =>
-         let
-             val k' = elabKind env k
-         in
-             (cunif env (loc, k'), k', [])
-         end
+         if !inSignature then
+             (conError env (CDisallowedWildcard loc);
+              (cerror, kerror, []))
+         else
+             let
+                 val k' = elabKind env k
+             in
+                 (cunif env (loc, k'), k', [])
+             end
 
  fun kunifsRemain k =
      case k of
@@ -4146,7 +4163,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
 
               | L.DSgn (x, sgn) =>
                 let
-                    val (sgn', gs') = elabSgn (env, denv) sgn
+                    val (sgn', gs') = enterSignature (fn () => elabSgn (env, denv) sgn)
                     val (env', n) = E.pushSgnNamed env x sgn'
                 in
                     ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, enD gs' @ gs))
@@ -4171,7 +4188,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
                                   else
                                       ()
 
-                         val formal = Option.map (elabSgn (env, denv)) sgno
+                         val formal = enterSignature (fn () => Option.map (elabSgn (env, denv)) sgno)
 
                          val (str', sgn', gs') =
                              case formal of
@@ -4221,7 +4238,7 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
                      end
                    | NONE =>
                      let
-                         val (sgn', gs') = elabSgn (env, denv) sgn
+                         val (sgn', gs') = enterSignature (fn () => elabSgn (env, denv) sgn)
                                            
                          val (env', n) = E.pushStrNamed env x sgn'
 
diff --git a/tests/wildsig.ur b/tests/wildsig.ur
new file mode 100644
index 00000000..336772a7
--- /dev/null
+++ b/tests/wildsig.ur
@@ -0,0 +1,7 @@
+signature S = sig
+    val x : _
+end
+
+structure M : S = struct
+    val x = 7
+end
-- 
cgit v1.2.3