Dependent if rewrite causes dependent goal to dissapear, giving kernel declaration has metavars

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

dependent if rewrite causes dependent goal to dissapear

Steps to Reproduce

variable {α : Type} [LT α] {c : α} [∀ m : α, Decidable (m=c)]

theorem c_lt {a : α} (hab : a = c) : c < a := sorry

def id_of_c_lt (m : α) : c < m → α := fun _ => m

theorem minimal_error (M m : α) (hm : c < m) (m_eq_M : m = M) (M_eq_c : M = c)
  (H : id_of_c_lt M (c_lt M_eq_c) = c) :
  (if h : m = c then id_of_c_lt m (c_lt h) else m) = c :=
by
  rw [dif_pos]
  . simp only [m_eq_M]
    rw [m_eq_M] at hm --useless rewrite of an assumption makes the hc case disappear
    exact H

example due to Sacha Huriot @kisarablue

Expected behavior: a second (probably unprovable goal remains

Actual behavior: (kernel) declaration has metavariables 'minimal_error'

Reproduces how often: 100%

Versions

latest nightly (1-12)

Start with the self-contained minimal_error theorem and reproduce the behavior around rw [m_eq_M] at hm. Investigate the dependent-if rewrite and kernel declaration handling; done means the reproduced case no longer leaves an undeclared metavariable, or the remaining goal is reported as expected.