#9017 closed bug (fixed)
Confusing error message with PolyKinds
Reported by: | edsko | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.0.1 |
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: | polykinds/T9017 |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
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 (7)
Changed 2 years ago by simonpj
comment:1 follow-up: ↓ 2 Changed 2 years ago by simonpj
comment:2 in reply to: ↑ 1 Changed 22 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.
comment:3 Changed 9 months ago by Richard Eisenberg <eir@…>
In 67465497/ghc:
comment:4 Changed 9 months ago by goldfire
- Resolution set to fixed
- Status changed from new to closed
- Test Case set to polykinds/T9017
This test case still produces a suboptimal message:
T9017.hs:8:7: error: • Couldn't match kind ‘k’ with ‘*’ ‘k’ is a rigid type variable bound by the type signature for: foo :: forall k k1 (a :: k1 -> k -> *) (b :: k1) (m :: k1 -> k). a b (m b) at T9017.hs:7:8 When matching the kind of ‘a’ • In the expression: arr return In an equation for ‘foo’: foo = arr return • Relevant bindings include foo :: a b (m b) (bound at T9017.hs:8:1) T9017.hs:8:7: error: • Couldn't match kind ‘k1’ with ‘*’ ‘k1’ is a rigid type variable bound by the type signature for: foo :: forall k k1 (a :: k1 -> k -> *) (b :: k1) (m :: k1 -> k). a b (m b) at T9017.hs:7:8 When matching the kind of ‘a’ • In the expression: arr return In an equation for ‘foo’: foo = arr return • Relevant bindings include foo :: a b (m b) (bound at T9017.hs:8:1)
We get two duplicate messages, and it's still quite hard to see what's going on.
Actually, a little more thought tells me the messages aren't quite duplicates: the kind-generalized type signature contains two different kind variables, both of which are distinct from *. With the type signature given, I think it's OK. I'm going to accept this output, but shout if you see a way to improve.
comment:5 Changed 9 months ago by Richard Eisenberg <eir@…>
In 779dfea1/ghc:
comment:6 Changed 8 months ago by thomie
- Milestone set to 8.0.1
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