Hello everyone,

     I stumbled on the following confusing behaviour of the type 
checker: given the definitions

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

    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

     the following type is inferred for the class m:

     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

    Perhaps some explicit annotation is needed here (like that for the 
polymorphic recursion
for functions).
    I found the following workaround: first we abstract the instance 
creation ("new m") 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

   which gives us the unconstrained type

    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

   Then we construct the instance creation explicitly polymorphic function:

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

  and finally the class we're looking for:

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

    The complete annotated source file is attached.
    This workaround however does not solve everything: we cannot 
actually inherit
from the m since it calls hardcoded "new m"; we should inherit from m' 
(with additional parameter)
instead and "tie the knot" on the toplevel.
     Are there better solutions? Please help :)

     Best regards,
     Dmitry Boulytchev,
     St.Petersburg State University,
     Russia.