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

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

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

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

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

a9ac4d0904b5547e612f9a394b24666c1ea02ccbChristian Maeder*** Error 5.6,

034f5450bcde2bfe9c94fa52f03c9592f872af5aChristian Maederwrong type of 'm'

034f5450bcde2bfe9c94fa52f03c9592f872af5aChristian Maeder expected: \ b : -Type . b

034f5450bcde2bfe9c94fa52f03c9592f872af5aChristian Maeder found: \ b : +Type . b