#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
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
