Invalid type class cache after a change in `MetavarContext`

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 is possible for the type class synthesis cache to become invalid when the MetavarContext changes. This is usually no problem because the function instantiateMVars is run on the goal, so if the MetavarContext changes, then the goal also changes. However, if the metavariable is hidden inside a let variable, this becomes a problem.

Context

I was trying to better understand type class synthesis cache, and came up with this example.

Steps to Reproduce

Create a metavariable ?m, and define a let variable a := ?m. First let ?m := Nat, and synthesize Inhabited a, and then let ?m := Int and synthesize Inhabited a again. Lean then finds the instInhabitedNat instance in the cache, and so it fails to find Int.instInhabited. Here's the code:

import Lean

open Lean Meta

run_meta do
  let m ← mkFreshExprMVar (Expr.sort levelOne)
  withLetDecl `a (Expr.sort levelOne) m fun a => do
    withMCtx (← getMCtx) do
      logInfo m! "{← isDefEq m (.const ``Nat [])}; {← trySynthInstance (.app (.const ``Inhabited [levelOne]) a)}"
    withMCtx (← getMCtx) do
      logInfo m! "{← isDefEq m (.const ``Int [])}; {← trySynthInstance (.app (.const ``Inhabited [levelOne]) a)}"

Expected behavior: [Clear and concise description of what you expect to happen]

The logInfo should give

true; (some instInhabitedNat)
true; (some Int.instInhabited)

Actual behavior: [Clear and concise description of what actually happens]

The logInfo gives

true; (some instInhabitedNat)
true; none

Versions

4.9.0-rc1

Additional Information

Impact

I doubt this ever comes up in practice, so there is not much 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 run_meta example using withMCtx, isDefEq, and trySynthInstance to reproduce the stale cache result. Read the MetavarContext and type class synthesis cache paths, including where instantiateMVars is applied. Done means the second synthesis returns Int.instInhabited after the metavariable changes from Nat to Int.