# HM inference examples

## let-inference

<https://stackoverflow.com/questions/44509154/let-inference-in-hindley-milner?rq=1>

`ex = \a -> let b = a in b + 1`

* First, we associate `a` with a fresh type variable, say `a :: t0`.
* Then we type `b = a`. We get `b :: t0` as well.
* However, and this is the key point, we should not generalize the type of `b` to `b :: forall t0. t0`. This is because we can only generalize over a tyvar which does not occur in the environment: here, instead, we do have `t0` in the environment since `a :: t0` is there.
* If you do generalize it, you will get a way too general type for `b`; then `b + 1` becomes `b+1 :: forall t0. Num t0 => t0`, and the whole term gets `forall t0 t1. Num t1 => t0 -> t1` since the types for `a` and `b` are unrelated (`t0`, once generalized, can be alpha-converted to `t1`).

1. a :: a
2. b :: b
3. (b = a) -> `b :: a`
4. (b + 1) :: Num a -> `b :: Num a`
5. ex ::

ex :: Num a => a -> a ex = \a -> let b = a in b + 1

ex :: Num a => a -> a ex a = let b = a in b + 1

ex :: Num a => a -> a ex a = a + 1