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?

Flick

Somone will hopefully be able to provide a more accurate and detailed answer, but AIUI OCaml does not have implicit subtype coercion because it'd make type inference undecidable. So you have to do it explicitly using the coercion operator: Foo 0 :> ([< a | b]) t – Benge

Are you really sure you want [< `a|`b], and not [> `a|`b] ? Types in return position should almost always be ">" types. – Burchette

@Benge thanks! That works. – Flick

@Burchette I believe so, for now ... but I'm still iterating on the design, I might settle for something else ultimately! – Flick

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

Erratum

Perfect, thanks! Key insight here. OCaml doesn't implicitly upcast. – Flick

The cast in this answer only works because 'a is a phantom type - it would let you cast to any type here. As mentioned in the comments on the question, you probably want > rather than < on the type. – Academic