Merge PR #8824: Do not check convertibility of pattern types in the kernel

1 files changed, 50 insertions, 31 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 18697d07e5..5515ff9767 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -68,7 +68,7 @@ type lft_constr_stack_elt =
     Zlapp of (lift * fconstr) array
   | Zlproj of Projection.Repr.t * lift
   | Zlfix of (lift * fconstr) * lft_constr_stack
-  | Zlcase of case_info * lift * fconstr * fconstr array
+  | Zlcase of case_info * lift * constr * constr array * fconstr subs
 and lft_constr_stack = lft_constr_stack_elt list
 
 let rec zlapp v = function
@@ -102,7 +102,7 @@ let pure_stack lfts stk =
                 let (lfx,pa) = pure_rec l a in
                 (l, Zlfix((lfx,fx),pa)::pstk)
             | (ZcaseT(ci,p,br,e),(l,pstk)) ->
-                (l,Zlcase(ci,l,mk_clos e p,Array.map (mk_clos e) br)::pstk))
+                (l,Zlcase(ci,l,p,br,e)::pstk))
   in
   snd (pure_rec lfts stk)
 
@@ -288,31 +288,13 @@ let conv_table_key infos k1 k2 cuniv =
   | RelKey n, RelKey n' when Int.equal n n' -> cuniv
   | _ -> raise NotConvertible
 
-let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
-  let rec cmp_rec pstk1 pstk2 cuniv =
-    match (pstk1,pstk2) with
-      | (z1::s1, z2::s2) ->
-          let cu1 = cmp_rec s1 s2 cuniv in
-          (match (z1,z2) with
-            | (Zlapp a1,Zlapp a2) -> 
-	       Array.fold_right2 f a1 a2 cu1
-            | (Zlproj (c1,_l1),Zlproj (c2,_l2)) ->
-              if not (Projection.Repr.equal c1 c2) then
-		raise NotConvertible
-	      else cu1
-            | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
-                let cu2 = f fx1 fx2 cu1 in
-                cmp_rec a1 a2 cu2
-            | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) ->
-                if not (fmind ci1.ci_ind ci2.ci_ind) then
-		  raise NotConvertible;
-		let cu2 = f (l1,p1) (l2,p2) cu1 in
-                Array.fold_right2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2 cu2
-            | _ -> assert false)
-      | _ -> cuniv in
-  if compare_stack_shape stk1 stk2 then
-    cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv
-  else raise NotConvertible
+exception IrregularPatternShape
+
+let rec skip_pattern n c =
+  if Int.equal n 0 then c
+  else match kind c with
+  | Lambda (_, _, c) -> skip_pattern (pred n) c
+  | _ -> raise IrregularPatternShape
 
 type conv_tab = {
   cnv_inf : clos_infos;
@@ -611,10 +593,31 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         | FProd _ | FEvar _), _ -> raise NotConvertible
 
 and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
-  compare_stacks
-    (fun (l1,t1) (l2,t2) cuniv -> ccnv CONV l2r infos l1 l2 t1 t2 cuniv)
-    (eq_ind)
-    lft1 stk1 lft2 stk2 cuniv
+  let f (l1, t1) (l2, t2) cuniv = ccnv CONV l2r infos l1 l2 t1 t2 cuniv in
+  let rec cmp_rec pstk1 pstk2 cuniv =
+    match (pstk1,pstk2) with
+      | (z1::s1, z2::s2) ->
+          let cu1 = cmp_rec s1 s2 cuniv in
+          (match (z1,z2) with
+            | (Zlapp a1,Zlapp a2) ->
+               Array.fold_right2 f a1 a2 cu1
+            | (Zlproj (c1,_l1),Zlproj (c2,_l2)) ->
+              if not (Projection.Repr.equal c1 c2) then
+                raise NotConvertible
+              else cu1
+            | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
+                let cu2 = f fx1 fx2 cu1 in
+                cmp_rec a1 a2 cu2
+            | (Zlcase(ci1,l1,p1,br1,e1),Zlcase(ci2,l2,p2,br2,e2)) ->
+                if not (eq_ind ci1.ci_ind ci2.ci_ind) then
+                  raise NotConvertible;
+                let cu2 = f (l1, mk_clos e1 p1) (l2, mk_clos e2 p2) cu1 in
+                convert_branches l2r infos ci1 e1 e2 l1 l2 br1 br2 cu2
+            | _ -> assert false)
+      | _ -> cuniv in
+  if compare_stack_shape stk1 stk2 then
+    cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv
+  else raise NotConvertible
 
 and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
   let lv1 = Array.length v1 in
@@ -629,6 +632,22 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
     fold 0 cuniv
   else raise NotConvertible
 
+and convert_branches l2r infos ci e1 e2 lft1 lft2 br1 br2 cuniv =
+  (** Skip comparison of the pattern types. We know that the two terms are
+      living in a common type, thus this check is useless. *)
+  let fold n c1 c2 cuniv = match skip_pattern n c1, skip_pattern n c2 with
+  | (c1, c2) ->
+    let lft1 = el_liftn n lft1 in
+    let lft2 = el_liftn n lft2 in
+    let e1 = subs_liftn n e1 in
+    let e2 = subs_liftn n e2 in
+    ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cuniv
+  | exception IrregularPatternShape ->
+    (** Might happen due to a shape invariant that is not enforced *)
+    ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cuniv
+  in
+  Array.fold_right3 fold ci.ci_cstr_nargs br1 br2 cuniv
+
 let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
   let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
   let infos = create_clos_infos ~evars reds env in