9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettvar b : Type

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettvar a : +Type

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimbletttype List a

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettfree type List a ::= Nil | Cons (head : a; tail : List a)

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettfree type

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettfree type

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettfree type

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettfree type Tree a ::= Leaf | Branch (head : Tree a; tail : Tree a)

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettgenerated type Tree1 a

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett ::= Leaf | Branch (head : Tree a; tail : Tree1 a)

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimbletttype Tree2 a ::= Leaf | Branch (head : Tree a; tail : Tree2 a)

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettfree types

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimbletteven a ::= rek (odd a);

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettodd a ::= rek (even a)

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblettfree type odd2 a ::= rek (even2 a)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimbletttype DList a := List (List a)

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblettclass Ord

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettvar o : Ord

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimbletttypes List o, DList o : Ord

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettclass

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy GimblettOrd < Type

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimbletttypes

34a4c8c6f861104cdc198282f30fae36cf3858adAndy GimblettDList : +Ord -> Ord;

34a4c8c6f861104cdc198282f30fae36cf3858adAndy GimblettDList : +Type -> Type;

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy GimblettList : +Ord -> Ord;

34a4c8c6f861104cdc198282f30fae36cf3858adAndy GimblettList : +Type -> Type;

34a4c8c6f861104cdc198282f30fae36cf3858adAndy GimblettTree : +Type -> Type;

34a4c8c6f861104cdc198282f30fae36cf3858adAndy GimblettTree1 : +Type -> Type;

34a4c8c6f861104cdc198282f30fae36cf3858adAndy GimblettTree2 : +Type -> Type;

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimbletteven : +Type -> Type;

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimbletteven2 : +Type -> Type;

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettodd : +Type -> Type;

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettodd2 : +Type -> Type

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimbletttype

34a4c8c6f861104cdc198282f30fae36cf3858adAndy GimblettDList := \ a : +Type . List (List a)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettvars

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimbletta : +Type %(var_2)%;

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettb : Type %(var_1)%;

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimbletto : Ord %(var_16)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettop Branch : forall a : Type . Tree a * Tree a -> Tree a

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett %(constructor)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettop Branch : forall a : Type . Tree a * Tree1 a -> Tree1 a

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett %(constructor)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettop Branch : forall a : Type . Tree a * Tree2 a -> Tree2 a

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett %(constructor)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettop Cons : forall a : Type . a * List a -> List a %(constructor)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettop Leaf : forall a : Type . Tree a %(constructor)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettop Leaf : forall a : Type . Tree1 a %(constructor)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettop Leaf : forall a : Type . Tree2 a %(constructor)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettop Nil : forall a : Type . List a %(constructor)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettop head : forall a : Type . List a -> a

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett %(selector of constructor(s)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Cons : forall a : Type . a * List a -> List a)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettop head : forall a : Type . Tree a -> Tree a

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett %(selector of constructor(s)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Branch : forall a : Type . Tree a * Tree a -> Tree a)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettop head : forall a : Type . Tree1 a -> Tree a

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett %(selector of constructor(s)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Branch : forall a : Type . Tree a * Tree1 a -> Tree1 a)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettop head : forall a : Type . Tree2 a -> Tree a

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett %(selector of constructor(s)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Branch : forall a : Type . Tree a * Tree2 a -> Tree2 a)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettop rek : forall a : Type . even a -> odd a %(constructor)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettop rek : forall a : Type . even2 a -> odd2 a %(constructor)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettop rek : forall a : Type . odd a -> even a %(constructor)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettop tail : forall a : Type . List a -> List a

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett %(selector of constructor(s)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Cons : forall a : Type . a * List a -> List a)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettop tail : forall a : Type . Tree a -> Tree a

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett %(selector of constructor(s)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Branch : forall a : Type . Tree a * Tree a -> Tree a)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettop tail : forall a : Type . Tree1 a -> Tree1 a

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett %(selector of constructor(s)

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett Branch : forall a : Type . Tree a * Tree1 a -> Tree1 a)%

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettop tail : forall a : Type . Tree2 a -> Tree2 a

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett %(selector of constructor(s)

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett Branch : forall a : Type . Tree a * Tree2 a -> Tree2 a)%

d40dd10adffcf341489a1310092fcc99de75f225Andy Gimblettforall a : Type; x_1 : a; x_2 : List a

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett. (op head : forall a : Type . List a -> a) (Cons (x_1, x_2)) = x_1

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett %(ga_select_head)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettforall a : Type; x_1 : a; x_2 : List a

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett. (op tail : forall a : Type . List a -> List a) (Cons (x_1, x_2))

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett = x_2 %(ga_select_tail)%

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettfree type List(a : +Type) ::= Cons (head : a; tail : List a) | Nil

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett %(ga_List)%

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettfree type List(a : +Type) ::= Cons (head : a; tail : List a) | Nil

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett %(ga_List)%

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblettfree type List(a : +Type) ::= Cons (head : a; tail : List a) | Nil

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett %(ga_List)%

aa0d5f8be9950e788884f7431cf4cb7bee74788cAndy Gimblettfree type List(a : +Type) ::= Cons (head : a; tail : List a) | Nil

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett %(ga_List)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettforall a : Type; x_1 : Tree a; x_2 : Tree a

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett. (op head : forall a : Type . Tree a -> Tree a)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett ((op Branch : forall a : Type . Tree a * Tree a -> Tree a)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett (x_1, x_2))

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett = x_1 %(ga_select_head)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettforall a : Type; x_1 : Tree a; x_2 : Tree a

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett. (op tail : forall a : Type . Tree a -> Tree a)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett ((op Branch : forall a : Type . Tree a * Tree a -> Tree a)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett (x_1, x_2))

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett = x_2 %(ga_select_tail)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettfree type Tree(a : +Type) ::=

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Branch (head : Tree a; tail : Tree a) | Leaf %(ga_Tree)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettforall a : Type; x_1 : Tree a; x_2 : Tree1 a

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett. (op head : forall a : Type . Tree1 a -> Tree a)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett ((op Branch : forall a : Type . Tree a * Tree1 a -> Tree1 a)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett (x_1, x_2))

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett = x_1 %(ga_select_head)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettforall a : Type; x_1 : Tree a; x_2 : Tree1 a

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett. (op tail : forall a : Type . Tree1 a -> Tree1 a)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett ((op Branch : forall a : Type . Tree a * Tree1 a -> Tree1 a)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett (x_1, x_2))

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett = x_2 %(ga_select_tail)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettgenerated type Tree1(a : +Type) ::=

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Branch (head : Tree a; tail : Tree1 a) | Leaf

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett %(ga_Tree1)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettforall a : Type; x_1 : Tree a; x_2 : Tree2 a

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett. (op head : forall a : Type . Tree2 a -> Tree a)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett ((op Branch : forall a : Type . Tree a * Tree2 a -> Tree2 a)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett (x_1, x_2))

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett = x_1 %(ga_select_head)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettforall a : Type; x_1 : Tree a; x_2 : Tree2 a

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett. (op tail : forall a : Type . Tree2 a -> Tree2 a)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett ((op Branch : forall a : Type . Tree a * Tree2 a -> Tree2 a)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett (x_1, x_2))

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett = x_2 %(ga_select_tail)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimbletttype Tree2(a : +Type) ::=

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett Branch (head : Tree a; tail : Tree2 a) | Leaf %(ga_Tree2)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettfree type even(a : +Type) ::= rek (odd a)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettfree type odd(a : +Type) ::= rek (even a) %(ga_even_odd)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettfree type odd2(a : +Type) ::= rek (even2 a) %(ga_even2_odd2)%

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett### Hint 1.5, is type variable 'b'

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett### Hint 2.5, is type variable 'a'

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett### Hint 4.11, redeclared type 'List'

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett*** Error 5.50-5.55,

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblettunbound type variable(s)

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett b in

34a4c8c6f861104cdc198282f30fae36cf3858adAndy Gimblett'List b'

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett*** Error 6.57, unexpected type argument 'b'

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett*** Error 7.50-7.61,

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblettillegal polymorphic recursion

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett expected: List a

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett found: List (List a)

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett*** Error 14.27-14.38,

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblettillegal polymorphic recursion

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett expected: odd2 a

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett found: odd2 (odd2 a)

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett### Hint 19.5, is type variable 'o'

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett