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?
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.