Kind variable falls out of scope in instance declaration

Consider the following code:

{-# LANGUAGE PolyKinds, DataKinds, KindSignatures, RankNTypes,
             TypeFamilies, FlexibleInstances, ScopedTypeVariables #-}

import GHC.Exts

data Nat = Zero | Succ Nat
data List a = Nil | Cons a (List a)

class SingE (a :: k) where
  type Demote a :: *

instance SingE (a :: Bool) where
  type Demote a = Bool
instance SingE (a :: Nat) where
  type Demote a = Nat
instance SingE (a :: Maybe k) where
  type Demote a = Maybe (Demote (Any :: k))
instance SingE (a :: List k) where
  type Demote (a :: List k) = List (Demote (Any :: k))

The instance for Maybe fails to compile because k is out of scope: Not in scope: type variable k'`

The instance for List fails to compile because the k in the type family instance is not recognized as the same k in the instance head:

    Kind mis-match
    An enclosing kind signature specified kind `List k1',
    but `a' has kind `List k'
    In the type `(a :: List k)'
    In the type instance declaration for `Demote'
    In the instance declaration for `SingE (a :: List k)'

Note that ScopedTypeVariables is enabled.

This was tested on GHC 7.5.20120519.

Trac metadata

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