Невозможно создать тип-полиморфные типы

Question

Следующий код не компилировать:

{-# 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 

с ошибкой

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 

Я подозреваю, что, как ticket я просто поданную, мне просто нужно совать GHC в правильном направлении. Кажется, что GHC считает, что все виды совпадают, но он просто отказывается заменить полиморфный тип args :: (*,*) на '(b0,b0). Другими словами, я думаю, что это своего рода полиморфный эквивалент GHC жалуясь Could not deduce a ~ Int в этом вполне допустимо, например:

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

g = f (3 :: Int) 

Любые предложения?

Answer 1

Благодаря комментариям я смог найти решение с использованием GADT, чтобы скрыть как ограничения, так и переменное количество параметров.

{-# 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 

По существу, типа семья CtxOf стала данные семьи. Идея состоит в том, чтобы сделать каждый экземпляр семейства GADT, содержащий ограничение (ранее определенное семейством типов), а также экзистенциальные типы, которые попали бы в тип pair/triple/etc.