8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovavars a, b : Type

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovagenerated type Set a ::= empty | add a (Set a)

097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina Sojakovagenerated type Sys b ::= node b (Set (Sys b))

097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina Sojakovatype Nat

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovavar a : Type

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovagenerated type CTree a ::= leaf a | branch (Nat ->? CTree a)

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovafree type L ::= abs (L -> L)

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovafree type Tree a b ::= leaf b | branch (a -> Tree a b)

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovafree type List a ::= nil | cons (a; List a)

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovafree type Tree a b ::= leaf a | branch (b -> List (Tree a b))

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovavar c : Type

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaop fold : (a -> c) -> ((b -> List c) -> c) -> Tree a b -> c

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovavars f : a -> c; g : (b -> List c) -> c; x : a;

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova s : b -> List (Tree a b)

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova. fold f g (leaf x) = f x

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova. def fold f g (branch s);

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovatypes

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovaCTree

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova: Type -> Type

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova %[generated type CTree(a : Type) ::=

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova branch (Nat ->? CTree a) | leaf (a)]%;

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovaL : Type %[free type L ::= abs (L -> L)]%;

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovaList

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova: Type -> Type

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova %[free type List(a : Type) ::= cons (a; List a) | nil]%;

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovaNat : Type;

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovaSet

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova: Type -> Type

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova %[generated type Set(a : Type) ::= add (a) (Set a) | empty]%;

097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina SojakovaSys

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova: Type -> Type

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova %[generated type Sys(b : Type) ::= node (b) (Set (Sys b))]%;

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina SojakovaTree

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova: Type -> Type -> Type

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova %[free type Tree(a : Type)(b : Type) ::=

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova branch (b -> List (Tree a b)) | leaf (a)]%

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovavars

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaa : Type %(var_5)%;

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovab : Type %(var_2)%;

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovac : Type %(var_12)%

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaop abs : (L -> L) -> L %(constructor)%

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaop add : forall a : Type . a -> Set a -> Set a %(constructor)%

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaop branch : forall a : Type . (Nat ->? CTree a) -> CTree a

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova %(constructor)%

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovaop branch : forall a : Type; b : Type

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova . (b -> List (Tree a b)) -> Tree a b

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova %(constructor)%

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovaop branch : forall a : Type; b : Type . (a -> Tree a b) -> Tree a b

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova %(constructor)%

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovaop cons : forall a : Type . a * List a -> List a %(constructor)%

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaop empty : forall a : Type . Set a %(constructor)%

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovaop fold : forall b : Type; a : Type; c : Type

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova . (a -> c) -> ((b -> List c) -> c) -> Tree a b -> c

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova %(op)%

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovaop leaf : forall a : Type . a -> CTree a %(constructor)%

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovaop leaf : forall a : Type; b : Type . a -> Tree a b %(constructor)%

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovaop nil : forall a : Type . List a %(constructor)%

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaop node : forall b : Type . b -> Set (Sys b) -> Sys b

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova %(constructor)%

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakovavars

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakovaf : a -> c;

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakovag : (b -> List c) -> c;

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakovas : b -> List (Tree a b);

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakovax : a

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakovagenerated type Set(a : Type) ::= add (a) (Set a) | empty %(ga_Set)%

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovagenerated type Sys(b : Type) ::= node (b) (Set (Sys b)) %(ga_Sys)%

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakovagenerated type CTree(a : Type) ::=

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova branch (Nat ->? CTree a) | leaf (a) %(ga_CTree)%

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakovafree type L ::= abs (L -> L) %(ga_L)%

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovafree type Tree(a : Type)(b : Type) ::=

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova branch (a -> Tree a b) | leaf (b) %(ga_Tree)%

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovafree type List(a : Type) ::= cons (a; List a) | nil %(ga_List)%

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovafree type Tree(a : Type)(b : Type) ::=

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova branch (b -> List (Tree a b)) | leaf (a) %(ga_Tree)%

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova. fold f g ((leaf : a -> Tree a b) x) = f x

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova. def fold f g ((branch : (b -> List (Tree a b)) -> Tree a b) s)

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova### Hint 1.6, is type variable 'a'

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova### Hint 1.8, is type variable 'b'

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova### Hint 6.5, is type variable 'a'

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova### Hint 6.5, rebound type variable 'a'

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova### Warning 15.24, overlapping declaration of 'leaf'

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova### Hint 15.11, redeclared type 'Tree'

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova### Hint 17.5, is type variable 'c'

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova### Hint 20.8, not a class 'a'

### Hint 20.8, not a class 'c'

### Hint 20.20, not a kind '(b -> List c) -> c'

### Hint 20.44, not a class 'a'

### Hint 20.51, not a kind 'b -> List (Tree a b)'

### Hint 21.13, in type of '(op leaf : forall a : Type . a -> CTree a)[_v45_a]'

typename 'CTree' (7.16)

is not unifiable with type 'Tree a' (20.10)

### Hint 22.18, in type of '(op branch :

forall a : Type . (Nat ->? CTree a) -> CTree a)[_v77_a]'

typename 'CTree' (7.16)

is not unifiable with type 'Tree a' (20.10)

### Hint 22.25, in type of '(var s : b -> List (Tree a b))'

typename 'List' (20.58)

is not unifiable with type 'Tree a' (20.10)

### Hint 22.25, untypable term (with type: a -> Tree a b)

's'