:::_ notation; switch to TooDeep error message

6 files changed, 17 insertions, 5 deletions

diff --git a/doc/manual.tex b/doc/manual.tex
index 9dbdb505..ebeb2d55 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -495,7 +495,7 @@ A tuple type $(\tau_1, \ldots, \tau_n)$ expands to a record type $\{1 = \tau_1,
 
 In general, several adjacent $\lambda$ forms may be combined into one, and kind and type annotations may be omitted, in which case they are implicitly included as wildcards.  More formally, for constructor-level abstractions, we can define a new non-terminal $b ::= x \mid (x :: \kappa) \mid X$ and allow composite abstractions of the form $\lambda b^+ \Rightarrow c$, elaborating into the obvious sequence of one core $\lambda$ per element of $b^+$.
 
-In some contexts, the parser isn't happy with token sequences like $x :: \_$, to indicate a constructor variable of wildcard kind.  In such cases, write the second two tokens as $::\hspace{-.05in}\_$, with no intervening spaces.
+In some contexts, the parser isn't happy with token sequences like $x :: \_$, to indicate a constructor variable of wildcard kind.  In such cases, write the second two tokens as $::\hspace{-.05in}\_$, with no intervening spaces.  Analogous syntax $:::\hspace{-.05in}\_$ is available for implicit constructor arguments.
 
 For any signature item or declaration that defines some entity to be equal to $A$ with classification annotation $B$ (e.g., $\mt{val} \; x : B = A$), $B$ and the preceding colon (or similar punctuation) may be omitted, in which case it is filled in as a wildcard.
 
diff --git a/src/elab_err.sig b/src/elab_err.sig
index fbe55a5b..3dfd5d4e 100644
--- a/src/elab_err.sig
+++ b/src/elab_err.sig
@@ -58,6 +58,7 @@ signature ELAB_ERR = sig
            | CRecordFailure of Elab.con * Elab.con * (Elab.con * Elab.con * Elab.con) option
            | TooLifty of ErrorMsg.span * ErrorMsg.span
            | TooUnify of Elab.con * Elab.con
+           | TooDeep
 
     val cunifyError : ElabEnv.env -> cunify_error -> unit
 
diff --git a/src/elab_err.sml b/src/elab_err.sml
index f8a16294..7d5e6be8 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -121,6 +121,7 @@ datatype cunify_error =
        | CRecordFailure of con * con * (con * con * con) option
        | TooLifty of ErrorMsg.span * ErrorMsg.span
        | TooUnify of con * con
+       | TooDeep
 
 fun cunifyError env err =
     case err of
@@ -162,6 +163,7 @@ fun cunifyError env err =
         (ErrorMsg.errorAt (#2 c1) "Substitution in constructor is blocked by a too-deep unification variable";
          eprefaces' [("Replacement", p_con env c1),
                      ("Body", p_con env c2)])
+      | TooDeep => ErrorMsg.error "Can't reverse-engineer unification variable lifting"
 
 datatype exp_error =
        UnboundExp of ErrorMsg.span * string
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 7bf687e2..dcae4650 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1079,13 +1079,13 @@
                  err COccursCheckFailed
              else
                  (r := SOME (squish nl c2All)
-                  handle CantSquish => err CIncompatible)
+                  handle CantSquish => err (fn _ => TooDeep))
            | (_, L'.CUnif (nl, _, _, _, r)) =>
              if occursCon r c1All then
                  err COccursCheckFailed
              else
                  (r := SOME (squish nl c1All)
-                  handle CantSquish => err CIncompatible)
+                  handle CantSquish => err (fn _ => TooDeep))
 
            | (L'.CUnit, L'.CUnit) => ()
 
diff --git a/src/urweb.grm b/src/urweb.grm
index 0c85ad7f..21c4a50c 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -212,7 +212,7 @@ fun tnamesOf (e, _) =
  | STRING of string | INT of Int64.int | FLOAT of Real64.real | CHAR of char
  | SYMBOL of string | CSYMBOL of string
  | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE
- | EQ | COMMA | COLON | DCOLON | DCOLONWILD | TCOLON | DOT | HASH | UNDER | UNDERUNDER | BAR
+ | EQ | COMMA | COLON | DCOLON | DCOLONWILD | TCOLON | TCOLONWILD | DOT | HASH | UNDER | UNDERUNDER | BAR
  | PLUS | MINUS | DIVIDE | DOTDOTDOT | MOD | AT
  | CON | LTYPE | VAL | REC | AND | FUN | MAP | UNIT | KUNIT | CLASS
  | DATATYPE | OF
@@ -394,7 +394,7 @@ fun tnamesOf (e, _) =
 %left ANDALSO
 %left ORELSE
 %nonassoc COLON
-%nonassoc DCOLON TCOLON
+%nonassoc DCOLON TCOLON DCOLONWILD TCOLONWILD
 %left UNION INTERSECT EXCEPT
 %right COMMA
 %right JOIN INNER CROSS OUTER LEFT RIGHT FULL
@@ -1111,6 +1111,14 @@ earga  : LBRACK SYMBOL RBRACK            (fn (e, t) =>
                                                  ((ECAbs (kcolon, SYMBOL, kind, e), loc),
                                                   (TCFun (kcolon, SYMBOL, kind, t), loc))
                                              end)
+       | LBRACK SYMBOL TCOLONWILD RBRACK (fn (e, t) =>
+                                             let
+                                                 val loc = s (LBRACKleft, RBRACKright)
+                                                 val kind = (KWild, loc)
+                                             in
+                                                 ((ECAbs (Implicit, SYMBOL, kind, e), loc),
+                                                  (TCFun (Implicit, SYMBOL, kind, t), loc))
+                                             end)
        | LBRACK cexp TWIDDLE cexp RBRACK(fn (e, t) =>
                                             let
                                                 val loc = s (LBRACKleft, RBRACKright)
diff --git a/src/urweb.lex b/src/urweb.lex
index a6df5f1b..fa8c5dde 100644
--- a/src/urweb.lex
+++ b/src/urweb.lex
@@ -371,6 +371,7 @@ xint = x[0-9a-fA-F][0-9a-fA-F];
 <INITIAL> "<="        => (Tokens.LE (pos yypos, pos yypos + size yytext));
 <INITIAL> ">="        => (Tokens.GE (pos yypos, pos yypos + size yytext));
 <INITIAL> ","         => (Tokens.COMMA (pos yypos, pos yypos + size yytext));
+<INITIAL> ":::_"      => (Tokens.TCOLONWILD (pos yypos, pos yypos + size yytext));
 <INITIAL> ":::"       => (Tokens.TCOLON (pos yypos, pos yypos + size yytext));
 <INITIAL> "::_"       => (Tokens.DCOLONWILD (pos yypos, pos yypos + size yytext));
 <INITIAL> "::"        => (Tokens.DCOLON (pos yypos, pos yypos + size yytext));