- A+

So I just recently learned about and started using `TypeApplications`

, and was wondering how we can generally know what type variables we're assigning. The documentation on `TypeApplications`

I found mentions:

What order is used to instantiate the type variables?

Left-to-right order of the type variables appearing in the foralls. This is the most logical order that occurs when the instantiation is done at the type-variable level. Nested foralls work slightly differently, but at a single forall location with multiple variables, left-to-right order takes place. (See below for nested foralls).

However I haven't found mention of how order of type variables in implicit foralls is determined. I tried looking at different examples with `-fprint-explicit-foralls`

to see if there was a simple pattern, but I'm getting different results in different versions of ghci. :/

In ghci version 8.0.2, I get:

`> :t (,,) (,,) :: forall {c} {b} {a}. a -> b -> c -> (a, b, c) `

while in ghci version 8.4.3, I get:

`> :t (,,) (,,) :: forall {a} {b} {c}. a -> b -> c -> (a, b, c) `

Then again, maybe that's simply a bug in how foralls were being printed in 8.0.2, because otherwise type applications seem to be done right-to-left with the variables of forall, contrary to what the documentation says:

`> :t (,,) @Bool (,,) @Bool :: forall {c} {b}. Bool -> b -> c -> (Bool, b, c) `

So are type variables put in implicit foralls always in the order they appear first left-to-right in the type body (including the constraints)?

TL;DR: When interested in `TypeApplication`

, use `:type +v`

.

### Don't use `:type`

Using `:type`

is misleading here. `:type`

infers the type of a whole expression. So when you write `:t (,)`

, the type checker looks at

`(,) :: forall a b. a -> b -> (a, b) `

and instantiates all the forall’s with fresh type variables

`(,) :: a1 -> b1 -> (a1, b1) `

which is necessary if you would apply `(,)`

. Alas, you don’t, so type inference is almost done, and it generalizes over all free variables, and you get, for example,

`(,) :: forall {b} {a}. a -> b -> (a, b) `

This step makes no guarantees over the order of the free variable, and the compiler is free to change.

Also note that it writes `forall {a}`

instead of `forall a`

, which means that you can’t use visible type application here.

### Use `:type +v`

But of course you can use `(,) @Bool`

– but here the type-checker treats the first expression differently and does not do this instantiation/generalization step.

And you can get this behaviour in GHCi as well – pass `+v`

to `:type`

:

`:type +v (,) (,) :: forall a b. a -> b -> (a, b) :type +v (,) @Bool (,) @Bool :: forall b. Bool -> b -> (Bool, b) `

Look, no `{…}`

around type variables!