Hi,
   
   Objective Caml's subtyping algorithm does not subtype under type
   constructors (but it does it under abbreviations), for the sake of
   efficiency. That is, eventhough colored_point :> point, you don't have
   colored_point option :> point option. This equation would be needed to
   check the subtyping in method move of example 2.
   
I must say I am really surprised.  

How about object types? Do they support co(ntra)-variant
subtype rules?

I would suggest to include a section about the subtype relation
in the ocaml documentation. Because IMHO anybody how knows
something about formal models for oo languages would expect
co(ntra)-variant subtype rules. 

In summary I think the lack of these subtype rules are a major
restriction of the ocaml language. Now it is not possible to mix
class types and (algebraic) data types in an application. Instead
a user has to decide beforehand what is more important for him:
algebraic data types and parametric polymorphism or object types
with code reuse and stepwise refinement.

Are there any plans to add the missing subtype rules to the type
system of ocaml?

Bye,

Hendrik