type ('a, 'b) t = 
    A of 'a * ('b, 'a) t 
  | B of 'a

(*
   The initial definition

   class ['a, 'b, 'ta, 'tb] m =
     object
       method t : ('a -> 'ta) -> ('b -> 'tb) -> ('a, 'b) t -> ('ta, 'tb) t = 
         fun fa fb s ->
           match s with
           | A (a, bat) -> A (fa a, (new m)#t fb fa bat)
           | B  a       -> B (fa a)
     end

   gives us the following type:

   class ['a, 'b, 'ta, 'c] m :
     object
       constraint 'b = 'a  <--- why?
       constraint 'c = 'ta <--- why?
       method t : ('a -> 'ta) -> ('a -> 'ta) -> ('a, 'a) t -> ('ta, 'ta) t
     end
*)

(* The modified version with the "new" abstracted away: *)

class ['a, 'b, 'ta, 'tb] m' f =
  object
    method t : ('a -> 'ta) -> ('b -> 'tb) -> ('a, 'b) t -> ('ta, 'tb) t = 
      fun fa fb s ->
        match s with
        | A (a, bat) -> A (fa a, (f ())#t fb fa bat)
        | B  a       -> B (fa a)
  end

(* Inferred type with no artificial constraints:

   class ['a, 'b, 'ta, 'tb] m' :
     (unit ->
      < t : ('b -> 'tb) -> ('a -> 'ta) -> ('b, 'a) t -> ('tb, 'ta) t; .. >) ->
      object
        method t : ('a -> 'ta) -> ('b -> 'tb) -> ('a, 'b) t -> ('ta, 'tb) t
      end
*)

(* Instance creation function: *)

let rec f : 'a 'b 'ta 'tb . unit -> <t : ('a -> 'ta) -> ('b -> 'tb) -> ('a, 'b) t -> ('ta, 'tb) t> = 
  fun () -> new m' f

class ['a, 'b, 'ta, 'tb] m = ['a, 'b, 'ta, 'tb] m' f

(* Ok now:
   class ['a, 'b, 'ta, 'tb] m' : ['a, 'b, 'ta, 'tb] m
*)