Conversion of polymorphic inductive types was incomplete in VM and native.

Was showing up when comparing e.g. prod Type Type with prod Type Type (!) with
a polymorphic prod.

5 files changed, 31 insertions, 37 deletions

diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 7ae66c485..0242fd461 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -63,10 +63,12 @@ and conv_atom env pb lvl a1 a2 cu =
     | Ameta _, _ | _, Ameta _ | Aevar _, _ | _, Aevar _ -> assert false
     | Arel i1, Arel i2 -> 
 	if Int.equal i1 i2 then cu else raise NotConvertible
-    | Aind ind1, Aind ind2 ->
-	if eq_puniverses eq_ind ind1 ind2 then cu else raise NotConvertible
-    | Aconstant c1, Aconstant c2 ->
-	if eq_puniverses eq_constant c1 c2 then cu else raise NotConvertible
+    | Aind (ind1,u1), Aind (ind2,u2) ->
+       if eq_ind ind1 ind2 then convert_instances ~flex:false u1 u2 cu
+       else raise NotConvertible
+    | Aconstant (c1,u1), Aconstant (c2,u2) ->
+       if Constant.equal c1 c2 then convert_instances ~flex:true u1 u2 cu
+       else raise NotConvertible
     | Asort s1, Asort s2 -> 
         sort_cmp_universes env pb s1 s2 cu
     | Avar id1, Avar id2 ->
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 2c111a55b..892557ac6 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -173,7 +173,7 @@ let is_cumul = function CUMUL -> true | CONV -> false
 type 'a universe_compare = 
   { (* Might raise NotConvertible *)
     compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a;
-    compare_instances: bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
+    compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
   } 
 
 type 'a universe_state = 'a * 'a universe_compare
@@ -185,8 +185,10 @@ type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.co
 let sort_cmp_universes env pb s0 s1 (u, check) =
   (check.compare env pb s0 s1 u, check)
 
-let convert_instances flex u u' (s, check) =
-  (check.compare_instances flex u u' s, check)
+(* [flex] should be true for constants, false for inductive types and
+   constructors. *)
+let convert_instances ~flex u u' (s, check) =
+  (check.compare_instances ~flex u u' s, check)
 
 let conv_table_key infos k1 k2 cuniv =
   if k1 == k2 then cuniv else
@@ -196,7 +198,7 @@ let conv_table_key infos k1 k2 cuniv =
     else 
       let flex = evaluable_constant cst (info_env infos) 
 	&& RedFlags.red_set (info_flags infos) (RedFlags.fCONST cst)
-      in convert_instances flex u u' cuniv
+      in convert_instances ~flex u u' cuniv
   | VarKey id, VarKey id' when Id.equal id id' -> cuniv
   | RelKey n, RelKey n' when Int.equal n n' -> cuniv
   | _ -> raise NotConvertible
@@ -590,7 +592,7 @@ let check_sort_cmp_universes env pb s0 s1 univs =
 let checked_sort_cmp_universes env pb s0 s1 univs =
   check_sort_cmp_universes env pb s0 s1 univs; univs
 
-let check_convert_instances _flex u u' univs =
+let check_convert_instances ~flex u u' univs =
   if Univ.Instance.check_eq univs u u' then univs
   else raise NotConvertible
 
@@ -630,7 +632,7 @@ let infer_cmp_universes env pb s0 s1 univs =
 	| CONV -> infer_eq univs u1 u2)
         else univs
 
-let infer_convert_instances flex u u' (univs,cstrs) =
+let infer_convert_instances ~flex u u' (univs,cstrs) =
   (univs, Univ.enforce_eq_instances u u' cstrs)
 
 let inferred_universes : (Univ.universes * Univ.Constraint.t) universe_compare =
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index c3cc7b2b6..0df26d627 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -37,7 +37,7 @@ type conv_pb = CONV | CUMUL
 type 'a universe_compare = 
   { (* Might raise NotConvertible *)
     compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a;
-    compare_instances: bool (* Instance of a flexible constant? *) -> 
+    compare_instances: flex:bool -> 
 		       Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
   } 
 
@@ -50,6 +50,11 @@ type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.co
 val sort_cmp_universes : env -> conv_pb -> sorts -> sorts ->
   'a * 'a universe_compare -> 'a * 'a universe_compare
 
+(* [flex] should be true for constants, false for inductive types and
+constructors. *)
+val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t ->
+  'a * 'a universe_compare -> 'a * 'a universe_compare
+
 val checked_universes : Univ.universes universe_compare
 val inferred_universes : (Univ.universes * Univ.Constraint.t) universe_compare
 
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index e0d968848..2e519789e 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -99,17 +99,15 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
 	  let ulen = Univ.UContext.size mib.Declarations.mind_universes in
           match stk1 , stk2 with
 	  | Zapp args1 :: stk1' , Zapp args2 :: stk2' ->
-	    assert (ulen <= nargs args1) ;
-            assert (ulen <= nargs args2) ;
-            for i = 0 to ulen - 1 do
-              let a1 = uni_lvl_val (arg args1 i) in
-              let a2 = uni_lvl_val (arg args2 i) in
-              let result = Univ.Level.equal a1 a2 in
-              if not result
-              then raise NotConvertible
-            done ;
-            conv_arguments env ~from:ulen k args1 args2
-              (conv_stack env k stk1' stk2' cu)
+	     assert (ulen <= nargs args1);
+             assert (ulen <= nargs args2);
+	     let u1 = Array.init ulen (fun i -> uni_lvl_val (arg args1 i)) in
+	     let u2 = Array.init ulen (fun i -> uni_lvl_val (arg args2 i)) in
+	     let u1 = Univ.Instance.of_array u1 in
+	     let u2 = Univ.Instance.of_array u2 in
+	     let cu = convert_instances ~flex:false u1 u2 cu in
+             conv_arguments env ~from:ulen k args1 args2
+			    (conv_stack env k stk1' stk2' cu)
 	  | _ -> raise NotConvertible
         else
 	  conv_stack env k stk1 stk2 cu
@@ -118,13 +116,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
       if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
 	conv_stack env k stk1 stk2 cu
       else raise NotConvertible
-  | Atype u1 , Atype u2 ->
-    let u1 = Vm.instantiate_universe u1 stk1 in
-    let u2 = Vm.instantiate_universe u2 stk2 in
-    sort_cmp_universes env pb (Type u1) (Type u2) cu
-  | Atype _ , Aid _
-  | Atype _ , Aind _
-  | Aid _ , Atype _
+  | Atype _ , _ | _, Atype _ -> assert false
   | Aind _, _ | Aid _, _ -> raise NotConvertible
 
 and conv_stack env ?from:(from=0) k stk1 stk2 cu =
@@ -190,13 +182,6 @@ and conv_arguments env ?from:(from=0) k args1 args2 cu =
       !rcu
     else raise NotConvertible
 
-let rec eq_puniverses f (x,l1) (y,l2) cu =
-  if f x y then conv_universes l1 l2 cu
-  else raise NotConvertible
-
-and conv_universes l1 l2 cu =
-  if Univ.Instance.equal l1 l2 then cu else raise NotConvertible
-
 let vm_conv_gen cv_pb env univs t1 t2 =
   try 
     let v1 = val_of_constr env t1 in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index bb1bc7d2e..0714c93b4 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1282,7 +1282,7 @@ let sigma_compare_sorts env pb s0 s1 sigma =
   | Reduction.CONV -> Evd.set_eq_sort env sigma s0 s1
   | Reduction.CUMUL -> Evd.set_leq_sort env sigma s0 s1
     
-let sigma_compare_instances flex i0 i1 sigma =
+let sigma_compare_instances ~flex i0 i1 sigma =
   try Evd.set_eq_instances ~flex sigma i0 i1
   with Evd.UniversesDiffer
      | Univ.UniverseInconsistency _ ->