OCaml function over polymorphic variants not sufficiently polymorphic?

Question

OCaml gives function `A -> 1 | _ -> 0 the type [> `A] -> int, but why isn't that [> ] -> int?

This is my reasoning:

• function `B -> 0 has type [<`B] -> int. Adding a `A -> 0 branch to make it function `A -> 1 | `B -> 0 loosens that to [<`A|`B] -> int. The function becomes more permissive in the type of argument it can accept. This makes sense.
• function _ -> 0 has type 'a -> int. This type is unifiable with [> ] -> int, and [> ] is an already open type (very permissive). Adding the `A -> 0 branch to make it function `A -> 1 | _ -> 0 restricts the type to [>`A] -> int. That doesn't make sense to me. Indeed, adding still another branch `C -> 1 will make it [>`A|`C] -> int, further restricting the type. Why?

Note: I am not looking for workarounds, I'd just like to to know the logic behind this behavior.

On a related note, function `A -> `A | x -> x has type ([>`A] as 'a) -> 'a, and while that is also a restrictive open type for the parameter, I can understand the reason. The type should unify with 'a -> 'a, [>` ] -> 'b, 'c -> [>`A]; the only way to do it seems to be ([>`A] as 'a) -> 'a.

Does it exist a similar reason for my first example?

Answer 1

A possible answer is that the type [> ] -> int would allow an argument (`A 3) but this isn't allowed for function `A -> 1 | _ -> 0. In other words, the type needs to record the fact that `A takes no parameters.

Answer 2

The reason is a very practical one:
In older versions of OCaml the inferred type was

[`A | .. ] -> int

which meant that A takes no argument but may be absent.

However this type is unifiable with

[`B |`C ] -> int

which results in `A being discarded without any kind of check.

It makes easy introducing errors with misspellings.
For this reason variant constructors must either appear in an upper or a lower bound.

Answer 3

The typing of (function `A -> 1 | _ -> 0) is reasonable, as explained by Jeffrey. The reason why

(function `A -> 1 | _ -> 0) ((fun x -> (match x with `B -> ()); x) `B)

fails to type-check should be explained, in my opinion, by the latter part of the expression. Indeed the function (fun x -> (match x with `B -> ()); x) has input type [< `B] while its parameter `B has type [> `B ]. The unification of both types gives the closed type [ `B ] which is not polymorphic. It cannot be unified with the input type [> `A ] that you get from (function `A -> 1 | _ -> 0).

Fortunately, polymorphic variants do not only rely on (row) polymorphism. You can also use subtyping in situations, such as this, one where you want to enlarge a closed type: [ `B ] is a subtype of, for example, [`A | `B] which is an instance of [> `A ]. Subtyping casts are explicit in OCaml, using the syntax (expr :> ty) (casting to some type), or (expr : ty :> ty) in case the domain type cannot be inferred correct.

You can therefore write:

let b = (fun x -> (match x with `B -> ()); x) `B in
(function `A -> 1 | _ -> 0) (b :> [ `A | `B ])

which is well-typed.