blob: 029a0caf7658e6094b8a235b331a868ddece0f5e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
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)). *)
|
