Special cases of handling higher ranks in the 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 bar function with a rank-2 type. Therefore, type inference should not 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 thing in a free style, this 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 someone confirm that this is specifically addressed in the GHC, or indicate where I am mistaken.

Answer 1

The main problem of type inference when there are types of a higher rank is the derivation of polymorphic types for lambda-related variables. In your first example, the only correct way to enter foo is to assign the polymorphic type f . In your second example, such a thing is not required. Instead, baz is just a (trivial) partial application of bar . A simple application of a higher rank polymorphic function without any lambda abstractions should always be possible without additional type annotations.

See also the relevant section in the GHC User Guide , as well as various research documents.