var a : +Type

type p a := Pred (Pred a) %% should be correct

type p a := Pred a %% should be wrong

type m (b : -Type) := b %%

type m (b : +Type) := b %% both contradict