Conv changing goals to metavariables with `pattern`.

[ericrbg]

Prerequisites

• [X] Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

example : ∀ p : Prop, p ↔ p := by
  conv => ext p; pattern p ↔ p; rw [iff_self]

/-
(kernel) declaration has metavariables '_example'

unsolved goals
⊢ ∀ (p : Prop), ?m.13 p -/

Context

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/conv.20giving.20metavariables is the Zulip thread about it.

Expected behavior: The unsolved goal should be ∀ (p : Prop), True.

Actual behavior: The unsolved goal is ⊢ ∀ (p : Prop), ?m.13 p, which is a weird metavariable.

Versions

Lean (version 4.3.0-rc1, commit baa4b68a7192, Release), OSX Sonoma 14.0

Impact

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