f905b9891657dd3eb454d98df87bb0d0cc3796d6Christian Maedertype p a := Pred (Pred a)

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder %% should be correct

395efaeb5bf61bc2bf355c1c029dffa09bc1d1edChristian Maedertype

f905b9891657dd3eb454d98df87bb0d0cc3796d6Christian Maedertype m b := b

7c35990c03276d1e675ea6f4ba38f47081620d77Christian Maeder %%

7c35990c03276d1e675ea6f4ba38f47081620d77Christian Maedertype m b := b

7c35990c03276d1e675ea6f4ba38f47081620d77Christian Maeder %% both contradict

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maedertypes

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maederm : -Type -> Type;

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maederp : +Type -> Type

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maedertypes

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maederm : -Type -> Type := \ b : -Type . b;

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maederp : +Type -> Type := \ a : +Type . Pred (Pred a)

5dca8f36562463e6f691d4d50efe5716d5299801Christian Maeder### Hint 2.27-2.32, wrong covariance of 'a'

5dca8f36562463e6f691d4d50efe5716d5299801Christian Maeder### Hint 2.27-2.32, no kind found for 'a'

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

7c35990c03276d1e675ea6f4ba38f47081620d77Christian Maeder*** Error 4.6, incompatible kind of: m

7c35990c03276d1e675ea6f4ba38f47081620d77Christian Maeder expected: -Type -> Type

7c35990c03276d1e675ea6f4ba38f47081620d77Christian Maeder found: +Type -> Type

7c35990c03276d1e675ea6f4ba38f47081620d77Christian Maeder