Moving forall with coerce

[David Feuer]

It appears, as far as I can tell, that GHC can't move a forall past an
-> with coerce. I was playing around with the MonadTrans instance for
Codensity, wanting (essentially) to write

lift = coerce (>>=)

This is legal:

instance MonadTrans Codensity where
  lift = frob
frob :: forall m a . Monad m => m a -> Codensity m a
frob = coerce (blah (Mag (>>=)) :: m a -> Mag2 m a)
newtype Mag m a = Mag (forall b . m a -> (a -> m b) -> m b)
newtype Mag2 m a = Mag2 (forall b . (a -> m b) -> m b)
blah :: Mag m a -> m a -> Mag2 m a
blah (Mag p) q = Mag2 (p q)

The problem is that there doesn't *seem* to be a way to implement blah
as a coercion. GHC doesn't recognize that

Mag m a

has the same representation as

m a -> Mag2 m a

The essential difference, as far as I can see, is that the `forall b`
is shifted across `m a ->`. It seems that this really shouldn't be an
issue, because

1. b is not free in `m a`
2. Type lambdas all compile away

Would it be worth trying to extend the Coercible mechanism to deal
with these kinds of situations? Or is there already some way to do it
that I've missed?

David