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

__<=>__ : Unit � Unit ->? Unit

__=__ : forall a : Type . a � a ->? Unit

__=>__ : Unit � Unit ->? Unit

__=e=__ : forall a : Type . a � a ->? Unit

__\/__ : Unit � Unit ->? Unit

def__ : forall a : Type . a ->? Unit

if__then__else__ : forall a : Type . Unit � a � a ->? a

not__ : Unit ->? Unit

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

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

(var x : t))

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

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

(var x : (((tuple3)(r))(s))(t)))