`exact?` doesn't close the goal

[shuxuezhuyi]

From https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/exact.3F.20doesn't.20close.20the.20goal

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]

[kbuzzard]

Right now on master, what's happening is that exact? reports

exact ((fun {α} [LinearOrderedAddCommGroup α] {a b} hb ↦ (abs_eq hb).mpr) h1 (Or.inl rfl)).symm

(which doesn't work), and what works is if you remove all the non-explicit inputs from the function, i.e.

  exact ((fun hb ↦ (abs_eq hb).mpr) h1 (Or.inl rfl)).symm

[kim-em]

Just noting that exact? is moving to the lean4 repository; I can't transfer issues across organisations, however.

[kim-em]

@kmill, is this something I can pin on the delaborator?

[kmill]

Yes, mostly. The problem is that the delaborator isn't showing that the implicit fun arguments are being passed to abs_eq_self. If you set pp.analyze to true, it seems to get it to pretty print enough to elaborate.

Though, you do have any idea where this weird fun is coming from from exact?? Could exact? do some beta reduction of the term if that fun can't be avoided? (Is it because SolveByElim uses intro? or maybe it's the implicit lambda feature?)

[kbuzzard]

Adding another example which a student found earlier this week:

import Mathlib.Tactic

-- works fine
example (x : ℝ) (hx : x ≠ 0) : |x| > 0 := by exact? -- Try this: exact abs_pos.mpr hx

-- suggestion doesn't work and is clearly strange
example (x : ℝ) : x ≠ 0 → |x| > 0 := by exact?
/-
Try this: exact fun a ↦
  (fun {α} [AddGroup α] [LinearOrder α]
        [CovariantClass α α (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1] {a} ↦
      abs_pos.mpr)
    a
-/

[kim-em]

If someone can make a no-imports reproduction, I will look into having exact? attempt some beta reduction to avoid this.