fix: syntax: do not qualify fresh kinds

src/Init/Lean/Data/Name.lean

@@ -27,6 +27,13 @@ def getPrefix : Name → Name
 | str p s _ => p
 | num p s _ => p
 
+def getRoot : Name → Name
+| anonymous             => anonymous
+| n@(str anonymous _ _) => n
+| n@(num anonymous _ _) => n
+| str n _ _             => getRoot n
+| num n _ _             => getRoot n
+
 def getNumParts : Name → Nat
 | anonymous => 0
 | str p _ _ => getNumParts p + 1

src/Init/Lean/Elab/Syntax.lean

@@ -153,10 +153,14 @@ pure kind
 private def elabKind (stx : Syntax) (catName : Name) : CommandElabM Name := do
 if stx.isNone then
   mkFreshKind catName
-else do
+else
   let kind := stx.getIdAt 1;
-  currNamespace ← getCurrNamespace;
-  pure (currNamespace ++ kind)
+  if kind.getRoot == `_kind then
+    -- unique fresh kind, do not qualify
+    pure kind
+  else do
+    currNamespace ← getCurrNamespace;
+    pure (currNamespace ++ kind)
 
 @[builtinCommandElab «syntax»] def elabSyntax : CommandElab :=
 fun stx => do

tests/lean/run/macro2.lean

@@ -2,6 +2,9 @@ new_frontend
 
 notation a `**`:50 b:50 => b * a * b
 notation "~" a => a+a
+namespace Foo
+notation "~~" a => a+a
+end Foo
 
 syntax term "+++":60 term:59 : term