Cumulativity: improve treatment of irrelevant universes.

In Reductionops.infer_conv we did not have enough information to
properly try to unify irrelevant universes. This requires changing the
Reduction.universe_compare type a bit.

2 files changed, 8 insertions, 29 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 130aa8cd7e..d37090a653 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -352,34 +352,13 @@ let exact_ise_stack2 env evd f sk1 sk2 =
     ise_stack2 evd (List.rev sk1) (List.rev sk2)
   else UnifFailure (evd, (* Dummy *) NotSameHead)
 
-let try_soft evd u u' =
-  let open Universes in
-  let make = Univ.Universe.make in
-  try Evd.add_universe_constraints evd (Constraints.singleton (make u,ULub,make u'))
-  with UState.UniversesDiffer | Univ.UniverseInconsistency _ -> evd
-
 (* Add equality constraints for covariant/invariant positions. For
    irrelevant positions, unify universes when flexible. *)
 let compare_cumulative_instances evd variances u u' =
-  let cstrs = Univ.Constraint.empty in
-  let soft = [] in
-  let cstrs, soft = Array.fold_left3 (fun (cstrs, soft) v u u' ->
-      let open Univ.Variance in
-      match v with
-      | Irrelevant -> cstrs, (u,u')::soft
-      | Covariant | Invariant -> Univ.Constraint.add (u,Univ.Eq,u') cstrs, soft)
-      (cstrs,soft) variances (Univ.Instance.to_array u) (Univ.Instance.to_array u')
-  in
-  match Evd.add_constraints evd cstrs with
-  | evd ->
-    Success (List.fold_left (fun evd (u,u') -> try_soft evd u u') evd soft)
-  | exception Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p)
-
-(* We should only compare constructors at convertible types, so this
-   is only an opportunity to unify universes. *)
-let compare_constructor_instances evd u u' =
-  Array.fold_left2 try_soft
-    evd (Univ.Instance.to_array u) (Univ.Instance.to_array u')
+  match Evarutil.compare_cumulative_instances CONV variances u u' evd with
+  | Inl evd ->
+    Success evd
+  | Inr p -> UnifFailure (evd, UnifUnivInconsistency p)
 
 let rec evar_conv_x ts env evd pbty term1 term2 =
   let term1 = whd_head_evar evd term1 in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 0a28f1fb84..47e2ba93bd 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1313,10 +1313,10 @@ let sigma_compare_instances ~flex i0 i1 sigma =
      | Univ.UniverseInconsistency _ ->
 	raise Reduction.NotConvertible
 
-let sigma_check_inductive_instances csts sigma =
-  try Evd.add_constraints sigma csts
-  with Evd.UniversesDiffer
-     | Univ.UniverseInconsistency _ ->
+let sigma_check_inductive_instances cv_pb variance u1 u2 sigma =
+  match Evarutil.compare_cumulative_instances cv_pb variance u1 u2 sigma with
+  | Inl sigma -> sigma
+  | Inr _ ->
     raise Reduction.NotConvertible
 
 let sigma_univ_state =