The implementation of the polymorphic variant subtype does not match the signature

Question

I have the following code:

module Test : sig type +'at val make : int -> [< `a | `b] t end = struct type 'at = Foo of int | Bar of string let make = function | 0 -> (Foo 0 : [`a] t) | _ -> (Bar "hi" : [`a] t) end 

As you can see, the abstract type 'at declared as covariant in its parameter of type 'a , and the constructor make declared as returning a subtype of variants of the polymorphic variant a or b .

In my make implementation, the return of the subtype [a] t must still follow the covariance rule, since the subtype is in the position of the return type.

However, I get the following error:

 Error: Signature mismatch: ... Values do not match: val make : int -> [ `a ] t is not included in val make : int -> [< `a | `b ] t File ".../cov.ml", line 3, characters 3-34: Expected declaration File ".../cov.ml", line 7, characters 7-11: Actual declaration 

Any suggestions on how to convince OCaml that the make function does indeed return a valid subtype [a | b] t [a | b] t ?

Answer 1

I did some experiments:

 # type 'at = Foo of int | Bar of string;; type 'at = Foo of int | Bar of string # let make = function | 0 -> (Foo 0 : [`a] t) | _ -> (Bar "hi" : [`a] t);; val make : int -> [ `a ] t = <fun> # (make : int -> [< `a | `b] t);; - : int -> [ `a ] t = <fun> # let make2 : int -> [< `a | `b] t = make;; val make2 : int -> [ `a ] t = <fun> # let make3 = (make :> int -> [< `a | `b] t);; val make3 : int -> [< `a | `b ] t = <fun> 

So, obviously, OCaml recognizes supertype relationships, but still prefers to stick to a more precise subtype, unless resorting to coercion. Others may know the theoretical reasons. But since your question was just

[...] how to convince OCaml [...]

my answer is: use such coercion

 module Test : sig type +'at val make : int -> [< `a | `b] t end = struct type 'at = Foo of int | Bar of string let make = (function | 0 -> (Foo 0 : [`a] t) | _ -> (Bar "hi" : [`a] t) :> int -> [< `a | `b] t) end