Evarconv fails to unify primitive projection with compatibility constant in closed terms

[Janno]

Description of the problem

#17788 fixed this for terms with evars but we didn't realize that we would have a different problem with closed terms since they are handed over to conversion immediately.

Require Import Ltac2.Ltac2.

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

Class C (P : Prop) := {}.

Goal forall (v : r 0) (Q P : Prop), C (v.(w _) P Q).
Proof.
  intros.

  #[local] Opaque w.

  Fail lazy_match! goal with
  | [ |- ?g ] =>
      let t := constr:(w 0) in
      let t := constr:(C ($t v P Q)) in
      Unification.unify (TransparentState.current ()) g t
  end.

What ends up failing ultimately is unfold_ref_with_args on w because w is marked opaque.

Coq Version

master

/cc @rlepigre

[herbelin]

Diverging a little more, what should we expect when typing About w? That it talks about the constant w, that it talks about the primitive field w, that it mentions both?

Or, conversely, should the constant w be considered as a special name canonically attached to the projection (e.g. as if it were just an eagerly-beta-reducing abbreviation for fun n (x : r n) => x.(w _)) or as an independent constant leaving its own life?

Incidentally, the reference manual seems to forget to mention that Opaque also applies to primitive projections. Maybe is it because it applies to primitive projections only "by accident", that is only indirectly via the existence of an associated constant? If it is intensional that it applies, I can make a quick fix to the manual. Then, in the longer term, for clarity, we should better have an explicit entry for projection names in the transparency state, no?