blob: e1206bb37a69508362001750157e91b8c7328777 (
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
|
Class sa (A:Type) := { }.
Record predicate A (sa:sa A) :=
{ pred_fun: A->Prop }.
Record ABC : Type :=
{ abc: Type }.
Record T :=
{ T_abc: ABC }.
(*
sa: forall _ : Type@{Top.179}, Prop
predicate: forall (A : Type@{Top.205}) (_ : sa A), Type@{max(Set+1, Top.205)}
T: Type@{Top.208+1}
ABC: Type@{Top.208+1}
abc: forall _ : ABC, Type@{Top.208}
Top.205 <= Top.179 predicate <= sa.A
Set < Top.208 Set < abc
Set < Top.205 Set < predicate
*)
Definition foo : predicate T (Build_sa T) :=
{| pred_fun:= fun w => True |}.
(* *)
(* Top.208 < Top.205 <--- added by foo *)
(* *)
Check predicate nat (Build_sa nat).
(*
The issue is that the template polymorphic universe of [predicate], Top.205, does not get replaced with the universe of [nat] in the above line.
-Jason Gross
8.5 -- predicate nat (Build_sa nat): Type@{max(Set+1, Top.205)}
8.5 EXPECTED -- predicate nat (Build_sa nat): Type@{Set+1}
8.4pl4 -- predicate nat {| |}: Type (* max(Set, (Set)+1) *)
*)
(* This works in 8.4pl4 and SHOULD work in 8.5 *)
Definition bar : ABC :=
{| abc:= predicate nat (Build_sa nat) |}.
(*
The term "predicate nat (Build_sa nat)" has type
"Type@{max(Set+1, Top.205)}"
while it is expected to have type "Type@{Top.208}"
(universe inconsistency: Cannot enforce Top.205 <=
Top.208 because Top.208 < Top.205).
*)
|
