Opened 5 years ago

Closed 5 years ago

Last modified 18 months ago

#6118 closed bug (fixed)

Kind variable falls out of scope in instance declaration

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.5
Keywords: PolyKinds Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: polykinds/T6118
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


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.

Change History (4)

comment:1 Changed 5 years ago by simonpj

difficulty: Unknown

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

    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.

comment:2 Changed 5 years ago by simonpj@…

commit 6a8b4290f002cbe042199116ae2d71955dc544a1

Author: Simon Peyton Jones <>
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(-)

comment:3 Changed 5 years ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: polykinds/T6118

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.

comment:4 Changed 18 months ago by Iceland_jack


-- twgv.hs:32:3-43: error: …
--     The RHS of an associated type declaration mentions ‘k’
--       All such variables must be bound on the LHS
-- Compilation failed.

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

Still fails, kind annotation needed:

instance SingE (a :: Maybe k) where
  type Demote (a ::Maybe k) = Maybe (Demote (Any :: k))
Note: See TracTickets for help on using tickets.