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 !
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
which yield the same error as yours:
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):
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
should visibly fail because it tries to store a value of type
a
, which is a non-sensical type outside of the body off
.By consequence, values with a locally abstract type can only be used by polymorphic function. For instance, this example
is fine because
id x
works for anyx
.The problem with a function like
is then that the type of
f
is not yet generalized inside its body, because type generalization in ML happens atlet
definition. The fix is therefore to explicitly tell to the compiler thatf
is polymorphic in its argument:Here,
'a. ...
is an universal quantification that should readforall 'a. ...
. This first line tells to the compiler that the functionf
is polymorphic in its first argument, whereas the second line explicitly introduces the locally abstract typea
to refine the packed module type. Splitting these two declarations is quite verbose, thus the shorthand notation combines both: