[Haskell-cafe] Rigid skolem type variable escaping scope
oleg at okmij.org
oleg at okmij.org
Thu Aug 23 13:27:02 CEST 2012
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.
More information about the Haskell-Cafe
mailing list