Evarconv does not handle opaque primitive projections correctly

[Janno]

Description of the problem

Evarconv considers opaque primitive projections not unifiable with themselves. The code below reproduces the problem in a roundabout way. (There is only one code path in Coq that calls Evarconv with transparency states that are not TransparentState.full!)

#[projections(primitive)]
Record r := { w : Prop -> Prop -> Prop }.

Set Typeclasses Filtered Unification. (* Only used to trigger evarconv code path *)
Class C (P : Prop) := {}.
Definition wand_apply (v : r) (P Q : Prop) : C (w v P Q) := Build_C _.
#[local] Hint Resolve wand_apply : typeclass_instances.

Goal forall (v : r) (Q P : Prop), C (w v P Q).
Proof.
  intros.
  Succeed typeclasses eauto.
  #[local] Hint Opaque w : typeclass_instances.
  Set Debug "unification,ho-unification".
  Fail typeclasses eauto.
Abort.

The example does not work on master because Typeclasses Filtered Unification has been removed. Our (closed source) OCaml plugin that first exhibited this problem only compiles with 8.17 right now so we do not know if the problem exists on master.

Coq Version

8.17

[rlepigre]

This can also be reproduced on master now, thanks to #17777 (see the new test case in #17788).