RankNTypes and the dot operator

Question

When I use RankNTypes, it seems that (.) operator doesn't work well. Where is this limitation documented?

{-# LANGUAGE RankNTypes, ImpredicativeTypes #-}

f :: Int -> (forall r. r -> r)
f = undefined

g :: (forall r. r -> r) -> Int
g = undefined

h :: Int -> Int
-- h v = g (f v) -- It works well
h = g . f -- I can't write it in this way

I get following errors.

[1 of 1] Compiling Main             ( test.hs, interpreted )

test.hs:11:9:
    Couldn't match type ‘r0 -> r0’ with ‘forall r. r -> r’
    Expected type: Int -> forall r. r -> r
      Actual type: Int -> r0 -> r0
    In the second argument of ‘(.)’, namely ‘f’
    In the expression: g . f
Failed, modules loaded: none.

Answer 1

Actually, f doesn't have type Int -> (forall r. r -> r), because GHC floats out every forall and class constraint to the top of the scope. So f's type is really forall r. Int -> r -> r.

For example, the following typechecks:

f :: Int -> (forall r. r -> r)
f = undefined

f' :: forall r. Int -> r -> r
f' = f

This makes the g . f composition ill-typed (we can see that the error message points explicitly at the discrepancy between r -> r and forall r. r -> r).

It would be probably better behavior for GHC to throw errors upon finding forall-s in wrong places, instead of silently floating them out.

There are several reasons why polymorphic return types (which are outlawed by floating-out forall-s) aren't allowed in GHC. For details you can refer to this paper (section 4.6 specifically). In short, they only make sense if there is solid support for impredicative instantiation, which GHC lacks. In the absence of impredicative types, floating-out allows more terms to typecheck and rarely causes inconvenience in real world code.