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.
c :: Test Identity
c = (cons :: Identity -> Test Identity) t
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 variable a is never instantiated to a polymorphic type automatically. Rather, a is replaced by an "unknown" fresh variable a0 (ranging over monomorphic types). This variable is then used to produce type equations, which are then solved using unification later on.
Example:
id id :: ??
Let's call the two occurrences as id0 and id1. We get
id0 id1 :: ??
id0 :: forall a. a->a
id1 :: forall a. a->a
Instantiate fresh variables
id0 :: a0 -> a0
id1 :: a1 -> a1
Unify argument type: a0 ~ (a1 -> a1).
id0 :: (a1 -> a1) -> (a1 -> a1)
id1 :: a1 -> a1
Apply.
id0 id1 :: a1 -> a1
Re-generalize.
id0 id1 :: forall a. a->a
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 unknown a1. This is however not what is happening in the inference algorithm.
We can achieve the latter instantiation if we resort to manual typing:
(id :: (forall a. a->a) -> (forall a. a->a)) id
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, the foralls 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).