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

type tuple1 : b -> a

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

type List : a -> b

var v : m List

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

type s1, r1, t1 < t

type s2 = r2 = t2

type s3 = {x : t . (fun __=__[tuple3 r s t]

: forall a : Type . a_v-1 * a_v-1 ->? Unit)

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

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

a < Type

b < Type

c < Type

d < Type

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

List : a -> b

Logical : Type := Unit ->? Unit

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

Unit : Type

[__] : 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_1)%

r : Type

r1 : Type < t

r2 : Type < (t2, r2, s2)

s : Type

s1 : Type < t

s2 : Type < (t2, r2, s2)

s3

: Type < t

= {x : t . (fun __=__[tuple3 r s t]

: forall a : Type . a_v-1 * a_v-1 ->? Unit)

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

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_v-1 * a_v-1 ->? Unit %(fun)%

__=>__ : ? Unit * ? Unit ->? Unit %(fun)%

__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

__\/__ : ? Unit * ? Unit ->? Unit %(fun)%

__if__ : ? Unit * ? Unit ->? Unit %(fun)%

__when__else__

: forall a : Type . a_v-1 * ? Unit * a_v-1 ->? a_v-1 %(fun)%

bottom : forall a : Type . a_v-1 %(fun)%

def__ : forall a : Type . a_v-1 ->? Unit %(fun)%

false : Unit %(fun)%

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

true : Unit %(fun)%

u : [r] %(var)%

v : m List %(var)%

: {s} %(var)%

x : tuple3 r s t %(var)%

�__ : ? Unit ->? Unit %(fun)%

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

*** Error 12.9, incompatible kind of: tuple3 r s

expected: Type

found: c -> d

*** Error 18.12, unexpected place '__'

*** Error 24.10, incompatible kind of: m

expected: Type

found: (a -> b) -> c

*** Error 26.12, incompatible kind of: tuple1

expected: a -> b

found: b -> a

*** Error 28.12, incompatible kind of: tuple3

expected: a -> b

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

*** Hint 30.5, is type variable 'nt'

*** Error 32.15, incompatible kind of: List

expected: b -> c

found: a -> b

*** Hint 38.17, in type of '(var x : t, var x : t)'

type 't * t' (38.14)

is not unifiable with type 'Unit ->? _var_4_v4 * _var_5_v5'

*** Hint 38.17, in type of '(var x : t, var x : tuple3 r s t)'

type 't * tuple3 r s t' (38.14)

is not unifiable with type 'Unit ->? _var_4_v4 * _var_5_v5'

*** Hint 38.17, in type of '(var x : tuple3 r s t, var x : t)'

type 'tuple3 r s t * t' (11.9)

is not unifiable with type 'Unit ->? _var_4_v4 * _var_5_v5'

*** Hint 38.17, in type of '(var x : tuple3 r s t, var x : tuple3 r s t)'

type 'tuple3 r s t * tuple3 r s t' (11.9)

is not unifiable with type 'Unit ->? _var_4_v4 * _var_5_v5'

*** Hint 38.19, in type of '(fun __=__[_var_3_v3] : forall a : Type . a_v-1 * a_v-1 ->? Unit)

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

typename 't' (11.20)

is not unifiable with type 'tuple3 r s t' (11.9)

*** Hint 38.19, in type of '(fun __=__[_var_3_v3] : forall a : Type . a_v-1 * a_v-1 ->? Unit)

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

typename 't' (11.20)

is not unifiable with type 'tuple3 r s t' (11.9)