id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,difficulty,testcase,blockedby,blocking,related
6118,Kind variable falls out of scope in instance declaration,goldfire,,"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.",bug,closed,normal,,Compiler,7.5,fixed,PolyKinds,,Unknown/Multiple,Unknown/Multiple,None/Unknown,Unknown,polykinds/T6118,,,