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)

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

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

*** Error 2.27-2.32, no kind found for 'Pred a'

*** Error 4.6,

wrong type of 'm'

expected: \ b : -Type . b

found: \ b : +Type . b