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 defini…

Accepted Answer

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)
```

Function composition and forall'ed types

Solution

Problem