isDefEq: constant approximation should permute binder telescope

Prerequisites

• 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

Given two metavariables whose types are telescope permutations of another

?m.1 : ∀ (x : Nat) (n : Fin x) (f : Fin x → Bool) (y : Nat), Bool
?m.2 : ∀ (x : Nat) (y : Nat) (n : Fin x) (f : Fin x → Bool), Bool

The following unification problem succeeds by constant approximation:

n : Nat, x : Fin n, f : Fin n → Bool 
⊢ ?m.1 n x f n =?= f x

whereas the following fails:

n : Nat, x : Fin n, f : Fin n → Bool 
⊢ ?m.2 n n x f =?= f x

Context

I stumbled over this while working on the new do elaborator. I wanted to use isDefEq to assign metavariables standing in for jump sites of join points.

Steps to Reproduce

Run the following metaprogram

import Lean

open Lean Meta

def withConstApprox (x : MetaM α) : MetaM α :=
  withConfig (fun config => { config with constApprox := true }) x

run_meta do
  -- ?m.1 : ∀ (x : Nat) (n : Fin x) (f : Fin x → Bool) (y : Nat), Bool
  let mvar1 ← mkFreshExprMVar <|
    mkForall `x .default Nat.mkType <|
    mkForall `n .default (mkApp (mkConst ``Fin) (.bvar 0)) <|
    mkForall `f .default (mkForall `n .default (mkApp (mkConst ``Fin) (.bvar 1)) (mkConst ``Bool)) <|
    mkForall `y .default Nat.mkType <|
    mkConst ``Bool
  -- ?m.2 : ∀ (x : Nat) (y : Nat) (n : Fin x) (f : Fin x → Bool), Bool
  let mvar2 ← mkFreshExprMVar <|
    mkForall `x .default Nat.mkType <|
    mkForall `y .default Nat.mkType <|
    mkForall `n .default (mkApp (mkConst ``Fin) (.bvar 1)) <|
    mkForall `f .default (mkForall `n .default (mkApp (mkConst ``Fin) (.bvar 2)) (mkConst ``Bool)) <|
    mkConst ``Bool
  -- x : Nat, n : Fin x, f : Fin x → Bool
  withLocalDeclD `x Nat.mkType fun x =>
  withLocalDeclD `n (mkApp (mkConst ``Fin) (.bvar 1)) fun n =>
  withLocalDeclD `f (mkForall `n .default (mkApp (mkConst ``Fin) x) (mkConst ``Bool)) fun f => do
    let lhs := mkApp4 mvar1 x n f x
    let rhs := mkApp f n
    unless ← withConstApprox <| isDefEq lhs rhs do
      throwError "{lhs} =?= {rhs} failed"
    logInfo m!"{lhs} =?= {rhs} succeeded"
    let lhs := mkApp4 mvar2 x x n f
    let rhs := mkApp f n
    unless ← withConstApprox <| isDefEq lhs rhs do
      throwError "{lhs} =?= {rhs} failed"

Expected behavior: Two log messages about successful unification

Actual behavior: failure on the second isDefEq

Versions

Lean 4.28.0-nightly-2025-12-25
Target: x86_64-unknown-linux-gnu

Impact

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

Start with the minimal metaprogram and the isDefEq constant-approximation path, using withConstApprox to reproduce both telescope-permutation cases. Compare the successful and failing unification calls, then verify that both log messages are produced without the second failure.