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

2.16: ### Hint:

no kind found for 'S'

expected: {Cpo}

found: {Type}

2.16: ### Hint:

no kind found for 'S'

expected: {Cppo}

found: {Type}

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

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

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

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

8.10: *** Error: unknown type variable 'a'

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

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

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

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

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

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

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

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

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

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

18.14-18.22: *** Error:

illegal recursive type synonym 'a5 a -> Unit'

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

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

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

22.9-24.22: *** Error:

illegal recursive type synonym 'a7 a -> Unit'

26.6: *** Error:

incompatible kind of: a2

expected: Type -> Type -> Type

found: Type -> Type