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

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

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

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

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

5.6: *** Error:

wrong type of 'm'

expected: \ b : -Type . b

found: \ b : +Type . b