diff options
Diffstat (limited to 'test-suite/success/polymorphism.v')
| -rw-r--r-- | test-suite/success/polymorphism.v | 52 |
1 files changed, 32 insertions, 20 deletions
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 3e90825ab..f57cbcc2b 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -316,26 +316,6 @@ Module Hurkens'. Polymorphic 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, k2 < k1. - Definition Z : box@{i1 j1 k1} W := {| unwrap := W |}. - Definition Z' : box@{i2 j2 k2} W := {| unwrap := W |}. - Lemma ZZ' : @eq (box@{i2 j2 k2} W) Z Z'. - Proof. - Set Printing All. Set Printing Universes. - cbv. - reflexivity. - Qed. - -End test_letin_subtyping. - Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw. Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _ @@ -372,3 +352,35 @@ Module Anonymous. Check collapsethemiddle@{_ _}. End Anonymous. + +Module F. + Context {A B : Type}. + Definition foo : Type := B. +End F. + +Set Universe Polymorphism. + +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. |