isDefEq: constant approximation should permute binder telescope

[sgraf812]

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.

[sgraf812]

The reason the second unification problem fails is because constant approximation will try

n : Nat
⊢ ?m.2 n =?= fun _n _x _f => f x

but that is not well-scoped. Instead, it should have tried to replace the second n with a fresh binder m, so that it tries the pattern

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

Replacing the second n with m is effectively like permuting the type of ?m.2 to look like the type of ?m.1, which constant approximation assigns to the pattern

?m.1 n x f := fun _n => f x

Of course, for "replace the second n with a fresh binder m" we must also do the same to all its forward dependencies. This is still better than the status quo, where we assume that all binders after the second n are forward dependencies of the second n (and thus will be replaced with an FVar that doesn't occur in the term to assign).

[sgraf812]

Hmm. I think my idea above is similar to quasiPatternApprox, but for a clash between args instead of LCtx and arg. In fact, approximation A3) talks about this and concludes that it is not viable to maintain. I should try and look for another workaround in the do elaborator then.