class a, b, c, d < Type

type r, s, t

type [__], {__} : a -> b

var u : [r]; v : {s}

type tuple3 : a -> b -> c -> d

var x : tuple3 r s t

var y : tuple3 r s

type tuple1 : b -> a

type m : (a -> b) -> c

var

type List : a -> b

var v : m List

var o1 : m

var o2 : m tuple1

var o3 : m tuple3

var nt : a -> (b -> c) -> c -> d

var o4 : nt r List s

type s1, r1, t1 < t

type s2 = r2 = t2

type s3

%% Classes ---------------------------------------------------------------

a < Type

b < Type

c < Type

d < Type

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

List : a -> b

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

Unit : Type := Unit

[__] : a -> b

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

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

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

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

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

m : (a -> b) -> c

nt : a -> (b -> c) -> c -> d %(var)%

r : Type

r1 : Type < t

r2 : Type < (t2, r2, s2)

s : Type

s1 : Type < t

s2 : Type < (t2, r2, s2)

s3 : Type

t : Type

t1 : Type < t

t2 : Type < (t2, r2, s2)

tuple1 : b -> a

tuple3 : a -> b -> c -> d

{__} : a -> b

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

__/\__ : 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)%

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

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

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

o1 : m %(var)%

o2 : m tuple1 %(var)%

o3 : m tuple3 %(var)%

o4 : nt r List s %(var)%

u : [r] %(var)%

v : m List %(var)%

: {s} %(var)%

x : tuple3 r s t %(var)%

y : tuple3 r s %(var)%

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

Error (line 12, column 9) incompatible kind of: tuple3 r s

expected: Type

found: c -> d

Error (line 18, column 12) unknown type '__'

Error (line 24, column 10) incompatible kind of: m

expected: Type

found: (a -> b) -> c

Error (line 26, column 12) incompatible kind of: tuple1

expected: a -> b

found: b -> a

Error (line 28, column 12) incompatible kind of: tuple3

expected: a -> b

found: a -> b -> c -> d

Hint (line 30, column 5) is type variable 'nt'

Error (line 32, column 15) incompatible kind of: List

expected: b -> c

found: a -> b

Hint (line 11, column 9) type 't' is not unifiable with 'tuple3 r s t'

Hint (line 11, column 9) type 't' is not unifiable with 'tuple3 r s t'

Error (line 38, column 19) ambiguous typings

(fun __=__ : forall a : Type . a � a ->? Unit) ((var x : t),

(var x : t))

(fun __=__ : forall a : Type . a �

a ->? Unit) ((var x : tuple3 r s t), (var x : tuple3 r s t))