[GHC] #6020: "Couldn't match kind" with free type variables and PolyKinds

[GHC]

#6020: "Couldn't match kind" with free type variables and PolyKinds
---------------------------------------+------------------------------------
 Reporter:  atnnn                      |          Owner:                  
     Type:  feature request            |         Status:  new             
 Priority:  normal                     |      Component:  Compiler        
  Version:  7.5                        |       Keywords:                  
       Os:  Unknown/Multiple           |   Architecture:  Unknown/Multiple
  Failure:  GHC rejects valid program  |       Testcase:                  
Blockedby:                             |       Blocking:                  
  Related:                             |  
---------------------------------------+------------------------------------
 In the following code, I was hoping that GHC could infer the more specific
 kind of the free variable y and the class Id in the head of the instance
 for Test.

 Also, the error message is confusing:

 - It says that 'True has kind k0 (maybe it's an impredicative kind?)

 - It refers to k0 as a type variable

 {{{

 {-# LANGUAGE DataKinds, FunctionalDependencies, FlexibleInstances,
              UndecidableInstances, PolyKinds, KindSignatures,
              ConstraintKinds, FlexibleContexts #-}

 import GHC.Prim (Constraint)

 class Id (a :: k) (b :: k) | a -> b
 instance Id a a

 class Test (x :: a) (y :: a) | x -> y
 instance (Id x y, Id y z) => Test x z

 test :: Test True True => ()
 test = ()
 }}}

 {{{
 >>> test
 <interactive>:54:1:
     Couldn't match kind `k0' with `Bool'
       `k0' is an unknown type variable
     Kind incompatibility when matching types:
       'True :: k0
       'True :: Bool
     When using functional dependencies to combine
       Id k0 a a,
         arising from the dependency `a -> b'
         in the instance declaration at /home/atnnn/code/type-
 prelude/testfoldl.hs:8:10
       Id Bool 'True 'True,
         arising from a use of `test' at <interactive>:54:1-4
     In the expression: test
 }}}

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6020>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler