Kind checking fails when using PolyKinds

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.

Trac metadata

Trac field	Value
Version	7.8.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import typechecker labels

Trac metadata

Trac field	Value
CC	→ facundominguez@gmail.com

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.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedInvalid

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

added Pnormal label