Visible refinement of class methods

Question

consider the following small ocaml class hierarchy:

class x = object method i = 0 end ;;
class y = object method x = new x end ;;
class x2 = object method i = 0 method j = 1 end ;;
class z = object method x = new x2 inherit y end;; (* type error *)

What I want to achieve is to refine the field x of class z w.r.t. class y and have that refinement visible at the type of z, i.e.

class z = object method x = (new x2 :> x) inherit y end;; 
(new z)#x#j;; (* type error *)

is not what I want to achieve.

I am pretty confident that there is a way to convinve the type checker of the compatibility of the refinement, but how?

Answer 1

It looks like it is difficult to do this directly: if you try to relax the type of method x in y using a type parameter,

class ['a] y = object
  constraint 'a = #x
  method x = new x
end

you can see that the type-checker forces 'a to be exactly x and not any subtype #x of x:

class ['a] y = object
  constraint 'a = x
  method x = new x
end

which will thus preclude any attempt to redefine method x with another type. However, it is possible to define classes that expects an object of type #x as argument, and to derive the original class y and class z from them:

class x = object method i = 0 end ;;

class ['a] y_gen (x:'a) = object
  constraint 'a = #x
  method x = x end
;;

class y = object inherit [x] y_gen (new x) end

class x2 = object method i = 0 method j = 1 end ;;

class ['a] z_gen (x:'a) = object
  constraint 'a = #x2
  inherit ['a] y_gen x
  method! x = x 
end;;

class z = object inherit [x2] z_gen (new x2) end

Furthermore, z is indeed a subtype of y, i.e. the following is correctly type-checked:

let my_z = new z
let my_y = (my_z :> y)