Instantiation of a rank 2 type fails for type synonyms

[paba]

The instantiation of a rank 2 type with a type containing type synonyms that rearrange or omit type variables fails.

For example, consider the following function:

mapR :: Functor f => (forall a. g a -> b) -> f (g a) -> f b
mapR f t = fmap f t

Now we want to instantiate the type variable g in the above type:

data F a = F a
type G a = F a

mapG :: Functor f =>  (forall a. G a -> b) -> f (G a) -> f b
mapG f t = mapR f t

This works fine. But if we change the definition of the type synonym G to

type G a = F ()

we get the following error message:

/home/paba/code/bug.hs:11:17:
    Could not deduce (a1 ~ ())
    from the context (Functor f)
      bound by the type signature for
                 mapG :: Functor f => (forall a1. G a1 -> b) -> f (G a) -> f b
      at /home/paba/code/bug.hs:11:1-19
      `a1' is a rigid type variable bound by
           a type expected by the context: F a1 -> b
           at /home/paba/code/bug.hs:11:12
    Expected type: F a -> b
      Actual type: G a0 -> b
    In the first argument of `mapR', namely `f'
    In the expression: mapR f t

This only happens for rank 2 types. If we change the type of mapR by removing the quantifier, the instantiation of the type of mapR succeeds.

[kosmikus]

AFAICS, GHC is correct to reject this program. You are trying to pass a function of type

forall a. F () -> b

in a position where

forall a. g a -> b

is expected.

[simonpj]

Ian's right.

Simon