congruence fails if universes differ, results in weird f_equal behavior

[samuelgruetter]

Set Universe Polymorphism.

Record Map(K V: Type) := {
  rep: Type;
  put: rep -> K -> V -> rep;
}.

Section Test.
  Universes u1 u2 u3 u4 u5 u6.

  Goal forall K V (M: Map K V) (k: K) (v: V) (m: rep K V M),
      put@{u1 u2 u3} K V M m k v = put@{u4 u5 u6} K V M m k v.
  Proof.
    intros.
    Fail congruence.
    reflexivity.

Desired behavior: congruence should succeed and solve the goal.

Moreover, since f_equal calls congruence, the following

  Goal forall K V (M: Map K V) (k: K) (v1 v2: V) (m: rep K V M),
      put@{u1 u2 u3} K V M m k v1 = put@{u4 u5 u6} K V M m k v2.
  Proof.
    intros.
    f_equal.

results in

2 subgoals (ID 28)
  
  K : Type
  V : Type
  M : Map K V
  k : K
  v1, v2 : V
  m : rep K V M
  ============================
  K = K -> V = V -> M = M -> m = m -> k = k -> v1 = v2 -> put K V M m k v1 = put K V M m k v2

subgoal 2 (ID 19) is:
 v1 = v2

instead of just the second subgoal.

Coq version: Both master (424c197, Apr 1), and 8.9 are affected.

Might be the same as #5481.

Thx @JasonGross for helping me isolate the problem.
/cc @andres-erbsen

[ejgallego]

You can try ssreflect congr put which will work for this case; dunno if an improvement in general.

[samuelgruetter]

If I do Require Import ssreflect., then congr put and congr _ indeed works. Why does ssreflect's congr need an extra argument?

[samuelgruetter]

The documentation of congr says that it "may expand some definitions or fixpoints". This sounds dangerous from a performance point of view and I would not like to depend on this, but rather use a congruence which does not do any unfolding.

[ppedrot]

AFAICT this really looks like a duplicate of #5481.

[ppedrot]

Duplicate of #5481