aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4519.v
blob: ccbc47d20f9b8d1785414d54d9df0ad5a5e7675f (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
Set Universe Polymorphism.
Section foo.
  Universe i.
  Context (foo : Type@{i}) (bar : Type@{i}).
  Definition qux@{i} (baz : Type@{i}) := foo -> bar.
End foo.
Set Printing Universes.
Print qux. (* qux@{Top.42 Top.43} =
fun foo bar _ : Type@{Top.42} => foo -> bar
     : Type@{Top.42} -> Type@{Top.42} -> Type@{Top.42} -> Type@{Top.42}
(* Top.42 Top.43 |=  *)
(* This is wrong; the first two types are equal, but the last one is not *)

qux is universe polymorphic
Argument scopes are [type_scope type_scope type_scope]
 *)
Check qux nat nat nat : Set.
Check qux nat nat Set : Set. (* Error:
The term "qux@{Top.50 Top.51} ?T ?T0 Set" has type "Type@{Top.50}" while it is 
expected to have type "Set"
(universe inconsistency: Cannot enforce Top.50 = Set because Set < Top.50). *)