30 | | because it cannot solve all the necessary constraints, even though the constraint can be solved in the general theory of natural numbers. The most common cause of this is when a programmer writes down a type signature, but GHC infers a slightly different type for the implementation. Now, GHC needs to check that the specified type is compatible with the implementation. If it fails do this, then the program will be rejected. The usual work-around in such situations is to modify the type signature so that it lists explicitly the constraints that GHC could not solve. If you encounter the same problem often, please consider sending an e-mail to the GHC mailing list to let us know. We might be able to teach GHC some more math! |
| 30 | because it cannot solve all the necessary constraints, even though the constraint can be solved in the general theory of natural numbers. The most common cause of this is when a programmer writes down a type signature, but GHC infers a slightly different type for the implementation. Now, GHC needs to check that the specified type is compatible with the implementation. If it fails to do this, then the program will be rejected. The usual work-around in such situations is to modify the type signature so that it lists explicitly the constraints that GHC could not solve. If you encounter the same problem often, please consider sending an e-mail to the GHC mailing list to let us know. We might be able to teach GHC some more math! |
33 | | Basic rules: |
34 | | {{{ |
35 | | instance m <= n -- for concrete numbers m, n with m <= n |
36 | | instance a <= a |
37 | | instance 0 <= a |
38 | | instance (a <= b, b <= c) => (a <= c) |
39 | | instance (a <= a + b) |
40 | | instance (b <= a + b) |
41 | | instance (1 <= b) => (a <= a * b) |
42 | | |
43 | | |
44 | | type instance m + n = mn -- for concrete numbers m, n, mn, with m + n = mn |
45 | | type instance 0 + a = a |
46 | | type instance a + a = 2 * a |
47 | | type instance a + m = m + a -- for a concrete number m |
48 | | |
49 | | |
50 | | type instance m * n = mn -- for concrete numbers m, n, mn, with m * n = mn |
51 | | type instance 0 * a = 0 |
52 | | type instance 1 * a = a |
53 | | type instance a * a = a ^ 2 |
54 | | type instance m * a = a * m -- for concrete numbers m |
55 | | |
56 | | type instance m ^ n = mn -- for concrete numbers m, n, mn, with m ^ n = mn |
57 | | type instance 1 ^ a = 1 |
58 | | type instance a ^ 0 = 1 |
59 | | type instance a ^ 1 = a |
60 | | -- type instance a ^ m = a simplifies to a <= 1 |
61 | | |
62 | | ... (there are more) ... |
63 | | |
64 | | }}} |
65 | | |
66 | | |