Why destructive substitution is disabled in first class module packing?

Question

Suppose these:

module type Foo = sig
  type t
  val foo : t -> t
end

module M = struct
  type t = int
  let foo t = t + 1
end

---

Then I do:

module type Goo = Foo with type t = int

module type Hoo = Foo with type t := int

let x = (module M : Goo) (* correct *)

let y = (module M : Hoo) (* correct *)

let z = (module M : Foo with type t = int) (* correct *)

Above all correct, no problem.

---

However, if I do

let z = (module M : Foo with type t := int) (* wrong *)

it is wrong, and error is given

Error: Parse error: "=" expected after [ident] (in [package_type_cstr])

---

Why I can't use := in first class module packing?

Answer 1

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.