GHC doesn't think a type is of kind *, despite having evidence for it
The easiest way to illustrate this bug is this:
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where
import Data.Kind (Type)
blah :: forall (a :: k). k ~ Type => a -> a
blah x = x
$ ghci Foo.hs
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Foo.hs, interpreted )
Foo.hs:8:43: error:
• Expected a type, but ‘a’ has kind ‘k’
• In the type signature:
blah :: forall (a :: k). k ~ Type => a -> a
I find this behavior quite surprising, especially since we have evidence that k ~ Type
in scope!
If the program above looks too contrived, consider a similar program that uses Typeable
. I want to write something like this:
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo where
import Data.Kind (Type)
import Data.Typeable
foo :: forall k (a :: k) proxy. (Typeable k, Typeable a)
=> proxy a -> String
foo _ =
case eqT :: Maybe (k :~: Type) of
Nothing -> "Non-Type kind"
Just Refl ->
case eqT :: Maybe (a :~: Int) of
Nothing -> "Non-Int type"
Just Refl -> "It's an Int!"
This exhibits the same problem. Despite the fact that we pattern-matched on a Refl
of type k :~: Type
, GHC refuses to consider the possibility that a :~: Int
is well kinded, even though (a :: k)
, and we learned from the first Refl
that k ~ Type
!
Trac metadata
Trac field | Value |
---|---|
Version | 8.0.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | goldfire |
Operating system | |
Architecture |