From 578b3b822fcc3d7c5c12e2d1c4c604ef1b78b048 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 7 Apr 2021 20:16:10 -0700
Subject: [PATCH] fix: do not use `nullKind` for `group` combinator

We use `nullKind` for the `group` parser combinator.
When pattern matching `nullKind` nodes, we check their arities.
So, error recovery often fails for parsers that use the `group`
combinator.
For example, we have the parser
```
def whereDecls := leading_parser "where " >> many1Indent (group (letRecDecl >> optional ";"))
```
If there is syntax error at `letRecDecl`, the node corresponding to
```
group (letRecDecl >> optional ";")
```
will contain only one child, and the pattern matching at
```
def expandWhereDecls (whereDecls : Syntax) (body : Syntax) : MacroM Syntax :=
  match whereDecls with
  | `(whereDecls|where $[$decls:letRecDecl $[;]?]*) => `(let rec $decls:letRecDecl,*; $body)
  | _ => Macro.throwUnsupported
```
fails, and we can't elaborate the partial syntax tree for
`letRecDecl`, and auto-completion will not work there.

We address this issue by using a new kind for the `group` combinator.
The idea is to pattern match `group` as we pattern match `node`s with
proper syntax node kinds. This change is consistent with the way we
use `group` where it mainly a convenience for saving us the trouble of
defining a new parser definition that is used only once.
---
 src/Init/Prelude.lean         | 1 +
 src/Lean/Elab/StructInst.lean | 2 +-
 src/Lean/Parser/Extra.lean    | 2 +-
 3 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 9e4da15fd0..7142f101df 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1673,6 +1673,7 @@ instance : Inhabited Syntax where
 /- Builtin kinds -/
 def choiceKind : SyntaxNodeKind := `choice
 def nullKind : SyntaxNodeKind := `null
+def groupKind : SyntaxNodeKind := `group
 def identKind : SyntaxNodeKind := `ident
 def strLitKind : SyntaxNodeKind := `strLit
 def charLitKind : SyntaxNodeKind := `charLit
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index e48995994d..d087d02b64 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -283,7 +283,7 @@ private def toFieldLHS (stx : Syntax) : Except String FieldLHS :=
     return FieldLHS.modifyOp stx stx[1]
   else
     -- Note that the representation of the first field is different.
-    let stx := if stx.getKind == nullKind then stx[1] else stx
+    let stx := if stx.getKind == groupKind then stx[1] else stx
     if stx.isIdent then
       return FieldLHS.fieldName stx stx.getId.eraseMacroScopes
     else match stx.isFieldIdx? with
diff --git a/src/Lean/Parser/Extra.lean b/src/Lean/Parser/Extra.lean
index 4b4fcaf925..d5aeee2098 100644
--- a/src/Lean/Parser/Extra.lean
+++ b/src/Lean/Parser/Extra.lean
@@ -49,7 +49,7 @@ attribute [runBuiltinParserAttributeHooks]
   withAntiquot (mkAntiquot "nameLit" nameLitKind) nameLitNoAntiquot
 
 @[runBuiltinParserAttributeHooks, inline] def group (p : Parser) : Parser :=
-  node nullKind p
+  node groupKind p
 
 @[runBuiltinParserAttributeHooks, inline] def many1Indent (p : Parser) : Parser :=
   withPosition $ many1 (checkColGe "irrelevant" >> p)