Where a simple `exact` works, but `exact?` does not

Stream: general

[Jeremy Kahn]

Here is a case where exact works, but exact? does not:

import Mathlib

example (r: ℕ) (α : Type) (a b: α) (ha: a ∈ List.replicate r b): a = b:= by
  exact List.eq_of_mem_replicate ha

example (r: ℕ) (α : Type) (a b: α) (ha: a ∈ List.replicate r b): a = b:= by
  exact?
  /-`exact?` could not close the goal. Try `apply?` to see partial suggestions.
  -/

Is there a simple explanation for this?

[Alex J. Best]

I think for efficiency reasons (i.e. too many possible matches that would dominate the cache) exact? skips all theorems whose conclusion is just a = b. This seems to come up periodically and the conclusion is often "someone should evaluate the impact of not doing this as it might not be relevant anymore" but as far as I know nobody did so (yet!)

[Kim Morrison]

See in particular https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/Tactic/LibrarySearch.lean#L100. It may be possible to drop * = * there, leaving just *

[Jeremy Kahn]

Learn something new every day! I actually found this example by accident, when trying to generate a minimal demonstration of exact? timing out for no reason. This was happening in another, much larger file, but that problem was fixed by restarting the file.