From e931c6b5b576e446151f14bc45eecd2d0965d36c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 15 Aug 2022 12:41:02 -0700
Subject: [PATCH] fix: bug at `toLCNF`

---
 src/Lean/Compiler/LCNF.lean | 2 +-
 tests/lean/run/lcnf2.lean   | 7 +++++++
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Compiler/LCNF.lean b/src/Lean/Compiler/LCNF.lean
index 30c9fc5284..f555477ece 100644
--- a/src/Lean/Compiler/LCNF.lean
+++ b/src/Lean/Compiler/LCNF.lean
@@ -440,7 +440,7 @@ where
         visitLet body (xs.push value)
       else
         let type' ← liftMetaM <| toLCNFType type
-        let value' ← visitChild value
+        let value' ← visit value
         let x ← mkLetDecl binderName type value type' value'
         visitLet body (xs.push x)
     | _ =>
diff --git a/tests/lean/run/lcnf2.lean b/tests/lean/run/lcnf2.lean
index b44b9e7eca..e367f40b94 100644
--- a/tests/lean/run/lcnf2.lean
+++ b/tests/lean/run/lcnf2.lean
@@ -33,3 +33,10 @@ noncomputable abbrev TupleN : (n : Fin 1) → TupleNTyp n.val
 
 set_option pp.proofs true
 #eval Compiler.compile #[``TupleN]
+
+
+def userControlled (a b : Nat) :=
+  let f := fun _ => a
+  f () + b
+
+#eval Compiler.compile #[``userControlled]