Haskell - Functor instance for generic polymorphic Algebraic Data Types using recursion-schemes

Question

Problem:

Recently I asked the following question on here, asking how to create a generic map function, and a generic instance of Functor for any arbitrary polymorphic ADT (Algebraic Data Type), like Lists, Trees, etc:

Functor instance for generic polymorphic ADTs in Haskell?

Now, I'm trying to reformulate the above to be compatible with recursion-schemes. I.e, instead of defining the base functor, and then define the type as its fixed point, I want to define the type on one hand, the base functor on the other, and correlate them using the Base family type.

So instead of doing this:

data ListF a b = NilF | ConsF a b
newtype Fix f = Fix { unFix :: f (Fix f) }
type List a = Fix (ListF a)

I want to do this:

data ListF a b = NilF | ConsF a b
data List a = Nil | Cons a (List a)
type instance Base (List a) = ListF a

This way I could leverage the power of the recursion-schemes library, while still being able to define a generic fmap for any of these polymorphic types. Not only that, but it's a more pleasant experience being able to use the "normal" type without it being a type synonym for the fix point.

Attempt:

Initially I thought about having a Bifunctor instance on one hand, and somehow coercing or making it equal to the corresponding Base family instance. At the moment I can only think about using a :~: b from Data.Type.Equality. This is what I've got so far:

{-# LANGUAGE TypeOperators, Rank2Types #-}
import Data.Bifunctor
import Data.Functor.Foldable
import Data.Type.Equality

gmap :: (Bifunctor p, Foldable (f a), Unfoldable (f b)) => 
        (forall x. p x :~: Base (f x)) -> (a -> b) -> f a -> f b
gmap refl f = cata alg
    where
        alg = embed . 
              castWith (apply refl Refl) . 
              bimap f id . 
              castWith (apply (sym refl) Refl)

My problem comes in trying to define an instance of Functor though. I don't know how to specify those specific type constraints when defining the instance. I was thinking about somehow creating a typeclass Equals, and doing something like this:

instance (Bifunctor p, Foldable (f a), Unfoldable (f b), Equals (p a) (Base (f a))) 
    => Functor f where

But I don't know if that's possible, nor if I'm approaching it in the right way (for instance I'm not sure if my definition of gmap is the correct one).

---

For reference, this is the definition of the generic gmap from the original SO question:

gmap :: (Bifunctor f) => (a -> b) -> Fix (f a) -> Fix (f b)
gmap f = unwrapFixBifunctor . cata alg . wrapFixBifunctor
  where
    alg = Fix . bimap f id

    unwrapFixBifunctor :: (Bifunctor f) => Fix (WrappedBifunctor f a) -> Fix (f a)
    unwrapFixBifunctor = Fix . unwrapBifunctor . fmap unwrapFixBifunctor . unFix

    wrapFixBifunctor :: (Bifunctor f) => Fix (f a) -> Fix (WrappedBifunctor f a)
    wrapFixBifunctor = Fix . fmap wrapFixBifunctor . WrapBifunctor . unFix

---

Update:

It was noted that the following definition of gmap would be more general, and would not need any weird application of type-level equality:

gmap :: (Foldable t, Unfoldable d, Bifunctor p, Base d ~ p b, Base t ~ p a)
        => (a -> b) -> t -> d
gmap f = cata ( embed . bimap f id )

However, I still can't find a way to create an instance of Functor that has similar type constraints

Answer 1

With a little help from @kosmikus, I was able to hack together a version that works, as long as you're OK with UndecidableInstances.

The idea is to remove all references to a and b from the context of gmap, by requiring forall x. Foldable (f x) and so on, encoded using the constraints package:

{-# LANGUAGE TypeFamilies, ScopedTypeVariables, TypeOperators, ConstraintKinds #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-}
import Data.Bifunctor
import Data.Functor.Foldable
import Data.Constraint
import Data.Constraint.Forall

-- https://stackoverflow.com/a/28067872/477476
class (p x ~ Base (f x)) => Based p f x
instance (p x ~ Base (f x)) => Based p f x

gmap :: forall p f a b. ( Bifunctor p 
                        , ForallF Foldable f
                        , ForallF Unfoldable f
                        , Forall (Based p f))
     => (a -> b) -> f a -> f b
gmap f = case (instF :: ForallF Foldable f :- Foldable (f a)) of
  Sub Dict -> case (instF :: ForallF Unfoldable f :- Unfoldable (f b)) of
    Sub Dict -> case (inst :: Forall (Based p f) :- Based p f a) of
      Sub Dict -> case (inst :: Forall (Based p f) :- Based p f b) of
        Sub Dict -> cata (embed . bimap f id)

With a and b out of the way, we can turn gmap into fmap:

{-# LANGUAGE UndecidableInstances #-}
instance (Bifunctor p, ForallF Foldable f, ForallF Unfoldable f, Forall (Based p f)) => Functor f where
    fmap = gmap

Edited to add: the trouble with the above instance is that it will match any type at the right kind, as noted by @gonzaw: if you have

data ListT a = NilT
             | ConsT a (ListT a)

data ListF a b = NilF
               | ConsF a b

type instance Base (ListT a) = ListF a

instance Bifunctor ListF where ...
instance Functor (ListF a) where ...
instance Foldable (ListT a) where ...
instance Unfoldable (ListT a) where ...

then you get more than you bargained for, and the generic Functor instance and the one for ListF a(!) overlap.

You can add one more layer of newtype wrappers to get around that: if instead, you have

newtype F f x = F{ unF ::  (f x) }

instance (Bifunctor p, ForallF Foldable f, ForallF Unfoldable f, Forall (Based p f)) => Functor (F f) where
    fmap f = F . gmap f . unF

type ListT' = F ListT

then finally the following typechecks:

*Main> unF . fmap (+1) . F $ ConsT 1 $ ConsT 2 NilT
ConsT 2 (ConsT 3 NilT)

Whether this extra layer of newtype wrapping is acceptable for you is something you'll have to decide.