Fix handling of opaque primitive projections in Evarconv

This fixes #17774.

doc/changelog/04-tactics/17788-opaque-primitive-evarconv.rst

@@ -0,0 +1,6 @@
+- **Fixed:**
+  ensure that opaque primitive projections are correctly handled by "Evarconv"
+  unification
+  (`#17788 <https://github.com/coq/coq/pull/17788>`_,
+  fixes `#17774 <https://github.com/coq/coq/issues/17774>`_,
+  by Rodolphe Lepigre).

pretyping/evarconv.ml

@@ -1147,6 +1147,36 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
           |Some (sk1',sk2'), Success i' -> evar_conv_x flags env i' CONV (Stack.zip i' (term1,sk1')) (Stack.zip i' (term2,sk2'))
           end
 
+        | Proj (p1,c1), Proj(p2,c2) when QProjection.Repr.equal env (Projection.repr p1) (Projection.repr p2) ->
+          begin match ise_stack2 true env evd (evar_conv_x flags) sk1 sk2 with
+          |_, (UnifFailure _ as x) -> x
+          |None, Success i' -> evar_conv_x flags env i' CONV c1 c2
+          |Some _, Success _ -> UnifFailure (evd,NotSameHead)
+          end
+
+        (* Catch the c.(p) ~= p c' cases *)
+        | Proj (p1,c1), Const (p2,_) when QConstant.equal env (Projection.constant p1) p2 ->
+          let c1 =
+            try Some (destApp evd (Retyping.expand_projection env evd p1 c1 []))
+            with Retyping.RetypeError _ -> None
+          in
+          begin match c1 with
+          | Some (c1,new_args) ->
+            rigids env evd (Stack.append_app new_args sk1) c1 sk2 term2
+          | None -> UnifFailure (evd,NotSameHead)
+          end
+
+        | Const (p1,_), Proj (p2,c2) when QConstant.equal env p1 (Projection.constant p2) ->
+          let c2 =
+            try Some (destApp evd (Retyping.expand_projection env evd p2 c2 []))
+            with Retyping.RetypeError _ -> None
+          in
+          begin match c2 with
+          | Some (c2,new_args) ->
+            rigids env evd sk1 term1 (Stack.append_app new_args sk2) c2
+          | None -> UnifFailure (evd,NotSameHead)
+          end
+
         | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Float _ | Array _ | Evar _ | Lambda _), _ ->
           UnifFailure (evd,NotSameHead)
         | _, (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Array _ | Evar _ | Lambda _) ->

test-suite/bugs/bug_17774.v

@@ -0,0 +1,48 @@
+Require Import Ltac2.Ltac2.
+
+#[projections(primitive)]
+Record r (n : nat) := { w : Prop -> Prop -> Prop }.
+
+Class C (P : Prop) := {}.
+
+Import Printf.
+Set Printing Primitive Projection Parameters.
+
+Goal forall (v : r 0) (Q P : Prop), C (v.(w _) P Q).
+Proof.
+  intros.
+
+  (* Succeeds before and after this PR. *)
+  Succeed lazy_match! goal with
+  | [ |- ?g ] =>
+      let t := open_constr:(C (v.(w _) _ _)) in
+      Unification.unify (TransparentState.current ()) g t
+  end.
+
+  #[local] Opaque w.
+
+  (* Succeeds only after #17788. *)
+  Succeed lazy_match! goal with
+  | [ |- ?g ] =>
+      let t := open_constr:(C (v.(w _) _ _)) in
+      Unification.unify (TransparentState.current ()) g t
+  end.
+
+  (* Succeeds only after #17788. *)
+  Succeed lazy_match! goal with
+  | [ |- ?g ] =>
+      let t := open_constr:(w _) in
+      let t := open_constr:(C ($t v _ _)) in
+      (*printf "Term: %t" t;*)
+      Unification.unify (TransparentState.current ()) g t
+  end.
+
+  (* Succeeds only after #17788. *)
+  Succeed lazy_match! goal with
+  | [ |- ?g ] =>
+      let t := open_constr:(w _) in
+      let t := open_constr:(C ($t v _ _)) in
+      (*printf "Term: %t" t;*)
+      Unification.unify (TransparentState.current ()) g t
+  end.
+Abort.