Merge PR #6740: Adding a sanity check on inductive variance subtyping.

1 files changed, 19 insertions, 0 deletions

diff --git a/test-suite/modules/cumpoly.v b/test-suite/modules/cumpoly.v
new file mode 100644
index 000000000..654b86cb4
--- /dev/null
+++ b/test-suite/modules/cumpoly.v
@@ -0,0 +1,19 @@
+Set Universe Polymorphism.
+
+(** Check that variance subtyping is respected. The signature T is asking for
+    invariance, while M provide an irrelevant implementation, which is deemed
+    legit.
+
+    There is currently no way to go the other way around, so it's not possible
+    to generate a counter-example that should fail with the wrong subtyping.
+*)
+
+Module Type T.
+Parameter t@{i|Set <= i} : Type@{i}.
+Cumulative Inductive I@{i|Set <= i} : Type@{i} := C : t@{i} -> I.
+End T.
+
+Module M : T.
+Definition t@{i|Set <= i} : Type@{i} := nat.
+Cumulative Inductive I@{i|Set <= i} : Type@{i} := C : t@{i} -> I.
+End M.