I don't understand why this program is not typable :
type Test a = forall z. (a -> z) -> z
cons :: a -> Test a
cons = \a -> \p -> p a
type Identity = forall x. x -> x
t :: Identity
t = \x -> x
c :: Test Identity
c = cons (t :: Identity)
main :: IO ()
main = do{
print "test"
}
I use option -XRankNTypes
with GHC.
I have the following error :
Couldn't match type `x0 -> x0' with `forall x. x -> x'
Expected type: Identity
Actual type: x0 -> x0
In the first argument of `cons', namely `(t :: Identity)'
In the expression: cons (t :: Identity)
In an equation for `c': c = cons (t :: Identity)
Could somebody help me?
Inference with
RankNTypes
is tricky. Try annotating the function instead of the argument.Why this is so requires delving into the intricacies of the type inference algorithm. Here's some intuition behind that.
Intuitively, whenever a polymorphic value
x :: forall a. F(a)
is used, the type variablea
is never instantiated to a polymorphic type automatically. Rather,a
is replaced by an "unknown" fresh variablea0
(ranging over monomorphic types). This variable is then used to produce type equations, which are then solved using unification later on.Example:
Let's call the two occurrences as
id0
andid1
. We getInstantiate fresh variables
Unify argument type:
a0 ~ (a1 -> a1)
.Apply.
Re-generalize.
Note that, in this specific case, we could have obtained the same final result by unifying
a0 ~ (forall a. a->a)
instead, and avoiding to generate the fresh unknowna1
. This is however not what is happening in the inference algorithm.We can achieve the latter instantiation if we resort to manual typing:
There are, however, some exceptions to the above discussion. The major one is rank-2 (and rank-N) types. When GHC knows a function is higher-ranked, its argument is handled differently: the
forall
-quantified variables occurring in its type are not replaced by unknowns. Rather, theforall
s are kept so that they can later be matched with the type expected by the function.I recommend reading the GHC user guide, which explains a bit what's going on. If you instead want all the gory details, you will need to refer to the papers describing the actual typing rules. (Actually, before reading those I'd learn some background in some simpler systems e.g. basic Hindley–Milner).