Metavariables under binders can create terms that can become type incorrect after basic tactics

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

It's possible to create type incorrect terms using core tactics when there are delayed assignment metavariables.

Context

This came up while debugging the clear_value tactic, which relies on isTypeCorrect to determine whether a value can actually be cleared. When there are delayed assigned metavariables under let declarations, the abstracted metavariable has a type that takes the let value as an argument. There is nothing in the types that ensures that this value actually has the definitional properties that it is meant to have. Because of this, it's possible to rw it to something else and create a type-incorrect term.

For clear_value specifically, I am working around the issue by instantiating metavariables first and hoping there are no unsolved goals appearing in any of the types. This works in the common case at least.

The issue was initially noticed in https://github.com/leanprover-community/mathlib4/issues/25053 and then pointed out in the comments on the clear_value tactic PR #8449.

Steps to Reproduce

Actual behavior: The following has a kernel-caught type mismatch.

theorem thm (n : Nat) : n = (1 + n) - 1 := by
  rw [Nat.one_add_sub_one]

example (n : Nat) : True := by
  have : 0 = (fun k : Nat => let v := n + 1; ?mv) 0 * 0 := by
    conv =>
      enter [2,1,0,k,v]
      rw [thm v]
    rw [Nat.mul_zero]
  case mv =>
    have hv : v = n + 1 := rfl
    exact k
  trivial
/-
(kernel) application type mismatch
  letFun ⋯
argument has type
  1 + v - 1 = 1 + v - 1
but function has type
  (v_1 : 1 + v - 1 = n + 1) → ((x : 1 + v - 1 = n + 1) → (fun hv => Nat) x) → (fun hv => Nat) v_1
-/

Expected behavior: No errors.

Versions

Lean 4.21.0-nightly-2025-05-26
Target: x86_64-unknown-linux-gnu

Additional Information

When set_option pp.mvars.delayed true, the first state in the have shows fun k => let v := n + 1; ?m.234 k v with ?m.234 : Nat → Nat → Nat. Notice that v is being passed as an argument. The ?mv metavariable has v : Nat := n + 1, and so the passed v must be definitionally equal to n + 1.

I'm not sure how this can be fixed; we do need to pass v as the second argument to link together the contexts. We don't want to abstract the lets while instantiating metavariables since there would be extra lets.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the minimal reproduction in the issue and inspect the core tactic paths involving delayed metavariables, let binders, rw, and isTypeCorrect. Done means the reproducer no longer allows a kernel-caught type mismatch while preserving the context-linking behavior described for clear_value.