aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4375.v
blob: 03af16535bb65186bc3297eb6f0c04009a549ab4 (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


Polymorphic Fixpoint g@{i} (t : Type@{i}) (n : nat) : Type@{i} :=
  t.


Module A.
Polymorphic Fixpoint foo@{i} (t : Type@{i}) (n : nat) : Type@{i} :=
  match n with
  | 0 => t
  | S n => bar t n
  end

with bar (t : Type@{i}) (n : nat) : Type@{i} :=
    match n with
    | 0 => t
    | S n => foo t n
    end.
End A.

Module B.
Polymorphic Fixpoint foo@{i} (t : Type@{i}) (n : nat) : Type@{i} :=
  match n with
  | 0 => t
  | S n => bar t n
  end

with bar@{i} (t : Type@{i}) (n : nat) : Type@{i} :=
    match n with
    | 0 => t
    | S n => foo t n
    end.
End B.

Module C.
Fail Polymorphic Fixpoint foo@{i} (t : Type@{i}) (n : nat) : Type@{i} :=
  match n with
  | 0 => t
  | S n => bar t n
  end

with bar@{j} (t : Type@{j}) (n : nat) : Type@{j} :=
    match n with
    | 0 => t
    | S n => foo t n
    end.
End C.

Module D.
Polymorphic Fixpoint foo@{i j} (t : Type@{i}) (n : nat) : Type@{i} :=
  match n with
  | 0 => t
  | S n => bar t n
  end

with bar@{i j} (t : Type@{j}) (n : nat) : Type@{j} :=
    match n with
    | 0 => t
    | S n => foo t n
    end.
End D.

Module E.
Fail Polymorphic Fixpoint foo@{i j} (t : Type@{i}) (n : nat) : Type@{i} :=
  match n with
  | 0 => t
  | S n => bar t n
  end

with bar@{j i} (t : Type@{j}) (n : nat) : Type@{j} :=
    match n with
    | 0 => t
    | S n => foo t n
    end.
End E.

(*
Polymorphic Fixpoint g@{i} (t : Type@{i}) (n : nat) : Type@{i} :=
  t.

Print g.

Polymorphic Fixpoint a@{i} (t : Type@{i}) (n : nat) : Type@{i} :=
  t
with b@{i} (t : Type@{i}) (n : nat) : Type@{i} :=
  t.

Print a.
Print b.
*)

Polymorphic CoInductive foo@{i} (T : Type@{i}) : Type@{i} :=
| A : foo T -> foo T.

Polymorphic CoFixpoint cg@{i} (t : Type@{i}) : foo@{i} t :=
  @A@{i} t (cg@{i} t).

Print cg.

Polymorphic CoFixpoint ca@{i} (t : Type@{i}) : foo@{i} t :=
  @A@{i} t (@cb@{i} t)
with cb@{i} (t : Type@{i}) : foo@{i} t :=
  @A@{i} t (@ca@{i} t).

Print ca.
Print cb.