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.

1 files changed, 27 insertions, 20 deletions

diff --git a/kernel/constr.mli b/kernel/constr.mli
index f7e4eecba..98c0eaa28 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -402,31 +402,38 @@ val iter : (constr -> unit) -> constr -> unit
 val iter_with_binders :
   ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit
 
+type constr_compare_fn = int -> constr -> constr -> bool
+
 (** [compare_head f c1 c2] compare [c1] and [c2] using [f] to compare
    the immediate subterms of [c1] of [c2] if needed; Cast's, binders
    name and Cases annotations are not taken into account *)
 
-val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool
+val compare_head : constr_compare_fn -> constr_compare_fn
+
+(** Convert a global reference applied to 2 instances. The int says
+   how many arguments are given (as we can only use cumulativity for
+   fully applied inductives/constructors) .*)
+type instance_compare_fn = global_reference -> int ->
+  Univ.Instance.t -> Univ.Instance.t -> bool
 
-(** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare
-   the immediate subterms of [c1] of [c2] if needed, [u] to compare universe
-   instances (the first boolean tells if they belong to a Constant.t), [s] to 
-   compare sorts; Cast's, binders name and Cases annotations are not taken 
-    into account *)
+(** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to
+   compare the immediate subterms of [c1] of [c2] if needed, [u] to
+   compare universe instances, [s] to compare sorts; Cast's, binders
+   name and Cases annotations are not taken into account *)
 
-val compare_head_gen : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
+val compare_head_gen : instance_compare_fn ->
   (Sorts.t -> Sorts.t -> bool) ->
-  (constr -> constr -> bool) ->
-  constr -> constr -> bool
+  constr_compare_fn ->
+  constr_compare_fn
 
 val compare_head_gen_leq_with :
   (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
   (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
-  (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
+  instance_compare_fn ->
   (Sorts.t -> Sorts.t -> bool) ->
-  (constr -> constr -> bool) ->
-  (constr -> constr -> bool) ->
-  constr -> constr -> bool
+  constr_compare_fn ->
+  constr_compare_fn ->
+  constr_compare_fn
 
 (** [compare_head_gen_with k1 k2 u s f c1 c2] compares [c1] and [c2]
     like [compare_head_gen u s f c1 c2], except that [k1] (resp. [k2])
@@ -435,10 +442,10 @@ val compare_head_gen_leq_with :
 val compare_head_gen_with :
   (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
   (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
-  (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
+  instance_compare_fn ->
   (Sorts.t -> Sorts.t -> bool) ->
-  (constr -> constr -> bool) ->
-  constr -> constr -> bool
+  constr_compare_fn ->
+  constr_compare_fn
 
 (** [compare_head_gen_leq u s f fle c1 c2] compare [c1] and [c2] using
     [f] to compare the immediate subterms of [c1] of [c2] for
@@ -447,11 +454,11 @@ val compare_head_gen_with :
     [s] to compare sorts for for subtyping; Cast's, binders name and
     Cases annotations are not taken into account *)
 
-val compare_head_gen_leq : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
+val compare_head_gen_leq : instance_compare_fn ->
   (Sorts.t -> Sorts.t -> bool) ->
-  (constr -> constr -> bool) ->
-  (constr -> constr -> bool) ->
-  constr -> constr -> bool
+  constr_compare_fn ->
+  constr_compare_fn ->
+  constr_compare_fn
 
 (** {6 Hashconsing} *)