bug: dsimp does not close reflexive equality goals if they are wrapped in metadata

[kmill]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

dsimp has a feature where it can close goals that can be solved by Eq.refl if the goal is obviously an equality and the LHS and RHS are defeq (up to reducible transparency). For example

example : ∀ (x : α × α), x = id x := by
  intro p
  -- `⊢ (x, y) = id (x, y)`
  dsimp
  -- closed goal

However, sometimes tactics can insert metadata around this equality and then dsimp no longer tries to use Eq.refl.

example : ∀ (x : α × α), x = id x := by
  intro (x, y)
  -- `⊢ (x, y) = id (x, y)`
  dsimp
  -- not done yet, goal `⊢ (x, y) = (x, y)`
  rfl

One can see the metadata (noImplicitLambda) by setting set_option pp.raw true.

(This was reported by Heather Macbeth on Zulip)

Here is another test that demonstrates the issue. Removing the have line removes the need for the rfl. The have line can also be replaced by refine no_implicit_lambda% ?_ to more explicitly introduce metadata.

example {α : Type _} (n : α) : n = n := by
  have := 0
  dsimp
  rfl

In Lean.Meta.dsimpGoal one can see that there is targetNew.eq? instead of targetNew.consumeMData.eq?, which is likely the cause. Other pattern matches in that function refer to targetNew.consumeMData rather than targetNew.

Versions

leanprover/lean4:v4.0.0-rc4