[GHC] #7972: Simplifier introduces unbound kind variables (caught by -dcore-lint)

[GHC]

#7972: Simplifier introduces unbound kind variables (caught by -dcore-lint)
-----------------------------+----------------------------------------------
Reporter:  diatchki          |          Owner:                         
    Type:  bug               |         Status:  new                    
Priority:  normal            |      Component:  Compiler (Type checker)
 Version:  7.7               |       Keywords:                         
      Os:  Unknown/Multiple  |   Architecture:  Unknown/Multiple       
 Failure:  None/Unknown      |      Blockedby:                         
Blocking:                    |        Related:                         
-----------------------------+----------------------------------------------
 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 cire-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
 }}}

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