fix: unhygiene in expandExplicitBinders

src/Init/NotationExtra.lean

@@ -46,7 +46,7 @@ def expandBrackedBindersAux (combinator : Syntax) (binders : Array Syntax) (body
   loop binders.size body
 
 def expandExplicitBinders (combinatorDeclName : Name) (explicitBinders : Syntax) (body : Syntax) : MacroM Syntax := do
-  let combinator := mkIdentFrom (← getRef) combinatorDeclName
+  let combinator := mkCIdentFrom (← getRef) combinatorDeclName
   let explicitBinders := explicitBinders[0]
   if explicitBinders.getKind == ``Lean.unbracketedExplicitBinders then
     let idents   := explicitBinders[0].getArgs
@@ -58,7 +58,7 @@ def expandExplicitBinders (combinatorDeclName : Name) (explicitBinders : Syntax)
     Macro.throwError "unexpected explicit binder"
 
 def expandBrackedBinders (combinatorDeclName : Name) (bracketedExplicitBinders : Syntax) (body : Syntax) : MacroM Syntax := do
-  let combinator := mkIdentFrom (← getRef) combinatorDeclName
+  let combinator := mkCIdentFrom (← getRef) combinatorDeclName
   expandBrackedBindersAux combinator #[bracketedExplicitBinders] body
 
 syntax unifConstraint := term patternIgnore(" =?= " <|> " ≟ ") term

tests/lean/expandExplicitBinders.lean

@@ -0,0 +1,7 @@
+namespace MySigma
+  /-- We define a new `Sigma` -/
+  def Sigma {α : Type u} (β : α → Type v)
+    := String
+
+  #reduce Σ a, a -- This should not reduce to `String`
+end MySigma

tests/lean/expandExplicitBinders.lean.expected.out

@@ -0,0 +1 @@
+(a : Type u_1) × a