ocaml polymorphic variant type inferred type too general

Question

I have this code

let my_fun: [`X | `Y | `Z] -> [`Z | `Y] = function
  | `X -> `Y
  | x -> x

It won't compile with message

11 |   | x -> x
          ^
Error: This expression has type [ `X | `Y | `Z ]
       but an expression was expected of type [ `Y | `Z ]
       The second variant type does not allow tag(s) `X

Why can't the complire infer the type [Z |Y] if it is clear that `X can be never returned from the function?

Answer 1

Why can't the compiler infer the type [Z |Y] if it is clear that `X can be never returned from the function?

A simpler example is:

if false then 0 else "hello"

The compiler has to reject it because typing in ML languages requires that both branches have the same type ¹, and types int and string cannot be unified; this is true even though you could say that there is no chance the expression could ever evaluate to 0 (keep in mind however that formally speaking, it makes no sense to say we evaluate an expression that is not part of the language as defined).

In a match expression, the types of the left part of all clauses must unify to the type of the expression being matched. So x in the last clause has the same type as the implicit argument in function, which is the input type declared in the signature. This is true whether or not `X is a valid value in that context.

You need to enumerate all the cases that are valid; if you need this often in your code then you'd better write a dedicated function for that:

let f : ([> `Y | `Z ] -> [`Y | `Z ] option) = function
  | (`Y|`Z) as u -> (Some u) 
  | _ -> None;

For example:

# f `O;;
- : [ `Y | `Z ] option = None
# f `Y;;
- : [ `Y | `Z ] option = Some `Y

See also Set-Theoretic Types for Polymorphic Variants ^(pdf)

---

[1] For comparison, in Common Lisp, which is dynamically typed, the equivalent expression is valid; a static analysis as done by SBCL's compiler can infer its type, i.e. a string of length 5:

> (describe (lambda () (if nil 0 "hello")))
....
Derived type: (FUNCTION NIL
               (VALUES (SIMPLE-ARRAY CHARACTER (5)) &OPTIONAL))

Answer 2

If the type of x was inferred to be [`Y | `Z], then it couldn't be used at type [`X | `Y | `Z] which would be strange since it is bound to an argument of that type.

You can use as patterns to get a binding with a refined type, like this:

let my_fun: [`X | `Y | `Z] -> [`Y | `Z] = function
  | `X -> `Y
  | (`Y | `Z) as yz -> yz

The #type_name patterns can be very useful if you want to do this for polymorphic variants with many cases.