I am playing around with trying to define a “dependent” version of visitors (à la Pottier) for GADTs, and I am running into an issue with OCaml type inference that I can’t figure out. Hopefully someone out there can explain it to me.
To set the scene, I have some GADT definitions, e.g.
type _ t0 = Z type (_,_) t1 = | A : ('a, 'a) t1 | B : ('a, 'b) t1 -> ('a, 'b t0) t1 type _ t2 = | C : 'a t2 | D : 'a t2 -> 'a t0 t2
Now, I can write a function that recurses on a value of type
('a, 'b) t1 in order to transform a value of type
'a t2 into one of type
'b t2, as follows.
let rec foo : type a b . (a, b) t1 -> a t2 -> b t2 = function | A -> (fun x -> x) | B v -> let f = foo v in (fun x -> D (f x))
Now, using a visitor class defined within a functor, I am trying to “abstract” the recursion over
('a, 'b) t1 values, to produce values of some abstract type
('a, 'b) t, which I can then instantiate to some concrete type by applying the functor.
module Reduce (X : sig type ('a, 'b) t end) = struct class ['self] reduce = object (self : 'self) method reduce_A : type a . (a, a) X.t = failwith "Must be overridden" method reduce_B : type a b . (a, b) X.t -> (a, b t0) X.t = failwith "Must be overridden" method reduce_t1 : type a b . (a, b) t1 -> (a, b) X.t = function | A -> self#reduce_A | B v -> let f = self#reduce_t1 v in self#reduce_B f end end
However, when I try to “implement” the
foo function by applying the functor, creating an object that overrides the methods appropriately, and then “extracting” the appropriate method, OCaml infers a type using weak type variables, even though the methods in the type inferred for the object appear to be appropriately generalised.
(* Why does OCaml only infer a type with weak type variables here? *) (* ('_weak1, '_weak2) t1 -> '_weak1 t2 -> '_weak2 t2 *) let bar = let module M = Reduce(struct type ('a, 'b) t = 'a t2 -> 'b t2 end) in let obj = object (self) inherit [_] M.reduce as super method! reduce_A = (fun v -> v) method! reduce_B f = (fun x -> D (f x)) end in (* This is the type inferred for the object, methods have generalised types < reduce_A : 'a. 'a t2 -> 'a t2; reduce_B : 'a 'b. ('a t2 -> 'b t2) -> 'a t2 -> 'b t0 t2; reduce_t1 : 'a 'b. ('a, 'b) t1 -> 'a t2 -> 'b t2 > *) obj#reduce_t1
Can someone explain to me why this is happening?
EDIT: I just figured it out, reading this post. The definition of the function needs to be eta-expanded.
let bar v x = let module M = Reduce(struct type ('a, 'b) t = 'a t2 -> 'b t2 end) in let obj = object (self) inherit [_] M.reduce as super method! reduce_A = (fun v -> v) method! reduce_B f = (fun x -> D (f x)) end in obj#reduce_t1 v x