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.