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.

6 files changed, 110 insertions, 91 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index b95068ebf..59dc5a221 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -548,39 +548,100 @@ let fold sigma f acc c = match kind sigma c with
   | CoFix (_,(lna,tl,bl)) ->
     Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
 
-let compare_gen k eq_inst eq_sort eq_constr c1 c2 =
-  (c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr c1 c2
+let compare_gen k eq_inst eq_sort eq_constr nargs c1 c2 =
+  (c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr nargs c1 c2
 
 let eq_constr sigma c1 c2 =
   let kind c = kind_upto sigma c in
-  let rec eq_constr c1 c2 =
-    compare_gen kind (fun _ -> Univ.Instance.equal) Sorts.equal eq_constr c1 c2
+  let rec eq_constr nargs c1 c2 =
+    compare_gen kind (fun _ _ -> Univ.Instance.equal) Sorts.equal eq_constr nargs c1 c2
   in
-  eq_constr (unsafe_to_constr c1) (unsafe_to_constr c2)
+  eq_constr 0 (unsafe_to_constr c1) (unsafe_to_constr c2)
 
 let eq_constr_nounivs sigma c1 c2 =
   let kind c = kind_upto sigma c in
-  let rec eq_constr c1 c2 =
-    compare_gen kind (fun _ _ _ -> true) (fun _ _ -> true) eq_constr c1 c2
+  let rec eq_constr nargs c1 c2 =
+    compare_gen kind (fun _ _ _ _ -> true) (fun _ _ -> true) eq_constr nargs c1 c2
   in
-  eq_constr (unsafe_to_constr c1) (unsafe_to_constr c2)
+  eq_constr 0 (unsafe_to_constr c1) (unsafe_to_constr c2)
 
 let compare_constr sigma cmp c1 c2 =
   let kind c = kind_upto sigma c in
-  let cmp c1 c2 = cmp (of_constr c1) (of_constr c2) in
-  compare_gen kind (fun _ -> Univ.Instance.equal) Sorts.equal cmp (unsafe_to_constr c1) (unsafe_to_constr c2)
+  let cmp nargs c1 c2 = cmp (of_constr c1) (of_constr c2) in
+  compare_gen kind (fun _ _ -> Univ.Instance.equal) Sorts.equal cmp 0 (unsafe_to_constr c1) (unsafe_to_constr c2)
 
-let test_constr_universes sigma leq m n =
+let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs =
+  let open Universes in
+  if not nargs_ok then enforce_eq_instances_univs false u u' cstrs
+  else
+    CArray.fold_left3
+      (fun cstrs v u u' ->
+         let open Univ.Variance in
+         let u = Univ.Universe.make u in
+         let u' = Univ.Universe.make u' in
+         match v with
+         | Irrelevant -> Constraints.add (u,ULub,u') cstrs
+         | Covariant ->
+           (match cv_pb with
+            | Reduction.CONV -> Constraints.add (u,UEq,u') cstrs
+            | Reduction.CUMUL -> Constraints.add (u,ULe,u') cstrs)
+         | Invariant -> Constraints.add (u,UEq,u') cstrs)
+      cstrs variances (Univ.Instance.to_array u) (Univ.Instance.to_array u')
+
+let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs =
+  let open Universes in
+  match mind.Declarations.mind_universes with
+  | Declarations.Monomorphic_ind _ ->
+    assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0);
+    cstrs
+  | Declarations.Polymorphic_ind _ ->
+     enforce_eq_instances_univs false u1 u2 cstrs
+  | Declarations.Cumulative_ind cumi ->
+    let num_param_arity = Reduction.inductive_cumulativity_arguments spec in
+    let variances = Univ.ACumulativityInfo.variance cumi in
+    compare_cumulative_instances cv_pb (Int.equal num_param_arity nargs) variances u1 u2 cstrs
+
+let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs =
+  let open Universes in
+  match mind.Declarations.mind_universes with
+  | Declarations.Monomorphic_ind _ ->
+    cstrs
+  | Declarations.Polymorphic_ind _ ->
+    enforce_eq_instances_univs false u1 u2 cstrs
+  | Declarations.Cumulative_ind cumi ->
+    let num_cnstr_args = Reduction.constructor_cumulativity_arguments spec in
+    let variances = Univ.ACumulativityInfo.variance cumi in
+    compare_cumulative_instances Reduction.CONV (Int.equal num_cnstr_args nargs) variances u1 u2 cstrs
+
+let eq_universes env sigma cstrs cv_pb ref nargs l l' =
+  if Univ.Instance.is_empty l then (assert (Univ.Instance.is_empty l'); true)
+  else
+    let l = Evd.normalize_universe_instance sigma l
+    and l' = Evd.normalize_universe_instance sigma l' in
+    let open Universes in
+    match ref with
+    | VarRef _ -> assert false (* variables don't have instances *)
+    | ConstRef _ ->
+      cstrs := enforce_eq_instances_univs true l l' !cstrs; true
+    | IndRef ind ->
+      let mind = Environ.lookup_mind (fst ind) env in
+      cstrs := cmp_inductives cv_pb (mind,snd ind) nargs l l' !cstrs;
+      true
+    | ConstructRef ((mi,ind),ctor) ->
+      let mind = Environ.lookup_mind mi env in
+      cstrs := cmp_constructors (mind,ind,ctor) nargs l l' !cstrs;
+      true
+
+let test_constr_universes env sigma leq m n =
   let open Universes in
   let kind c = kind_upto sigma c in
   if m == n then Some Constraints.empty
-  else 
+  else
     let cstrs = ref Constraints.empty in
-    let eq_universes strict l l' = 
-      let l = EInstance.kind sigma (EInstance.make l) in
-      let l' = EInstance.kind sigma (EInstance.make l') in
-      cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in
-    let eq_sorts s1 s2 = 
+    let cv_pb = if leq then Reduction.CUMUL else Reduction.CONV in
+    let eq_universes ref nargs l l' = eq_universes env sigma cstrs Reduction.CONV ref nargs l l'
+    and leq_universes ref nargs l l' = eq_universes env sigma cstrs cv_pb ref nargs l l' in
+    let eq_sorts s1 s2 =
       let s1 = ESorts.kind sigma (ESorts.make s1) in
       let s2 = ESorts.kind sigma (ESorts.make s2) in
       if Sorts.equal s1 s2 then true
@@ -597,24 +658,25 @@ let test_constr_universes sigma leq m n =
 	   (Sorts.univ_of_sort s1,ULe,Sorts.univ_of_sort s2) !cstrs; 
 	 true)
     in
-    let rec eq_constr' m n = compare_gen kind eq_universes eq_sorts eq_constr' m n in
+    let rec eq_constr' nargs m n = compare_gen kind eq_universes eq_sorts eq_constr' nargs m n in
     let res =
       if leq then
-        let rec compare_leq m n =
-          Constr.compare_head_gen_leq_with kind kind eq_universes leq_sorts eq_constr' leq_constr' m n
-        and leq_constr' m n = m == n || compare_leq m n in
-        compare_leq m n
+        let rec compare_leq nargs m n =
+          Constr.compare_head_gen_leq_with kind kind leq_universes leq_sorts
+            eq_constr' leq_constr' nargs m n
+        and leq_constr' nargs m n = m == n || compare_leq nargs m n in
+        compare_leq 0 m n
       else
-        Constr.compare_head_gen_with kind kind eq_universes eq_sorts eq_constr' m n
+        Constr.compare_head_gen_with kind kind eq_universes eq_sorts eq_constr' 0 m n
     in
     if res then Some !cstrs else None
 
-let eq_constr_universes sigma m n =
-  test_constr_universes sigma false (unsafe_to_constr m) (unsafe_to_constr n)
-let leq_constr_universes sigma m n =
-  test_constr_universes sigma true (unsafe_to_constr m) (unsafe_to_constr n)
+let eq_constr_universes env sigma m n =
+  test_constr_universes env sigma false (unsafe_to_constr m) (unsafe_to_constr n)
+let leq_constr_universes env sigma m n =
+  test_constr_universes env sigma true (unsafe_to_constr m) (unsafe_to_constr n)
 
-let compare_head_gen_proj env sigma equ eqs eqc' m n =
+let compare_head_gen_proj env sigma equ eqs eqc' nargs m n =
   let kind c = kind_upto sigma c in
   match kind_upto sigma m, kind_upto sigma n with
   | Proj (p, c), App (f, args)
@@ -624,29 +686,28 @@ let compare_head_gen_proj env sigma equ eqs eqc' m n =
           let pb = Environ.lookup_projection p env in
           let npars = pb.Declarations.proj_npars in
 	  if Array.length args == npars + 1 then
-	    eqc' c args.(npars)
+            eqc' 0 c args.(npars)
 	  else false
       | _ -> false)
-  | _ -> Constr.compare_head_gen_with kind kind equ eqs eqc' m n
+  | _ -> Constr.compare_head_gen_with kind kind equ eqs eqc' nargs m n
 
 let eq_constr_universes_proj env sigma m n =
   let open Universes in
   if m == n then Some Constraints.empty
   else 
     let cstrs = ref Constraints.empty in
-    let eq_universes strict l l' = 
-      cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in
-    let eq_sorts s1 s2 = 
+    let eq_universes ref l l' = eq_universes env sigma cstrs Reduction.CONV ref l l' in
+    let eq_sorts s1 s2 =
       if Sorts.equal s1 s2 then true
       else
 	(cstrs := Constraints.add 
 	   (Sorts.univ_of_sort s1, UEq, Sorts.univ_of_sort s2) !cstrs;
 	 true)
     in
-    let rec eq_constr' m n = 
-      m == n ||	compare_head_gen_proj env sigma eq_universes eq_sorts eq_constr' m n
+    let rec eq_constr' nargs m n =
+      m == n || compare_head_gen_proj env sigma eq_universes eq_sorts eq_constr' nargs m n
     in
-    let res = eq_constr' (unsafe_to_constr m) (unsafe_to_constr n) in
+    let res = eq_constr' 0 (unsafe_to_constr m) (unsafe_to_constr n) in
     if res then Some !cstrs else None
 
 let universes_of_constr env sigma c =
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 36b6093d0..28c9dd3c2 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -198,9 +198,12 @@ val whd_evar : Evd.evar_map -> constr -> constr
 
 val eq_constr : Evd.evar_map -> t -> t -> bool
 val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool
-val eq_constr_universes : Evd.evar_map -> t -> t -> Universes.Constraints.t option
-val leq_constr_universes : Evd.evar_map -> t -> t -> Universes.Constraints.t option
+val eq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option
+val leq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option
+
+(** [eq_constr_universes_proj] can equate projections and their eta-expanded constant form. *)
 val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option
+
 val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool
 
 (** {6 Iterators} *)
diff --git a/engine/termops.ml b/engine/termops.ml
index 35258762a..20b6b3504 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -914,12 +914,9 @@ let vars_of_global_reference env gr =
 (* Tests whether [m] is a subterm of [t]:
    [m] is appropriately lifted through abstractions of [t] *)
 
-let dependent_main noevar univs sigma m t =
+let dependent_main noevar sigma m t =
   let open EConstr in
-  let eqc x y =
-    if univs then not (Option.is_empty (eq_constr_universes sigma x y))
-    else eq_constr_nounivs sigma x y
-  in
+  let eqc x y = eq_constr_nounivs sigma x y in
   let rec deprec m t =
     if eqc m t then
       raise Occur
@@ -936,11 +933,8 @@ let dependent_main noevar univs sigma m t =
   in
   try deprec m t; false with Occur -> true
 
-let dependent sigma c t = dependent_main false false sigma c t
-let dependent_no_evar sigma c t = dependent_main true false sigma c t
-
-let dependent_univs sigma c t = dependent_main false true sigma c t
-let dependent_univs_no_evar sigma c t = dependent_main true true sigma c t
+let dependent sigma c t = dependent_main false sigma c t
+let dependent_no_evar sigma c t = dependent_main true sigma c t
 
 let dependent_in_decl sigma a decl =
   let open NamedDecl in
diff --git a/engine/termops.mli b/engine/termops.mli
index ef3cb91be..3b0c4bba6 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -108,8 +108,6 @@ val free_rels : Evd.evar_map -> constr -> Int.Set.t
 (** [dependent m t] tests whether [m] is a subterm of [t] *)
 val dependent : Evd.evar_map -> constr -> constr -> bool
 val dependent_no_evar : Evd.evar_map -> constr -> constr -> bool
-val dependent_univs : Evd.evar_map -> constr -> constr -> bool
-val dependent_univs_no_evar : Evd.evar_map -> constr -> constr -> bool
 val dependent_in_decl : Evd.evar_map -> constr -> named_declaration -> bool
 val count_occurrences : Evd.evar_map -> constr -> constr -> int
 val collect_metas : Evd.evar_map -> constr -> int list
diff --git a/engine/universes.ml b/engine/universes.ml
index c74467405..70ed6311e 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -242,7 +242,7 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
      [kind1,kind2], because [kind1] and [kind2] may be different,
      typically evaluating [m] and [n] in different evar maps. *)
   let cstrs = ref accu in
-  let eq_universes strict = UGraph.check_eq_instances univs in
+  let eq_universes _ _ = UGraph.check_eq_instances univs in
   let eq_sorts s1 s2 = 
     if Sorts.equal s1 s2 then true
     else
@@ -251,45 +251,12 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
       | None -> false
       | Some accu -> cstrs := accu; true
   in
-  let rec eq_constr' m n = 
-    Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n
+  let rec eq_constr' nargs m n =
+    Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' nargs m n
   in
-  let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in
+  let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' 0 m n in
   if res then Some !cstrs else None
 
-let compare_head_gen_proj env equ eqs eqc' m n =
-  match kind m, kind n with
-  | Proj (p, c), App (f, args)
-  | App (f, args), Proj (p, c) -> 
-      (match kind f with
-      | Const (p', u) when Constant.equal (Projection.constant p) p' -> 
-          let pb = Environ.lookup_projection p env in
-          let npars = pb.Declarations.proj_npars in
-	  if Array.length args == npars + 1 then
-	    eqc' c args.(npars)
-	  else false
-      | _ -> false)
-  | _ -> Constr.compare_head_gen equ eqs eqc' m n
-      
-let eq_constr_universes_proj env m n =
-  if m == n then true, Constraints.empty
-  else 
-    let cstrs = ref Constraints.empty in
-    let eq_universes strict l l' = 
-      cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in
-    let eq_sorts s1 s2 = 
-      if Sorts.equal s1 s2 then true
-      else
-	(cstrs := Constraints.add 
-	   (Sorts.univ_of_sort s1, UEq, Sorts.univ_of_sort s2) !cstrs;
-	 true)
-    in
-    let rec eq_constr' m n = 
-      m == n ||	compare_head_gen_proj env eq_universes eq_sorts eq_constr' m n
-    in
-    let res = eq_constr' m n in
-    res, !cstrs
-
 (* Generator of levels *)
 type universe_id = DirPath.t * int
 
diff --git a/engine/universes.mli b/engine/universes.mli
index 8e6b8f60c..a86b9779b 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -102,10 +102,6 @@ val eq_constr_univs_infer_with :
   (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
   UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option
 
-(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
-    application grouping and the universe constraints in [c]. *)
-val eq_constr_universes_proj : env -> constr -> constr -> bool universe_constrained
-
 (** Build a fresh instance for a given context, its associated substitution and 
     the instantiated constraints. *)