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
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
var b : Type
var a : +Type
type List a
free type List a ::= Nil | Cons (head : a; tail : List a)
free type
free type
free type
free type Tree a ::= Leaf | Branch (head : Tree a; tail : Tree a)
generated type Tree1 a
::= Leaf | Branch (head : Tree a; tail : Tree1 a)
type Tree2 a ::= Leaf | Branch (head : Tree a; tail : Tree2 a)
free types
even a ::= rek (odd a);
odd a ::= rek (even a)
free type odd2 a ::= rek (even2 a)
type DList a := List (List a)
class Ord
var o : Ord
types List o, DList o : Ord
class
Ord < Type
types
DList : +Ord -> Ord;
DList : +Type -> Type;
List : +Ord -> Ord;
List : +Type -> Type;
Tree : +Type -> Type;
Tree1 : +Type -> Type;
Tree2 : +Type -> Type;
even : +Type -> Type;
even2 : +Type -> Type;
odd : +Type -> Type;
odd2 : +Type -> Type
type
DList (a : +Type) := List (List a)
vars
a : +Type %(var_2)%;
b : Type %(var_1)%;
o : Ord %(var_16)%
op Branch : forall a : Type . Tree a * Tree a -> Tree a
%(constructor)%
op Branch : forall a : Type . Tree a * Tree1 a -> Tree1 a
%(constructor)%
op Branch : forall a : Type . Tree a * Tree2 a -> Tree2 a
%(constructor)%
op Cons : forall a : Type . a * List a -> List a %(constructor)%
op Leaf : forall a : Type . Tree a %(constructor)%
op Leaf : forall a : Type . Tree1 a %(constructor)%
op Leaf : forall a : Type . Tree2 a %(constructor)%
op Nil : forall a : Type . List a %(constructor)%
op head : forall a : Type . List a -> a
%(selector of constructor(s)
Cons : forall a : Type . a * List a -> List a)%
op head : forall a : Type . Tree a -> Tree a
%(selector of constructor(s)
Branch : forall a : Type . Tree a * Tree a -> Tree a)%
op head : forall a : Type . Tree1 a -> Tree a
%(selector of constructor(s)
Branch : forall a : Type . Tree a * Tree1 a -> Tree1 a)%
op head : forall a : Type . Tree2 a -> Tree a
%(selector of constructor(s)
Branch : forall a : Type . Tree a * Tree2 a -> Tree2 a)%
op rek : forall a : Type . even a -> odd a %(constructor)%
op rek : forall a : Type . even2 a -> odd2 a %(constructor)%
op rek : forall a : Type . odd a -> even a %(constructor)%
op tail : forall a : Type . List a -> List a
%(selector of constructor(s)
Cons : forall a : Type . a * List a -> List a)%
op tail : forall a : Type . Tree a -> Tree a
%(selector of constructor(s)
Branch : forall a : Type . Tree a * Tree a -> Tree a)%
op tail : forall a : Type . Tree1 a -> Tree1 a
%(selector of constructor(s)
Branch : forall a : Type . Tree a * Tree1 a -> Tree1 a)%
op tail : forall a : Type . Tree2 a -> Tree2 a
%(selector of constructor(s)
Branch : forall a : Type . Tree a * Tree2 a -> Tree2 a)%
forall a : Type; x_1 : a; x_2 : List a
. (op head : forall a : Type . List a -> a) (Cons (x_1, x_2)) = x_1
%(ga_select_head)%
forall a : Type; x_1 : a; x_2 : List a
. (op tail : forall a : Type . List a -> List a) (Cons (x_1, x_2))
= x_2 %(ga_select_tail)%
free type List(a : +Type) ::= Cons (head : a; tail : List a) | Nil
%(ga_List)%
free type List(a : +Type) ::= Cons (head : a; tail : List a) | Nil
%(ga_List)%
free type List(a : +Type) ::= Cons (head : a; tail : List a) | Nil
%(ga_List)%
free type List(a : +Type) ::= Cons (head : a; tail : List a) | Nil
%(ga_List)%
forall a : Type; x_1 : Tree a; x_2 : Tree a
. (op head : forall a : Type . Tree a -> Tree a)
((op Branch : forall a : Type . Tree a * Tree a -> Tree a)
(x_1, x_2))
= x_1 %(ga_select_head)%
forall a : Type; x_1 : Tree a; x_2 : Tree a
. (op tail : forall a : Type . Tree a -> Tree a)
((op Branch : forall a : Type . Tree a * Tree a -> Tree a)
(x_1, x_2))
= x_2 %(ga_select_tail)%
free type Tree(a : +Type) ::=
Branch (head : Tree a; tail : Tree a) | Leaf %(ga_Tree)%
forall a : Type; x_1 : Tree a; x_2 : Tree1 a
. (op head : forall a : Type . Tree1 a -> Tree a)
((op Branch : forall a : Type . Tree a * Tree1 a -> Tree1 a)
(x_1, x_2))
= x_1 %(ga_select_head)%
forall a : Type; x_1 : Tree a; x_2 : Tree1 a
. (op tail : forall a : Type . Tree1 a -> Tree1 a)
((op Branch : forall a : Type . Tree a * Tree1 a -> Tree1 a)
(x_1, x_2))
= x_2 %(ga_select_tail)%
generated type Tree1(a : +Type) ::=
Branch (head : Tree a; tail : Tree1 a) | Leaf
%(ga_Tree1)%
forall a : Type; x_1 : Tree a; x_2 : Tree2 a
. (op head : forall a : Type . Tree2 a -> Tree a)
((op Branch : forall a : Type . Tree a * Tree2 a -> Tree2 a)
(x_1, x_2))
= x_1 %(ga_select_head)%
forall a : Type; x_1 : Tree a; x_2 : Tree2 a
. (op tail : forall a : Type . Tree2 a -> Tree2 a)
((op Branch : forall a : Type . Tree a * Tree2 a -> Tree2 a)
(x_1, x_2))
= x_2 %(ga_select_tail)%
type Tree2(a : +Type) ::=
Branch (head : Tree a; tail : Tree2 a) | Leaf %(ga_Tree2)%
free type even(a : +Type) ::= rek (odd a)
free type odd(a : +Type) ::= rek (even a) %(ga_even_odd)%
free type odd2(a : +Type) ::= rek (even2 a) %(ga_even2_odd2)%
1.5: ### Hint: is type variable 'b'
2.5: ### Hint: is type variable 'a'
4.11-4.14: ### Hint: redeclared type 'List'
5.50-5.55: *** Error:
unbound type variable(s)
b in
'List b'
6.57: *** Error: unexpected type argument 'b'
7.50-7.61: *** Error:
illegal polymorphic recursion
expected: List a
found: List (List a)
14.27-14.38: *** Error:
illegal polymorphic recursion
expected: odd2 a
found: odd2 (odd2 a)
19.5: ### Hint: is type variable 'o'