Cannot instantiate kind-polymorphic types

Question

The following code fails to compile:

{-# 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 ctx
            -> Proxy params
            -> (forall (args :: k) . (CtxOf ctx args) => Proxy args -> Bool)
            -> [Bool]

instance Run ctx '[] where
  runAll _ _ _ = []

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 pctx (Proxy::Proxy params) f)

wrap1Arg :: forall a b . (a ~ b) 
  => (Proxy '(a,b) -> Bool) -> Proxy '(a,b) -> Bool
wrap1Arg f = f

map1Arg :: (forall a (b :: k) . (a ~ b) => Proxy '(a,b) -> Bool) -> [Bool]
map1Arg g = runAll (Proxy::Proxy BasicCtxD) (Proxy::Proxy '[ '(Int,Int)]) $ wrap1Arg g

with the error

Could not deduce ((~) ((,) * *) args '(b0, b0))
from the context (CtxOf ((,) * *) BasicCtxD args)
  bound by a type expected by the context:
             CtxOf ((,) * *) BasicCtxD args => Proxy ((,) * *) args -> Bool
  at Main.hs:31:13-86
  ‘args’ is a rigid type variable bound by
         a type expected by the context:
           CtxOf ((,) * *) BasicCtxD args => Proxy ((,) * *) args -> Bool
         at Main.hs:31:13
Expected type: Proxy ((,) * *) args -> Bool
  Actual type: Proxy ((,) * *) '(b0, b0) -> Bool
In the second argument of ‘($)’, namely ‘wrap1Arg g’
In the expression:
  runAll (Proxy :: Proxy BasicCtxD) (Proxy :: Proxy '['(Int, Int)]) $ wrap1Arg g

I suspect that, like the ticket I just filed, I just need to poke GHC in the right way. It seems GHC thinks all of the kinds match up, but it's simply refusing to replace the polymorphic type args :: (*,*) with '(b0,b0). Put another way, I think it's the kind-polymorphic equivalent of GHC complaining Could not deduce a ~ Int in this perfectly valid example:

f :: (Num a) => a -> a
f = undefined

g = f (3 :: Int)

Any suggestions?

Answer 1

Thanks to the comments, I was able to figure out a solution using GADTs to hide both the constraints and the variable number of parameters.

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

import Data.Proxy

data family CtxOf ctx

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

instance Run ctx '[] where
  runAll _ _ = []


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


wrap1Arg :: (forall a (b :: k) . (a ~ b) => Proxy '(a,b) -> Bool) -> CtxOf BasicCtxD -> Bool
wrap1Arg f (BasicCtx p) = f p

map1Arg :: (forall a (b :: k) . (a ~ b) => Proxy '(a,b) -> Bool) -> [Bool]
map1Arg g = runAll (Proxy::Proxy '[ '(Int,Int)]) $ wrap1Arg g

Essentially, the type family CtxOf became a data family. The idea is to make each instance of the family a GADT holding a constraint (that was previously defined by the type family), along with the existential types that would have gone in the type pair/triple/etc.