[Caml-list] First-class Functor Forgetting for Free

[David Sheets <sheets@alum.mit.edu>]

What issue prevents functions over first-class modules from forgetting
the first-class modules' type constraints?

That is, given:

###############

module type D = sig
  type t

  val x : t
  val f : t -> int
end

module type C = sig
  val q : int
end

module F(X : D) : C = struct
  let q = X.(f x)
end

let f x =
  let module X = (val x : D) in
  let module Q = struct
    let q = X.(f x)
  end in
  (module Q : C)

let x =
  let module X = struct
    type t = int

    let x = 2
    let f x = x * 3
  end in
  (module X : D with type t = int)

;;
let module X = (val x : D with type t = int) in
let module M = F(X) in
(* let x = (module (val x : D with type t = int) : D) in*)
let module M' = (val f x : C) in

Printf.printf "M.q  is %d\n%!" M.q;
Printf.printf "M'.q is %d\n%!" M'.q;
()

###############

Why must I uncomment (* let x = (module (val x : D with type t = int)
: D) in*) to compile?

I understand why structural subtyping requires a module cast but I
don't see why type relaxation would.
I looked at the generated assembly and this line seems to disappear.

Why is it needed?

Thanks,

David