I think I've found a GHC bug in PolyKinds, but I'm not sure if it's a bug, or whether I misunderstand GHC's kind system.

Consider this module:

Under ghc-7.4.0.20111219, this fails to compile, with error message

> /tmp/test3/Test.hs:8:8:

>     Couldn't match kind `BOX' against `*'

>     Kind incompatibility when matching types:

>       k0 :: BOX

>       [*] :: *

>     In the expression: ProxyC

>     In an equation for `test': test = ProxyC

I think GHC is wrong in flagging an error here.

Here's how I understand it. The type constructor Proxy has kind

> Proxy :: forall (k :: BOX). k -> *

The value constructor ProxyC has type

> ProxyC :: forall (k :: BOX). forall (t :: k). Proxy t

The type '[Int, Bool] has kind

> '[Int, Bool] :: [*]

But what is the sort of [*]? The GHC manual (http://www.haskell.org/ghc/dist/stable/docs/html/users_guide/kind-polymorphism-and-promotion.html) says "all kinds have sort BOX", and so we should have

> [*] :: BOX          (1)

However, the error message above seems to suggest that

> [*] :: *            (2)

which disagrees with (1).

To add to the confusion, note that the module compiles if the line "test = ProxyC" is replaced by "test = undefined". So it seems that (1) holds when checking the type signature, but (2) holds when checking the expression.

As I said, I suspect this is simply a GHC bug, but I'm not sure. Should I post a bug report on GHC Trac?

Cheers,

Reiner