aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/modules/cumpoly.v
blob: 654b86cb440c7397552de432cc4a24ad02342cfb (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
Set Universe Polymorphism.

(** Check that variance subtyping is respected. The signature T is asking for
    invariance, while M provide an irrelevant implementation, which is deemed
    legit.

    There is currently no way to go the other way around, so it's not possible
    to generate a counter-example that should fail with the wrong subtyping.
*)

Module Type T.
Parameter t@{i|Set <= i} : Type@{i}.
Cumulative Inductive I@{i|Set <= i} : Type@{i} := C : t@{i} -> I.
End T.

Module M : T.
Definition t@{i|Set <= i} : Type@{i} := nat.
Cumulative Inductive I@{i|Set <= i} : Type@{i} := C : t@{i} -> I.
End M.