From d0600b3750c1dfd02ed7529eb62e56e2fcce086f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 4 Sep 2022 16:56:42 -0700
Subject: [PATCH] fix: incorrect binder name being used

cc @hargoniX
---
 src/Lean/Compiler/LCNF/InferType.lean | 5 ++---
 tests/lean/run/lcnfBinderNameBug.lean | 9 +++++++++
 2 files changed, 11 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/lcnfBinderNameBug.lean

diff --git a/src/Lean/Compiler/LCNF/InferType.lean b/src/Lean/Compiler/LCNF/InferType.lean
index 94afc84382..c7eaa05d35 100644
--- a/src/Lean/Compiler/LCNF/InferType.lean
+++ b/src/Lean/Compiler/LCNF/InferType.lean
@@ -202,9 +202,8 @@ def mkAuxJpDecl (params : Array Param) (code : Code) (prefixName := `_jp) : Comp
   mkAuxFunDecl params code prefixName
 
 def mkAuxJpDecl' (fvarId : FVarId) (code : Code) (prefixName := `_jp) : CompilerM FunDecl := do
-  let y ← mkFreshBinderName `_y
-  let yType ← inferType (.fvar fvarId)
-  let params := #[{ fvarId, binderName := y, type := yType }]
+  let localDecl ← getLocalDecl fvarId
+  let params := #[{ fvarId, binderName := localDecl.userName, type := localDecl.type }]
   mkAuxFunDecl params code prefixName
 
 def instantiateForall (type : Expr) (params : Array Param) : CoreM Expr :=
diff --git a/tests/lean/run/lcnfBinderNameBug.lean b/tests/lean/run/lcnfBinderNameBug.lean
new file mode 100644
index 0000000000..da8f895c4b
--- /dev/null
+++ b/tests/lean/run/lcnfBinderNameBug.lean
@@ -0,0 +1,9 @@
+import Lean
+
+def test (a : Nat) :=
+  let foo := match a with
+  | .zero => a
+  | .succ b => b
+  Nat.add foo .zero
+
+#eval Lean.Compiler.compile #[``test]