Opened 14 months ago

Closed 14 months ago

Last modified 14 months ago

#9000 closed bug (invalid)

Kind checking fails when using PolyKinds

Reported by: facundo.dominguez Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.8.2
Keywords: Cc: facundominguez@…
Operating System: Linux Architecture: x86_64 (amd64)
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description

GHC HEAD and earlier versions are failing on the following program:

{-# LANGUAGE PolyKinds #-}
import GHC.Exts(Any)
f = (undefined :: a -> m a) :: Any -> Any Any
../tmp/test-polykinds.hs:3:6:
    Couldn't match kind ‘k1’ with ‘*’
      ‘k1’ is a rigid type variable bound by
           an expression type signature: Any -> Any Any
           at ../tmp/test-polykinds.hs:3:5
    Expected type: Any -> Any Any
      Actual type: Any -> m0 Any
    In the expression: (undefined :: a -> m a) :: Any -> Any Any
    In an equation for ‘f’:
        f = (undefined :: a -> m a) :: Any -> Any Any

Rewriting the program as follows has compilation succeed.

f = (undefined :: a -> m a) `asTypeOf` (undefined :: Any -> Any Any)

And removing the PolyKinds extension also has compilation succeed.

Change History (3)

comment:1 Changed 14 months ago by facundo.dominguez

  • Cc facundominguez@… added

comment:2 Changed 14 months ago by goldfire

  • Resolution set to invalid
  • Status changed from new to closed

This (admittedly bizarre) behavior is (arguably) correct.

Let's look at the kinds of the different pieces. In the type a -> m a, the kinds are fixed. We must have (a :: *) and (m :: * -> *). However, in the type Any -> Any Any, a kind variable comes in. Annotating each Any, we get (Any :: *) -> (Any :: k1 -> *) (Any :: k1). Why are these different? Because the a is repeated in the first type, but every Any is independent in the second.

In the failing version of the code, the outer type signature is more general than the inner one, which is no good.

With asTypeOf, in contrast, GHC unifies the two types, and the kind variable k1 is unified with *, yielding a successful compilation. Although it may seem strange that the :: use case and the asTypeOf use case differ, consider False :: a and False `asTypeOf` (undefined :: a). The first fails and the second succeeds.

Because kinds are implicit by default, this sort of unexpected behavior comes up fairly often. My best suggestion is to use -fprint-explicit-kinds liberally to try to detect when this is happening.

comment:3 Changed 14 months ago by facundo.dominguez

The option -fprint-explicit-kinds improves a lot the error message. Thanks for the good summary.

Note: See TracTickets for help on using tickets.