типизация рекурсивных модулей

В статье Лероя о том, как рекурсивные модули типизируются в OCaml, написано, что модули проверяются в среде, состоящей из приближений типов модулей:

module rec A = ... and B = ... and C = ...

Окружающая среда {A -> приблизительно (A); B -> приблизительно (B); C -> приблизительно (C)} сначала создается, а затем используется для вычисления типов A, B и C.

Я заметил, что в некоторых случаях приближения недостаточно хороши, и проверка типов не выполняется. В частности, при помещении источников модулей компиляции в определение рекурсивного модуля проверка типов может завершиться ошибкой, тогда как компилятор смог скомпилировать модули компиляции отдельно.

Возвращаясь к моему первому примеру, я обнаружил, что решением было бы ввести A в исходной приближенной среде, а затем ввести B в этой исходной среде, расширенной новым вычисляемым типом A, и ввести C в предыдущий env с новым вычисляемым типом B и так далее.

Прежде чем исследовать больше, я хотел бы знать, проводилась ли какая-либо предыдущая работа по этому вопросу, показывающая, что такая схема компиляции для рекурсивных модулей безопасна или небезопасна? Есть ли контрпример, показывающий небезопасную программу, правильно набранную по этой схеме?