`synthInstance` cache pollution under different configuration settings

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

After synthInstance has failed once under one configuration (Lean.Meta.Config) it will always fail under another configuration even if the call with the different configuration would succeed.
The comment above SynthInstanceCacheKey indicates that the typeclass resolution would use a fixed configuration; however this is not the case, synthInstanceCore? keeps all configuration settings except isDefEqStuckEx, transparency, foApprox, ctxApprox, constApprox and univApprox; this is a potential oversight.

Context

Attempted refactor of NegZeroClass.

Steps to Reproduce

class Test (α : Type) where
  data : Nat

class SuperTest (α : Type) extends Test α where
  data_is_42 : Test.data α = 42

structure A where
  data : Nat

instance : Test A := ⟨42⟩

instance : SuperTest A where
  data_is_42 := rfl

example : True := by
  let x := A
  suffices Test.data x = 42 from trivial
  rw [SuperTest.data_is_42] -- works

example : True := by
  let x := A
  suffices Test.data x = 42 from trivial
  try fail_if_success simp only [SuperTest.data_is_42] -- cache entry ❌️ `SuperTest A` for `zetaDelta := false`
  rw [SuperTest.data_is_42] -- but now we have `zetaDelta := true`, still: fail!

Expected behavior:
Adding a tactic that does nothing to the goal shouldn't change the behavior of any tactics that come after.
Note: Ideally the synthInstance call would not be affected by the surrounding zetaDelta := false and the simp would succeed (since it does succeed in the case of a mixin class SuperTest (α : Type) [Test α]). To reflect this, the test includes a fail_if_success that makes sure that the rw still has a goal even if the simp succeeded.

Actual behavior:
The first version succeeds but adding a tactic that does nothing to the goal makes it fail.

Versions

Lean 4.34.0, commit 49ff95727f98d43984726b26742d17a1ceea9dd5

Impact

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

Start by reproducing the minimal Lean example, then read the SynthInstanceCacheKey comment and the synthInstanceCore? entry point. Trace which Lean.Meta.Config settings affect instance synthesis and its cache key. Done means a regression test confirms that a failed lookup under one configuration does not prevent a later lookup under another configuration from succeeding.