Opened 3 years ago

Closed 3 years ago

Last modified 3 years 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 Rev(s):
Wiki Page:


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
    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 3 years ago by facundo.dominguez

Cc: facundominguez@… added

comment:2 Changed 3 years ago by goldfire

Resolution: invalid
Status: newclosed

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 3 years 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.