var a : +Type

type p a := Pred (Pred a)

%% should be correct

type m b := b

%%

types

m : -Type -> Type;

p : +Type -> Type

types

m := \ b : -Type . b;

p := \ a : +Type . Pred (Pred a)

var

a : +Type %(var_1)%

### Hint 1.5, is type variable 'a'

### Hint 3.18, wrong covariance of 'a'

### Hint 3.18, no kind found for 'a'

*** Error 3.13-3.18, no kind found for 'Pred a'

*** Error 5.6,

wrong type of 'm'

expected: \ b : -Type . b

found: \ b : +Type . b