id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc	os	architecture	failure	difficulty	testcase	blockedby	blocking	related
5798	PolyKinds: couldn't match kind `BOX' against `*'	reinerp		"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 {{{[*] :: *}}}.
"	bug	closed	normal	7.4.2	Compiler (Type checker)	7.4.1-rc1	fixed	PolyKinds		Unknown/Multiple	Unknown/Multiple	GHC rejects valid program	Unknown	polykinds/T5798