Kind variable generalization problem

[goldfire]

Consider the following tangle of definitions:

{-# LANGUAGE KindSignatures, RankNTypes, PolyKinds, GADTs,
             FlexibleContexts, DataKinds, TypeFamilies #-}

import GHC.Exts

data family Sing (a :: k)
class SingKind (Any :: k) => SingI (s :: k) where
  sing :: Sing s
data SingInstance :: k -> * where 
  SingInstance :: SingI a => SingInstance a
class (b ~ Any) => SingKind (b :: k) where
  singInstance :: forall (a :: k). Sing a -> SingInstance a

When compiling (with 7.5.20120620), I get this error message:

    Kind mis-match
    The first argument of `SingKind' should have kind `k1',
    but `Any' has kind `k'
    In the class declaration for `SingI'

I believe that the code should compile, though I'll admit I'm not 100% convinced.

[simonpj]

Great. Fixed in HEAD, test added. I think this was the commit

Author: Simon Peyton Jones <simonpj@microsoft.com>
 Date:   Tue Jul 10 16:02:03 2012 +0100

     More changes to kind inference for type and class declarations

     These should fix #7024 and #7022, among others.

     The main difficulty was that we were getting occ-name clashes
     between kind and type variables in TyCons, when spat into an
     interface file. The new scheme is to tidy TyCons during the
     conversoin into IfaceSyn, rather than trying to generate them
     pre-tidied, which was the already-unsatisfactory previous plan.

     There is the usual wave of refactorig as well.

  compiler/iface/MkIface.lhs          |  129
 +++++++++++++++++++++-----------
  compiler/typecheck/TcHsType.lhs     |  143
 ++++++++++++++++++++---------------
  compiler/typecheck/TcRnDriver.lhs   |    8 +-
  compiler/typecheck/TcRnTypes.lhs    |   40 +++++++---
  compiler/typecheck/TcRules.lhs      |    3 +-
  compiler/typecheck/TcTyClsDecls.lhs |  110 +++++++++++++-------------
  compiler/types/Kind.lhs             |    9 ++-
  7 files changed, 267 insertions(+), 175 deletions(-)