First-Class Modules: Type Escaping from Unpack Signatures

The Constraint of Local Abstraction

In OCaml, a type instantiated within an unpacked module cannot be promoted to a global abstraction without altering the enclosing signature. The `unpack` expression introduces a locally abstract type for every abstract type defined in the signature. This type is existentially quantified and strictly confined to the scope of the `unpack` expression. This design ensures that different packings of the same signature remain interchangeable, maintaining parametricity.

Functor Application vs. First-Class Packing

When the objective is maintaining type identity across parametric polymorphism, the mechanisms differ significantly:

• Functor Application: module N = F(M) preserves type identity if the resulting signature explicitly exposes concrete types (e.g., type t = M.t). Because the functor operates at compile-time on module definitions, the compiler can track the identity.
• First-Class Modules: Packing a module erases identity because the packed value carries only the signature, not the path to the original module. It hides the concrete implementation behind an abstract interface.

Relaxing the Boundary

There is no native compiler mechanism to relax the local abstraction constraint for types exported via include or module type extensions. The boundary is enforced at the `unpack` site; include merely copies signature components and does not reify the hidden type. To bypass this, one must use specific architectural patterns:

1. Signature Exposure: Modify the signature to expose the concrete type (type t = int, for example) so it is no longer abstract.
2. Functor Wrapping: Use a functor to compute with the type and return a first-class module whose signature reveals the specific type being used.
3. Witness Patterns: Use GADTs or a type _ t witness packed alongside the module to recover type equality at use sites.

Recursive module signatures (module rec) do not change this rule; each `unpack` still introduces fresh locally abstract types. Mutual recursion across packed modules requires explicit type equalities in the signatures to resolve correctly.