aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/modules
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/modules')
-rw-r--r--test-suite/modules/cumpoly.v19
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.