Incorrect transparency used to expose differences

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

In pretty much all uses of addPPExplicitToExposeDiff, the isDefEq calls nested in addPPExplicitToExposeDiff run under the wrong transparency, namely, always on default transparency. This causes some unfortunate error messages where two different expressions (under e.g. reducible transparency) are shown with the exact same pretty-printing even after addPPExplicitToExposeDiff.

Context

Report by someone on discord.

Steps to Reproduce

class MyClass (α : Type) where
  data : Nat

-- make a diamond
instance inst1 : MyClass Nat where data := 3
instance inst2 : MyClass Nat where data := id 3

/--
error: Tactic `rfl` failed: The left-hand side
  @id Nat (MyClass.data Nat)
is not definitionally equal to the right-hand side
  @id Nat (MyClass.data Nat)

⊢ id (MyClass.data Nat) = id (MyClass.data Nat)
-/
#guard_msgs in
example : id inst1.data = id inst2.data := by
  with_reducible rfl

Expected behavior:
Under reducible transparency, the two MyClass.data calls are not defeq, namely, the instance arguments are not equivalent under with_reducible_and_instances. Thus, this difference should be exposed by writing:

The left-hand side
  @id Nat (@MyClass.data Nat inst1)
is not definitionally equal to the right-hand side
  @id Nat (@MyClass.data Nat inst2)

Actual behavior:
The defeq check failed but the pretty-printed versions are exactly the same.

Versions

Lean 4.33.0, commit 75591856794182559e5a3713bdf8aa00c52fc7ca

Impact

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

Start with the addPPExplicitToExposeDiff entry point and inspect its nested isDefEq calls, using the minimal Lean reproduction and its with_reducible context as the test case. Done means the #guard_msgs output exposes the distinct inst1 and inst2 instance arguments instead of printing identical expressions.