I’m not sure if below is the minimal code example, but what I’m trying to accomplish is the function k
below, which takes a function and a first-class module, and the function is just a forwarding function for something in the first-class module. I want to give these forwarding functions a type but I don’t want to expose the 't
type variable because it is not really necessary, I’m just trying to enforce the relationship in the forwarding function.
Is this possible?
The error is:
This expression has type (module FOO with type t = F.t)
but an expression was expected of type (module FOO with type t = $V_'t)
Type F.t = t is not compatible with type $V_'t
module type FOO = sig
type t
val get : unit -> t
val bar : t -> string
end
module Fimpl : FOO = struct
type t = int
let get () = 4
let bar = string_of_int
end
type 'a f = V : ((module FOO with type t = 't) -> 't -> 'a) -> 'a f
let bar (type t) (module F : FOO with type t = t) (t:t) =
F.bar t
let k (type t) (V f) (module F : FOO with type t = t) =
let t = F.get () in
f (module F) t
let () = ignore (k (V bar) (module Fimpl))
1 Like
The short answer is that you need a universal quantifier for 't
, not an existential one. We can swap your GADT out for a record field to achieve that:
type 'a f = { f : 't. ((module FOO with type t = 't) -> 't -> 'a) }
let bar (type t) (module F : FOO with type t = t) (t:t) =
F.bar t
let k (type t) { f } (module F : FOO with type t = t) =
let t = F.get () in
f (module F) t
let () = ignore (k { f = bar } (module Fimpl))
Your definition of f
– with the existential binding for 't
– means that any given 'a f
is a forwarding function for values of some type 't
that was known at construction time but is not recovered via pattern matching. The error message is complaining about this: the specific existentially-bound type $V_'t
might not equal F.t
as far as the type checker is concerned.
Switching 'a f
to use a universal quantifier for 't
flips this around: the consumer of the 'a f
value gets to pick whichever instantiation they want, and the provider must show that they are compatible with any possible choice by passing a polymorphic function. (This seems to be the semantics you want.)
Hope this helps.
2 Likes
Thank you very much! I never would have come across that on my own. That solves my type issues! And thank you for the explanation.
1 Like