GHC requires kind-polymorphic signatures on class head

I have the following compiling example:

{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, KindSignatures, 
             MultiParamTypeClasses, PolyKinds, RankNTypes, 
             ScopedTypeVariables, TypeFamilies, TypeOperators #-}

import Data.Proxy
import GHC.Prim

type family CtxOf d (args :: k) :: Constraint

class Run ctx (params :: [k]) where
  runAll :: Proxy params
            -> Proxy ctx
            -> (forall (args :: k) . (CtxOf ctx args) => Proxy args -> Bool)
            -> [Bool]

data BasicCtxD
type instance CtxOf BasicCtxD '(a,b) = (a ~ b)
instance (Run BasicCtxD params, a ~ b) 
  => Run BasicCtxD ( '(a,b) ': params) where
  runAll _ pctx f = (f (Proxy::Proxy '(a,b))) : 
      (runAll (Proxy::Proxy params) pctx f)

But if I move the kind signature of params to its occurrence in the signature of runAll:

class Run ctx params where
  runAll :: Proxy (params :: [k])
            -> Proxy ctx
            -> (forall (args :: k) . (CtxOf ctx args) => Proxy args -> Bool)
            -> [Bool]

I get a couple of nasty (and confusing) compile errors.

Main.hs:20:25:
    Couldn't match kind ‘k1’ with ‘(,) k k’
      ‘k1’ is a rigid type variable bound by
           the type signature for
             runAll :: Proxy ('(a, b) : params)
                       -> Proxy BasicCtxD
                       -> (forall (args :: k1).
                           CtxOf BasicCtxD args =>
                           Proxy args -> Bool)
                       -> [Bool]
           at Main.hs:20:3
    Expected type: Proxy args0
      Actual type: Proxy '(a, b)
    Relevant bindings include
      f :: forall (args :: k1).
           CtxOf BasicCtxD args =>
           Proxy args -> Bool
        (bound at Main.hs:20:17)
      runAll :: Proxy ('(a, b) : params)
                -> Proxy BasicCtxD
                -> (forall (args :: k1).
                    CtxOf BasicCtxD args =>
                    Proxy args -> Bool)
                -> [Bool]
        (bound at Main.hs:20:3)
    In the first argument of ‘f’, namely ‘(Proxy :: Proxy '(a, b))’
    In the first argument of ‘(:)’, namely
      ‘(f (Proxy :: Proxy '(a, b)))’
    In the expression:
      (f (Proxy :: Proxy '(a, b)))
      : (runAll (Proxy :: Proxy params) pctx f)

Main.hs:21:42:
    Could not deduce (k1 ~ (,) k k)
    from the context (CtxOf BasicCtxD args)
      bound by a type expected by the context:
                 CtxOf BasicCtxD args => Proxy args -> Bool
      at Main.hs:21:8-42
      ‘k1’ is a rigid type variable bound by
           the type signature for
             runAll :: Proxy ('(a, b) : params)
                       -> Proxy BasicCtxD
                       -> (forall (args :: k1).
                           CtxOf BasicCtxD args =>
                           Proxy args -> Bool)
                       -> [Bool]
           at Main.hs:20:3
    Expected type: Proxy args -> Bool
      Actual type: Proxy args1 -> Bool
    Relevant bindings include
      f :: forall (args :: k1).
           CtxOf BasicCtxD args =>
           Proxy args -> Bool
        (bound at Main.hs:20:17)
      runAll :: Proxy ('(a, b) : params)
                -> Proxy BasicCtxD
                -> (forall (args :: k1).
                    CtxOf BasicCtxD args =>
                    Proxy args -> Bool)
                -> [Bool]
        (bound at Main.hs:20:3)
    In the third argument of ‘runAll’, namely ‘f’
    In the second argument of ‘(:)’, namely
      ‘(runAll (Proxy :: Proxy params) pctx f)’

It seems to me that the two definitions of the class are equivalent, so it would be nice if they both compiled. It wasn't obvious to me that the kind signature had to go on the class parameter rather than somewhere else.

Trac metadata

Trac field	Value
Version	7.10.2-rc2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture