`synthPending` doesn't respect metavariable context depth

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

The function Lean.Meta.synthPending tries to assign a metavariable by synthesizing a type class instance. However before assigning the metavariable it doesn't check if the metavariable is allowed to be assigned w.r.t. the metavariable context depth. Since unification calls synthPending, this breaks the invariant that low depth metavariables are not assigned by isDefEq. This can lead to unexpected outcomes in isDefEq and type class search.

Context

I ran into this bug while working on #lean4 > One line change gives type class search speedup of 17%.

Steps to Reproduce

Run the following:

import Lean
open Lean
run_meta do
  let e := mkApp (.const ``Add [0]) (.const ``Nat [])
  let goal ← Meta.mkFreshExprMVar e
  Meta.withNewMCtxDepth do
    logInfo m! "{← Meta.synthPending goal.mvarId!}"

Expected behavior:

synthPending returns false and doesn't assign the metavariable

Actual behavior:

synthPending returns true and assigns the metavariable

Versions

Lean 4.23.0-nightly-2025-08-04

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

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

Start with the Lean.Meta.synthPending implementation and the supplied run_meta reproduction, then inspect how metavariable context depth is checked during unification. Confirm the current behavior and make the reproduction return false without assigning the metavariable; done means the depth invariant remains intact in this case.