Typing constraints through functor parameter


#1

Hi everyone,

consider the following not working example:

module type CS = sig
  type t
  type content

  val make: content -> t
  val to_string: t -> string
end

module C : CS with type content = int = struct
  type content = int
  type t = { x: content }

  let make x = { x }
  let to_string { x } = string_of_int x
end

module type S = sig
  module C: CS

  val f: C.t -> unit
end

module Make(C: CS) : S = struct
  module C = C

  let f c = print_endline (C.to_string c)
end

module M = Make(C)

let _ =
  let c = C.make 0 in
  M.f (M.C.make 0)

Here is my problem: whereas the sharing constraint with type content = int allows me to call directly C.make with an int, I need, in order to use M.f to use M.C.make.

But the compiler will output about the integer:
Error: This expression has type int but an expression was expected of type M.C.content

Is there a way to somehow force the sharing constraint to be visible through the instantiation of the functor ?
I tried for example module M = Make(C : CS with type content = int), without success.


#2

Your problem is actually different here.

The issue is that you don’t expose the fact that M.C = C. The C in the module type S is not linked to the input C. This can be solved by changing the definition of Make:

module Make(C: CS) : S with module C = C = struct
  module C = C

  let f c = print_endline (C.to_string c)
end

#3

Oh! Thank you, I did’nt know constraints were not only about types.


#4

In fact, my use case was a bit more complex, since I use first-class modules.
But I managed to get things done with:

module M = Make(C)

module type S' = S with module C = C

let m = (module M: S')
module M' = (val m: S')

let _ = M'.f (M'.C.make 0)

Is there a reason why one can’t use module constraint directly?, as in:

let m = (module M: S with module C = C)
module M' = (val m: S with module C = C)