Special cases in handling of higher rank types in GHC?

Question

Consider this example from a GHCi session:

Prelude> :set -XRankNTypes
Prelude> let bar :: (forall a.[a]->[a]) -> [Int]; bar f = f [1,2,3]

This defines a funcion bar with rank-2 type. Hence, type inference should not be able to infer the correct type for:

Prelude> let foo f = bar f

And indeed,

<interactive>:7:17:
Couldn't match type `t' with `[a] -> [a]'
  `t' is a rigid type variable bound by
      the inferred type of foo :: t -> [Int] at <interactive>:7:5
In the first argument of `bar', namely `f'
In the expression: bar f
In an equation for `foo': foo f = bar f

Surprisingly, if we write the same in point free style it works:

Prelude> let baz = bar
Prelude> :t baz
baz :: (forall a. [a] -> [a]) -> [Int]

How is it that type inference can infer a higher rank type here? Can anybody confirm that this is treated specially in GHC, or point out where I err.

Answer 1

The main problem of type inference in the presence of higher-rank types is inferring polymorphic types for lambda-bound variables. In your first example, the only correct way to type foo is to assign a polymorphic type to f. In your second example, no such thing is needed. Instead, baz is just a (trivial) partial application of bar. Merely applying a higher-rank polymorphic function, without any lambda abstractions, should always be possible without additional type annotations.

See also the appropriate section in the GHC User's Guide as well as various research papers.