|
Revision 11877, 470 bytes
(checked in by maeder, 5 months ago)
|
|
disallowed explicit pseudo type notation following := (assign)
|
-
Property svn:eol-style set to
native
-
Property svn:keywords set to
Author Date Id Revision
|
| Line | |
|---|
| 1 | var a : +Type |
|---|
| 2 | type p a := Pred (Pred a) |
|---|
| 3 | %% should be correct |
|---|
| 4 | type m b := b |
|---|
| 5 | %% |
|---|
| 6 | types |
|---|
| 7 | m : -Type -> Type; |
|---|
| 8 | p : +Type -> Type |
|---|
| 9 | types |
|---|
| 10 | m := \ b : -Type . b; |
|---|
| 11 | p := \ a : +Type . Pred (Pred a) |
|---|
| 12 | var |
|---|
| 13 | a : +Type %(var_1)% |
|---|
| 14 | ### Hint 1.5, is type variable 'a' |
|---|
| 15 | ### Hint 3.18, wrong covariance of 'a' |
|---|
| 16 | ### Hint 3.18, no kind found for 'a' |
|---|
| 17 | *** Error 3.13-3.18, no kind found for 'Pred a' |
|---|
| 18 | *** Error 5.6, |
|---|
| 19 | wrong type of 'm' |
|---|
| 20 | expected: \ b : -Type . b |
|---|
| 21 | found: \ b : +Type . b |
|---|