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.

[simonpj]

I'm on this. When fixed I get this message for the Maybe instance:

T6118.hs:20:3:
    Variable occurs more often than in instance head
      in the type family application: Demote k (Any k)
    (Use -XUndecidableInstances to permit this)

This is because of the conservative termination-checking rules for type functions. These rules could perhaps be loosened a bit to account for kind polymorphism, but I'm not quite sure how they should be loosened.

[simonpj@…]

commit 6a8b4290f002cbe042199116ae2d71955dc544a1

Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Tue May 22 15:14:48 2012 +0100

    Fix scoping of kind variables in instance declarations
    
    Fixes Trac #6118

 compiler/hsSyn/HsTypes.lhs   |   29 +++++++++++++++++---------
 compiler/rename/RnBinds.lhs  |    2 +-
 compiler/rename/RnSource.lhs |   46 +++++++++++++++++++++++++++--------------
 3 files changed, 50 insertions(+), 27 deletions(-)

[simonpj]

OK I've fixed the bug. But I did have to add -XUndecidableInstances to make the type instances go through. Less conservative termination tests welcomed. Anything involving kind polymorphism is going to involve multiple occurrences of the kind variable on the RHS. The kind is seldom the index; but it can be.