From 8fdd835bc58640d9819cef13e30428d10abdca56 Mon Sep 17 00:00:00 2001
From: "coqbot-app[bot]" <50967743+coqbot-app[bot]@users.noreply.github.com>
Date: Fri, 8 Sep 2023 10:01:50 +0000
Subject: [PATCH] Merge PR #17788: Correctly handle opaque primitive
 projections in Evarconv

Reviewed-by: SkySkimmer
Ack-by: ppedrot
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
---
 .../17788-opaque-primitive-evarconv.rst       |  6 +++
 pretyping/evarconv.ml                         | 30 ++++++++++++
 test-suite/bugs/bug_17774.v                   | 48 +++++++++++++++++++
 3 files changed, 84 insertions(+)
 create mode 100644 doc/changelog/04-tactics/17788-opaque-primitive-evarconv.rst
 create mode 100644 test-suite/bugs/bug_17774.v

diff --git a/doc/changelog/04-tactics/17788-opaque-primitive-evarconv.rst b/doc/changelog/04-tactics/17788-opaque-primitive-evarconv.rst
new file mode 100644
index 0000000000000..671ff766db03f
--- /dev/null
+++ b/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).
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 28df44238add3..974354c499080 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1148,6 +1148,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 _) ->
diff --git a/test-suite/bugs/bug_17774.v b/test-suite/bugs/bug_17774.v
new file mode 100644
index 0000000000000..fb5a4c495f448
--- /dev/null
+++ b/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 #17788. *)
+  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.