From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 test-suite/modules/polymorphism.v | 81 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 81 insertions(+)
 create mode 100644 test-suite/modules/polymorphism.v

(limited to 'test-suite/modules/polymorphism.v')

diff --git a/test-suite/modules/polymorphism.v b/test-suite/modules/polymorphism.v
new file mode 100644
index 00000000..63eaa382
--- /dev/null
+++ b/test-suite/modules/polymorphism.v
@@ -0,0 +1,81 @@
+Set Universe Polymorphism.
+
+(** Tests for module subtyping of polymorphic terms *)
+
+Module Type S.
+
+Section Foo.
+
+Universes i j.
+Constraint i <= j.
+
+Parameter foo : Type@{i} -> Type@{j}.
+
+End Foo.
+
+End S.
+
+(** Same constraints *)
+
+Module OK_1.
+
+Definition foo@{i j} (A : Type@{i}) : Type@{j} := A.
+
+End OK_1.
+
+Module OK_1_Test : S := OK_1.
+
+(** More general constraints *)
+
+Module OK_2.
+
+Inductive X@{i} : Type@{i} :=.
+Definition foo@{i j} (A : Type@{i}) : Type@{j} := X@{j}.
+
+End OK_2.
+
+Module OK_2_Test : S := OK_2.
+
+(** Wrong instance length *)
+
+Module KO_1.
+
+Definition foo@{i} (A : Type@{i}) : Type@{i} := A.
+
+End KO_1.
+
+Fail Module KO_Test_1 : S := KO_1.
+
+(** Less general constraints *)
+
+Module KO_2.
+
+Section Foo.
+
+Universe i j.
+Constraint i < j.
+
+Definition foo (A : Type@{i}) : Type@{j} := A.
+
+End Foo.
+
+End KO_2.
+
+Fail Module KO_Test_2 : S := KO_2.
+
+(** Less general constraints *)
+
+Module KO_3.
+
+Section Foo.
+
+Universe i j.
+Constraint i = j.
+
+Definition foo (A : Type@{i}) : Type@{j} := A.
+
+End Foo.
+
+End KO_3.
+
+Fail Module KO_Test_3 : S := KO_3.
-- 
cgit v1.2.3