Subtype coercion with first-class modules

Question

Given the following module signatures, where B subsumes A:

module type A = sig
  type t
end

module type B = sig
  type t
  val x: t
end

Normally, any module that satisfies B will then also satisfy A. This does not extend automatically to first-class modules however, because of course it's a different type language that doesn't allow automatic unification with subtypes. But manual coercion should still work, should it not? (It does in fact if the module signatures only contain type definitions, but not if it contains values.)

let f (_: (module A)) = ()
let g (b: (module B)) = f (b :> (module A)) (* Error: Type (module B) is not a subtype of (module A) *)

Is this a fundamental limitation of first-class modules? What are the rules that determine whether a module type is a subtype of another in the core type language? And is there a practical workaround?

Answer 1

Type coercion is a type-level only operation in OCaml. In other words, it is expected to be a no-op at runtime.

To preserve this property, subtyping for first-class modules needs to use a restricted module subtyping relationship: (module A) <: (module B) if and only if A<:B and all runtime components of both module types appear at the same position.

For instance, this is fine:

module type A = sig
  type x = int
  type y = float
  val x : x
  val y :y
end
module type B = sig
  val x:int
  val y:float
end
let f (x:(module A) list) = (x:>(module B) list)

because both module types agrees that the first runtime component is x, and the second one is y. Contrarily

module type C = sig
  val y:int
  val x:float
end
let f (x:(module C) list) = (x:>(module B) list)

fails because the two module types disagrees on the position of the fields x and y.

Similarly, it is important to note that it is the position that matters,

module type With_hole = sig
  type t = int
  val x:float
  val intron: int;
  val y:int;
end
let f (x:(module With_hole) list) = (x:>(module B) list)

fails because the y field is at the third position in the With_hole module and at the second position in B. Beware that extensible variant constructor are values too:

type exn += X

create a runtime value (the extension constructor).

Lastly, in presence of submodules, all the submodules of A and B must be runtime-equivalent subtypes for A and B to be runtime-equivalent subtypes. In other words, this works:

module type A_nested = sig
  module M: A
end

module type B_nested = sig
  module M:B
end
let ok (x: (module A_nested)) = (x:> (module B_nested))

because the fields of the two submodules M are the same (same type and same position). But this doesn't:

module type C_nested = sig
  module M: C
end
let error (x:(module C_nested)) = (x :> (module B_nested))

since in order to convert C_nested into B_nested, we will need to permute the fields of the submodule M of C_nested.