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