LET REC recursive expression static typing rule
It seems you discovered the difference between a set of typing rules and an algorithm for type inference.

Typing rules only define a relation among 1) a type environment, 2) a term, and 3) a type. Their purpose is only to precisely define a mathematical relation $\Gamma \vdash t: \tau$.

Once we have such definition, we do not automatically get a type checking algorithm. That is, in general, there is no algorithm described by the rules which, given $\Gamma,t,\tau$, is able to test whether $\Gamma \vdash t: \tau$ holds. (In some cases, such an algorithm could even fail to exist!)

Similarly, we do not automatically obtain a type inference algorithm, which given $\Gamma,t$ is able to find a related $\tau$ (when it exists).

The type checking/type inference algorithm must be devised independently.

Now, it is true that in many cases the algorithms can follow the rules quite closely. The rule for non-recursive LET you mention is one nice example, since it is clear how to turn it into an algorithm. For recursive LETs, we are not that lucky.

A typical strategy to type check/infer recursive LETs is to introduce a fresh type variable in the environment, and then perform type checking on the body while generating a set of constraints. For instance, consider this example

let-rec f (x: int) = 1 + f(x) in f(0)


We discover immediately that f : int -&gt; ???. Let's introduce a fresh type variable R for the result, and say f : int -&gt; R.

We then type check 1 + f(x) assuming the environment f: int -&gt; R , x: int.
Here + is applied to arguments 1: int and f(x): R. Assuming + requires its arguments to be of the same type, this forces the constraint int = R.
If + also returns the same type, we obtain another constraint int = R (redundant, in this case).

Finally, we solve the constraints, discovering R = int.

Note that in the general case we might be less lucky, since more complex types could be involved.

let-rec f(x: int) = (2, fst(f(x-1)))


Here, we discover f: int -&gt; R, then we see that R must be a pair type R = A*B, then A=int (because of the 2). Moreover, we get f(x-1):R so fst(f(x-1)): A, hence B=A. We conclude f: int-&gt;(int*int).

It is not trivial to generate these constraints, or to solve them (usually through a unification algorithm). In the scientific literature we can find several algorithms which perform this, but they are not obvious at first.