Opened 2 years ago

Closed 9 months ago

Last modified 8 months ago

#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)

kind-diff (4.9 KB) - added by simonpj 2 years ago.

Download all attachments as: .zip

Change History (7)

Changed 2 years ago by simonpj

comment:1 follow-up: Changed 2 years 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 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:

Add kind equalities to GHC.

This implements the ideas originally put forward in
"System FC with Explicit Kind Equality" (ICFP'13).

There are several noteworthy changes with this patch:
 * We now have casts in types. These change the kind
   of a type. See new constructor `CastTy`.

 * All types and all constructors can be promoted.
   This includes GADT constructors. GADT pattern matches
   take place in type family equations. In Core,
   types can now be applied to coercions via the
   `CoercionTy` constructor.

 * Coercions can now be heterogeneous, relating types
   of different kinds. A coercion proving `t1 :: k1 ~ t2 :: k2`
   proves both that `t1` and `t2` are the same and also that
   `k1` and `k2` are the same.

 * The `Coercion` type has been significantly enhanced.
   The documentation in `docs/core-spec/core-spec.pdf` reflects
   the new reality.

 * The type of `*` is now `*`. No more `BOX`.

 * Users can write explicit kind variables in their code,
   anywhere they can write type variables. For backward compatibility,
   automatic inference of kind-variable binding is still permitted.

 * The new extension `TypeInType` turns on the new user-facing
   features.

 * Type families and synonyms are now promoted to kinds. This causes
   trouble with parsing `*`, leading to the somewhat awkward new
   `HsAppsTy` constructor for `HsType`. This is dispatched with in
   the renamer, where the kind `*` can be told apart from a
   type-level multiplication operator. Without `-XTypeInType` the
   old behavior persists. With `-XTypeInType`, you need to import
   `Data.Kind` to get `*`, also known as `Type`.

 * The kind-checking algorithms in TcHsType have been significantly
   rewritten to allow for enhanced kinds.

 * The new features are still quite experimental and may be in flux.

 * TODO: Several open tickets: #11195, #11196, #11197, #11198, #11203.

 * TODO: Update user manual.

Tickets addressed: #9017, #9173, #7961, #10524, #8566, #11142.
Updates Haddock submodule.

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:

Test #9017 in polykinds/T9017

comment:6 Changed 8 months ago by thomie

  • Milestone set to 8.0.1
Note: See TracTickets for help on using tickets.