[Haskell-cafe] Rigid skolem type variable escaping scope

[Simon Peyton-Jones]

| This compiles just fine, as I would expect.  But now let's say I want
| to change it to make IntFn a newtype:
| 
|     newtype IntFn a = IntFn (a -> Int)
| 
|     bar :: (forall a. (FooClass a) => IntFn a) -> Bool
|     bar (IntFn fn) = foo fn

The easiest way is to imagine transforming the function to System F. I'll ignore the (FooClass a) bit since it's irrelevant.  We'd get

bar = \(x :: forall a. IntFn a).
      ...what?...

We can't do case-analysis on x; it has a for-all type, so we must instantiate it. But at what type?  Let's guess some random type 'b':

bar = \(x : forall a. IntFn a).
      case (x b) of 
        IntFn (f :: b -> Int) -> foo f

But now we are in trouble.  'foo' itself needs an argument of type (forall a. a->Int).  So we need a big lambda

bar = \(x : forall a. IntFn a).
      case (x b) of 
        IntFn (f :: b -> Int) -> foo (/\a. f)

But this is obviously wrong because 'b' escapes the /\a.

I don't know if I can explain it better than that

Simon


| 
| I had expected this to compile too.  But instead, I get an error like
| this one (using GHC 7.4.1):
| 
|     Couldn't match type `a0' with `a'
|       because type variable `a' would escape its scope
|     This (rigid, skolem) type variable is bound by
|       a type expected by the context: FooClass a => a -> Int
|     The following variables have types that mention a0
|       fn :: a0 -> Int (bound at <the line number that implements bar>)
|     In the first argument of `foo', namely `fn'
|     In the expression: foo fn
|     In an equation for `bar': bar (IntFn fn) = foo fn
| 
| I don't think I am grasping why adding the layer of newtype
| wrapping/unwrapping, without otherwise changing the types, introduces
| this problem.  Seems to me like the newtype version would also be type-
| safe if GHC allowed it (am I wrong?), and I'm failing to understand why
| GHC can't allow it.  Is there a simple explanation, or else some
| reading that someone could point me to?  (-:
| 
| Cheers,
| -Matt
| 
| 
| _______________________________________________
| Haskell-Cafe mailing list
| Haskell-Cafe at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell-cafe