PolyKinds: couldn't match kind `BOX' against `*'
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 [*] :: *
.
Trac metadata
Trac field | Value |
---|---|
Version | 7.4.1-rc1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |