Using Data.Constraint.Forall with equality restrictions

Question

Say I have a function like this:

{-# LANGUAGE ScopedTypeVariables #-}

class C a where

foo :: forall f a b. (C (f a), C (f b)) => f a -> f b
foo = _

Now, if I wanted to move the area aand bto the right of the type of restrictions typeclass in the type foo(for example, because I want to use foofor the implementation of the method typeclass, to be polymorphic in aand b), it can be done with a bit of work with Data.Constraint.Forall:

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ConstraintKinds, TypeOperators #-}
import Data.Constraint
import Data.Constraint.Forall

foo' :: forall f. (ForallF C f) => forall a b. f a -> f b
foo' = helper
  where
    helper :: forall a b. f a -> f b
    helper = case (instF :: ForallF C f :- C (f a)) of
        Sub Dict -> case (instF :: ForallF C f :- C (f b)) of
            Sub Dict -> foo

Now, my question is, suppose I change my function to something related to types:

{-# LANGUAGE TypeFamilies, ScopedTypeVariables #-}

type family F a :: * -> *

bar :: forall f g a b. (F (f a) ~ g a, F (f b) ~ g b) => f a -> f b
bar = _

Is there a way to adapt the technique described above?

Here is what I tried:

{-# LANGUAGE TypeFamilies, ScopedTypeVariables #-}
{-# LANGUAGE ConstraintKinds, TypeOperators #-}
import Data.Constraint
import Data.Constraint.Forall

type F'Eq f g x = F (f x) ~ g x

bar' :: forall f g. (Forall (F'Eq f g)) => forall a b. f a -> f b
bar' = helper
  where
    helper :: forall a b. f a -> f b
    helper = case (inst :: Forall (F'Eq f g) :- F'Eq f g a) of
        Sub Dict -> case (inst :: Forall (F'Eq f g) :- F'Eq f g b) of
            Sub Dict -> bar

But (unsurprisingly) this fails due to the synonym for the unsaturated type:

A type synonym ‘F'Eq’must have 3 arguments, but given 2

In an expression type signature: Forall (F'Eq f g) :- F'Eq f g a

In the expression: (inst :: Forall (F'Eq f g) :- F'Eq f g a)

Answer 1

:

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-}

class (F (f x) ~ g x) => F'Eq f g x
instance (F (f x) ~ g x) => F'Eq f g x

bar' :: forall f g. (Forall (F'Eq f g)) => forall a b. f a -> f b
bar' = helper
  where
    helper :: forall a b. f a -> f b
    helper = case (inst :: Forall (F'Eq f g) :- F'Eq f g a) of
        Sub Dict -> case (inst :: Forall (F'Eq f g) :- F'Eq f g b) of
            Sub Dict -> bar