Fix handling of opaque primitive projections in Evarconv

This fixes #17774.
coq · Jul 3, 2023 · 906121a · 906121a
1 parent c0e7d0c
commit 906121a
Show file tree

Hide file tree

Showing 2 changed files with 36 additions and 0 deletions.
diff --git a/doc/changelog/04-tactics/17788-opaque-primitive-evarconv.rst 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
@@ -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 p.c ~= 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 _) ->