This note summarizes the A Type System for Recursive Modules ‘s requirement for coherence when defining recursive modules, specifically addressing why certain module aliasing patterns must be rejected.

The scenario involves defining a recursive module X that requires its internal structure A to satisfy a signature SOME_SIG (which contains abstract types).

Example	Definition Pattern	Type System Status	Reason
Example 3	structure B = SOME_MOD;``structure A :> SOME_SIG = B	Ill-Typed(Must be rejected)	The unconstrained definition of B gives the type checker transparent knowledge of B’s internal types (e.g., B.t=int). When A is defined as a copy of B and then sealed by SOME_SIG (which requires A.t to be abstract), the recursive environment X is simultaneously aware of two conflicting facts about the same underlying type entity: X.A.t is abstract, but the identical X.B.t is concrete. This violates the coherence invariant of the recursive type system, leading to the “double vision problem” and guaranteed unsoundness if allowed.
Example 2	structure B :> SOME\_SIG = SOME\_MOD;``structure A = B	Well-Typed	Sealing (:>SOME_SIG) is applied to B before the alias A is created. This ensures B.t is immediately a safe, abstract type tied to the X path, and A merely becomes a coherent alias of the already-abstract B.

导出到 Google 表格

In summary, a sound recursive module calculus (like RMC) must reject definitions where a transparent, unsealed alias is created first and then constrained later, as this leaks concrete type information into the recursive scope, thereby defeating the core principle of data abstraction.

The issue in Example 3 is about how abstract types behave when they are copied or aliased before they are sealed by a signature, which can lead to a violation of the “same-module-same-type” guarantee.

Here is a detailed breakdown of why Example 3 is problematic in a powerful module system like OCaml’s (specifically, the RMC calculus discussed by Dreyer).

The Core Problem: Type Identity and Opaque Sealing

In OCaml’s module system, abstract types inside a module are identified by their path. For a module M with an abstract type t, the type is globally known as M.t.

The critical difference between your three examples hinges on whether the structure being defined is immediately sealed (Examples 1 and 2) or whether an internal copy is made before sealing (Example 3).

Case 1 & 2 (OK): Immediate Sealing Preserves Abstraction

In Examples 1 and 2, the module definition is constrained immediately:

OCaml

(* Case 1: Direct Sealing *)
structure A :> SOME_SIG = SOME_MOD

(* Case 2: Sealing a Named Copy *)
structure B :> SOME_SIG = SOME_MOD; structure A = B

In both cases, SOME_MOD is sealed (constrained by the signature SOME_SIG) when its components are assigned to a public name (A or B).

Result: All abstract types within A (or B) that are defined in SOME_SIG are now abstract types belonging to module A.
Crucially, if SOME_MOD contained an abstract type t, that type is now uniquely identified by the path A.t. Any other use of SOME_MOD will produce a different abstract type. This is the correct, safe, generative behavior for abstract data types.

Case 3 (Problematic): Leaking Internal Identity

In Example 3, a non-sealed module is created first, and then the public module A is defined as a sealed copy of it:

OCaml

(* Case 3: Problematic Copying *)
structure B = SOME_MOD;              (* 👈 B is NOT sealed. *)
structure A :> SOME_SIG = B          (* 👈 A is a sealed copy of B. *)

Step 1: structure B = SOME_MOD
- Since there is no signature constraint, B gets the fully transparent (inferred) signature of SOME_MOD.
- If SOME_MOD contains a type t = int, then B.t is transparently equal to int.
Step 2: structure A :> SOME_SIG = B
- A is sealed by SOME_SIG. If SOME_SIG says A.t is abstract (type t), A successfully hides the fact that A.t is int.
The Leak: Although A is sealed, the full, transparent definition of the structure still exists under the internal name B.

If the recursive body (rec (...) struct ... end) attempts to reference the recursive variable X within another component (let’s call it C), we run into trouble:

Reference 1: C might refer to the abstract type X.A.t.
Reference 2: C might refer to the transparent type X.B.t.

Since A is defined as a copy of B before sealing, the type system would have to infer that X.A.t and X.B.t are the same underlying type entity.

However:

X.A.t is supposed to be abstract (due to the recursive signature).
X.B.t is fully transparent (due to the unsealed definition).

This conflict creates an unsoundness known as the “double vision problem” in recursive modules: the type system simultaneously sees the type as abstract (via X.A) and concrete (via X.B). It essentially leaks the concrete identity of a type that was intended to be abstract, breaking the fundamental guarantee of data abstraction.

In Summary (The Parenthetical Note)

“Though A is internally a copy of B, it should not be public knowledge that the abstract types in SOME_MOD …”

Your note correctly identifies the problem:

The existence of the unconstrained name B inside the recursive definition provides an alias that bypasses the sealing of A. If the recursive body later uses B, it can access the internal concrete representation of what should be an abstract type when viewed through A. This violates the integrity of the abstract type X.A.t, which is essential for type soundness in a recursive setting

A static view:

That is the precise scenario where the problem manifests.

If the recursive body contains only A and B as defined in your Example 3, the type-checking would still fail in a sound type system like RMC (Recursive ML-style Module Calculus), even if you don’t define a third component C.

The issue is not about using the conflict in a third module C; the conflict is introduced the moment the unconstrained alias B is created inside the recursive scope.

Here is why:

The Problem: Violating Coherence (X’s Signature)

The recursive definition is checked against the external signature X provided in the rec binding:

rec(X:sig structure A : SOME_SIG end) struct… end

This binding means that X.A must satisfy SOME_SIG. If SOME_SIG contains an abstract type type t, then X.A.t must be an abstract type—its identity is tied to the path X.A.

When the body is type-checked:

structure B = SOME_MOD: B is assigned the fully transparent signature of SOME_MOD. If SOME_MOD has a type t = int, then B.t is transparently equal to int.
structure A :> SOME_SIG = B: A is sealed by SOME_SIG.

The type checker has a duty to ensure that the defined module has a signature that is a subtype of the recursive signature. The inferred signature of the body is:

sig structure B : …end and A:SOME_SIG

In a sound system like RMC, the type identity rules dictate that the path X.B.t (derived from the unsealed B) and X.A.t(derived from the sealed A) must not clash.

The creation of the alias B where B.t has a transparent definition (int), while X.A.t is required to be abstract, introduces a violation of the system’s coherence invariant. The type checker cannot maintain the illusion that X.A.t is abstract while simultaneously knowing that the identical, co-defined path X.B.t is concrete.

Why Example 3 Fails vs. Example 2 Succeeds

The difference is where the sealing happens:

Example	Sealing Position	Abstraction Level	Resulting Types
Example 2 (OK)	Sealing happens beforethe alias A is defined.	The type A.t is immediately abstract.	A.t is a fresh abstract type. B.t is an alias of A.t, sharing the abstract identity.
Example 3 (Fails)	The transparent alias Bis defined first.	B.t is concrete/transparent before A is defined.	B.t is a concrete type (e.g., `int`). A.t is a constrained copy of B.t, creating a conflict in the recursive type environment X.

导出到 Google 表格

In Example 3, the existence of the non-sealed, transparent structure B contaminates the recursive context X, making it impossible to soundly define the other component A as abstractly as X’s signature requires.

In essence, the problem is not a run-time bug, but a type system invariant failure that prevents the code from compiling in the first place, thus enforcing the integrity of abstract data types within recursion.

A summary

The Role of Type Invariants

The type system (RMC, in this case) is designed to reject Example 3 not because an explicit, unsound usage has been demonstrated yet (like the module C), but because the definition itself violates a necessary type invariant for the entire recursive structure to be considered sound.

Here is the breakdown of why this is the only correct approach:

Safety First: A type system must be sound. It must ensure that if a program type-checks, it will not lead to runtime errors (like treating an abstract type as a concrete integer).
The Recursive Assumption: When you write rec (X : SOME_SIG) struct ... end, the type checker assumes that the resulting module will satisfy SOME_SIG and uses the variable X in the body of the structure as if it already satisfied it.
The Invariant Failure:
- The signature requires X.A.t to be abstract.
- The structure defines the transparent alias B such that B.t is concrete (e.g., int).
- Since A is defined as a sealed copy of B, the type system internally knows that A.t and B.t are the same type entity.

The failure occurs because the recursive assumption requires X.A.t to be abstract, but the internal definition of the very structure that is supposed to become X immediately gives it a concrete, exposed alias (B.t). This creates the “double vision problem” where the type is simultaneously abstract and concrete under the recursive path X.

Conclusion

You’ve understood the core design principle: The type system must reject Example 3 to guarantee that no future, more complex code (like module C) could exploit the internal alias B to violate the abstraction boundary required by the recursive signature X.

By failing at the definition stage, the system ensures that the crucial invariant—that X is a coherent, abstract structure—is never broken.

Tony's Wiki

Explorer

Double Vision Problem - Abstract Types vs. Unconstrained Aliases in Recursive Modules