Allow using cumulativity without forcing strict constraints.

Previously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative
inductive would try to generate a constraint [i = j] and use
cumulativity only if this resulted in an inconsistency. This is
confusingly different from the behaviour with [Type] and means
cumulativity can only be used to lift between universes related by
strict inequalities. (This isn't a kernel restriction so there might
be some workaround to send the kernel the right constraints, but
not in a nice way.)

See modified test for more details of what is now possible.

Technical notes:

When universe constraints were inferred by comparing the shape of
terms without reduction, cumulativity was not used and so too-strict
equality constraints were generated. Then in order to use cumulativity
we had to make this comparison fail to fall back to full conversion.

When unifiying 2 instances of a cumulative inductive type, if there
are any Irrelevant universes we try to unify them if they are
flexible.

4 files changed, 86 insertions, 109 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index fe2e86a48..130aa8cd7 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -352,10 +352,34 @@ let exact_ise_stack2 env evd f sk1 sk2 =
     ise_stack2 evd (List.rev sk1) (List.rev sk2)
   else UnifFailure (evd, (* Dummy *) NotSameHead)
 
-let check_leq_inductives evd cumi u u' =
-  let u = EConstr.EInstance.kind evd u in
-  let u' = EConstr.EInstance.kind evd u' in
-  Evd.add_constraints evd (Reduction.get_cumulativity_constraints CUMUL cumi u u')
+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')
 
 let rec evar_conv_x ts env evd pbty term1 term2 =
   let term1 = whd_head_evar evd term1 in
@@ -446,103 +470,56 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     else evar_eqappr_x ts env' evd CONV out2 out1
   in
   let rigids env evd sk term sk' term' =
-    let check_strict () =
-      let univs = EConstr.eq_constr_universes evd term term' in
-      match univs with
-      | Some univs ->
-        begin
-          let cstrs = Universes.to_constraints (Evd.universes evd) univs in
-          try Success (Evd.add_constraints evd cstrs)
-          with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p)
-        end
-      | None ->
-        UnifFailure (evd, NotSameHead)
+    let check_strict evd u u' =
+      let cstrs = Univ.enforce_eq_instances u u' Univ.Constraint.empty in
+      try Success (Evd.add_constraints evd cstrs)
+      with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p)
     in
-    let first_try_strict_check cond u u' try_subtyping_constraints =
-      if cond then
-        let univs = EConstr.eq_constr_universes evd term term' in
-        match univs with
-        | Some univs ->
-          begin
-            let cstrs = Universes.to_constraints (Evd.universes evd) univs in
-            try Success (Evd.add_constraints evd cstrs)
-            with Univ.UniverseInconsistency p -> try_subtyping_constraints ()
-          end
-        | None ->
-          UnifFailure (evd, NotSameHead)
-      else
-        UnifFailure (evd, NotSameHead)
-    in
-    let compare_heads evd = 
+    let compare_heads evd =
       match EConstr.kind evd term, EConstr.kind evd term' with
-      | Const (c, u), Const (c', u') ->
-        check_strict ()
-      | Ind (ind, u), Ind (ind', u') ->
-        let check_subtyping_constraints () =
-          let nparamsaplied = Stack.args_size sk in
-          let nparamsaplied' = Stack.args_size sk' in
-          begin
-            let mind = Environ.lookup_mind (fst ind) env in
-            match mind.Declarations.mind_universes with
-            | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
-              UnifFailure (evd, NotSameHead)
-            | Declarations.Cumulative_ind cumi ->
-              begin
-                let num_param_arity =
-                  mind.Declarations.mind_nparams + 
-                  mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs
-                in
-                if not (num_param_arity = nparamsaplied
-                        && num_param_arity = nparamsaplied') then
-                  UnifFailure (evd, NotSameHead)
-                else
-                  begin
-                    let evd' = check_leq_inductives evd cumi u u' in
-                    Success (check_leq_inductives evd' cumi u' u)
-                  end
-              end
+      | Const (c, u), Const (c', u') when Constant.equal c c' ->
+        let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
+        check_strict evd u u'
+      | Const _, Const _ -> UnifFailure (evd, NotSameHead)
+      | Ind ((mi,i) as ind , u), Ind (ind', u') when Names.eq_ind ind ind' ->
+        if EInstance.is_empty u && EInstance.is_empty u' then Success evd
+        else
+          let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
+          let mind = Environ.lookup_mind mi env in
+          let open Declarations in
+          begin match mind.mind_universes with
+            | Monomorphic_ind _ -> assert false
+            | Polymorphic_ind _ -> check_strict evd u u'
+            | Cumulative_ind cumi ->
+              let nparamsaplied = Stack.args_size sk in
+              let nparamsaplied' = Stack.args_size sk' in
+              let needed = Reduction.inductive_cumulativity_arguments (mind,i) in
+              if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed)
+              then check_strict evd u u'
+              else
+                compare_cumulative_instances evd (Univ.ACumulativityInfo.variance cumi) u u'
           end
-        in
-        first_try_strict_check (Names.eq_ind ind ind') u u' check_subtyping_constraints
-      | Construct (cons, u), Construct (cons', u') ->
-        let check_subtyping_constraints () =
-          let ind, ind' = fst cons, fst cons' in
-          let j, j' = snd cons, snd cons' in
-          let nparamsaplied = Stack.args_size sk in
-          let nparamsaplied' = Stack.args_size sk' in
-          let mind = Environ.lookup_mind (fst ind) env in
-          match mind.Declarations.mind_universes with
-          | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
-            UnifFailure (evd, NotSameHead)
-          | Declarations.Cumulative_ind cumi ->
-            begin
-              let num_cnstr_args =
-                let nparamsctxt =
-                  mind.Declarations.mind_nparams + 
-                  mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs
-                in
-                nparamsctxt + 
-                mind.Declarations.mind_packets.(snd ind).
-                  Declarations.mind_consnrealargs.(j - 1)
-              in
-              if not (num_cnstr_args = nparamsaplied 
-                      && num_cnstr_args = nparamsaplied') then
-                UnifFailure (evd, NotSameHead)
+      | Ind _, Ind _ -> UnifFailure (evd, NotSameHead)
+      | Construct (((mi,ind),ctor as cons), u), Construct (cons', u')
+        when Names.eq_constructor cons cons' ->
+        if EInstance.is_empty u && EInstance.is_empty u' then Success evd
+        else
+          let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
+          let mind = Environ.lookup_mind mi env in
+          let open Declarations in
+          begin match mind.mind_universes with
+            | Monomorphic_ind _ -> assert false
+            | Polymorphic_ind _ -> check_strict evd u u'
+            | Cumulative_ind cumi ->
+              let nparamsaplied = Stack.args_size sk in
+              let nparamsaplied' = Stack.args_size sk' in
+              let needed = Reduction.constructor_cumulativity_arguments (mind,ind,ctor) in
+              if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed)
+              then check_strict evd u u'
               else
-                begin
-                  (** Both constructors should be liftable to the same supertype
-                      at which we compare them, but we don't have access to that type in
-                      untyped unification. We hence try to enforce that one is lower
-                      than the other, also unifying more universes in the process.
-                      If this fails we just leave the universes as is, as in conversion. *)
-                  try Success (check_leq_inductives evd cumi u u')
-                  with Univ.UniverseInconsistency _ ->
-                    try Success (check_leq_inductives evd cumi u' u)
-                    with Univ.UniverseInconsistency e -> Success evd
-                end
-            end
-        in
-        first_try_strict_check (Names.eq_constructor cons cons') u u' check_subtyping_constraints
+                Success (compare_constructor_instances evd u u')
+          end
+      | Construct _, Construct _ -> UnifFailure (evd, NotSameHead)
       | _, _ -> anomaly (Pp.str "")
     in
     ise_and evd [(fun i ->
@@ -789,7 +766,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	     allow this identification (first-order unification of universes). Otherwise
 	     fallback to unfolding.
 	  *)
-	  let univs = EConstr.eq_constr_universes evd term1 term2 in
+          let univs = EConstr.eq_constr_universes env evd term1 term2 in
           match univs with
           | Some univs ->
 	      ise_and i [(fun i -> 
@@ -1096,7 +1073,7 @@ let apply_on_subterm env evdref f c t =
     (* By using eq_constr, we make an approximation, for instance, we *)
     (* could also be interested in finding a term u convertible to t *)
     (* such that c occurs in u *)
-    let eq_constr c1 c2 = match EConstr.eq_constr_universes !evdref c1 c2 with
+    let eq_constr c1 c2 = match EConstr.eq_constr_universes env !evdref c1 c2 with
     | None -> false
     | Some cstr ->
       try ignore (Evd.add_universe_constraints !evdref cstr); true
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index c9030be2d..96d80741a 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1337,7 +1337,7 @@ type conv_fun_bool =
 
 let solve_refl ?(can_drop=false) conv_algo env evd pbty evk argsv1 argsv2 =
   let evdref = ref evd in
-  let eq_constr c1 c2 = match EConstr.eq_constr_universes !evdref c1 c2 with
+  let eq_constr c1 c2 = match EConstr.eq_constr_universes env !evdref c1 c2 with
   | None -> false
   | Some cstr ->
     try ignore (Evd.add_universe_constraints !evdref cstr); true
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 44a69d1c1..0a28f1fb8 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -698,7 +698,7 @@ let magicaly_constant_of_fixbody env sigma reference bd = function
       match constant_opt_value_in env (cst,u) with
       | None -> bd
       | Some t ->
-        let csts = EConstr.eq_constr_universes sigma (EConstr.of_constr t) bd in
+        let csts = EConstr.eq_constr_universes env sigma (EConstr.of_constr t) bd in
         begin match csts with
         | Some csts ->
           let subst = Universes.Constraints.fold (fun (l,d,r) acc ->
@@ -1332,9 +1332,9 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
     let b, sigma = 
       let ans =
 	if pb == Reduction.CUMUL then 
-	  EConstr.leq_constr_universes sigma x y
+          EConstr.leq_constr_universes env sigma x y
 	else
-	  EConstr.eq_constr_universes sigma x y
+          EConstr.eq_constr_universes env sigma x y
       in
       let ans = match ans with
       | None -> None
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f4269a2c5..1cd8d3940 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -568,10 +568,10 @@ let force_eqs c =
 	Universes.Constraints.add c' acc) 
     c Universes.Constraints.empty
 
-let constr_cmp pb sigma flags t u =
+let constr_cmp pb env sigma flags t u =
   let cstrs =
-    if pb == Reduction.CONV then EConstr.eq_constr_universes sigma t u
-    else EConstr.leq_constr_universes sigma t u
+    if pb == Reduction.CONV then EConstr.eq_constr_universes env sigma t u
+    else EConstr.leq_constr_universes env sigma t u
   in 
   match cstrs with
   | Some cstrs ->
@@ -736,7 +736,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 	| Evar (evk,_ as ev), Evar (evk',_)
             when not (Evar.Set.mem evk flags.frozen_evars)
               && Evar.equal evk evk' ->
-            let sigma',b = constr_cmp cv_pb sigma flags cM cN in
+            let sigma',b = constr_cmp cv_pb env sigma flags cM cN in
             if b then
 	      sigma',metasubst,evarsubst
             else
@@ -918,7 +918,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
   and unify_not_same_head curenvnb pb opt (sigma, metas, evars as substn : subst0) cM cN =
     try canonical_projections curenvnb pb opt cM cN substn
     with ex when precatchable_exception ex ->
-    let sigma', b = constr_cmp cv_pb sigma flags cM cN in
+    let sigma', b = constr_cmp cv_pb env sigma flags cM cN in
       if b then (sigma', metas, evars)
       else
 	try reduce curenvnb pb opt substn cM cN
@@ -1087,7 +1087,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
     else 
       let sigma, b = match flags.modulo_conv_on_closed_terms with
 	| Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n
-	| _ -> constr_cmp cv_pb sigma flags m n in
+        | _ -> constr_cmp cv_pb env sigma flags m n in
 	if b then Some sigma
 	else if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
         | Some (cv_id, cv_k), (dl_id, dl_k) ->