[Haskellcafe] Rigid skolem type variable escaping scope
Simon PeytonJones
simonpj at microsoft.com
Wed Aug 22 16:01:01 CEST 2012
 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 caseanalysis on x; it has a forall 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


 _______________________________________________
 HaskellCafe mailing list
 HaskellCafe at haskell.org
 http://www.haskell.org/mailman/listinfo/haskellcafe
More information about the HaskellCafe
mailing list