mk_hcongr_lemma produces subsingleton equality obligations

[digama0]

Prerequisites

• [X] 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.
    • Specifically, check out the wishlist, open RFCs, or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

This issue was originally noticed in the congr tactic, but it reduces to an implementation detail in the builtin mk_hcongr_lemma.

structure foo :=
  (P : Prop)
  (p : P)

structure bar :=
  (A : Type)
  (P : A → Prop)
  (a : A)
  (p : P a)

run_cmd do
  c ← tactic.mk_const `foo.mk,
  ⟨t, p, k⟩ ← tactic.mk_hcongr_lemma c,
  tactic.trace t  -- ∀ (P P' : Prop), P = P' → ∀ (p : P) (p' : P'), p == p' → {P := P, p := p} == {P := P', p := p'}

Notice that a heterogeneous equality has been generated for the p argument. In this case, one can use mk_congr_lemma instead, which produces the correct

 ∀ (P P_1 : Prop), P = P_1 → ∀ (p : P) (p_1 : P_1), {P := P, p := p} = {P := P_1, p := p_1}

but in more complicated cases, such as structure bar, mk_congr_lemma fails (because heterogeneous equalities are required), and mk_hcongr_lemma is the fallback. AFAICT mk_hcongr_lemma does only the obvious thing of producing an equality for each parameter, heterogeneous after the first, regardless of its congr_arg_kind status.