diff options
Diffstat (limited to 'test-suite/bugs/closed/4519.v')
-rw-r--r-- | test-suite/bugs/closed/4519.v | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4519.v b/test-suite/bugs/closed/4519.v new file mode 100644 index 00000000..ccbc47d2 --- /dev/null +++ b/test-suite/bugs/closed/4519.v @@ -0,0 +1,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). *)
\ No newline at end of file |