If I have a type parameter that appears in both covariant and contravariant positions, then it is invariant, and OCaml will not allow me to annotate the parameter with + or -. For example, this class of mutable references:

class ['a] rw (init : 'a) = object
  val mutable v = init
  method get = v
  method set x = v <- x
end

This code will not compile with [+'a] or [-'a]. However, the class can be (manually) decomposed into separate covariant and contravariant parts:

class [+'a] ro (init : 'a) = object val mutable v = init method get = v end
class [-'a] wo (init : 'a) = object val mutable v = init method set x = v <- x end
class ['a] rw init = object inherit ['a] ro init inherit! ['a] wo init end

I can always coerce from 'a rw to 'a ro or 'a wo, when I want to restrict access to the reference as read-only or write-only. Those types will then allow coercions that would not be permitted on 'a rw. For example, given this pair of classes:

class super = object end
class sub = object method foo = () end

The compiler will accept (new ro (new sub) :> super ro) as well as (new wo (new super) :> sub wo).

However, I didn't actually need to annotate the type parameters in my definitions of 'a ro and 'a wo; OCaml would have inferred them. And these coercions are all compile-time operations.

So, it seems that the OCaml type checker knows which methods of my first definition of 'a rw use 'a in a covariant or contravariant position. Would it be possible to implement use-site variance in OCaml based on this?

I'm imagining an expression like (new rw 0 :> +'a rw) that would give an object of type 'a ro, without the programmer having to declare any such type, or decompose his class manually. OCaml would automatically select only those methods where 'a appears only in covariant positions. Similarly, -'a rw would produce an object of type 'a wo.

Is this feasible, or is the situation more complicated than I've described?