classes a, b, c, d

types r : a;

s : a;

s : b;

t : c

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

vars 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 z : m [__]

type List : a -> b

var w : m List

var

var

var

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

var

types s1, r1, t1 < t

types s2 = r2 = t2

type s3 = {x : t . x = x}

classes

a < Type;

b < Type;

c < Type;

d < Type

types

List : a -> b;

[__] : a -> b;

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

r : a;

r1 : c;

r2 : Type;

s : a;

s : b;

s1 : c;

s2 : Type;

s3 : Type;

t : c;

t1 : c;

t2 : Type;

tuple1 : b -> a;

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

{__} : a -> b

types

r1 < t;

s1 < t;

s3 < t;

t1 < t

types

r2 := t2;

s2 := t2

var

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

vars

u : [ r ];

v : { s };

w : m List;

x : tuple3 r s t;

z : m [__]

forall x : t . (x in s3) <=> x = x

7.6: ### Hint: not a kind '[r]'

7.8-7.10: ### Hint: a non-compound list: [r]

7.14: ### Hint: not a kind '{s}'

11.7: ### Hint: not a kind 'tuple3 r s t'

12.7: ### Hint: not a kind 'tuple3 r s'

12.9-12.18: *** Error:

no kind found for 'tuple3 r s'

expected: {Type}

found: {c -> d}

18.7: ### Hint: not a kind 'm [__]'

18.11-18.14: ### Hint: a non-compound list: [__]

22.7: ### Hint: not a kind 'm List'

24.8: ### Hint: not a class 'm'

24.10: *** Error:

no kind found for 'm'

expected: {Type}

found: {(a -> b) -> c}

26.8: ### Hint: not a kind 'm tuple1'

26.12-26.17: ### Hint:

no kind found for 'tuple1'

expected: {a -> b}

found: {b -> a}

26.10-26.12: *** Error: no kind found for 'm tuple1'

28.8: ### Hint: not a kind 'm tuple3'

28.12-28.17: ### Hint:

no kind found for 'tuple3'

expected: {a -> b}

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

28.10-28.12: *** Error: no kind found for 'm tuple3'

30.5-30.6: ### Hint: is type variable 'nt'

32.8: ### Hint: not a kind 'nt r List s'

32.15-32.18: ### Hint:

no kind found for 'List'

expected: {b -> c}

found: {a -> b}

32.10-32.20: *** Error: no kind found for 'nt r List s'

38.12: ### Hint: rebound variable 'x'