[Haskell-cafe] Inference for RankNTypes

[Francesco Mazzoli]

Hi list,

I am a bit puzzled by the behaviour exemplified by this code:

    {-# LANGUAGE RankNTypes #-}

    one :: (forall a. a -> a) -> b -> b
    one f = f

    two = let f = flip one in f 'x' id
    three = (flip one :: b -> (forall a. a -> a) -> b) 'x' id
    four = flip one 'x' id

Try to guess if this code typechecks, and if not what’s the error.

While `two' and `three' are fine, GHC (7.4.1 and 7.6.1) complains about `four':

    Line 8: 1 error(s), 0 warning(s)
    
    Couldn't match expected type `forall a. a -> a'
                with actual type `a0 -> a0'
    In the third argument of `flip', namely `id'
    In the expression: flip one 'x' id
    In an equation for `four': four = flip one 'x' id

So for some reason the quantified variable in `id' gets instantiated before it
should, and I have no idea why.

Any ideas?

Francesco