Simplifier introduces unbound kind variables (caught by -dcore-lint)

I encountered a problem in GHC (happens with 7.6.3 and HEAD), where compiling with optimizations (-O2) results in invalid core (unbound kind variable).

I managed to reduce my example to the following:

{-# LANGUAGE DataKinds, PolyKinds, KindSignatures #-}
{-# LANGUAGE ExistentialQuantification, UndecidableInstances, TypeFamilies #-}

module Test where

-- Kind-level proxies.
data {-kind-} K (a :: *) = KP

-- A type with 1 kind-polymorphic type argument.
data T (n :: k)

-- A type with 1 kind argument.
data F (kp :: K k)

-- A class with 1 kind argument.
class (kp ~ KP) => C (kp :: K k) where
  f :: T (a :: k) -> F kp

-- A type with 1 kind argument.
-- Contains an existentially quantified type-variable of this kind.
data SomeT (kp :: K k) = forall (n :: k). Mk (T n)

-- Show `SomeT` by converting it to `F`, using `C`.
instance (C kp, Show (F kp)) => Show (SomeT kp) where
  show (Mk x) = show (f x) 

I compiled it with these flags:

ghc-stage2 -c -O2 -dcore-lint test.hs

Part of the core-lint complaint is:

*** Core Lint errors : in result of Simplifier ***
<no location info>: Warning:
    In the expression: ww_snF
                         @ n_akd
                         (x_aie
                          `cast` (Sym
                                    (Nth:0
                                       ((forall (a_ai7 :: k_aj7).
                                         <Test.T k_ajF a_ai7> -> Test.F <k_ajF> cobox_dkK)@n_akd))
                                  :: Test.T k_ajF n_akd ~# Test.T k_ajF n_akd))
    @ (k_aj7 :: BOX) is out of scope

Trac metadata

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