Polymorphic variant subtype implementation does not match signature

Question

I have the following code:

module Test : sig
  type +'a t
  val make : int -> [< `a | `b] t
end = struct
  type 'a t = Foo of int | Bar of string

  let make = function
    | 0 -> (Foo 0 : [`a] t)
    | _ -> (Bar "hi" : [`a] t)
end

As you may note, the abstract type 'a t is declared as being covariant in its type parameter 'a, and the make constructor is declared as returning a subtype of the polymorphic variant cases a or b.

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

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 really is returning a valid subtype of [a | b] t?

Answer 1

I did some experiments:

# type 'a t = Foo of int | Bar of string;;
type 'a t = 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, apparently OCaml does recognize the supertype relationship but still prefers to stick to the more exact subtype unless given a coercion. Others may know the type theoretic reasons. But as your question was just

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

my answer is: Use coercions like so

module Test : sig
  type +'a t
  val make : int -> [< `a | `b] t
end = struct
  type 'a t = Foo of int | Bar of string

  let make = (function
    | 0 -> (Foo 0 : [`a] t)
    | _ -> (Bar "hi" : [`a] t)
    :> int -> [< `a | `b] t)
end