Sharing constraints on non-abstract types

Learning
1

I know how to use sharing constraints over abstract types, but this time I wanted the type to have a constructor. A minimal example could be:

module type Key = sig
  type t = T of string
end

val create_foo : (module Key with type t = 'k) -> ('k * string) list -> foo

But this fails with:

In this `with' constraint, the new definition of t
does not match its original definition in the constrained signature

And I don’t think there’s a way to write that constraint in the first place. Is it possible? I know I could move the constructor to a type outside Key and drop the constraint, but I did not want instances of Key to be compatible. In the end, I went with a different API so I’m asking out of curiosity.

1 Like
2

You may add a proxy abstract type and the hypothesis that the two types are equal.

type ('a, 'b) eq =
  | Eq : ('a, 'a) eq

module type Key = sig
  type t = T of string

  type t'

  val eq : (t, t') eq
end

val create_foo : (module Key with type t' = 'k) -> ('k * string) list -> foo

create_foo just have to destruct the hypothesis to use the constructor on values of type 'k. For instance:


type foo = (string * string) list

let create_foo (type k)
    (m : (module Key with type t' = k)) (l : (k * string) list) : foo =
  let module M = (val m) in
  let Eq = M.eq in
  l |> List.map (fun (M.T s, s') -> (s, s'))