From eb25b975015daba3c7ea32d03fe601f41532797d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 16 Jan 2021 08:23:45 -0800
Subject: [PATCH] fix: pattern variables cannot shadow each other

---
 src/Lean/PrettyPrinter/Delaborator/Builtins.lean | 12 +++++++++---
 tests/lean/match1.lean.expected.out              |  2 +-
 2 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 1e08f4844d..f76528847b 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -188,9 +188,15 @@ private def skippingBinders {α} (numParams : Nat) (x : Array Name → DelabM α
 where
   loop : Nat → Array Name → DelabM α
     | 0,   varNames => x varNames
-    | n+1, varNames =>
-      withBindingBodyUnusedName fun id => do
-        loop n (varNames.push id.getId)
+    | n+1, varNames => do
+      let varName ← (← getExpr).bindingName!.eraseMacroScopes
+      -- Pattern variables cannot shadow each other
+      if varNames.contains varName then
+        let varName := (← getLCtx).getUnusedName varName
+        loop n (varNames.push varName)
+      else
+        withBindingBodyUnusedName fun id => do
+          loop n (varNames.push id.getId)
 
 /--
   Delaborate applications of "matchers" such as
diff --git a/tests/lean/match1.lean.expected.out b/tests/lean/match1.lean.expected.out
index 7e3f972815..8641cfd2b2 100644
--- a/tests/lean/match1.lean.expected.out
+++ b/tests/lean/match1.lean.expected.out
@@ -34,7 +34,7 @@ fun (x : Nat × Nat) =>
 fun (x x_1 : Option Nat) =>
   match x, x_1 with 
   | some a, some b => some (a + b)
-  | x, x => none : Option Nat → Option Nat → Option Nat
+  | x, x_2 => fun (x : Option Nat) => none : Option Nat → Option Nat → Option Nat
 fun (x : Nat) =>
   (match x with 
     | 0 => id