From 636857d2e77ee26b4b193f3bbefee253c07dfbff Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 15 Mar 2019 10:01:16 -0300
Subject: [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.
---
 test-suite/success/cumulativity.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3