types S, T

type Binary := S * S -> T

var s : Type

type MyPred s := s ->? Unit

type MyAlias t := t ->? Unit

type a1 a b := a -> b -> Unit

type a1 a b := a -> b -> Unit

type a1 a b := a -> b -> Unit

type a2 a b := a -> Unit

type a3 a a := a -> Unit

type a4 a a := a -> Unit

type a5 a

type

type a6 a

type a7 a := a6 a -> Unit

type

type a2 : Type -> Type

types

Binary : Type;

MyAlias : Type -> Type;

MyPred : Type -> Type;

S : Type;

T : Type;

a1 : Type -> Type -> Type;

a2 : Type -> Type -> Type;

a3 : Type -> Type -> Type;

a4 : Type -> Type -> Type;

a5 : Type -> Type;

a6 : Type -> Type;

a7 : Type -> Type

types

Binary := S * S -> T;

MyAlias := \ t : Type . t ->? Unit;

MyPred := \ s : Type . s ->? Unit;

a1 := \ a : Type . \ b : Type . a -> b -> Unit;

a2 := \ a : Type . \ b : Type . a -> Unit;

a3 := \ a : Type . \ a : Type . a -> Unit;

a4 := \ a : Type . \ a : Type . a -> Unit;

a7 := \ a : Type . a6 a -> Unit

var

s : Type %(var_1)%

### Hint 3.5, is type variable 's'

*** Error 5.14, unknown type variable 't'

*** Error 7.9, unknown type variable 'a'

*** Error 7.11, unknown type variable 'b'

*** Error 8.15, unknown type variable 'a'

*** Error 8.19, unknown type variable 'b'

### Hint 8.6, redeclared type 'a1'

*** Error 9.9, unknown type variable 'a'

*** Error 9.16, unknown type variable 'b'

### Hint 9.6, redeclared type 'a1'

*** Error 11.15, unknown type variable 'a'

*** Error 11.19, unknown type variable 'b'

*** Error 13.15, unknown type variable 'a'

*** Error 13.15, duplicates at '(13,19)' for 'a'

*** Error 15.9, unknown type variable 'a'

*** Error 15.9, duplicates at '(15,11)' for 'a'

*** Error 17.9, unknown type variable 'a'

*** Error 19.9, unknown type variable 'a'

*** Error 19.14-19.22,

illegal recursive type synonym 'a5 a -> Unit'

*** Error 21.9, unknown type variable 'a'

*** Error 23.9, unknown type variable 'a'

*** Error 25.9, unknown type variable 'a'

*** Error 23.9-25.22, illegal recursive type synonym 'a7 a -> Unit'

*** Error 27.6,

incompatible kind of: a2

expected: Type -> Type -> Type

found: Type -> Type