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?
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 ifA<:B
and all runtime components of both module types appear at the same position.For instance, this is fine:
because both module types agrees that the first runtime component is
x
, and the second one isy
. Contrarilyfails because the two module types disagrees on the position of the fields
x
andy
.Similarly, it is important to note that it is the position that matters,
fails because the
y
field is at the third position in theWith_hole
module and at the second position inB
. Beware that extensible variant constructor are values too:create a runtime value (the extension constructor).
Lastly, in presence of submodules, all the submodules of
A
andB
must be runtime-equivalent subtypes forA
andB
to be runtime-equivalent subtypes. In other words, this works:because the fields of the two submodules
M
are the same (same type and same position). But this doesn't:since in order to convert
C_nested
intoB_nested
, we will need to permute the fields of the submoduleM
ofC_nested
.