PolyKinds: couldn't match kind `BOX' against `*'

[Reiner Pope]

Hi all,

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:

> {-# LANGUAGE PolyKinds #-}
> 
> module Test where
> 
> data Proxy t = ProxyC
> 
> test :: Proxy '[Int, Bool]
> test = ProxyC           -- doesn't compile
> -- test = undefined     -- compiles

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



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120118/20e34a7d/attachment-0001.htm>