To infer `letrec x = e in e'`

, you infer the type of `e`

and guess a monotype `x : tau`

for `x`

at the same time, and then you generalize this monotype into a type scheme `x : sigma`

to check `e'`

. Operationally, this can be described as "type-check `e`

with a fresh inference variable `'_a`

for `x`

.

To infer `letrec x1 = e1 and x2 = e2 in e'`

, you infer `e1`

and `e2`

, guessing monotypes for `x1`

and `x2`

at the same time, and then you generalize both to type-check `e'`

. (Or: create inference variables `x: '_a, y : '_b`

, and type-check `e1`

then `e2`

.)

You can do slightly better in cases where some definitions don’t depend on others, so that the recursive definitions can be ordered – there is a non-trivial topological sorting into several strongly-conneected components. For example, if `e1`

needs `x`

and `y`

but `e2`

only needs `x`

, you can first infer the type of `e2`

, guessing a monotype for `x`

, then generalize the type of `e2`

before checking `e1`

(so it infers a monotype for `x`

, but gets a polymorphic scheme for `e2`

); this can type-check more programs. For example:

```
let rec x n =
if n = 0 then []
else (y n "foo", y n true) :: x (n - 1)
and y n z =
if n = 0 then z
else y (n - 1) z
in ...
```

Finally, if you support polymorphic recursion through explicit annotations, you can refine the way you do the topological sorting above, by *not* considering as a dependency the mention of a recursive variable that is explicitly annotated (terms do not “need” explicitly-annotated variables in the sense above).

Note: you mention a paper by Figueiredo and Camarão, which is a sort of tutorial implementation. I would be careful with this paper, because the system it implements, which is presented in an earlier work of their, is probably incorrect: it claims to provide a decidable inference procedure for polymorphic recursion without annotations, which is known to be undecidable. (See Re: Decidable polymorphic recursion? , Re: Decidable polymorphic recursion? for the heated details).