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]