Search code examples
ocamlpolymorphic-variants

ocaml polymorphic variant type inferred type too general

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?

Solution

  • 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 1, 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))