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, 42 insertions, 0 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 6b3ce048f..8db603715 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -813,6 +813,34 @@ let subterm_source evk (loc,k) =
     | _ -> evk in
   (loc,Evar_kinds.SubEvar evk)
 
+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 cv_pb variances u u' sigma =
+  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 when cv_pb == Reduction.CUMUL ->
+        Univ.Constraint.add (u,Univ.Le,u') cstrs, 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 sigma cstrs with
+  | sigma ->
+    Inl (List.fold_left (fun sigma (u,u') -> try_soft sigma u u') sigma soft)
+  | exception Univ.UniverseInconsistency p -> Inr p
+
+let compare_constructor_instances evd u u' =
+  Array.fold_left2 try_soft
+    evd (Univ.Instance.to_array u) (Univ.Instance.to_array u')
 
 (** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
     [u] up to existential variable instantiation and equalisable
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 373875bd0..e289ca169 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -203,6 +203,20 @@ val kind_of_term_upto : evar_map -> Constr.constr ->
     assumed to be an extention of those in [sigma1]. *)
 val eq_constr_univs_test : evar_map -> evar_map -> Constr.constr -> Constr.constr -> bool
 
+(** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns
+   [Inl sigma'] where [sigma'] is [sigma] augmented with universe
+   constraints such that [u1 cv_pb? u2] according to [variance].
+   Additionally flexible universes in irrelevant positions are unified
+   if possible. Returns [Inr p] when the former is impossible. *)
+val compare_cumulative_instances : Reduction.conv_pb -> Univ.Variance.t array ->
+  Univ.Instance.t -> Univ.Instance.t -> evar_map ->
+  (evar_map, Univ.univ_inconsistency) Util.union
+
+(** We should only compare constructors at convertible types, so this
+   is only an opportunity to unify universes. *)
+val compare_constructor_instances : evar_map ->
+  Univ.Instance.t -> Univ.Instance.t -> evar_map
+
 (** {6 Removing hyps in evars'context}
 raise OccurHypInSimpleClause if the removal breaks dependencies *)