The signature for this packaged module couldn't be inferred in recursive function

Question

I'm still trying to figure out how to split code when using mirage and it's myriad of first class modules. I've put everything I need in a big ugly Context module, to avoid having to pass ten modules to all my functions, one is pain enough.

I have a function to receive commands over tcp :

let recvCmds (type a) (module Ctx : Context with type chan = a) nodeid chan = ...

After hours of trial and errors, I figured out that I needed to add (type a) and the "explicit" type chan = a to make it work. Looks ugly, but it compiles. But if I want to make that function recursive :

let rec recvCmds (type a) (module Ctx : Context with type chan = a) nodeid chan =
  Ctx.readMsg chan >>= fun res ->
  ... more stuff ...
  |> OtherModule.getStorageForId (module Ctx)
  ... more stuff ...
  recvCmds (module Ctx) nodeid chan

I pass the module twice, the first time no problem but I get an error on the recursion line :

The signature for this packaged module couldn't be inferred.

and if I try to specify the signature I get

This expression has type a but an expression was expected of type 'a
The type constructor a would escape its scope

And it seems like I can't use the whole (type chan = a) thing. If someone could explain what is going on, and ideally a way to work around it, it'd be great. I could just use a while of course, but I'd rather finally understand these damn modules. Thanks !

Answer 1

The pratical answer is that recursive functions should universally quantify their locally abstract types with let rec f: type a. .... = fun ... .

More precisely, your example can be simplified to

module type T = sig type t end 
let rec f (type a) (m: (module T with type t = a)) = f m

which yield the same error as yours:

Error: This expression has type (module T with type t = a) but an expression was expected of type 'a The type constructor a would escape its scope

This error can be fixed with an explicit forall quantification: this can be done with the short-hand notation (for universally quantified locally abstract type):

let rec f: type a.  (module T with type t = a) -> 'never = fun m -> f m

The reason behind this behavior is that locally abstract type should not escape the scope of the function that introduced them. For instance, this code

let ext_store = ref None
let store x = ext_store := Some x
let f (type a) (x:a) = store x

should visibly fail because it tries to store a value of type a, which is a non-sensical type outside of the body of f.

By consequence, values with a locally abstract type can only be used by polymorphic function. For instance, this example

  let id x = x
  let f (x:a) : a = id x

is fine because id x works for any x.

The problem with a function like

 let rec f (type a) (m: (module T with type t = a)) = f m

is then that the type of f is not yet generalized inside its body, because type generalization in ML happens at let definition. The fix is therefore to explicitly tell to the compiler that f is polymorphic in its argument:

 let rec f: 'a. (module T with type t = 'a) -> 'never =
   fun (type a) (m:(module T with type t = a)) -> f m

Here, 'a. ... is an universal quantification that should read forall 'a. .... This first line tells to the compiler that the function f is polymorphic in its first argument, whereas the second line explicitly introduces the locally abstract type a to refine the packed module type. Splitting these two declarations is quite verbose, thus the shorthand notation combines both:

let rec f: type a.  (module T with type t = a) -> 'never = fun m -> f m