var b : Type

var a : Type+

type List(a : Type+)

free type List(a : Type+) ::= Nil |

Cons (head:a; tail:List a)

free type List(a : Type+) ::= Nil |

Cons (head:a; tail:List b)

free type List(a : Type+) ::= Nil |

Cons (head:a; tail:List a b)

free type List(a : Type+) ::= Nil |

Cons (head:a; tail:List (List a))

free type Tree(a : Type+) ::= Leaf |

Branch (head:Tree a; tail:Tree a)

generated {type Tree1(a : Type+) ::= Leaf |

Branch (head:Tree a; tail:Tree1 a)}

type Tree2(a : Type+) ::= Leaf |

Branch (head:Tree a; tail:Tree2 a)

free type even(a : Type+) ::= rek (odd a);

odd(a : Type+) ::= rek (even a)

free type even2(a : Type+) ::= rek (odd2 (odd2 a));

odd2(a : Type+) ::= rek (even2 a)

%% Type Constructors -----------------------------------------------------

List : Type+ -> Type %[free type __ a : Type+ ::=

Nil : -> __]%

Pred : Type -> Type := \ a : Type . a ->? Unit

Tree : Type+ -> Type %[free type __ a : Type+ ::=

Leaf : -> __

Branch : Tree a � Tree a -> __ (head : Tree a)(tail : Tree a)]%

Tree1 : Type+ -> Type %[generated type __ a : Type+ ::=

Leaf : -> __

Branch : Tree a � Tree1 a -> __ (head : Tree a)(tail : Tree1 a)]%

Tree2 : Type+ -> Type %[type __ a : Type+ ::=

Leaf : -> __

Branch : Tree a � Tree2 a -> __ (head : Tree a)(tail : Tree2 a)]%

Unit : Type := Unit

__-->__ : Type- -> Type+ -> Type

__-->?__ : Type- -> Type+ -> Type

__->__ : Type- -> Type+ -> Type

__->?__ : Type- -> Type+ -> Type

__�__ : Type+ -> Type+ -> Type

a : Type+ %(var)%

b : Type %(var)%

even : Type+ -> Type %[free type __ a : Type+ ::=

rek : odd a -> __ (%(even a.rek.sel_[1,1])% :? odd a)]%

even2 : Type+ -> Type %[free type __ a : Type+ ::=]%

odd : Type+ -> Type %[free type __ a : Type+ ::=

rek : even a -> __ (%(odd a.rek.sel_[1,1])% :? even a)]%

odd2 : Type+ -> Type %[free type __ a : Type+ ::=

rek : even2 a -> __ (%(odd2 a.rek.sel_[1,1])% :? even2 a)]%

%% Assumptions -----------------------------------------------------------

%(even a.rek.sel_[1,1])% : forall a : Type+ . even a ->? odd a %(select from even constructed by

rek : forall a : Type+ . odd a -> even a)%

%(odd a.rek.sel_[1,1])% : forall a : Type+ . odd a ->? even a %(select from odd constructed by

rek : forall a : Type+ . even a -> odd a)%

%(odd2 a.rek.sel_[1,1])% : forall a : Type+ . odd2 a ->? even2 a %(select from odd2 constructed by

rek : forall a : Type+ . even2 a -> odd2 a)%

Branch : forall a : Type+ . Tree a �

Tree2 a -> Tree2 a %(construct Tree2)%

: forall a : Type+ . Tree a �

Tree1 a -> Tree1 a %(construct Tree1)%

: forall a : Type+ . Tree a � Tree a -> Tree a %(construct Tree)%

Cons : forall a : Type+ . a � List a -> List a %(construct List)%

Leaf : forall a : Type+ . Tree2 a %(construct Tree2)%

: forall a : Type+ . Tree1 a %(construct Tree1)%

: forall a : Type+ . Tree a %(construct Tree)%

Nil : forall a : Type+ . List a %(construct List)%

__/\__ : Unit � Unit ->? Unit %(Fun)%

__<=>__ : Unit � Unit ->? Unit %(Fun)%

__=__ : forall a : Type . a � a ->? Unit %(Fun)%

__=>__ : Unit � Unit ->? Unit %(Fun)%

__=e=__ : forall a : Type . a � a ->? Unit %(Fun)%

__\/__ : Unit � Unit ->? Unit %(Fun)%

__if__ : Unit � Unit ->? Unit %(Fun)%

__when__else__ : forall a : Type . a � Unit � a ->? a %(Fun)%

def__ : forall a : Type . a ->? Unit %(Fun)%

false : Unit %(Fun)%

head : forall a : Type+ . Tree2 a -> Tree a %(select from Tree2 constructed by

Branch : forall a : Type+ . Tree a �

Tree2 a -> Tree2 a)%

: forall a : Type+ . Tree1 a -> Tree a %(select from Tree1 constructed by

Branch : forall a : Type+ . Tree a �

Tree1 a -> Tree1 a)%

: forall a : Type+ . Tree a -> Tree a %(select from Tree constructed by

Branch : forall a : Type+ . Tree a � Tree a -> Tree a)%

: forall a : Type+ . List a -> a %(select from List constructed by

Cons : forall a : Type+ . a � List a -> List a)%

if__then__else__ : forall a : Type . Unit � a � a ->? a %(Fun)%

not__ : Unit ->? Unit %(Fun)%

rek : forall a : Type+ . even2 a -> odd2 a %(construct odd2)%

: forall a : Type+ . even a -> odd a %(construct odd)%

: forall a : Type+ . odd a -> even a %(construct even)%

tail : forall a : Type+ . Tree2 a -> Tree2 a %(select from Tree2 constructed by

Branch : forall a : Type+ . Tree a �

Tree2 a -> Tree2 a)%

: forall a : Type+ . Tree1 a -> Tree1 a %(select from Tree1 constructed by

Branch : forall a : Type+ . Tree a �

Tree1 a -> Tree1 a)%

: forall a : Type+ . Tree a -> Tree a %(select from Tree constructed by

Branch : forall a : Type+ . Tree a � Tree a -> Tree a)%

: forall a : Type+ . List a -> List a %(select from List constructed by

Cons : forall a : Type+ . a � List a -> List a)%

true : Unit %(Fun)%

%% Diagnostics -----------------------------------------------------------

*** Hint 1.5, is type variable 'b'

*** Hint 2.5, is type variable 'a'

*** Warning 4.11, redeclared type 'List'

*** Error 5.50, unbound type variable(s)

b : Type in 'List b'

*** Warning 5.11, redeclared type 'List'

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

*** Error 6.50, unbound type variable(s)

b : Type in 'List a b'

*** Warning 6.11, redeclared type 'List'

*** Error 7.50, illegal polymorphic recursion

expected: List a

found: List (List a)

*** Warning 7.11, redeclared type 'List'

*** Error 14.27, illegal polymorphic recursion

expected: odd2 a

found: odd2 (odd2 a)