fix: loose bound variables in Sym.dsimp binder telescopes (#14029)

This PR fixes a `Sym.dsimp` bug that could produce an ill-typed term,
causing the kernel to reject the resulting goal with errors such as
`application type mismatch` or `function expected`. It triggered when a
`let`/`λ`/`∀` binder's type or value referenced an earlier binder in the
same telescope.

A regression test `tests/elab/sym_dsimp_bug.lean` reproduces the
original kernel error and confirms `dsimp` now produces a well-typed
goal.

Author: leodemoura

src/Lean/Meta/Sym/DSimp/Forall.lean

@@ -22,7 +22,11 @@ where
   go (e : Expr) (fvars : Array Expr) (modified : Bool) : DSimpM Result := do
     match e with
     | .forallE n d b c =>
-      match (← dsimp (← instantiateRevBetaS d fvars)) with
+      -- Instantiate the binder domain against the already-introduced `fvars` *before* creating
+      -- the local declaration, otherwise the decl retains loose bound variables referring to
+      -- earlier binders in this telescope.
+      let d ← instantiateRevBetaS d fvars
+      match (← dsimp d) with
       | .rfl _ => withLocalDecl n c d fun x => go b (fvars.push x) modified
       | .step d' _ => withLocalDecl n c d' fun x => go b (fvars.push x) true
     | _ =>

src/Lean/Meta/Sym/DSimp/Lambda.lean

@@ -22,7 +22,11 @@ where
   go (e : Expr) (fvars : Array Expr) (modified : Bool) : DSimpM Result := do
     match e with
     | .lam n d b c =>
-      match (← dsimp (← instantiateRevBetaS d fvars)) with
+      -- Instantiate the binder domain against the already-introduced `fvars` *before* creating
+      -- the local declaration, otherwise the decl retains loose bound variables referring to
+      -- earlier binders in this telescope.
+      let d ← instantiateRevBetaS d fvars
+      match (← dsimp d) with
       | .rfl _ => withLocalDecl n c d fun x => go b (fvars.push x) modified
       | .step d' _ => withLocalDecl n c d' fun x => go b (fvars.push x) true
     | _ =>

src/Lean/Meta/Sym/DSimp/Let.lean

@@ -19,7 +19,13 @@ where
   go (e : Expr) (fvars : Array Expr) (modified : Bool) : DSimpM Result := do
     match e with
     | .letE n t v b nd =>
-      match (← dsimp (← instantiateRevBetaS t fvars)), (← dsimp (← instantiateRevBetaS v fvars)) with
+      -- Instantiate the binder type and value against the already-introduced `fvars` *before*
+      -- creating the local declaration. Using the raw `t`/`v` would leave loose bound variables
+      -- (referring to earlier binders in this telescope) in the decl, which get misinterpreted
+      -- once the decl is zeta-expanded under a different binder.
+      let t ← instantiateRevBetaS t fvars
+      let v ← instantiateRevBetaS v fvars
+      match (← dsimp t), (← dsimp v) with
       | .rfl _, .rfl _ =>
         withLetDecl n t v (nondep := nd) fun x => go b (fvars.push x) modified
       | .step t' _, .rfl _ =>

tests/elab/sym_dsimp_bug.lean

@@ -0,0 +1,33 @@
+/-! # Regression test for `Sym.dsimp` binder handling
+
+`dsimp` introduces telescope binders by re-instantiating each binder's type/value
+against the free variables already introduced. A previous version created the local
+declarations from the *raw* binder type/value, leaving loose bound variables that were
+later misinterpreted when the declaration was zeta-expanded under a different binder
+(here the `_unit` lambda), producing an ill-typed term the kernel rejected. -/
+
+inductive Effects where
+  | done_val : BitVec 64 → Effects
+  | other : Effects
+  | require_exec_access : (Unit → Effects) → Effects
+
+def Effects.All (post : Effects → Prop) : Effects → Prop
+  | .done_val v => post (.done_val v)
+  | .other => False
+  | .require_exec_access cont => (cont ()).All post
+
+structure MyState where
+  zf : Bool
+
+register_sym_dsimp myVariant where
+  pre := proj
+
+set_option warn.sorry false
+
+theorem test_error (x : BitVec 64) (post : Effects → Prop) :
+    let v := x + 1
+    let status := MyState.mk (v == 0)
+    Effects.All post (Effects.require_exec_access (fun _unit => if status.zf then Effects.done_val v else Effects.other)) := by
+  sym =>
+  dsimp myVariant
+  sorry