From 3f6c5f17db30c2a2dcaca1b9e9faec4e2cf04b95 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 22 Feb 2023 17:07:31 +0100 Subject: [PATCH] fix: unhygiene in `expandExplicitBinders` --- src/Init/NotationExtra.lean | 4 ++-- tests/lean/expandExplicitBinders.lean | 7 +++++++ tests/lean/expandExplicitBinders.lean.expected.out | 1 + 3 files changed, 10 insertions(+), 2 deletions(-) create mode 100644 tests/lean/expandExplicitBinders.lean create mode 100644 tests/lean/expandExplicitBinders.lean.expected.out diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean index 670a321724..8e025b0f2a 100644 --- a/src/Init/NotationExtra.lean +++ b/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 diff --git a/tests/lean/expandExplicitBinders.lean b/tests/lean/expandExplicitBinders.lean new file mode 100644 index 0000000000..536477bdb4 --- /dev/null +++ b/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 diff --git a/tests/lean/expandExplicitBinders.lean.expected.out b/tests/lean/expandExplicitBinders.lean.expected.out new file mode 100644 index 0000000000..e334da3cbc --- /dev/null +++ b/tests/lean/expandExplicitBinders.lean.expected.out @@ -0,0 +1 @@ +(a : Type u_1) × a