blob: d11ae20b8dd733a72b016bfc4a25b40bf2a4834c (
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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
|
Set Printing Universes.
Module AutoYes.
Inductive Box (A:Type) : Type := box : A -> Box A.
About Box.
(* This checks that Box is template poly, see module No for how it fails *)
Universe i j. Constraint i < j.
Definition j_lebox (A:Type@{j}) := Box A.
Definition box_lti A := Box A : Type@{i}.
End AutoYes.
Module AutoNo.
Unset Auto Template Polymorphism.
Inductive Box (A:Type) : Type := box : A -> Box A.
About Box.
Universe i j. Constraint i < j.
Definition j_lebox (A:Type@{j}) := Box A.
Fail Definition box_lti A := Box A : Type@{i}.
End AutoNo.
Module Yes.
#[universes(template)]
Inductive Box@{i} (A:Type@{i}) : Type@{i} := box : A -> Box A.
About Box.
Universe i j. Constraint i < j.
Definition j_lebox (A:Type@{j}) := Box A.
Definition box_lti A := Box A : Type@{i}.
End Yes.
Module No.
#[universes(template=no)]
Inductive Box (A:Type) : Type := box : A -> Box A.
About Box.
Universe i j. Constraint i < j.
Definition j_lebox (A:Type@{j}) := Box A.
Fail Definition box_lti A := Box A : Type@{i}.
End No.
Module DefaultProp.
Inductive identity (A : Type) (a : A) : A -> Type := id_refl : identity A a a.
(* By default template polymorphism does not interact with inductives
which naturally fall in Prop *)
Check (identity nat 0 0 : Prop).
End DefaultProp.
Module ExplicitTemplate.
#[universes(template)]
Inductive identity@{i} (A : Type@{i}) (a : A) : A -> Type@{i} := id_refl : identity A a a.
(* Weird interaction of template polymorphism and inductive types
which naturally fall in Prop: this one is template polymorphic but not on i:
it just lives in any universe *)
Check (identity Type nat nat : Prop).
End ExplicitTemplate.
Polymorphic Definition f@{i} : Type@{i} := nat.
Polymorphic Definition baz@{i} : Type@{i} -> Type@{i} := fun x => x.
Section Foo.
Universe u.
Context (A : Type@{u}).
Inductive Bar :=
| bar : A -> Bar.
Set Universe Minimization ToSet.
Inductive Baz :=
| cbaz : A -> baz Baz -> Baz.
Inductive Baz' :=
| cbaz' : A -> baz@{Set} nat -> Baz'.
(* 2 constructors, at least in Set *)
Inductive Bazset@{v} :=
| cbaz1 : A -> baz@{v} Bazset -> Bazset
| cbaz2 : Bazset.
Eval compute in ltac:(let T := type of A in exact T).
Inductive Foo : Type :=
| foo : A -> f -> Foo.
End Foo.
Set Printing Universes.
(* Cannot fall back to Prop or Set anymore as baz is no longer template-polymorphic *)
Fail Check Bar True : Prop.
Fail Check Bar nat : Set.
About Baz.
Check cbaz True I.
(** Neither can it be Set *)
Fail Check Baz nat : Set.
(** No longer possible for Baz' which contains a type in Set *)
Fail Check Baz' True : Prop.
Fail Check Baz' nat : Set.
Fail Check Bazset True : Prop.
Fail Check Bazset True : Set.
(** We can force the universe instantiated in [baz Bazset] to be [u], so Bazset lives in max(Set, u). *)
Constraint u = Bazset.v.
(** As u is global it is already > Set, so: *)
Definition bazsetex@{i | i < u} : Type@{u} := Bazset Type@{i}.
(* Bazset is closed for universes u = u0, cannot be instantiated with Prop *)
Definition bazseetpar (X : Type@{u}) : Type@{u} := Bazset X.
(** Would otherwise break singleton elimination and extraction. *)
Fail Check Foo True : Prop.
Fail Check Foo True : Set.
Definition foo_proj {A} (f : Foo A) : nat :=
match f with foo _ _ n => n end.
Definition ex : Foo True := foo _ I 0.
Check foo_proj ex.
(** See failure/Template.v for a test of the unsafe Unset Template Check usage *)
Module AutoTemplateTest.
Set Warnings "+auto-template".
Section Foo.
Universe u'.
Context (A : Type@{u'}).
(* Not failing as Bar cannot be made template polymorphic at all *)
Inductive Bar :=
| bar : A -> Bar.
End Foo.
End AutoTemplateTest.
Module TestTemplateAttribute.
Section Foo.
Universe u.
Context (A : Type@{u}).
(* Failing as Bar cannot be made template polymorphic at all *)
Fail #[universes(template)] Inductive Bar :=
| bar : A -> Bar.
End Foo.
End TestTemplateAttribute.
Module SharingWithoutSection.
Inductive Foo A (S:= fun _ => Set : ltac:(let ty := type of A in exact ty))
:= foo : S A -> Foo A.
Fail Check Foo True : Prop.
End SharingWithoutSection.
Module OkNotCovered.
(* Here it happens that box is safe but we don't see it *)
Section S.
Universe u.
Variable A : Type@{u}.
Inductive box (A:Type@{u}) := Box : A -> box A.
Definition B := Set : Type@{u}.
End S.
Fail Check box True : Prop.
End OkNotCovered.
|
