In OCaml 4.01 and earlier, first-class modules are typed nominatively. In other words, their type is based on the name of the module type used, not its structure. For example:
OCaml version 4.01.0
# module type T = sig type t end;;
module type T = sig type t end
# module type S = sig type t end;;
module type S = sig type t end
# let f (x : (module T)) : (module S) = x;;
Characters 38-39:
let f (x : (module T)) : (module S) = x;;
^
Error: This expression has type (module T)
but an expression was expected of type (module S)
This requires that the module type has a name:
# type t = (module sig type t end);;
Characters 17-20:
type t = (module sig type t end);;
^^^
Error: Syntax error
Destructive substitution is disallowed because it creates a new module type without a name. Regular substitution is fine because S with type t = int
, is still an S
, we just know more about its definition. S with type t := int
is not an S
it has different components to an S
since it lacks a t
type.
Recently (Mantis, SVN), the type-checking of first-class modules has been changed to be structural instead of nominative:
OCaml version 4.02.0+dev5-2014-04-29
# module type T = sig type t end;;
module type T = sig type t end
# module type S = sig type t end;;
module type S = sig type t end
# let f (x : (module T)) : (module S) = x;;
val f : (module T) -> (module S) = <fun>
This means that first-class modules could be created for types which have no name. However, this has not been done yet and will not be available in 4.02. So, in versions after 4.02 it may indeed be possible to use destructive substitution in first-class module types.