I'm taking a programming languages course and had a question regarding the typing rules for a recursive `let rec` expression in a static typing system.

To be more specific, we're using the textbook *Essentials of Programming Languages (3e) - Friedman & Wand*.

<br>

To give some rough background, here's how the author describes the typing rule for a normal `let` binding expression:

[![enter image description here][1]][1]


To briefly describe it for anybody unfamiliar with the notation, `type-of` is a function used to evaluate the type of the given expression.

According to the typing rule, we evaluate `exp1` first, which would give us type $t_1$. Then we extend our current environment so $var$ is mapped to $t_1$. Using this new environment, we evaluate the $body$ of the expression which gives us our final type.

<br>

Here's how a `let-rec` recursive binding's typing rule is defined:

[![enter image description here][2]][2]

The main problem that I'm having is how to understand the order of evaluation. According to the typing rule, it seems as though we're extending the environment first with $var$ and $p$, but where are we getting the types to map them to from?

  [1]: https://i.sstatic.net/yZ92y.png
  [2]: https://i.sstatic.net/jTZhn.png