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

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maederm := \ b : -Type . b;

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maederp := \ a : +Type . Pred (Pred a)

93b7bcd9dcf6b2dc4549b5ef261c688d1c4a7dd7Christian Maeder### Hint 2.32, wrong covariance of 'a'

93b7bcd9dcf6b2dc4549b5ef261c688d1c4a7dd7Christian Maeder### Hint 2.32, no kind found for 'a'

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

98b443335df9c77328edb9dbf3ed565535317249Christian Maeder*** Error 4.6,

034f5450bcde2bfe9c94fa52f03c9592f872af5aChristian Maederwrong type of 'm'

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

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