From 64b56ee86fa8e32afd7802a9c5567ee9f15dd386 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 12 Oct 2020 16:21:06 +0200
Subject: Check types when converting irrelevant terms in old unification

Fixes probably many strange issues such as the example in #13171
---
 pretyping/unification.ml | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 207a03d80f..32dd805b30 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
-- 
cgit v1.2.3