Ответ 1
Во-первых, обратите внимание, что Leroy (или Ocaml) не разрешает module rec без явных аннотаций подписи. Так что это скорее
module rec A : SA = ... and B : SB = ... and C : SC = ...
и аппроксимативная среда: {A: approx (SA), B: approx (SB), C: approx (SC)}.
Неудивительно, что некоторые типы типов проверяют тип, если они определены отдельно, но не тогда, когда они определены рекурсивно. В конце концов, то же самое верно и для деклараций на языке ядра: в "let rec" рекурсивные вхождения связанных переменных мономорфны, а при раздельных объявлениях "let" вы можете использовать предыдущие переменные полиморфно. Интуитивно, причина в том, что вы не можете иметь все знания, которые вам нужны, чтобы вывести более либеральные типы, прежде чем вы действительно проверили определения.
Что касается вашего предложения, проблема заключается в том, что он делает конструкцию module rec несимметричной, т.е. порядок имеет значение в потенциально тонкой форме. Это нарушает дух рекурсивных определений (по крайней мере, в ML), который всегда должен быть безразличным к упорядочению.
В общем, проблема с рекурсивной типизацией - это не столько надежность, сколько полнота. Вы не хотите, чтобы система типов, которая вообще неразрешима, или спецификация которой зависит от алгоритмических артефактов (например, порядок проверки).
В более общем примечании хорошо известно, что обработка Ocaml рекурсивных модулей является довольно ограничительной. Проделана работа, например. Наката и Гаррига, что еще больше продвигает свои пределы. Тем не менее, я убежден, что в конечном итоге вы не сможете получить столь же либеральные, как вам бы хотелось (и это относится и к другим аспектам его модульной системы типа, например, функторам), не отказываясь от чисто синтаксического подхода Ocaml к набору модулей, Но тогда я предвзятый.:)