OCaml Module Signatures and First-Class Modules: Static Type Safety vs. Dynamic Selection

The short answer

OCaml keeps type inference consistent because a first-class module is not an untyped value: it is a value of the form (module S), where S is an explicit module type. When you unpack it and apply a functor, the compiler performs an ordinary signature-matching check at that point. Dynamic selection changes which implementation you get, never whether it satisfies the required signature. Sealed (abstract) types survive the round trip: unpacking introduces fresh abstract type identities, so nothing outside the signature can rely on the hidden representation.

How unpacking preserves type inference

A module becomes a value with the coercion (module M : S), and is turned back into a module with one of two valid forms:

let (module M : S) = v in ...
(* or *)
let module M = (val v : S) in ...

Note there are no pack/unpack keywords in OCaml; the coercions above are the actual syntax. Once re-bound, M is an ordinary static module identifier, and a functor application such as module R = Make(M) is checked exactly as if M had been defined statically. The compiler verifies M's module type against the functor's parameter signature structurally, at the application site.

The subtlety is abstract types. Each unpack of a first-class module introduces fresh abstract type identities (existential-style). Two modules unpacked from the same value at different points therefore have incompatible abstract types unless the compiler can see they came from the same unpack. This is why the usual pattern is to unpack once, at the outermost scope, and pass the resulting module around:

module type SERVICE = sig
  type t
  val create : unit -> t
  val run : t -> string
end

module Make (S : SERVICE) = struct
  let start () = S.run (S.create ())
end

let pick verbose : (module SERVICE) =
  if verbose then (module Verbose_service : SERVICE)
  else (module Quiet_service : SERVICE)

let () =
  let (module S) = pick true in
  let module R = Make (S) in
  print_endline (R.start ())

If Make required something the chosen implementation lacked, the error is reported at the functor application, even though the choice of implementation happened at runtime.

Constraints on sealed modules crossing back into the static world

• Opacity is preserved. If the signature seals a type (type t with no manifest), the functor's body can only use t through the operations the signature exposes. Passing the module as a value first does not weaken this.
• Identity is per-unpack. Because each unpack creates fresh abstract types, you cannot unpack the same value twice and expect the two t types to unify. Unpack once and share the binding.
• The annotation must be explicit. A first-class module value carries its module type, so the compiler needs a concrete signature at the coercion or unpack site; it will not infer one from later use.
• Scope is lexical. The re-bound module identifier is only visible inside the let ... in body, which is what guarantees the fresh abstract types cannot escape and be confused with anything else.

Static vs. dynamic at a glance

Aspect	Functor (static)	First-class module (dynamic)
Selection time	Compile time	Runtime
Type checking	Signature match at application	Same check, after explicit unpack
Abstract types	Fixed identity	Fresh identity per unpack
Typical use	Generic components, specialization	Plugins, config-driven backends

Practical guidance

Use functors when the dependency is known statically; reach for first-class modules only at the genuine runtime decision point, and convert back to a static module immediately so the rest of the code stays in the functor world. One caveat worth flagging for review: deeply nested runtime selection can hinder cross-module inlining compared to purely static applications, so keep the dynamic boundary narrow. The examples above assume OCaml 4.x/5.x semantics; verify with ocamlc -i that inferred interfaces match your expectations.