ccnv: skip conversions implied by terms having the same type

When converting [fun x : A => e] and [fun x : A' => e'] if I know they
have the same type [forall x : A, B] I know that [A == A'] (Pi-injectivity).

When converting constructors we can skip parameters.

For perf reasons we switch the order of comparing arguments so that
it's left to right, otherwise the optimisation is skipping an
opportunity to fail early leading to eg +100% compile time for
mathcomp-odd-order (1.4ks to 2.8ks).

The main entry point [clos_gen_conv] does not assume there is a common
type. Indeed some callers do not preserve that property, leading to
errors. I encountered the following before I stopped assuming:
- [nsatz] in 2145.v and in the test suite Nsatz.v
- some [apply] call in HoTT (in field_of_fractions.v)

When converting types (which have a common type), since optimisations
are on lambdas and constructors they're not blocked. This accounts for
all kernel calls except module subtyping (rare).

In the future we may want to expose a way to pass [idtypes:true] so
that subtyping and the well-behaved parts of unification could take
advantage.

Author: SkySkimmer

clib/cArray.ml

@@ -37,6 +37,8 @@ sig
   val fold_left_i : (int -> 'a -> 'b -> 'a) -> 'a -> 'b array -> 'a
   val fold_right2 :
     ('a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c
+  val fold_right2_i :
+    (int -> 'a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c
   val fold_left2 :
     ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
   val fold_left3 :
@@ -243,6 +245,16 @@ let fold_right2 f v1 v2 a =
   if Array.length v2 <> lv1 then invalid_arg "Array.fold_right2";
   fold a lv1
 
+let fold_right2_i f v1 v2 a =
+  let lv1 = Array.length v1 in
+  let rec fold a n =
+    if n=0 then a
+    else
+      let k = n-1 in
+      fold (f k (uget v1 k) (uget v2 k) a) k in
+  if Array.length v2 <> lv1 then invalid_arg "Array.fold_right2";
+  fold a lv1
+
 let fold_left2 f a v1 v2 =
   let lv1 = Array.length v1 in
   let rec fold a n =

clib/cArray.mli

@@ -62,6 +62,8 @@ sig
   val fold_left_i : (int -> 'a -> 'b -> 'a) -> 'a -> 'b array -> 'a
   val fold_right2 :
     ('a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c
+  val fold_right2_i :
+    (int -> 'a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c
   val fold_left2 :
     ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
   val fold_left3 :

kernel/reduction.ml

@@ -288,30 +288,43 @@ 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 =
+let zlapp_skip skip = function
+  | Zlapp a ->
+    let la = Array.length a in
+    if la >= skip then 0 else skip - la
+  | _ -> (* assert (skip == 0); *) 0
+
+let compare_stacks ~skip f fmind lft1 stk1 lft2 stk2 cuniv =
+  let rec cmp_rec skip 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 (Constant.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
+          let cuniv = compare_stack_el skip z1 z2 cuniv in
+          cmp_rec (zlapp_skip skip z1) s1 s2 cuniv
+      | _ -> cuniv
+  and compare_stack_el skip z1 z2 cuniv =
+    match (z1,z2) with
+    | (Zlapp a1,Zlapp a2) ->
+      if skip == 0
+      then Array.fold_left2 (fun cuniv a1 a2 -> f a1 a2 cuniv) cuniv a1 a2
+      else Array.fold_left2_i (fun i cuniv a1 a2 ->
+          if i < skip then cuniv else f a1 a2 cuniv)
+          cuniv a1 a2
+    | (Zlproj (c1,l1),Zlproj (c2,l2)) ->
+      if not (Constant.equal c1 c2) then
+        raise NotConvertible
+      else cuniv
+    | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
+      let cuniv = f fx1 fx2 cuniv in
+      cmp_rec 0 a1 a2 cuniv
+    | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) ->
+      if not (fmind ci1.ci_ind ci2.ci_ind) then
+        raise NotConvertible;
+      let cuniv = f (l1,p1) (l2,p2) cuniv in
+      Array.fold_right2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2 cuniv
+    | _ -> assert false
+  in
   if compare_stack_shape stk1 stk2 then
-    cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv
+    cmp_rec skip (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv
   else raise NotConvertible
 
 type conv_tab = {
@@ -325,12 +338,27 @@ type conv_tab = {
 (** The same heap separation invariant must hold for the fconstr arguments
     passed to each respective side of the conversion function below. *)
 
+(** About the [idtyps] argument:
+
+    We should only be converting well-typed terms with a common type,
+   but some callers (outside the kernel) do not respect this
+   invariant.
+
+    We assume that terms are well-typed (leading to "Conversion test
+   raised an anomaly"). This means that when converting applications
+   if the heads convert the arguments have a common type. Then we can
+   use that information for optimisation, skipping some conversions.
+
+    eg if I have [P : (forall x : A, B) -> foo] and my conversion
+   problem is [P (fun x : A0 => e) == P (fun x : A1 => e')] when I
+   convert the lambdas I may assume [A0 == A == A1]. *)
+
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
-let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
-  eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
+let rec ccnv ~idtyps cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
+  eqappr ~idtyps cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
 
 (* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *)
-and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
+and eqappr ~idtyps cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
   Control.check_for_interrupt ();
   (* First head reduce both terms *)
   let ninfos = infos_with_reds infos.cnv_inf betaiotazeta in
@@ -394,52 +422,52 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
                | Some def1 -> ((lft1, (def1, v1)), appr2)
 	       | None -> raise NotConvertible) 
 	 in
-           eqappr cv_pb l2r infos app1 app2 cuniv)
+           eqappr ~idtyps cv_pb l2r infos app1 app2 cuniv)
 
     | (FProj (p1,c1), FProj (p2, c2)) ->
       (* Projections: prefer unfolding to first-order unification,
 	 which will happen naturally if the terms c1, c2 are not in constructor
 	 form *)
       (match unfold_projection infos.cnv_inf p1 with
       | Some s1 ->
-        eqappr cv_pb l2r infos (lft1, (c1, (s1 :: v1))) appr2 cuniv
+        eqappr ~idtyps cv_pb l2r infos (lft1, (c1, (s1 :: v1))) appr2 cuniv
       | None ->
         match unfold_projection infos.cnv_inf p2 with
         | Some s2 ->
-          eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv
+          eqappr ~idtyps cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv
 	| None -> 
           if Constant.equal (Projection.constant p1) (Projection.constant p2)
 	     && compare_stack_shape v1 v2 then
             let el1 = el_stack lft1 v1 in
             let el2 = el_stack lft2 v2 in
-            let u1 = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in
+            let u1 = ccnv ~idtyps:false CONV l2r infos el1 el2 c1 c2 cuniv in
               convert_stacks l2r infos lft1 lft2 v1 v2 u1
 	  else (* Two projections in WHNF: unfold *)
 	    raise NotConvertible)
 
     | (FProj (p1,c1), t2) ->
       (match unfold_projection infos.cnv_inf p1 with
       | Some s1 ->
-         eqappr cv_pb l2r infos (lft1, (c1, (s1 :: v1))) appr2 cuniv
+         eqappr ~idtyps cv_pb l2r infos (lft1, (c1, (s1 :: v1))) appr2 cuniv
       | None -> 
 	 (match t2 with 
 	  | FFlex fl2 ->
             (match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with
               | Some def2 ->
-                 eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv
+                 eqappr ~idtyps cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv
               | None -> raise NotConvertible)
 	  | _ -> raise NotConvertible))
 
     | (t1, FProj (p2,c2)) ->
       (match unfold_projection infos.cnv_inf p2 with
       | Some s2 ->
-         eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv
+         eqappr ~idtyps cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv
       | None -> 
 	 (match t1 with 
 	  | FFlex fl1 ->
             (match unfold_reference infos.cnv_inf infos.lft_tab fl1 with
               | Some def1 ->
-                 eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv
+                 eqappr ~idtyps cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv
               | None -> raise NotConvertible)
 	  | _ -> raise NotConvertible))
 
@@ -453,17 +481,19 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         let (_,ty2,bd2) = destFLambda mk_clos hd2 in
         let el1 = el_stack lft1 v1 in
         let el2 = el_stack lft2 v2 in
-        let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in
-        ccnv CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv
+        let cuniv = if idtyps then cuniv (* Pi injectivity *)
+          else ccnv ~idtyps:true CONV l2r infos el1 el2 ty1 ty2 cuniv
+        in
+        ccnv ~idtyps CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv
 
     | (FProd (_,c1,c2), FProd (_,c'1,c'2)) ->
         if not (is_empty_stack v1 && is_empty_stack v2) then
 	  anomaly (Pp.str "conversion was given ill-typed terms (FProd).");
 	(* Luo's system *)
         let el1 = el_stack lft1 v1 in
         let el2 = el_stack lft2 v2 in
-        let cuniv = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in
-        ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv
+        let cuniv = ccnv ~idtyps:true CONV l2r infos el1 el2 c1 c'1 cuniv in
+        ccnv ~idtyps:true cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv
 
     (* Eta-expansion on the fly *)
     | (FLambda _, _) ->
@@ -473,7 +503,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           anomaly (Pp.str "conversion was given unreduced term (FLambda).")
         in
         let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
-        eqappr CONV l2r infos
+        eqappr ~idtyps CONV l2r infos
 	  (el_lift lft1, (bd1, [])) (el_lift lft2, (hd2, eta_expand_stack v2)) cuniv
     | (_, FLambda _) ->
         let () = match v2 with
@@ -482,7 +512,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	  anomaly (Pp.str "conversion was given unreduced term (FLambda).")
 	in
         let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
-        eqappr CONV l2r infos
+        eqappr ~idtyps CONV l2r infos
 	  (el_lift lft1, (hd1, eta_expand_stack v1)) (el_lift lft2, (bd2, [])) cuniv
 
     (* only one constant, defined var or defined rel *)
@@ -495,7 +525,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
               unfoldings, we perform reduction with all flags on. *)
             let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos.cnv_inf)) in
             let r1 = whd_stack (infos_with_reds infos.cnv_inf all) infos.lft_tab def1 v1 in
-            eqappr cv_pb l2r infos (lft1, r1) appr2 cuniv
+            eqappr ~idtyps cv_pb l2r infos (lft1, r1) appr2 cuniv
 	| None -> 
 	   match c2 with
 	   | FConstruct ((ind2,j2),u2) ->
@@ -512,7 +542,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           (** Symmetrical case of above. *)
           let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos.cnv_inf)) in
           let r2 = whd_stack (infos_with_reds infos.cnv_inf all) infos.rgt_tab def2 v2 in
-          eqappr cv_pb l2r infos appr1 (lft2, r2) cuniv
+          eqappr ~idtyps cv_pb l2r infos appr1 (lft2, r2) cuniv
         | None -> 
 	   match c1 with
 	   | FConstruct ((ind1,j1),u1) ->
@@ -540,17 +570,17 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 
     | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
       if Int.equal j1 j2 && eq_ind ind1 ind2 then
-        if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
-          let cuniv = convert_instances ~flex:false u1 u2 cuniv in
-          convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+        let mind = Environ.lookup_mind (fst ind1) (info_env infos.cnv_inf) in
+        let nargs = CClosure.stack_args_size v1 in
+        if not (Int.equal nargs (CClosure.stack_args_size v2))
+        then raise NotConvertible
         else
-          let mind = Environ.lookup_mind (fst ind1) (info_env infos.cnv_inf) in
-          let nargs = CClosure.stack_args_size v1 in
-          if not (Int.equal nargs (CClosure.stack_args_size v2))
-          then raise NotConvertible
-          else
-            let cuniv = convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv in
-            convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+          let cuniv = convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv in
+          let skip = if idtyps (* Ind injectivity *)
+            then mind.Declarations.mind_nparams
+            else 0
+          in
+          convert_stacks ~skip l2r infos lft1 lft2 v1 v2 cuniv
       else raise NotConvertible
 
     (* Eta expansion of records *)
@@ -610,9 +640,9 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
      | (FRel _ | FAtom _ | FInd _ | FFix _ | FCoFix _
         | 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)
+and convert_stacks ?(skip=0) l2r infos lft1 lft2 stk1 stk2 cuniv =
+  compare_stacks ~skip
+    (fun (l1,t1) (l2,t2) cuniv -> ccnv ~idtyps:true CONV l2r infos l1 l2 t1 t2 cuniv)
     (eq_ind)
     lft1 stk1 lft2 stk2 cuniv
 
@@ -624,7 +654,7 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
     let rec fold n cuniv =
       if n >= lv1 then cuniv
       else
-        let cuniv = ccnv CONV l2r infos lft1 lft2 v1.(n) v2.(n) cuniv in
+        let cuniv = ccnv ~idtyps:true CONV l2r infos lft1 lft2 v1.(n) v2.(n) cuniv in
         fold (n+1) cuniv in
     fold 0 cuniv
   else raise NotConvertible
@@ -637,7 +667,7 @@ let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
     lft_tab = create_tab ();
     rgt_tab = create_tab ();
   } in
-  ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs
+  ccnv ~idtyps:false cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs
 
 
 let check_eq univs u u' =