Pattern match on hlist to functions with first-class module type constrains

Learning
1

Hi,

I tried to adapt the answer of this post to store first-class module in the list:

module type S = sig
  type t
end

type _ t =
  | Nil : unit t
  | Cons : (module S with type t = 'a) * 'b t -> ('a -> 'b) t

let rec tofun : type a. a t -> a -> unit =
  function
  | Nil -> fun f -> ()
  | Cons (type b) ( (module C : S with type t = b), xs) ->
      fun f -> tofun xs (f C.t)

but I got an error:

Error: Existential types introduced in a constructor pattern
       must be bound by a type constraint on the argument.

I thought it was bound since it is mentioned in the type constraint.

Any help is welcome.

1 Like
2

There are two issues I see with your code:

  • C.t is a type so it cannot be used as a value in f C.t. You may have meant:

    module type S = sig
  type t
  val x: t
end

    and use f C.x instead of f C.t.

  • Exstential types introduced by a constructor must be bound by a top-level type constraint, something like

    | Cons (type a b) ((module C), xs : (module S with type t = a) * b t) ->

    instead of

    | Cons (type b) ( (module C : S with type t = b), xs) ->

    should work.

Cheers,
Nicolas

3

Oups!. Very confused about this one. I guess I would have seen after I fixed the first issue.

Thank you very much. I was trying to only constraint the first parameter of the Cons constructor whereas the solution was to constraint the pair of parameter.

I added a pair of parenthesis to make clear that the constraint is not only for the second parameter.

Regards,
Nico

4

It is harmless, but not strictly needed either: the type constraint operator : binds less strongly than the pair constructor ,.

Cheers,
Nicolas