[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?  (-:


More information about the Haskell-Cafe mailing list