[4.14] Type [> Cycle ] is not compatible with type [> Cycle ]

[kit-ty-kate]

I got this error when compiling capnp-rpc.1.2.1 with the 4.14 branch (3f170f3)

#=== ERROR while compiling capnp-rpc.1.2.1 ====================================#
# context              2.1.1 | linux/x86_64 | ocaml-variants.4.14.0+trunk | file:///home/opam/opam-repository
# path                 ~/.opam/4.14/.opam-switch/build/capnp-rpc.1.2.1
# command              ~/.opam/opam-init/hooks/sandbox.sh build dune build -p capnp-rpc -j 71
# exit-code            1
# env-file             ~/.opam/log/capnp-rpc-19-6699a9.env
# output-file          ~/.opam/log/capnp-rpc-19-6699a9.out
### output ###
#       ocamlc capnp-rpc/.capnp_rpc.objs/byte/capnp_rpc__Struct_proxy.{cmi,cmo,cmt} (exit 2)
# (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -g -bin-annot -I capnp-rpc/.capnp_rpc.objs/byte -I /home/opam/.opam/4.14/lib/asetmap -I /home/opam/.opam/4.14/lib/astring -I /home/opam/.opam/4.14/lib/fmt -I /home/opam/.opam/4.14/lib/logs -I /home/opam/.opam/4.14/lib/stdint -no-alias-deps -open Capnp_rpc__ -o capnp-rpc/.capnp_rpc.objs/byte/capnp_rpc__Struct_proxy.cmo -c -impl capnp-rpc/struct_proxy.ml)
# File "capnp-rpc/struct_proxy.ml", line 1:
# Error: The implementation capnp-rpc/struct_proxy.ml
#        does not match the interface (inferred signature):  ... ...
#        In module Make:
#        Class declarations do not match:
#          class virtual ['promise] t :
#            'promise ->
#            object
#              val mutable blocker : C.base_ref option
#              val id : Capnp_rpc__.Debug.OID.t
#              val virtual name : string
#              val mutable state : 'promise state
#              method blocker : C.base_ref option
#              method cap : C.Wire.Path.t -> C.cap
#              method check_invariants : unit
#              method clear_blocker : unit
#              method private virtual do_pipeline :
#                'promise ->
#                C.Wire.Path.t -> C.struct_resolver -> C.Wire.Request.t -> unit
#              method field_blocker : C.Wire.Path.t -> C.base_ref option
#              method field_check_invariants : Field_map.key -> unit
#              method field_dec_ref : Field_map.key -> unit
#              method field_pp : Field_map.key -> Format.formatter -> unit
#              method private field_resolved : C.cap -> unit
#              method virtual field_sealed_dispatch :
#                C.Wire.Path.t -> 'a Capnp_rpc__.S.brand -> 'a option
#              method field_update_rc : Field_map.key -> int -> unit
#              method field_when_resolved :
#                C.Wire.Path.t -> (C.cap -> unit) -> unit
#              method private virtual on_resolve :
#                'promise -> C.struct_ref -> unit
#              method pipeline :
#                C.Wire.Path.t -> C.struct_resolver -> C.Wire.Request.t -> unit
#              method pp : Format.formatter -> unit
#              method private virtual pp_unresolved : 'promise Fmt.t
#              method resolve : C.struct_ref -> unit
#              method resolver : C.struct_resolver
#              method response : C.Wire.Response.t C.or_error option
#              method sealed_dispatch : 'a Capnp_rpc__S.brand -> 'a option
#              method private virtual send_cancel : 'promise -> unit
#              method set_blocker : C.base_ref -> (unit, [> `Cycle ]) result
#              method update_rc : int -> unit
#              method private update_target : 'promise -> unit
#              method when_resolved :
#                (C.Wire.Response.t C.or_error -> unit) -> unit
#            end
#        does not match
#          class virtual ['promise] t :
#            'promise ->
#            object
#              val mutable blocker : C.base_ref option
#              val id : Capnp_rpc__.Debug.OID.t
#              val virtual name : string
#              val mutable state : 'promise state
#              method blocker : C.base_ref option
#              method cap : C.Wire.Path.t -> C.cap
#              method check_invariants : unit
#              method clear_blocker : unit
#              method private virtual do_pipeline :
#                'promise ->
#                C.Wire.Path.t -> C.struct_resolver -> C.Wire.Request.t -> unit
#              method field_blocker : C.Wire.Path.t -> C.base_ref option
#              method field_check_invariants : Field_map.key -> unit
#              method field_dec_ref : Field_map.key -> unit
#              method field_pp : Field_map.key -> Format.formatter -> unit
#              method private field_resolved : C.cap -> unit
#              method virtual field_sealed_dispatch :
#                C.Wire.Path.t -> 'a Capnp_rpc__.S.brand -> 'a option
#              method field_update_rc : Field_map.key -> int -> unit
#              method field_when_resolved :
#                C.Wire.Path.t -> (C.cap -> unit) -> unit
#              method private virtual on_resolve :
#                'promise -> C.struct_ref -> unit
#              method pipeline :
#                C.Wire.Path.t -> C.struct_resolver -> C.Wire.Request.t -> unit
#              method pp : Format.formatter -> unit
#              method private virtual pp_unresolved : 'promise Fmt.t
#              method resolve : C.struct_ref -> unit
#              method resolver : C.struct_resolver
#              method response : C.Wire.Response.t C.or_error option
#              method sealed_dispatch : 'a Capnp_rpc__S.brand -> 'a option
#              method private virtual send_cancel : 'promise -> unit
#              method set_blocker : C.base_ref -> (unit, [> `Cycle ]) result
#              method update_rc : int -> unit
#              method private update_target : 'promise -> unit
#              method when_resolved :
#                (C.Wire.Response.t C.or_error -> unit) -> unit
#            end
#        The method set_blocker has type
#          C.base_ref -> (unit, [> `Cycle ]) result
#        but is expected to have type C.base_ref -> (unit, [> `Cycle ]) result
#        Type [> `Cycle ] is not compatible with type [> `Cycle ] 

[Octachron]

This is a change of behavior introduced by 6e5b863 in #8516.

The capnp-rpc code can be reduced to:

class type ct = object
  method m : [> `A]
end
class virtual c = object (self: 'self)
  method m = `A
  method fix = (self :> ct)
end

The unbound type variable in the definition of the method m is bound indirectly by the coercion to ct, and what happens afterward depends on which side of #8516 we are.
(Both using an explicit constraint on 'self or an explicit universal quantification in m fixes the issue for all version.)

[Octachron]

Having another looks, a similar example is rejected in previous version of OCaml

class always_rejected = object (self)
  method x = None
  method me = (self :> < x: 'a. 'a option ; .. > )
end

so the pre-4.14 behavior for polymorphic variants is really brittle.

[kit-ty-kate]

After talking with @Octachron who seems to think this change of behaviour is expected. I’ve sent a fix to the package affected by this change (mirage/capnp-rpc#244)

However we agreed that the error message should at least be improved a little from:

Type [> `Cycle ] is not compatible with type [> `Cycle ] 

to something like:

Type [> `Cycle ] as 'a is not compatible with type [> `Cycle ] as 'b

or similar, to help users encountering this issue enderstanding that the issue is not in the type-checker but a the type-system limitation.

[Octachron]

I still plan to address this issue at some point. However, printing the ... as 'a annotation when the annotation is useful requires more work on the type printer: I am thus moving the issue to after 5.0 .