[GHC] #13337: GHC doesn't think a type is of kind *, despite having evidence for it

24 Feb 2017

      #13337: GHC doesn't think a type is of kind *, despite having evidence for it
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.2
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The easiest way to illustrate this bug is this:

 {{{#!hs
 {-# 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:

 {{{#!hs
 {-# 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`!

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13337
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler