From 72bb7cf3647792dcb31c7f97a21784cc174b380b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sat, 20 Sep 2025 09:26:46 -0700
Subject: [PATCH] fix: `infer_let` in the kernel (#10476)

This PR fixes the dead `let` elimination code in the kernel's
`infer_let` function.

Closes #10475
---
 src/kernel/type_checker.cpp | 34 +---------------------------------
 tests/lean/run/10475.lean   | 29 +++++++++++++++++++++++++++++
 2 files changed, 30 insertions(+), 33 deletions(-)
 create mode 100644 tests/lean/run/10475.lean

diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 36a039e6ff..98d7022094 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -195,33 +195,15 @@ expr type_checker::infer_app(expr const & e, bool infer_only) {
     }
 }
 
-static void mark_used(unsigned n, expr const * fvars, expr const & b, bool * used) {
-    if (!has_fvar(b)) return;
-    for_each(b, [&](expr const & x) {
-            if (!has_fvar(x)) return false;
-            if (is_fvar(x)) {
-                for (unsigned i = 0; i < n; i++) {
-                    if (fvar_name(fvars[i]) == fvar_name(x)) {
-                        used[i] = true;
-                        return false;
-                    }
-                }
-            }
-            return true;
-        });
-}
-
 expr type_checker::infer_let(expr const & _e, bool infer_only) {
     flet<local_ctx> save_lctx(m_lctx, m_lctx);
     buffer<expr> fvars;
-    buffer<expr> vals;
     expr e = _e;
     while (is_let(e)) {
         expr type = instantiate_rev(let_type(e), fvars.size(), fvars.data());
         expr val  = instantiate_rev(let_value(e), fvars.size(), fvars.data());
         expr fvar = m_lctx.mk_local_decl(m_st->m_ngen, let_name(e), type, val);
         fvars.push_back(fvar);
-        vals.push_back(val);
         if (!infer_only) {
             ensure_sort_core(infer_type_core(type, infer_only), type);
             expr val_type = infer_type_core(val, infer_only);
@@ -233,21 +215,7 @@ expr type_checker::infer_let(expr const & _e, bool infer_only) {
     }
     expr r = infer_type_core(instantiate_rev(e, fvars.size(), fvars.data()), infer_only);
     r = cheap_beta_reduce(r); // use `cheap_beta_reduce` (to try) to reduce number of dependencies
-    buffer<bool, 128> used;
-    used.resize(fvars.size(), false);
-    mark_used(fvars.size(), fvars.data(), r, used.data());
-    unsigned i = fvars.size();
-    while (i > 0) {
-        --i;
-        if (used[i])
-            mark_used(i, fvars.data(), vals[i], used.data());
-    }
-    buffer<expr> used_fvars;
-    for (unsigned i = 0; i < fvars.size(); i++) {
-        if (used[i])
-            used_fvars.push_back(fvars[i]);
-    }
-    return m_lctx.mk_pi(used_fvars, r);
+    return m_lctx.mk_pi(fvars, r, true);
 }
 
 expr type_checker::infer_proj(expr const & e, bool infer_only) {
diff --git a/tests/lean/run/10475.lean b/tests/lean/run/10475.lean
new file mode 100644
index 0000000000..e1fb654bfb
--- /dev/null
+++ b/tests/lean/run/10475.lean
@@ -0,0 +1,29 @@
+import Lean
+open Lean
+
+/--
+info: let y : Type := Prop;
+let x : y := True;
+p x
+---
+info: let y : Type := Prop;
+let x : y := True;
+x
+---
+info: let y : Type := Prop;
+y
+-/
+#guard_msgs in
+set_option pp.letVarTypes true in
+example (p : ∀ a, a) :
+    (let y := Prop; let x : y := True; p x) = p True := by
+  run_tac
+    let env ← Lean.getEnv
+    let lctx ← getLCtx
+    let_expr Eq _ lhs _ := (← Elab.Tactic.getMainTarget) | unreachable!
+    logInfo lhs
+    let ty ← ofExceptKernelException <| Lean.Kernel.check env lctx lhs
+    logInfo ty
+    let sort ← ofExceptKernelException <| Lean.Kernel.check env lctx ty
+    logInfo sort
+  trivial