OCaml Typechecking Problem With Functors and Polymorphic Variants

Question

I have a problem using functors in OCaml. I have a module type TASK that is used to have different kinds of tasks:

module type TASK = sig
  type task_information
  type task_information_as_lists

  type abstract_u_set_type
  module AbstractUSet : Set.S with type t = abstract_u_set_type

  val mk_task_information : task_information_as_lists -> task_information
end

A module of type TASK will contain algorithms that use nodes. These nodes will have different types. I therefore built TASK_NODE:

module type TASK_NODE = sig
  type t
  val compare : t -> t -> int
  val to_string : t -> string
end

task_information_as_lists from TASK will be a list containing different types, but every task will have different types in that list. As I cannot have something like module Game : (TASK with with type u := int list) with functors, I've created a module type INFO_CARRIER. For every different module of type TASK I want to have a different module of type INFO_CARRIER that will hold the information what type task_information_as_lists actually is.

This is the module type INFO_CARRIER:

module type INFO_CARRIER = sig
  module INODE : TASK_NODE
  type u = [`V of INODE.t list | `E of INODE.t] list
end

For testing, I want to have string TASK_NODES, and an INFO_CARRIER that can convey a type u like type u = [`V of string list | `E of string] list.

So I built StringTaskNode and StringInfoCarrier, and also a StringTask to use the nodes:

module StringTaskNode : TASK_NODE = struct
  type t = string
  let compare = compare
  let to_string s = "Node " ^ s
end

module StringInfoCarrier (TN : TASK_NODE) : (INFO_CARRIER with module INODE = TN) = struct
  module INODE = TN
  type u = [`V of TN.t list | `E of TN.t] list
end

module StringTask (TN : TASK_NODE) (IC : INFO_CARRIER with module INODE = TN) : 
  (TASK with type task_information_as_lists := IC.u with type abstract_u_set_type := Set.Make(IC.INODE).t) = struct
  module N = IC.INODE
  module AbstractUSet = Set.Make(IC.INODE)

  type task_information = {v_nodes : AbstractUSet.t ; e_nodes : N.t}

  let mk_task_information info_list =
    match info_list with
    | (`V v)::(`E e)::[] -> {v_nodes = AbstractUSet.of_list v ; e_nodes = e;}
    | _ -> raise .... (* raising an error here *)
end

I then have another module ProdFP that will do some computation for a task:

module ProdFP 
  (TN : TASK_NODE) 
  (IC : INFO_CARRIER with module INODE=TN) 
  (TA : TASK with type abstract_u_set_type:=u with type task_information_as_lists:=IC.u) = struct
  ...
end

So far, no errors happen. But when I bring everything together in Test, I get:

Error: This expression has type
  [`E of string | `V of string list]
but an expression was expected of type
SIC.u = [`E of SIC.INODE.t | `V of SIC.INODE.t list]
Type string is not compatible with type
  SIC.INODE.t = STN.t

This is the testing module:

module Test = struct
  module STN = StringTaskNode
  module SIC = StringInfoCarrier(STN)
  module ST = StringTask(STN)(SIC)
  module PF = ProdFP(STN)(SIC)(ST)

  let v_list =["a";"b"]
  let e = "c"
  let info_as_list = [`V v_list ; `E e]

  let info = ST.mk_task_information info_as_list (* THIS IS WHERE THE ERROR HAPPENS *)
end

I know, this is a very long post, but I've tried to include as much information as necessary. It would be so great if you could help me :)

octachron octachron · Accepted Answer · 2020-03-23T14:46:07

It looks like the problem is just the signature constraint in the definition of the StringTaskNode module:

module StringTaskNode : TASK_NODE = struct
...
end

This constraint makes the type StringTaskNode.t abstract and thus hides the equality STN.t = string. Removing the constraint,

module StringTaskNode = struct
...
end

should resolve this specific issue.

OCaml Typechecking Problem With Functors and Polymorphic Variants

1 Answers