Is it possible to derive a Traversable instance via another type constructor?

Question

Suppose we have some class Foo such that an instance of Foo f gives us everything necessary to implement Functor f, Foldable f and Traversable f. To avoid overlapping instances, can witness this relationship between Foo and Functor, Foldable, Traversable under a newtype wrapper:

type Foo :: (Type -> Type) -> Constraint
class Foo f
  where
  {- ... -}

type FoonessOf :: (Type -> Type) -> Type -> Type
newtype FoonessOf f a = FoonessOf (f a)

instance Foo f => Functor (FoonessOf f)
  where
  fmap = _

instance Foo f => Foldable (FoonessOf f)
  where
  foldMap = _

instance Foo f => Traversable (FoonessOf f)
  where
  traverse = _

Now suppose we have some type constructor:

data Bar a = Bar {- ... -}

such that there is an:

instance Foo Bar
  where
  {- ... -}

We'd like to equip Bar with the instances implied by its "Foo-ness". Since Bar a is Coercible to FoonessOf Bar a, we'd expect to be able to derive the instances via the FoonessOf Bar:

deriving via (FoonessOf Bar) instance Functor Bar
deriving via (FoonessOf Bar) instance Foldable Bar

And this works handily for typeclasses such as Functor and Foldable

Unfortunately when we try to do the same thing with Traversable, things go awry:

[typecheck -Wdeferred-type-errors] [E] • Couldn't match representation of type ‘f1 (Foo Bar a1)’
                           with that of ‘f1 (Bar a1)’
    arising from a use of ‘ghc-prim-0.6.1:GHC.Prim.coerce’
  NB: We cannot know what roles the parameters to ‘f1’ have;
    we must assume that the role is nominal
• In the expression:
      ghc-prim-0.6.1:GHC.Prim.coerce
        @(Foo Bar (f a) -> f (Foo Bar a)) @(Bar (f a) -> f (Bar a))
        (sequenceA @(Foo Bar)) ::
        forall (f :: TYPE ghc-prim-0.6.1:GHC.Types.LiftedRep
                     -> TYPE ghc-prim-0.6.1:GHC.Types.LiftedRep)
               (a :: TYPE ghc-prim-0.6.1:GHC.Types.LiftedRep).
        Applicative f => Bar (f a) -> f (Bar a)
  In an equation for ‘sequenceA’:
      sequenceA
        = ghc-prim-0.6.1:GHC.Prim.coerce
            @(Foo Bar (f a) -> f (Foo Bar a)) @(Bar (f a) -> f (Bar a))
            (sequenceA @(Foo Bar)) ::
            forall (f :: TYPE ghc-prim-0.6.1:GHC.Types.LiftedRep
                         -> TYPE ghc-prim-0.6.1:GHC.Types.LiftedRep)
                   (a :: TYPE ghc-prim-0.6.1:GHC.Types.LiftedRep).
            Applicative f => Bar (f a) -> f (Bar a)
  When typechecking the code for ‘sequenceA’
    in a derived instance for ‘Traversable Bar’:
    To see the code I am typechecking, use -ddump-deriv
  In the instance declaration for ‘Traversable Bar’
——————————————————————————————————————————————————————————————————————————————
...

So the questions I have are:

1. Is it possible to come up with some other scheme for deriving-via the instance Traversable Bar?
2. Is it possible to come up with some modification of the Traversable class that can be derived via a newtype?

Answer 1

I suspect the answer to 1. is: no, the situation cannot be salvaged, and it is impossible to obtain an instance of Traversable using DerivingVia.

---

As far as 2. goes, it's useful to try and reproduce the problem in a simpler context. Consider the following:

-- Remember to turn on ScopedTypeVariables!

data A = A
newtype B = B A

a :: forall f. f A -> f A
a = id

b :: forall f. f B -> f B
b = coerce $ a @f

It seems like this should work, but alas:

[typecheck -Wdeferred-type-errors] [E] • Couldn't match representation of type ‘f A’ with that of ‘f B’
    arising from a use of ‘coerce’
  NB: We cannot know what roles the parameters to ‘f’ have;
    we must assume that the role is nominal
• In the expression: coerce $ a @f
  In an equation for ‘b’: b = coerce $ a @f
• Relevant bindings include
    b :: f B -> f B

---

The problem has to do with the "roles" of type constructors' parameters, and the way role inference works. For our purposes, roles come in two varieties: "representational" and "non-representational". Also for our purposes, the difference between the two can be approximated to the following: a type constructor F :: Type -> Type has a parameter of a "representational" role if there is an instance of Representational F, where:

type Representational :: (Type -> Type) -> Constraint
type Representational f = forall x y. Coercible x y => Coercible (f x) (f y)

Otherwise, the parameter of F is non-representational.

---

The typechecker lets you annotate the roles of type parameters in various places (although strangely enough, not in the kind). Sadly, there is no way to annotate the roles of a higher kinded type variable. What we can do however is just ask for Representational f directly:

b' :: forall f. Representational f => f B -> f B
b' = coerce $ a @f

which now typechecks. This suggests a possible way to tweak the Traversable typeclass to make it derivable via coercions.

---

Now let's look at the type of the Traversable operation sequenceA:

class Traversable t
  where
  sequenceA :: forall f. Applicative f => forall a. t (f a) -> f (t a)
  {- ... -}

NB: There's that pesky forall f again, meaning f is taken to have a type parameter of a nominal role.

What DerivingVia is going to do is attempt to coerce between:

sequenceA @T1 :: forall f. Applicative f => forall a. T1 (f a) -> f (T2 a)

and:

sequenceA @T2 :: forall f. Applicative f => forall a. T2 (f a) -> f (T2 a)

Despite T1 (FoonessOf Bar) and T2 (Bar) being "parametrically" coercible, this coercion will fail, because the coercion of the entire operation will decompose eventually to the coercion the typechecker complained about:

Couldn't match representation of type
‘f1 (Foo Bar a1)’
with that of
‘f1 (Bar a1)’

This doesn't work because of f's parameter being considered to have a nominal role, as we discussed.

As with our simplified example above, the fix is straightforward: just ask for Representational f:

type Traversable' :: (Type -> Type) -> Constraint
class Traversable' t
  where
  traverse :: (Representational f, Applicative f) => (a -> f b) -> t (f a) -> f (t b)

And now at last we can derive an instance of Traversable' via the FoonessOf Bar:

instance Foo f => Traversable' (FoonessOf f)
  where
  traverse = _

deriving via (FoonessOf Bar) instance Traversable' Bar