[Haskell-cafe] Rigid skolem type variable escaping scope
Matthew Steele
mdsteele at alum.mit.edu
Wed Aug 22 13:25:03 CEST 2012
While working on a project I have come across a new-to-me corner case of the type system that I don't think I understand, and I am hoping that someone here can enlighten me.
Here's a minimal setup. Let's say I have some existing code like this:
{-# LANGUAGE Rank2Types #-}
class FooClass a where ...
foo :: (forall a. (FooClass a) => a -> Int) -> Bool
foo fn = ...
Now I want to make a type alias for these (a -> Int) functions, and give myself a new way to call foo. I could do this:
type IntFn a = a -> Int
bar :: (forall a. (FooClass a) => IntFn a) -> Bool
bar fn = foo fn
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
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
More information about the Haskell-Cafe
mailing list