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 a2 a b := a -> Unit

type a3 a a := a -> Unit

type a4 a a := a -> Unit

type a5 a

type a6 a

type a7 a := a6 a -> Unit

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 2.16,

no kind found for 'S'

expected: {Cpo}

found: {Type}

### Hint 2.16,

no kind found for 'S'

expected: {Cppo}

found: {Type}

### 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.10, unknown type variable 'a'

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

### Hint 8.6-8.7, redeclared type 'a1'

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

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

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

*** Error 12.10, duplicates at '(12,14)' for 'a'

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

*** Error 14.9, duplicates at '(14,11)' for 'a'

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

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

*** Error 18.14-18.22,

illegal recursive type synonym 'a5 a -> Unit'

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

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

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

*** Error 22.9-24.22, illegal recursive type synonym 'a7 a -> Unit'

*** Error 26.6,

incompatible kind of: a2

expected: Type -> Type -> Type

found: Type -> Type