Goal pretty-printing doesn't respect `pp.instantiateMVars`

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

When pretty-printing goals, metavariables are always instantiated in hypotheses and the goal type regardless of the setting of pp.instantiateMVars. This is bad when debugging problems with metavariables because important information might be invisible.

Context

#mathlib4 > tauto bug @ 💬

Steps to Reproduce

import Lean

open Lean Elab Tactic
elab "show_goal_type" : tactic => do
  let goal ← getMainGoal
  goal.withContext do
    logInfo m!"real goal type: {(← goal.getType)}"
    logInfo m!"ppGoal:\n{goal}"

set_option pp.instantiateMVars false

/--
info: real goal type: ?α
---
info: ppGoal:
⊢ True
-/
#guard_msgs (info) in
example : True := by
  apply id
  show_goal_type
  sorry

Expected behavior:
The setting pp.instantiateMVars is respected, showing the real type of ?α.

Actual behavior:
The fact that the goal type is a metavariable is not visible from the goal view.

Versions

Lean 4.33.0-nightly-2026-07-03

Impact

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

Start with the self-contained Lean reproducer, especially the show_goal_type tactic and goal.withContext/ppGoal output; trace the goal pretty-printing path that handles hypotheses and goal types. Done when pp.instantiateMVars false keeps the metavariable visible in the goal view and the reproducer's expected messages pass.