Opened 12 months ago

Last modified 5 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)

kind-diff (4.9 KB) - added by simonpj 12 months ago.

Download all attachments as: .zip

Change History (3)

Changed 12 months ago by simonpj

comment:1 follow-up: Changed 12 months ago by simonpj

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:

T9017.hs:8:7:
    Couldn't match kind `k1' with `*'
      `k1' is a rigid type variable bound by
           the type signature for foo :: a b (m b) at T9017.hs:7:8
    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 T9017.hs:8:1)
    In the expression: arr return
    In an equation for `foo': foo = arr return

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

comment:2 in reply to: ↑ 1 Changed 5 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.

Note: See TracTickets for help on using tickets.