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 [*] :: *.