
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