I'm having trouble understanding why the type inferred for this statement `fun f g x -> f (g x)`

would be this...

```
('a -> 'b) -> ('c -> 'a) -> 'c -> 'b = <fun>
^^^^
```

instead of this ...

```
('a -> 'b) -> ('c -> 'a) -> 'a -> 'b = <fun>
^^^^^
```

I gathered that

variable `x -> 'c`

function `f`

:

```
input = g x -> 'a
output = f g x -> 'b
```

function `g`

:

```
input = x -> 'c
output = g x -> 'a
```

`f ( g x)`

:

```
input = g x -> 'a ( According to the solution, this should be 'c ? I'm not sure why... does the parenthesis change anything ? )
^^^^^^^^^^^
output = f g x -> 'b
```

Breaking down the function to this `f g x -> g x -> f g x`

I got this `('a -> 'b) -> ('c -> 'a) -> 'a -> 'b = <fun>`

Could anyone lend a little hint as to why this is wrong ?

tl;dr

`(g x) : 'a`

is the type of the *result* of applying `g`

to `x`

. But the type of `x`

itself is `'c`

.

Type inference in ML works like this:

First, you have a function

`fun f g x -> f (g x)`

the type of the lambda, say `Tlam0`

, is

`Tlam0 == Tf -> Tg -> Tx -> Tbody`

stepping into the body, we find that it is the result of `f`

is applied to something, so `f`

must be a function:

```
TBody == <app f ??> == Tfo
Tf == Tfi -> Tfo
```

Next, look at the thing applied to `f`

`Tfi == <app g ??> == Tgo`

Because `g`

is applied to something, `g`

is a function

`Tg == Tgi -> Tgo`

Now examine the type of the argument to `g`

, which is just the `x`

we passed in as an argument to the lambda.

```
Tx == Tx
Tgi == Tx
```

And we're done examining the whole body expression.

Now substitute everything back:

```
Tx == Tx
Tgi == Tx
Tg == Tgi -> Tgo == Tx -> Tgo
Tfi = Tgo
Tf == Tfi -> Tfo == Tgo -> Tfo
Tbody == Tfo
----------------------------
Tlam0 == Tf -> Tg -> Tx -> Tbody
== (Tgo -> Tfo) -> (Tx -> Tgo) -> Tx -> Tfo
```

Now just rename all the placeholders to ABC's

```
Tx == a
Tg == a -> b
Tf == b -> c
Tbody == c
----------------------------
Tlam0 == Tf -> Tg -> Tx -> Tbody
== (b -> c) -> (a -> b) -> a -> c
```

Which by alpha-conversion is equivalent to the inferred type of

`('a -> 'b) -> ('c -> 'a) -> 'c -> 'b`

(i.e. if you just picked different characters.)