<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">Hi all,<div><br></div><div>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.</div><div><br></div><div>Consider this module:</div><div><br></div><div><div>> {-# LANGUAGE PolyKinds #-}</div><div>> </div><div>> module Test where</div><div>> </div><div>> data Proxy t = ProxyC</div><div>> </div><div>> test :: Proxy '[Int, Bool]</div><div>> test = ProxyC -- doesn't compile</div><div>> -- test = undefined -- compiles</div></div><div><br></div><div>Under ghc-7.4.0.20111219, this fails to compile, with error message</div><div><br></div><div>> /tmp/test3/Test.hs:8:8:</div><div>> Couldn't match kind `BOX' against `*'</div><div>> Kind incompatibility when matching types:</div><div>> k0 :: BOX</div><div>> [*] :: *</div><div>> In the expression: ProxyC</div><div>> In an equation for `test': test = ProxyC</div><div><br></div><div>I think GHC is wrong in flagging an error here.</div><div><br></div><div>Here's how I understand it. The type constructor Proxy has kind</div><div><br></div><div>> Proxy :: forall (k :: BOX). k -> *</div><div><br></div><div>The value constructor ProxyC has type</div><div><br></div><div>> ProxyC :: forall (k :: BOX). forall (t :: k). Proxy t</div><div><br></div><div>The type '[Int, Bool] has kind</div><div><br></div><div>> '[Int, Bool] :: [*]</div><div><br></div><div>But what is the sort of [*]? The GHC manual (<a href="http://www.haskell.org/ghc/dist/stable/docs/html/users_guide/kind-polymorphism-and-promotion.html">http://www.haskell.org/ghc/dist/stable/docs/html/users_guide/kind-polymorphism-and-promotion.html</a>) says "all kinds have sort BOX", and so we should have</div><div><br></div><div>> [*] :: BOX (1)</div><div><br></div><div>However, the error message above seems to suggest that</div><div><br></div><div>> [*] :: * (2)</div><div><br></div><div>which disagrees with (1).</div><div><br></div><div>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.</div><div><br></div><div>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?</div><div><br></div><div>Cheers,</div><div>Reiner</div><div><br></div><div><br></div><div><br></div></body></html>