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-polymorphi...) 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