Вывод типа с взаимной рекурсией

Я думал о том, как вывод типов работает в следующей программе OCaml:

let rec f x = (g x) + 5
and g x = f (x + 5);;

Конечно, программа совершенно бесполезна (бесконечный цикл) , а как насчет типов? OCaml говорит:

val f : int -> int = <fun>
val g : int -> int = <fun>

Это в точности моя интуиция, но откуда алгоритм вывода типов знает об этом?

Скажем, алгоритм сначала рассматривает «f»: единственное ограничение, которое он может получить, это то, что возвращаемый тип «g» "должно быть" int ", и поэтому его собственный возвращаемый тип также" int ". Но он не может вывести тип своего аргумента по определению «f».

С другой стороны, если он сначала рассматривает «g», он может видеть, что тип его собственного аргумента должен быть «int». Но, не рассмотрев раньше «f», он не может знать, что тип возвращаемого значения «g» также является «int».

В чем заключается магия?