Generalise kind of ForallT

[Icelandjack]

Can the kind of ForallT be generalised

-- ForallT :: (k4 -> Constraint) -> ((k1 -> k2) -> k3 -> k4) -> Constraint
ForallT :: (k3 -> Constraint) -> (k1 -> k2 -> k3)

I need this to model PipeKit from Faster Coroutine Pipelines

class ForallT Monad pipe => PipeKit pipe where
  input :: pipe i o i
  output :: o -> pipe i o ()
  -- ...

---

Works by removing kind annotations

class    p (t a b)        => R p t a b
instance p (t a b)        => R p t a b

class    Forall (R p t a) => Q p t a
instance Forall (R p t a) => Q p t a

class    Forall (Q p t)   => ForallT p t
instance Forall (Q p t)   => ForallT p t

instT :: forall p t f a. ForallT p t :- p (t f a)
instT = Sub $
  case inst :: Forall (Q p t) :- Q p t f of { Sub Dict ->
  case inst :: Forall (R p t f) :- R p t f a of
    Sub Dict -> Dict }

[RyanGlScott]

It's certainly possible. This patch would suffice:

diff --git a/src/Data/Constraint/Forall.hs b/src/Data/Constraint/Forall.hs                
index 3932f29..f628993 100644                                                             
--- a/src/Data/Constraint/Forall.hs
+++ b/src/Data/Constraint/Forall.hs
@@ -139,11 +139,11 @@ class Forall (R p t a) => Q (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) (a ::
 instance Forall (R p t a) => Q p t a
 
 -- | A representation of the quantified constraint @forall f a. p (t f a)@.
-class Forall (Q p t) => ForallT (p :: k4 -> Constraint) (t :: (k1 -> k2) -> k3 -> k4)
+class Forall (Q p t) => ForallT (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3)
 instance Forall (Q p t) => ForallT p t
 
 -- | Instantiate a quantified @'ForallT' p t@ constraint at types @f@ and @a@.
-instT :: forall (p :: k4 -> Constraint) (t :: (k1 -> k2) -> k3 -> k4) (f :: k1 -> k2) (a :: k3). ForallT p t :- p (t f a)
+instT :: forall (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) (f :: k1) (a :: k2). ForallT p t :- p (t f a)
 instT = Sub $
   case inst :: Forall (Q p t) :- Q p t f of { Sub Dict ->
   case inst :: Forall (R p t f) :- R p t f a of

The question is whether this would be desirable from a kind inference perspective. I'm guessing the current kind signature of ForallT was meant to be reminiscent of monad transformers, and generalizing the kind signature further makes this similarity less clear, especially if you used it incorrectly and saw the resulting error message.

But perhaps if you're using Data.Constraint.ForallT in the first place, you're already well aware of the risk of confusing error messages, and this wouldn't be so bad. :)

[Icelandjack]

It could also be given a different name (the Forall suffix naming scheme remains a mystery to me)

[oerjan]

I initially implemented the new system's ForallT precisely as you suggest, but restricted it again because it broke one of the packages on Hackage. See this pull request.

[sjoerdvisscher]

I'm no longer using ForallT, it didn't really work after all: sjoerdvisscher/free-functors@643cd1d

But of course it might break something else.

I guess Forall2 would be a sensible name for this one? With ForallT being the same with an extra kind annotation?