Properly handling polymorphic inductive subtyping in the kernel.

Before this patch, inductive subtyping was enforcing syntactic equality
of the variable instance, instead of reasoning up to alpha-renaming.

1 files changed, 87 insertions, 0 deletions

diff --git a/test-suite/modules/polymorphism2.v b/test-suite/modules/polymorphism2.v
new file mode 100644
index 000000000..7e3327eee
--- /dev/null
+++ b/test-suite/modules/polymorphism2.v
@@ -0,0 +1,87 @@
+Set Universe Polymorphism.
+
+(** Tests for module subtyping of polymorphic terms *)
+
+Module Type S.
+
+Section Foo.
+
+Universes i j.
+Constraint i <= j.
+
+Inductive foo : Type@{i} -> Type@{j} :=.
+
+End Foo.
+
+End S.
+
+(** Same constraints *)
+
+Module OK_1.
+
+Section Foo.
+
+Universes i j.
+Constraint i <= j.
+
+Inductive foo : Type@{i} -> Type@{j} :=.
+
+End Foo.
+
+End OK_1.
+
+Module OK_1_Test : S := OK_1.
+
+(** More general constraints *)
+
+Module OK_2.
+
+Inductive foo@{i j} : Type@{i} -> Type@{j} :=.
+
+End OK_2.
+
+Module OK_2_Test : S := OK_2.
+
+(** Wrong instance length *)
+
+Module KO_1.
+
+Inductive foo@{i} : Type@{i} -> Type@{i} :=.
+
+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.
+
+Inductive foo : Type@{i} -> Type@{j} :=.
+
+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.
+
+Inductive foo : Type@{i} -> Type@{j} :=.
+
+End Foo.
+
+End KO_3.
+
+Fail Module KO_Test_3 : S := KO_3.