<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>&gt; {-# LANGUAGE PolyKinds #-}</div><div>&gt;&nbsp;</div><div>&gt; module Test where</div><div>&gt;&nbsp;</div><div>&gt; data Proxy t = ProxyC</div><div>&gt;&nbsp;</div><div>&gt; test :: Proxy '[Int, Bool]</div><div>&gt; test = ProxyC &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; -- doesn't compile</div><div>&gt; -- test = undefined &nbsp; &nbsp; -- compiles</div></div><div><br></div><div>Under&nbsp;ghc-7.4.0.20111219, this fails to compile, with error message</div><div><br></div><div>&gt; /tmp/test3/Test.hs:8:8:</div><div>&gt; &nbsp; &nbsp; Couldn't match kind `BOX' against `*'</div><div>&gt; &nbsp; &nbsp; Kind incompatibility when matching types:</div><div>&gt; &nbsp; &nbsp; &nbsp; k0 :: BOX</div><div>&gt; &nbsp; &nbsp; &nbsp; [*] :: *</div><div>&gt; &nbsp; &nbsp; In the expression: ProxyC</div><div>&gt; &nbsp; &nbsp; 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>&gt; Proxy :: forall (k :: BOX). k -&gt; *</div><div><br></div><div>The value constructor ProxyC has type</div><div><br></div><div>&gt; 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>&gt; '[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>&gt; [*] :: BOX &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;(1)</div><div><br></div><div>However, the error message above seems to suggest that</div><div><br></div><div>&gt; [*] :: * &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;(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>