Opened 2 years ago

Closed 2 years 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 Difficulty: Unknown
Test Case: polykinds/T6118 Blocked By:
Blocking: Related Tickets:

Description

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 (3)

comment:1 Changed 2 years ago by simonpj

  • Difficulty set to Unknown

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.

comment:2 Changed 2 years ago by 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(-)

comment:3 Changed 2 years ago by simonpj

  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case set to 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.

Note: See TracTickets for help on using tickets.