lean-0004: Kernel infer_let ignores dependencies in let-binding types

The kernel's infer_let decides which variables to abstract in the result type without accounting for dependencies in the type of a let binding, so inferType/check can return an expression with a loose free variable and a second check on it fails. The second kernel bug found by the Lean4Lean verification; the reporter did not find an exploit.

Reproduction

Shows the bug on Lean v4.24.0. Adapted from #10475. bugs/lean-0004.lean

/-
On v4.24.0 the second `Kernel.check` fails with "type expected", because the first
returned a type with a loose free variable. On v4.25.0 and later all three checks succeed.
From the issue, with `trivial` added to close the goal.
-/

import Lean
open Lean

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 (_, lhs, _) := (← Elab.Tactic.getMainTarget).eq?.get!
    logInfo lhs -- let y := Prop; let x : y := True; p x
    let ty ← ofExceptKernelException <| Lean.Kernel.check env lctx lhs
    logInfo ty -- let x : _kernel_fresh.0 := True; x
    let sort ← ofExceptKernelException <| Lean.Kernel.check env lctx ty
    logInfo sort -- (kernel) type expected: x
  trivial