"Couldn't match kind" with free type variables and PolyKinds

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

Trac metadata

Trac field	Value
Version	7.5
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture