Consider this function:

```
tuple2Int :: (x -> Int) -> (a, b) -> (Int, Int)
tuple2Int f (a, b) = (f a, f b)
```

…which wouldn’t work. Why? Because of `f a`

, the type checker deduces that `x~a`

(`x`

is equivalent to `a`

); because of `f b`

, the type checker also deduces that `x~b`

. Therefore, `a~x~b`

, which is obviously false for most cases.

With `RankNTypes`

, we can instead write the type signature of the function as `tuple2Int' :: (forall x. x -> Int) -> (a, b) -> (Int, Int)`

. This way, the compiler knows that it should use two seperate `x`

’s for `a`

and `b`

. It therefore deduces that `x1~a`

and `x2~b`

and because it is not enforced that `x1~x2`

, there is no problem at all!

### Go Deeper

What’s going on?

First, we need to learn the cruel and ugly fact that NO so-called “generic” function in Haskell is actually generic in essence. What does this mean? Let’s consider `length :: [a] -> Int`

. It looks pretty generic to me as I can use it on any type of list, you may say. This is true, but what happens under the hood is that the compiler *specializes* a version of the function with concrete type (i.e. no type variable like `a`

) everytime you use it. For example, when you do `length [1, 2, 3]`

, a specialized version `length(Int) :: [Int] -> Int`

is magically created by the compiler to accomodate you; when you do `length "abcdefg"`

, similarly a `length(Char) [Char] -> Int`

is created. Just remember this for now.

Just as we use `\x -> ...`

to define a lambda function with variable `x`

, we use `forall a. ...`

to define a type with type variable `a`

. Therefore, suppose that we can construct the **type of a function** by a data constructor `FunctionType a b`

, where `a`

and `b`

are **values** that represent types, our `(forall x. x -> Int)`

in the last paragraph would be equivalent to `\x -> FunctionType x Int`

. You also need to remember this.

And then, a crash course in lambda calculus. Consider this lambda function: `\x y -> x + y + z`

. We call `x`

and `y`

**bound variables**, because their appearance is bound by the `\x y`

part of the function. We call `z`

a **free variable**, because it is defined “elsewhere” and is thus not bound by the `\x y`

part. End of the crash course.

With the three things we just learned, we can touch on the problem. Firstly, we have a rule that **no type variables in a type contruction can be free**. For example, we can’t write a type-level function like `\x -> FunctionType x y`

, or formally `forall x. x -> y`

, because `y`

is free. This is a very strict rule and obviously we don’t want to be scolded by the compiler every now and then just because of it, so we have another catch-all rule: **if a type variable is not explicitly bound, it is then treated as bound at the beginning of the expression.** What does this mean? Suppose we have a type

`a -> a`

(or `FunctionType a a`

with our syntax). Because you see no `forall`

in its type signature, technically `a`

is free. This is when the rule kicks in: because `a`

is not *explicitly*bound, we treat the whole type as

`forall a. a -> a`

(or `\a -> FunctionType a a`

) and voila! The first rule is automatically satisfied. How nice.Generic functions in Haskell are all defined this way. `id`

, for example, has type `forall a. a -> a`

. Our `tuple2Int`

, because it has `x`

, `a`

and `b`

that all appear to be free, has type `forall x a b. (x -> Int) -> (a, b) -> (Int, Int)`

by the second rule. This is where our problem arises: when we are using this function, the compiler needs to create a concrete version of it (in other words, it needs to assign types to `x`

, `a`

and `b`

). Furthremore, because `x`

is scoped on the **whole** type expression, it must takes the same value everywhere. An example:

```
foo = (\x -> x + (\y -> x + 3) 4) 5
bar = (\f -> f 2 + f 3 + f 4) (\x -> x + 2)
```

In `foo`

, because `x`

is bound at the very beginning, it is scoped over the whole expression. Therefore, it must always takes the value `5`

. On the contrary, in `bar`

, because `x`

is bound only inside the second pair of brackets, it can take different values of `2`

, `3`

, and `4`

elsewhere (i.e. inside the first pair of brackets).

Back to `tuple2Int`

. What type should the compiler assign to `x`

? It sees that `a`

can be applied to `x -> Int`

, so `a`

and `x`

must be the same. Similar deduction goes for `b`

and `x`

. Therefore, unless `a`

and `b`

are the same type, we would have a type contradiction.

Now make sure that you understand the problem, and we’ll proceed to its solution.