Consider the following program:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Bug where

import Data.Coerce
import Data.Kind

type Representational1 m = (forall a b. Coercible a b => Coercible (m a) (m b) :: Constraint)

class Representational1 f => Functor' f where
  fmap' :: (a -> b) -> f a -> f b

class Functor' f => Applicative' f where
  pure'  :: a -> f a
  (<*>@) :: f (a -> b) -> f a -> f b

class Functor' t => Traversable' t where
  traverse' :: Applicative' f => (a -> f b) -> t a -> f (t b)

-- Typechecks
newtype T1 m a = MkT1 (m a) deriving Functor'
instance Traversable' m => Traversable' (T1 m) where
  traverse' :: forall f a b. (Applicative' f) => (a -> f b) -> T1 m a -> f (T1 m b)
  traverse' = coerce @((a -> f b) ->    m a -> f    (m b))
                     @((a -> f b) -> T1 m a -> f (T1 m b))
                     traverse'

-- Doesn't typecheck
newtype T2 m a = MkT2 (m a) deriving Functor'
instance Traversable' m => Traversable' (T2 m) where
  traverse' = coerce @(forall f a b. Applicative' f => (a -> f b) ->    m a -> f    (m b))
                     @(forall f a b. Applicative' f => (a -> f b) -> T2 m a -> f (T2 m b))
                     traverse'

This defines a variant of Functor that has forall a b. Coercible a b. Coercible (m a) (m b) as a superclass, and also defines versions of Applicative and Traversable that use this Functor variant. This is towards the ultimate goal of defining Traversable' à la GeneralizedNewtypeDeriving.

This attempt (using InstanceSigs) typechecks:

newtype T1 m a = MkT1 (m a) deriving Functor'
instance Traversable' m => Traversable' (T1 m) where
  traverse' :: forall f a b. (Applicative' f) => (a -> f b) -> T1 m a -> f (T1 m b)
  traverse' = coerce @((a -> f b) ->    m a -> f    (m b))
                     @((a -> f b) -> T1 m a -> f (T1 m b))
                     traverse'

However, this version (which is closer to what GeneralizedNewtypeDeriving would actually create) does //not// typecheck:

newtype T2 m a = MkT2 (m a) deriving Functor'
instance Traversable' m => Traversable' (T2 m) where
  traverse' = coerce @(forall f a b. Applicative' f => (a -> f b) ->    m a -> f    (m b))
                     @(forall f a b. Applicative' f => (a -> f b) -> T2 m a -> f (T2 m b))
                     traverse'

$ ghc-cq/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:38:15: error:
    • Couldn't match representation of type ‘f1 (m b1)’
                               with that of ‘f1 (T2 m b1)’
        arising from a use of ‘coerce’
      NB: We cannot know what roles the parameters to ‘f1’ have;
        we must assume that the role is nominal
    • In the expression:
        coerce
          @(forall f a b. Applicative' f => (a -> f b) -> m a -> f (m b))
          @(forall f a b.
            Applicative' f => (a -> f b) -> T2 m a -> f (T2 m b))
          traverse'
      In an equation for ‘traverse'’:
          traverse'
            = coerce
                @(forall f a b. Applicative' f => (a -> f b) -> m a -> f (m b))
                @(forall f a b.
                  Applicative' f => (a -> f b) -> T2 m a -> f (T2 m b))
                traverse'
      In the instance declaration for ‘Traversable' (T2 m)’
    • Relevant bindings include
        traverse' :: (a -> f b) -> T2 m a -> f (T2 m b)
          (bound at Bug.hs:38:3)
   |
38 |   traverse' = coerce @(forall f a b. Applicative' f => (a -> f b) ->    m a -> f    (m b))
   |               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

Shouldn't it, though? These instance declarations out to be equivalent (morally, at least).