Based on some initial feedback, I'm providing some further information:

What I have is a whole bunch of functors that look like this:

module Make(S : OrderedType) = struct

module SM = Map.Make(S)

module SS = Set.Make(S)

module SC = CustomFunctor.Make(S)

(* where SC has exposed maps and sets in its interface *)

...

(* many more similar modules/functors *)

...

let foo () : SS.t =

SC.run SS.empty

end

I don't really want to define the type of Make because I have to constrain that SS, SM, and SC all preserve applicative identity in a type constraint. Then I have to do the same thing for every CustomFunctor as well. Worst, it's difficult to tell when things have been broken because exactly which equality is missing is completely opaque in the type checking -- especially when most of the uses of these modules is just plumbing (to preserve applicative identity).

Thanks all,

Arlen

On Thu, Sep 20, 2018 at 10:29 AM Arlen Cox <arlencox@gmail.com> wrote:

Hi everyone,

I'm having some trouble getting some code that relies heavily on applicative functors to type check. Does anyone know what I'm doing wrong with this?

module type S = sig
module T : Set.OrderedType
module ST : module type of Set.Make(T)
end

module Make(T_in : Set.OrderedType) : S (* <- ERROR *)
with module T = T_in
   and module ST = Set.Make(T_in)
= struct
module T = T_in
module ST = Set.Make(T_in)
end

I get the following error message referencing the above point in the program.

Error: In this `with' constraint, the new definition of ST
       does not match its original definition in the constrained signature:
       ...
       Type declarations do not match:
         type t = Set.Make(T_in).t
       is not included in
         type t = Set.Make(T).t
       File "set.mli", line 68, characters 4-10: Expected declaration
       File "set.mli", line 68, characters 4-10: Actual declaration

It seems to me that since T = T_in, but applicative functors should make the type of Set.Make(T) = Set.Make(T_in). Does this not work this way?

Note that if I change the definition of S slightly, the same definition of Make now type checks:

module type S = sig
module T : Set.OrderedType
module ST : Set.S with type elt = T.t
end

This solution is undesirable because I have a number of modules whose types would require an excessive number of "with module ... = ..." constraints to constrain in this way. Is there a better way of getting this to type check?

Thank you,
Arlen