Function composition and forall'ed types

Question

Let's say we have some code like this, which typechecks just fine:

{-# LANGUAGE RankNTypes #-}

data Foo a

type A a = forall m. Monad m => Foo a -> m ()
type PA a = forall m. Monad m => Foo a -> m ()
type PPFA a = forall m. Monad m => Foo a -> m ()

_pfa :: PPFA a -> PA a
_pfa = _pfa

_pa :: PA a -> A a
_pa = _pa

_pp :: PPFA a -> A a
_pp x = _pa $ _pfa x

main :: IO ()
main = putStrLn "yay"

We note that _pp x = _pa $ _pfa x is too verbose, and we try to replace it with _pp = _pa . _pfa. Suddenly the code doesn't typecheck anymore, failing with error messages similar to

• Couldn't match type ‘Foo a0 -> m0 ()’ with ‘PA a’
  Expected type: (Foo a0 -> m0 ()) -> Foo a -> m ()
    Actual type: PA a -> A a

I guess this is due to m in the definition of type aliases being forall'd — indeed, replacing m with some exact type fixes the issue. But the question is: why does forall break things in this case?

Bonus points for trying to figure out why replacing dummy recursive definitions of _pfa and _pa with usual _pfa = undefined results in GHC complaining about unification variables and impredicative polymorphism:

• Cannot instantiate unification variable ‘a0’
  with a type involving foralls: PPFA a -> Foo a -> m ()
    GHC doesn't yet support impredicative polymorphism
• In the expression: undefined
  In an equation for ‘_pfa’: _pfa = undefined

Answer 1

Just to be clear, when you write:

_pa :: PA a -> A a

The compiler expands the type synonyms and then moves the quantifiers and constraints upward, like so:

_pa
  :: forall a.
     (forall m1. Monad m1 => Foo a -> m1 ())
  -> (forall m2. Monad m2 => Foo a -> m2 ())

_pa
  :: forall m2 a. (Monad m2)
  => (forall m1. Monad m1 => Foo a -> m1 ())
  -> Foo a -> m2 ()

So _pa has a rank-2 polymorphic type, because it has a forall nested to the left of a function arrow. Same goes for _pfa. They expect polymorphic functions as arguments.

To answer the actual question, I’ll first show you something strange. These both typecheck:

_pp :: PPFA a -> A a
_pp x = _pa $ _pfa x

_pp :: PPFA a -> A a
_pp x = _pa (_pfa x)

This, however, does not:

apply :: (a -> b) -> a -> b
apply f x = f x

_pp :: PPFA a -> A a
_pp x = apply _pa (_pfa x)

Unintuitive, right? This is because the application operator ($) is special-cased in the compiler to allow instantiating its type variables with polymorphic types, in order to support runST $ do { … } rather than runST (do { … }).

Composition (.), however, is not special-cased. So when you call (.) on _pa and _pfa, it instantiates their types first. Thus you end up trying to pass the non-polymorphic result of _pfa, of the type (Foo a0 -> m0 ()) -> Foo a -> m () mentioned in your error message, to the function _pa, but it expects a polymorphic argument of type P a, so you get a unification error.

undefined :: a doesn’t typecheck because it tries to instantiate a with a polymorphic type, an instance of impredicative polymorphism. That’s a hint as to what you should do—the standard way of hiding impredicativity is with a newtype wrapper:

newtype A a = A { unA :: forall m. Monad m => Foo a -> m () }
newtype PA a = PA { unPA :: forall m. Monad m => Foo a -> m () }
newtype PPFA a = PPFA { unPPFA :: forall m. Monad m => Foo a -> m () }

Now this definition compiles without error:

_pp :: PPFA a -> A a
_pp = _pa . _pfa

With the cost that you need to explicitly wrap and unwrap to tell GHC when to abstract and instantiate:

_pa :: PA a -> A a
_pa x = A (unPA x)

Answer 2

Instantiating polymorphic type variables with polymorphic types is called impredicative polymorphism. -- GHC user guide

As the error message indicates, GHC only allows a type variable to be instantiated with a monomorphic, rank 0 type. My guess is that type checking with impredicative polymorphism is trickier to implement than it may seem.