Merge PR#613: Cumulativity for inductive types

4 files changed, 169 insertions, 2 deletions

diff --git a/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v
index e3b5e9435..672fb3f13 100644
--- a/test-suite/bugs/closed/3330.v
+++ b/test-suite/bugs/closed/3330.v
@@ -41,6 +41,8 @@ Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function
 
 Open Scope function_scope.
 
+Set Printing Universes. Set Printing All.
+
 Inductive paths {A : Type} (a : A) : A -> Type :=
   idpath : paths a a.
 
@@ -156,7 +158,8 @@ Delimit Scope morphism_scope with morphism.
 
 Delimit Scope category_scope with category.
 Delimit Scope object_scope with object.
-
+Set Printing Universes.
+Set Printing All.
 Record PreCategory :=
   Build_PreCategory' {
       object :> Type;
@@ -1069,7 +1072,7 @@ Section Adjunction.
   Variable F : Functor C D.
   Variable G : Functor D C.
 
-  Let Adjunction_Type := 
+ Let Adjunction_Type := 
     Eval simpl in (hom_functor D) o (F^op, 1) <~=~> (hom_functor C) o (1, G).
 
   Record AdjunctionHom :=
diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v
new file mode 100644
index 000000000..a978f6b90
--- /dev/null
+++ b/test-suite/coqchk/cumulativity.v
@@ -0,0 +1,67 @@
+Set Universe Polymorphism.
+Set Inductive Cumulativity.
+Set Printing Universes.
+
+Inductive List (A: Type) := nil | cons : A -> List A -> List A.
+
+Section ListLift.
+  Universe i j.
+
+  Constraint i < j.
+
+  Definition LiftL {A} : List@{i} A -> List@{j} A := fun x => x.
+
+End ListLift.
+
+Lemma LiftL_Lem A (l : List A) : l = LiftL l.
+Proof. reflexivity. Qed.
+
+Section ListLower.
+  Universe i j.
+
+  Constraint i < j.
+
+  Definition LowerL {A : Type@{i}} : List@{j} A -> List@{i} A := fun x => x.
+
+End ListLower.
+
+Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l.
+Proof. reflexivity. Qed.
+(*
+I disable these tests because cqochk can't process them when compiled with
+   ocaml-4.02.3+32bit and camlp5-4.16 which is the case for Travis!
+
+   I have added this file (including the commented parts below) in
+   test-suite/success/cumulativity.v which doesn't run coqchk on them.
+*)
+(* Inductive Tp := tp : Type -> Tp. *)
+
+(* Section TpLift. *)
+(*   Universe i j. *)
+
+(*   Constraint i < j. *)
+
+(*   Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x. *)
+
+(* End TpLift. *)
+
+(* Lemma LiftC_Lem (t : Tp) : LiftTp t = t. *)
+(* Proof. reflexivity. Qed. *)
+
+(* Section TpLower. *)
+(*   Universe i j. *)
+
+(*   Constraint i < j. *)
+
+(*   Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x. *)
+
+(* End TpLower. *)
+
+
+(* Section subtyping_test. *)
+(*   Universe i j. *)
+(*   Constraint i < j. *)
+
+(*   Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2. *)
+
+(* End subtyping_test. *)
\ No newline at end of file
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
new file mode 100644
index 000000000..ebf817cfc
--- /dev/null
+++ b/test-suite/success/cumulativity.v
@@ -0,0 +1,65 @@
+Set Universe Polymorphism.
+Set Inductive Cumulativity.
+Set Printing Universes.
+
+Inductive List (A: Type) := nil | cons : A -> List A -> List A.
+
+Section ListLift.
+  Universe i j.
+
+  Constraint i < j.
+
+  Definition LiftL {A} : List@{i} A -> List@{j} A := fun x => x.
+
+End ListLift.
+
+Lemma LiftL_Lem A (l : List A) : l = LiftL l.
+Proof. reflexivity. Qed.
+
+Section ListLower.
+  Universe i j.
+
+  Constraint i < j.
+
+  Definition LowerL {A : Type@{i}} : List@{j} A -> List@{i} A := fun x => x.
+
+End ListLower.
+
+Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l.
+Proof. reflexivity. Qed.
+
+Inductive Tp := tp : Type -> Tp.
+
+Section TpLift.
+  Universe i j.
+
+  Constraint i < j.
+
+  Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x.
+
+End TpLift.
+
+Lemma LiftC_Lem (t : Tp) : LiftTp t = t.
+Proof. reflexivity. Qed.
+
+Section TpLower.
+  Universe i j.
+
+  Constraint i < j.
+
+  Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x.
+
+End TpLower.
+
+
+Section subtyping_test.
+  Universe i j.
+  Constraint i < j.
+
+  Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2.
+
+End subtyping_test.
+
+Record A : Type := { a :> Type; }.
+
+Record B (X : A) : Type := { b : X; }.
\ No newline at end of file
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 66ff55edc..ecc988507 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -352,3 +352,35 @@ Module Anonymous.
   Check collapsethemiddle@{_ _}.
 
 End Anonymous.
+
+Module F.
+  Context {A B : Type}.
+  Definition foo : Type := B.
+End F.
+
+Set Universe Polymorphism.
+
+Cumulative Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }.
+
+Section test_letin_subtyping.
+  Universe i j k i' j' k'.
+  Constraint j < j'.
+
+  Context (W : Type) (X : box@{i j k} W).
+  Definition Y := X : box@{i' j' k'} W.
+
+  Universe i1 j1 k1 i2 j2 k2.
+  Constraint i1 < i2.
+  Constraint k2 < k1.
+  Context (V : Type).
+
+  Definition Z : box@{i1 j1 k1} V := {| unwrap := V |}.
+  Definition Z' : box@{i2 j2 k2} V := {| unwrap := V |}.
+  Lemma ZZ' : @eq (box@{i2 j2 k2} V) Z Z'.
+  Proof.
+    Set Printing All. Set Printing Universes.
+    cbv.
+    reflexivity.
+  Qed.
+
+End test_letin_subtyping.