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

type tuple1 : b -> a

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

var

type List : a -> b

var v : m List

var

var

var

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

var

type s1, r1, t1 < t

type s2 = r2 = t2

type s3 : Type := t

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

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

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

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

bottom : forall a : Type . a %(fun)%

def__ : forall a : Type . a ->? 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)%

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

*** Error 38.19, ambiguous typings

'(fun __=__[t] : forall a : Type . a * a ->? Unit)

(var x : t, var x : t)' (38.19)

'(fun __=__[tuple3 r s t] : forall a : Type . a * a ->? Unit)

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