Merge PR #13182: Check types when converting irrelevant terms in old unification

Reviewed-by: gares

2 files changed, 39 insertions, 1 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 4d37c0ef60..982814fdfc 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -687,6 +687,17 @@ let eta_constructor_app env sigma f l1 term =
       | _ -> assert false)
   | _ -> assert false
 
+(* If the terms are irrelevant, check that they have the same type. *)
+let careful_infer_conv ~pb ~ts env sigma m n =
+  if Retyping.relevance_of_term env sigma m == Sorts.Irrelevant &&
+     Retyping.relevance_of_term env sigma n == Sorts.Irrelevant
+  then
+    let tm = Retyping.get_type_of env sigma m in
+    let tn = Retyping.get_type_of env sigma n in
+    Option.bind (infer_conv ~pb:CONV ~ts env sigma tm tn)
+      (fun sigma -> infer_conv ~pb ~ts env sigma m n)
+  else infer_conv ~pb ~ts env sigma m n
+
 let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top env cv_pb flags m n =
   let rec unirec_rec (curenv,nb as curenvnb) pb opt ((sigma,metasubst,evarsubst) as substn : subst0) curm curn =
     let cM = Evarutil.whd_head_evar sigma curm
@@ -1127,7 +1138,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
       None
     else
       let ans = match flags.modulo_conv_on_closed_terms with
-        | Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n
+        | Some convflags -> careful_infer_conv ~pb:cv_pb ~ts:convflags env sigma m n
         | _ -> constr_cmp cv_pb env sigma flags m n in
       match ans with
       | Some sigma -> ans
diff --git a/test-suite/success/sprop_uip.v b/test-suite/success/sprop_uip.v
index eae1b75689..c9377727db 100644
--- a/test-suite/success/sprop_uip.v
+++ b/test-suite/success/sprop_uip.v
@@ -121,6 +121,33 @@ Proof.
   simpl. Fail check.
 Abort.
 
+Module HoTTStyle.
+  (* a small proof which tests destruct in a tricky case *)
+
+  Definition ap {A B} (f:A -> B) {x y} (e : seq x y) : seq (f x) (f y).
+  Proof. destruct e. reflexivity. Defined.
+
+  Section S.
+    Context
+      (A : Type)
+      (B : Type)
+      (f : A -> B)
+      (g : B -> A)
+      (section : forall a, seq (g (f a)) a)
+      (retraction : forall b, seq (f (g b)) b).
+
+    Lemma bla (P : B -> Type) (a : A) (F : forall a, P (f a))
+      : seq_rect _ (f (g (f a))) (fun a _ => P a) (F (g (f a))) (f a) (retraction (f a)) = F a.
+    Proof.
+      lazy.
+      change (retraction (f a)) with (ap f (section a)).
+      destruct (section a).
+      reflexivity.
+    Qed.
+  End S.
+
+End HoTTStyle.
+
 (* check that extraction doesn't fall apart on matches with special reduction *)
 Require Extraction.