congr hogging up holes

Stream: mathlib4

[Eric Rodriguez]

import Mathlib.Tactic.Convert

example (h : False) : False := by
  have : 1 + 1 = 3 := by
    convert rfl
    contradiction
  rw [iff_self ?h]
  /- synthetic hole has already been defined and assigned to value incompatible with the current context
  h_congr_thm✝ Nat (1 + 1) (1 + 1) (Eq.refl (1 + 1)) 3 (1 + 1) (absurd h (of_decide_eq_false (Eq.refl (decide False)))) -/

h_congr_thm seems to be from congr!, but I can't seem to get a simple mwe with congr!.

[Kyle Miller]

Here's with congr!:

example (h : False) : False := by
  have : (1 + 1 = 3) = (?a = ?a) := by
    congr!
    contradiction
  rw [iff_self ?h]

[Kyle Miller]

There's nothing in congr! that's directly using the name h, but maybe somehow there's an h in a parameter name to the congruence theorem that is being applied, and so this apply is responsible for it indirectly?