ocaml type over-binding due to specialized recursive use of type

Question

I have a parameterized type that recursively uses itself but with a type parameter specialized and when I implement a generic operator, the type of that operator is bound too tightly because of the case that handles the specialized sub-tree. The first code sample shows the problem, and the second shows a workaround that I'd rather not use because the real code has quite a few more cases so duplicating code this way is a maintenance hazard.

Here's a minimal test case that shows the problem:

module Op1 = struct
  type 'a t = A | B  (* 'a is unused but it and the _ below satisfy a sig *)

  let map _ x = match x with
    | A -> A
    | B -> B
end

module type SIG = sig
  type ('a, 'b) t =
    | Leaf  of 'a * 'b
    (* Here a generic ('a, 'b) t contains a specialized ('a, 'a Op1.t) t. *)
    | Inner of 'a * ('a, 'a Op1.t) t * ('a, 'b) t

  val map : ('a -> 'b) -> ('a_t -> 'b_t) -> ('a, 'a_t) t -> ('b, 'b_t) t
end

module Impl : SIG = struct
  type ('a, 'b) t =
    | Leaf  of 'a * 'b
    | Inner of 'a * ('a, 'a Op1.t) t * ('a, 'b) t

  (* Fails signature check:
       Values do not match:
         val map :
           ('a -> 'b) ->
           ('a Op1.t -> 'b Op1.t) -> ('a, 'a Op1.t) t -> ('b, 'b Op1.t) t
       is not included in
         val map :
           ('a -> 'b) -> ('a_t -> 'b_t) -> ('a, 'a_t) t -> ('b, 'b_t) t
   *)
  let rec map f g n = match n with
    | Leaf  (a, b)    -> Leaf  (f a, g b)
    (* possibly because rec call is applied to specialized sub-tree *)
    | Inner (a, x, y) -> Inner (f a, map f (Op1.map f) x, map f g y)
end

This modified version of Impl.map fixed the problem but introduces a maintenance hazard.

  let rec map f g n = match n with
    | Leaf  (a, b)    -> Leaf  (f a, g b)
    | Inner (a, x, y) -> Inner (f a, map_spec f x, map f g y)
  and map_spec f n = match n with
    | Leaf  (a, b)    -> Leaf  (f a, Op1.map f b)
    | Inner (a, x, y) -> Inner (f a, map_spec f x, map_spec f y)

Is there any way to get this to work without duplicating the body of let rec map?

---

Applying gasche's solution yields the following working code:

let rec map
    : 'a 'b 'c 'd . ('a -> 'b) -> ('c -> 'd) -> ('a, 'c) t -> ('b, 'd) t
  = fun f g n -> match n with
    | Leaf  (a, b)    -> Leaf  (f a, g b)
    | Inner (a, x, y) -> Inner (f a, map f (Op1.map f) x, map f g y)

Answer 1

This style of recursion in datatype definitions is called "non-regular": the recursive type 'a t is reused at an instance foo t where foo is different from the single variable 'a used in the definition. Another well-known example is the type of full binary trees (with exactly 2^n leaves):

type 'a full_tree =
  | Leaf of 'a
  | Node of ('a * 'a) full_tree

Recursive functions that operate these datatypes typically suffer from the monomorphic recursion restriction of languages with type inference. When you do type inference you have to make a guess at what the type of a recursive function may be, before type-checking its body (as it may be use inside). ML languages refine this guess by unification/inference, but only monomorphic types may be inferred. If your function makes polymorphic uses of itself (it calls itself recursively on a different type that what it took as input), this cannot be inferred (it is undecidable in the general case).

let rec depth = function
| Leaf _ -> 1
| Node t -> 1 + depth t
                      ^
   Error: This expression has type ('a * 'a) full_tree
   but an expression was expected of type 'a full_tree

Since 3.12, OCaml allows to use an explicit polymorphic annotation of the form 'a 'b . foo, meaning forall 'a 'b. foo:

let rec depth : 'a . 'a full_tree -> int = function
| Leaf _ -> 1
| Node t -> 1 + depth t

You could do the same in your example. However, I wasn't able to compile the type after using the annotation you have in your module signature, as it appear to be wrong (the 'a_t are just weird). Here is what I used to make it work:

let rec map : 'a 'b . ('a -> 'b) -> ('a Op1.t -> 'b Op1.t) ->
                      ('a, 'a Op1.t) t -> ('b, 'b Op1.t) t
= fun f g n -> match n with
  | Leaf  (a, b)    -> Leaf  (f a, g b)
  | Inner (a, x, y) -> Inner (f a, map f (Op1.map f) x, map f g y)