class a, b, c, d

type r, s, t

type [, { : a -> b

var

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

b

c

d

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

List : a -> b

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

Unit : Type := Unit

[ : a -> b

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)%

v : (m)(List) %(var)%

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

y : ((tuple3)(r))(s) %(var)%

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

Error (line 7, column 9) illegal type '[r]'

Error (line 7, column 16) illegal type '{s}'

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

expected: Type -> Type

found: Type

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

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

expected: (Type -> Type) -> Type

found: Type

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

expected: Type -> Type

found: Type -> Type -> Type -> Type

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

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)))