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
```