Parametric locally abstract type

I'm trying to figure out how to write a function depending on a module with a parametric type but I can't find anything similar anywhere. I tried to reduce the problem as much as possible and ended up with this dummy example.

module type Mappable = sig
  type 'a t
  val map : ('a -> 'b) -> 'a t -> 'b t
end

let plus (type m) (module M : Mappable with type 'a t = 'a m) (xs : int m) = 
  M.map (fun x -> x + 1) xs

which yields the error Error: Syntax error: module-expr expected.

If I drop the 'a, I end up with the following error.

Error: In this `with' constraint, the new definition of t
       does not match its original definition in the constrained signature:
       Type declarations do not match: type t is not included in type 'a t
       They have different arities.

What's the correct syntax to do this?

Solution

I believe what you want to do here is impossible in OCaml 4.02.3. Let see a simplified version without the type variable:

module type Mappable = sig
  type t
  val map : ('a -> 'b) -> t -> t
end

let plus (type m) (module M : Mappable with type t = m) (xs : m) = 
  M.map (fun x -> x + 1) xs

The above is typable and plus has the following type:

val plus : (module Mappable with type t = 'm) -> 'm -> 'm

the type m in its definition is abstracted to a variable 'm.

Now, back to your original code and think what the type plus is supposed to have. Since you are trying to abstract m by (type m), it should be:

val plus : (module Mappable with type 'a t = 'a 'm) -> 'a 'm -> 'a 'm

Unfortunately, OCaml does not support the higher kinded polymorphism which allows this form of type 'a 'm. It seems the first class module typing is carefully implemented not to introduce it.

You can see the following short paper which explains the current (unfortunate) status of the higher kinded polymorphism in OCaml. This explains a workaround: how to encode it in the current OCaml framework with a cost of explicit coersions:

https://ocamllabs.github.io/higher/lightweight-higher-kinded-polymorphism.pdf

I have never tried by myself but the same workaround could be applied to your example.