From fb2fea2744c3543e4600a5912850ec580f11639b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 10 Oct 2020 06:42:45 -0700
Subject: [PATCH] fix: explicit syntax kind in `macro_rules`

---
 src/Lean/Elab/Syntax.lean                  | 21 ++++++++++-----------
 tests/lean/run/stxKindInsideNamespace.lean | 12 ++++++++++++
 2 files changed, 22 insertions(+), 11 deletions(-)
 create mode 100644 tests/lean/run/stxKindInsideNamespace.lean

diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 919d685f90..72a73ab1b6 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -214,19 +214,19 @@ pure $ Lean.addMacroScope mainModule (mkKindName catName) scp
 def Macro.mkFreshKind (catName : Name) : MacroM Name :=
 Macro.addMacroScope (mkKindName catName)
 
+def mkKind (stx : Syntax) : CommandElabM Name := do
+let kind := stx.getId;
+if kind.hasMacroScopes then
+  pure kind
+else do
+  currNamespace ← getCurrNamespace;
+  pure (currNamespace ++ kind)
+
 private def elabKindPrio (stx : Syntax) (catName : Name) : CommandElabM (Name × Nat) := do
 if stx.isNone then do
   k ← mkFreshKind catName;
   pure (k, 0)
 else
-  let mkKind (stx : Syntax) : CommandElabM Name := do {
-    let kind := stx.getId;
-    if kind.hasMacroScopes then
-      pure kind
-    else do
-      currNamespace ← getCurrNamespace;
-      pure (currNamespace ++ kind)
-  };
   let arg := stx.getArg 1;
   if arg.getKind == `Lean.Parser.Command.parserKind then do
     k ← mkKind (arg.getArg 0);
@@ -242,7 +242,6 @@ else
   else
     throwError "unexpected syntax kind/priority"
 
-
 /- We assume a new syntax can be treated as an atom when it starts and ends with a token.
    Here are examples of atom-like syntax.
    ```
@@ -344,8 +343,8 @@ else do
 adaptExpander $ fun stx => match_syntax stx with
 | `(macro_rules $alts:matchAlt*)           => elabNoKindMacroRulesAux alts
 | `(macro_rules | $alts:matchAlt*)         => elabNoKindMacroRulesAux alts
-| `(macro_rules [$kind] $alts:matchAlt*)   => elabMacroRulesAux kind.getId alts
-| `(macro_rules [$kind] | $alts:matchAlt*) => elabMacroRulesAux kind.getId alts
+| `(macro_rules [$kind] $alts:matchAlt*)   => do k ← mkKind kind; elabMacroRulesAux k alts
+| `(macro_rules [$kind] | $alts:matchAlt*) => do k ← mkKind kind; elabMacroRulesAux k alts
 | _                                        => throwUnsupportedSyntax
 
 @[builtinMacro Lean.Parser.Command.mixfix] def expandMixfix : Macro :=
diff --git a/tests/lean/run/stxKindInsideNamespace.lean b/tests/lean/run/stxKindInsideNamespace.lean
new file mode 100644
index 0000000000..9103957e6d
--- /dev/null
+++ b/tests/lean/run/stxKindInsideNamespace.lean
@@ -0,0 +1,12 @@
+new_frontend
+
+namespace Foo
+
+syntax[foo] "bla!" term : term
+
+macro_rules[foo]
+| `(bla! $x) => pure x
+
+#check bla! 10
+
+end Foo