[GHC] #5798: PolyKinds: couldn't match kind `BOX' against `*'

[GHC]

#5798: PolyKinds: couldn't match kind `BOX' against `*'
---------------------------------------+------------------------------------
 Reporter:  reinerp                    |          Owner:                         
     Type:  bug                        |         Status:  new                    
 Priority:  normal                     |      Component:  Compiler (Type checker)
  Version:  7.4.1-rc1                  |       Keywords:  PolyKinds              
       Os:  Unknown/Multiple           |   Architecture:  Unknown/Multiple       
  Failure:  GHC rejects valid program  |       Testcase:                         
Blockedby:                             |       Blocking:                         
  Related:                             |  
---------------------------------------+------------------------------------
 This module fails to compile:

 {{{
 {-# LANGUAGE PolyKinds #-}

 module Test where

 data Proxy t = ProxyC

 test :: Proxy '[Int, Bool]
 test = ProxyC           -- doesn't compile
 -- test = undefined     -- compiles
 }}}

 The compilation error is
 {{{
 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
 }}}

 However, this module is indeed well-typed, -sorted, and -kinded. The types
 and kinds should be as follows:

 {{{
 Proxy :: forall (k :: BOX). k -> *
 ProxyC :: forall (k :: BOX). forall (t :: k). Proxy t
 '[Int, Bool] :: [*]
 [*] :: BOX
 }}}

 However, the error message suggests that GHC gives {{{[*]}}} the sort
 {{{*}}}, instead of {{{BOX}}}. This is wrong.

 Note that the module compiles if {{{test = ProxyC}}} is replaced with
 {{{test = undefined}}}. So it seems that type-checking of type signature
 sets {{{[*] :: BOX}}}, whereas type-checking of the value expression sets
 {{{[*] :: *}}}.

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/5798>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler