[Haskell-cafe] Rigid skolem type variable escaping scope

[Matthew Steele]

On Aug 22, 2012, at 3:02 PM, Lauri Alanko wrote:

> Quoting "Matthew Steele" <mdsteele at alum.mit.edu>:
> 
>>    {-# LANGUAGE Rank2Types #-}
>> 
>>    class FooClass a where ...
>> 
>>    foo :: (forall a. (FooClass a) => a -> Int) -> Bool
>>    foo fn = ...
> 
>>    newtype IntFn a = IntFn (a -> Int)
>> 
>>    bar :: (forall a. (FooClass a) => IntFn a) -> Bool
>>    bar (IntFn fn) = foo fn
> 
> In case you hadn't yet discovered it, the solution here is to unpack the IntFn a bit later in a context where the required type argument is known:
> 
> bar ifn = foo (case ifn of IntFn fn -> fn)
> 
> Hope this helps.

Ah ha, thank you!  Yes, this solves my problem.

However, I confess that I am still struggling to understand why unpacking earlier, as I originally tried, is invalid here.  The two implementations are:

1) bar ifn = case ifn of IntFn fn -> foo fn
2) bar ifn = foo (case ifn of IntFn fn -> fn)

Why is (1) invalid while (2) is valid?  Is is possible to make (1) valid by e.g. adding a type signature somewhere, or is there something fundamentally wrong with it?  (I tried a few things that I thought might work, but had no luck.)

I can't help feeling like maybe I am missing some small but important piece from my mental model of how rank-2 types work.  (-:  Maybe there's some paper somewhere I need to read?

Cheers,
-Matt