[Haskell-cafe] Rigid skolem type variable escaping scope

[oleg at okmij.org]

Matthew Steele asked why foo type-checks and bar doesn't:
>   class FooClass a where ...
> 
>   foo :: (forall a. (FooClass a) => a -> Int) -> Bool
>   foo fn = ...
> 
>   newtype IntFn a = IntFn (a -> Int)
> 
>   bar :: (forall a. (FooClass a) => IntFn a) -> Bool
>   bar (IntFn fn) = foo fn

This and further questions become much simpler if we get a bit more
explicit. Imagine we cannot write type signatures like those of foo
and bar (no higher-ranked type signatures). But we can define
higher-rank newtypes. Since we can't give foo the higher-rank
signature, we must re-write it, introducing the auxiliary
newtype FaI.

> {-# LANGUAGE Rank2Types #-}

> class FooClass a where m :: a
>
> instance FooClass Int where m = 10
>
> newtype FaI = FaI{unFaI :: forall a. (FooClass a) => a -> Int}

> foo :: FaI -> Bool
> foo fn = ((unFaI fn)::(Char->Int)) m > 0

We cannot apply fn to a value: we must first remove the wrapper FaI
(and instantiate the type using the explicit annotation -- otherwise
the type-checker has no information how to select the FooClass
instance).

Let's try writing bar in this style. The first attempt

> newtype IntFn a = IntFn (a -> Int)
> newtype FaIntFn = FaIntFn{unFaIntFn:: forall a. FooClass a => IntFn a}
>
> bar :: FaIntFn -> Bool
> bar (IntFn fn) = foo fn

does not work: 
    Couldn't match expected type `FaIntFn' with actual type `IntFn t0'
    In the pattern: IntFn fn

Indeed, the argument of bar has the type FaIntFn rather than IntFn, so
we cannot pattern-match on IntFn. We must first remove the IntFn
wrapper. For example:

> bar :: FaIntFn -> Bool
> bar x = case unFaIntFn x of
>          IntFn fn  -> foo fn

That doesn't work for another reason: 
    Couldn't match expected type `FaI' with actual type `a0 -> Int'
    In the first argument of `foo', namely `fn'
    In the expression: foo fn

foo requires the argument of the type FaI, but fn is of the type
a0->Int. To get the desired FaI, we have to apply the wrapper FaI:

> bar :: FaIntFn -> Bool
> bar x = case unFaIntFn x of
>          IntFn fn  -> foo (FaI fn)

And now we get the desired error message, which should become clear:

    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 /tmp/h.hs:16:16)
    In the first argument of `FaI', namely `fn'
    In the first argument of `foo', namely `(FaI fn)'

When we apply FaI to fn, the type-checker must ensure that fn is
really polymorphic. That is, free type variable in fn's type do not
occur elsewhere type environment: see the generalization rule in the
HM type system. When we removed the wrapper
unFaIntFn, we instantiated the quantified type variable a with some
specific (but not yet determined) type a0. The variable fn receives
the type fn:: a0 -> Int. To type-check FaI fn, the type checker should
apply this rule

	G |- fn :: FooClass a0 => a0 -> Int
        -----------------------------------
        G |- FaI fn :: FaI

provided a0 does not occur in G. But it does occur: G has the binding
for fn, with the type a0 -> Int, with the undesirable occurrence of
a0.

To solve the problem then, we somehow need to move this problematic binding fn
out of G. That binding is introduced by the pattern-match. So, we
should move the pattern-match under the application of FaI:

> bar x = foo (FaI (case unFaIntFn x of IntFn fn  -> fn))

giving us the solution already pointed out.

> So my next question is: why does unpacking the newtype via pattern
> matching suddenly limit it to a single monomorphic type?

Because that's what removing wrappers like FaI does. There is no way
around it. That monomorphic type can be later generalized again, if
the side-condition for the generalization rule permits it.

You might have already noticed that `FaI' is like big Lambda of System
F, and unFaI is like System F type application. That's exactly what
they are:
     http://okmij.org/ftp/Haskell/types.html#some-impredicativity

My explanation is a restatement of the Simon Peyton-Jones explanation,
in more concrete, Haskell terms.