[kernel] Fix compare_head_gen_leq_with to use [leq] on applications

This fixes an incompleteness of subtyping on cumulative inductives,
where I@{i} A <= I@{j} A should imply i <= j, i = j or no relation
depending on the variance of I's universe.

2 files changed, 10 insertions, 1 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 11958c9108..d74c96af84 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -860,7 +860,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t
   | App (c1, l1), App (c2, l2) ->
     let len = Array.length l1 in
     Int.equal len (Array.length l2) &&
-    eq (nargs+len) c1 c2 && Array.equal_norefl (eq 0) l1 l2
+    leq (nargs+len) c1 c2 && Array.equal_norefl (eq 0) l1 l2
   | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq 0 c1 c2
   | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal (eq 0) l1 l2
   | Const (c1,u1), Const (c2,u2) ->
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index 3d97f27b16..31fed98952 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -137,3 +137,12 @@ Module WithIndex.
   Monomorphic Constraint i < j.
   Definition bar : eq mkfoo@{i} mkfoo@{j} := eq_refl _.
 End WithIndex.
+
+Module CumulApp.
+
+  (* i is covariant here, and we have one parameter *)
+  Inductive foo@{i} (A : nat) : Type@{i+1} := mkfoo (B : Type@{i}).
+
+  Definition bar@{i j|i<=j} := fun x : foo@{i} 0 => x : foo@{j} 0.
+
+End CumulApp.