exact? doesn't close the goal

Stream: general

[Wen Yang]

I find that the suggestion from exact? doesn't always close the goal. For example:

import Mathlib.Analysis.NormedSpace.Basic
variable (a : ℝ) (h1 : 0 ≤ a)
example : a = dist a 0 := by
  rw [dist_eq_norm]
  simp
  exact?
  -- Try this: exact Eq.symm ((fun {α} [LinearOrderedRing α] {a} => abs_eq_self.mpr) h1)

It doesn't close the goal, since

typeclass instance problem is stuck, it is often due to metavariables
  LinearOrderedRing ?m.551

What actually close the goal is:

rw_mod_cast [abs_eq_self.mpr h1]

Is that a normal behavior?

[Scott Morrison]

Could you open an issue on the mathlib4 repository for this one? It's not clear to me if this is a problem in exact?, a problem in the pretty printer, or something else.

[Wen Yang]

I have opened an issue at https://github.com/leanprover-community/mathlib4/issues/6937