a9ac4d0904b5547e612f9a394b24666c1ea02ccbChristian Maedervar a : +Type

f905b9891657dd3eb454d98df87bb0d0cc3796d6Christian Maedertype p a := Pred (Pred a)

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder %% should be correct

f905b9891657dd3eb454d98df87bb0d0cc3796d6Christian Maedertype m b := b

7c35990c03276d1e675ea6f4ba38f47081620d77Christian Maeder %%

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maedertypes

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maederm : -Type -> Type;

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maederp : +Type -> Type

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maedertypes

a39175891082dc8a598e5630e5558cb08b84ac0aChristian Maederm (b : -Type) := b;

a39175891082dc8a598e5630e5558cb08b84ac0aChristian Maederp (a : +Type) := Pred (Pred a)

a9ac4d0904b5547e612f9a394b24666c1ea02ccbChristian Maedervar

a9ac4d0904b5547e612f9a394b24666c1ea02ccbChristian Maedera : +Type %(var_1)%

3aa7e4492a7e28b37d1a0b23f5bfe2109f87d4d6Christian Maeder1.5: ### Hint: is type variable 'a'

3aa7e4492a7e28b37d1a0b23f5bfe2109f87d4d6Christian Maeder3.18: ### Hint: wrong covariance of 'a'

3aa7e4492a7e28b37d1a0b23f5bfe2109f87d4d6Christian Maeder3.18: ### Hint: no kind found for 'a'

3aa7e4492a7e28b37d1a0b23f5bfe2109f87d4d6Christian Maeder3.13-3.18: *** Error: no kind found for 'Pred a'

5de34eba726f63d1522bf17a857309a6208ce0b5Christian Maeder5.6: *** Error:

5de34eba726f63d1522bf17a857309a6208ce0b5Christian Maederwrong type of 'm'

5de34eba726f63d1522bf17a857309a6208ce0b5Christian Maeder expected: \ b : -Type . b

5de34eba726f63d1522bf17a857309a6208ce0b5Christian Maeder found: \ b : +Type . b