diff options
Diffstat (limited to 'test-suite/bugs/opened/HoTT_coq_093.v')
| -rw-r--r-- | test-suite/bugs/opened/HoTT_coq_093.v | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_093.v b/test-suite/bugs/opened/HoTT_coq_093.v new file mode 100644 index 0000000000..029a0caf76 --- /dev/null +++ b/test-suite/bugs/opened/HoTT_coq_093.v @@ -0,0 +1,37 @@ +(** It would be nice if we had more lax constraint checking of inductive types, and had variance annotations on their universes *) +Set Printing All. +Set Printing Implicit. +Set Printing Universes. +Set Universe Polymorphism. + +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. +Arguments idpath {A a} , [A] a. + +Notation "x = y" := (@paths _ x y) : type_scope. + +Section lift. + Let lift_type : Type. + Proof. + let U0 := constr:(Type) in + let U1 := constr:(Type) in + let unif := constr:(U0 : U1) in + exact (U0 -> U1). + Defined. + + Definition Lift : lift_type := fun A => A. +End lift. + +Goal forall (A : Type) (x y : A), @paths A x y -> @paths (Lift A) x y. +intros A x y p. +compute in *. +Fail exact p. (* Toplevel input, characters 21-22: +Error: +In environment +A : Type (* Top.15 *) +x : A +y : A +p : @paths (* Top.15 *) A x y +The term "p" has type "@paths (* Top.15 *) A x y" +while it is expected to have type "@paths (* Top.18 *) A x y" +(Universe inconsistency: Cannot enforce Top.18 = Top.15 because Top.15 +< Top.18)). *) |