From 91e3100e30d0862bc4dca9eb957f62d8ebd80149 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 18 Jun 2021 17:43:51 +0200
Subject: [PATCH] fix: properly resolve syntax kinds in macro/elab_rules

---
 src/Lean/Elab/Syntax.lean | 10 ++++++++--
 src/Lean/Elab/Util.lean   | 15 +++++++--------
 2 files changed, 15 insertions(+), 10 deletions(-)

diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 5873fdeb29..7a62ca142d 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.Elab.Command
 import Lean.Parser.Syntax
+import Lean.Elab.Util
 
 namespace Lean.Elab.Term
 /-
@@ -279,6 +280,11 @@ private partial def isAtomLikeSyntax (stx : Syntax) : Bool :=
   else
     kind == `Lean.Parser.Syntax.atom
 
+def resolveSyntaxKind (k : Name) : CommandElabM Name := do
+  checkSyntaxNodeKindAtNamespaces k (← getCurrNamespace)
+  <|>
+  throwError "invalid syntax node kind '{k}'"
+
 @[builtinCommandElab «syntax»] def elabSyntax : CommandElab := fun stx => do
   let `($[$doc?:docComment]? $attrKind:attrKind syntax $[: $prec? ]? $[(name := $name?)]? $[(priority := $prio?)]? $[$ps:stx]* : $catStx) ← pure stx
     | throwUnsupportedSyntax
@@ -382,7 +388,7 @@ def expandNoKindMacroRulesAux (alts : Array Syntax) (cmdName : String) (mkCmd :
   | `($[$doc?:docComment]? $attrKind:attrKind macro_rules (kind := $kind) | $x:ident => $rhs) =>
     `($[$doc?:docComment]? @[$attrKind:attrKind macro $kind] def myMacro : Macro := fun $x:ident => $rhs)
   | `($[$doc?:docComment]? $attrKind:attrKind macro_rules (kind := $kind) $alts:matchAlt*) =>
-    do elabMacroRulesAux doc? attrKind ((← getCurrNamespace) ++ kind.getId) alts
+    do elabMacroRulesAux doc? attrKind (← resolveSyntaxKind kind.getId) alts
   | _  => throwUnsupportedSyntax
 
 @[builtinMacro Lean.Parser.Command.mixfix] def expandMixfix : Macro := fun stx =>
@@ -630,7 +636,7 @@ def elabElabRulesAux (doc? : Option Syntax) (attrKind : Syntax) (k : SyntaxNodeK
     expandNoKindMacroRulesAux alts "elab_rules" fun kind? alts =>
       `($[$doc?:docComment]? $attrKind:attrKind elab_rules $[(kind := $(mkIdent <$> kind?))]? $[: $cat?]? $[<= $expty?]? $alts:matchAlt*)
   | `($[$doc?:docComment]? $attrKind:attrKind elab_rules (kind := $kind) $[: $cat?]? $[<= $expty?]? $alts:matchAlt*) =>
-    do elabElabRulesAux doc? attrKind ((← getCurrNamespace) ++ kind.getId) cat? expty? alts
+    do elabElabRulesAux doc? attrKind (← resolveSyntaxKind kind.getId) cat? expty? alts
   | _  => throwUnsupportedSyntax
 
 @[builtinMacro Lean.Parser.Command.elab]
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index 0bebe240c8..1fc0fca766 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -66,23 +66,22 @@ def addMacroStack {m} [Monad m] [MonadOptions m] (msgData : MessageData) (macroS
         msgData ++ Format.line ++ "while expanding" ++ indentD elem.before)
       msgData
 
-def checkSyntaxNodeKind (k : Name) : AttrM Name := do
+def checkSyntaxNodeKind [Monad m] [MonadEnv m] [MonadError m] (k : Name) : m Name := do
   if Parser.isValidSyntaxNodeKind (← getEnv) k then pure k
   else throwError "failed"
 
-def checkSyntaxNodeKindAtNamespacesAux (k : Name) : Name → AttrM Name
-  | n@(Name.str p _ _) => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespacesAux k p
+def checkSyntaxNodeKindAtNamespaces [Monad m] [MonadEnv m] [MonadError m] (k : Name) : Name → m Name
+  | n@(Name.str p _ _) => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespaces k p
+  | Name.anonymous     => checkSyntaxNodeKind k
   | _ => throwError "failed"
 
-def checkSyntaxNodeKindAtNamespaces (k : Name) : AttrM Name := do
+def checkSyntaxNodeKindAtCurrentNamespaces (k : Name) : AttrM Name := do
   let ctx ← read
-  checkSyntaxNodeKindAtNamespacesAux k ctx.currNamespace
+  checkSyntaxNodeKindAtNamespaces k ctx.currNamespace
 
 def syntaxNodeKindOfAttrParam (defaultParserNamespace : Name) (stx : Syntax) : AttrM SyntaxNodeKind := do
   let k ← Attribute.Builtin.getId stx
-  checkSyntaxNodeKind k
-  <|>
-  checkSyntaxNodeKindAtNamespaces k
+  checkSyntaxNodeKindAtCurrentNamespaces k
   <|>
   checkSyntaxNodeKind (defaultParserNamespace ++ k)
   <|>