Opened 17 months ago
Last modified 10 months ago
#9017 new bug
Confusing error message with PolyKinds
Reported by: | edsko | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 7.8.2 |
Keywords: | Cc: | goldfire | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Revisions: |
Description
Consider the following example code:
import Control.Arrow foo :: a b (m b) foo = arr return
if we typecheck this we rightly get two errors about missing instances (Arrow a, Monad m). However, if we enable PolyKinds we get the following error message:
T.hs:4:7: Kind incompatibility when matching types: a0 :: * -> * -> * a :: k1 -> k -> * Expected type: a b (m b) Actual type: a0 b0 (m0 b0) Relevant bindings include foo :: a b (m b) (bound at T.hs:4:1) In the expression: arr return In an equation for ‘foo’: foo = arr return
I can sort of see where this is coming from if I think really hard :), so perhaps it's not a bug per se, but it's definitely confusing; and it's a pity that a type error (forgotten type qualifier) is reported as a kind error.
Attachments (1)
Change History (3)
Changed 16 months ago by simonpj
comment:1 follow-up: ↓ 2 Changed 16 months ago by simonpj
comment:2 in reply to: ↑ 1 Changed 10 months ago by thomie
- Cc goldfire added
- Component changed from Compiler to Compiler (Type checker)
I think it'd better to wait for Richard's upcoming work in which he gives us full-on kind equalities. Now we can use the kind equality to solve the type equality and all will be well.
I agree that this is bad. We really want more information about what goes wrong with the kind equality.
At the moment, when we get a kind-incompatible type equality, such as a:k ~ b:*, we generate a "derived" kind equality k ~ *. In this case k is a skolem constant, so the constraint is insoluble. But derived constraints are discarded before error message generation (for good reason) so we only see the type-equality problem.
We could instead generate a "wanted" kind equality; that would not be discarded, and we'd get a better error message:
Could still do with improvement (the foralls in the "bound by" message are invisible), but better.
Sadly, a new wanted constraint should be used to solve the constraint that gave rise to it, otherwise we generate the same wanted constraint many times. And that is what happens here: we get two copies of the same error messages.
With some faff we could elimate the dup, but I think it'd better to wait for Richard's upcoming work in which he gives us full-on kind equalities. Now we can use the kind equality to solve the type equality and all will be well.
Meanwhile I attach my diff.
Simon