[Haskell-cafe] Rigid skolem type variable escaping scope

[Matthew Steele]

On Aug 22, 2012, at 4:32 PM, Erik Hesselink wrote:

> On Wed, Aug 22, 2012 at 10:13 PM, Matthew Steele <mdsteele at alum.mit.edu> wrote:
>> 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?
> 
> Look at it this way: the argument ifn has a type that says that *for
> any type a you choose* it is an IntFn. But when you have unpacked it
> by pattern matching, it only contains a function (a -> Int) for *one
> specific type a*. At that point, you've chosen your a.
> 
> The function foo wants an argument that works for *any* type a. So
> passing it the function from IntFn isn't enough, since that only works
> for *one specific a*. So you pass it a case expression that produces a
> function for *any a*, by unpacking the IntFn only inside.

Okay, that does make sense, and I can see now why (2) works while (1) doesn't.

So my next question is: why does unpacking the newtype via pattern matching suddenly limit it to a single monomorphic type?  As you said, ifn has the type "something that can be an (IntFn a) for any a you choose".  Since an (IntFn a) is just a newtype around an (a -> Int), why, when you unpack ifn into (IntFn fn), is the type of fn not "something that can be an (a -> Int) for any a you choose"?  Is it possible to add a local type annotation to force fn to remain polymorphic?

Cheers,
-Matt