[Caml-list] polymorphic variants in match statements

["Milan Stanojević" <milanst@gmail.com>]

Hi, we're trying to understand the type inference with polymorphic
variants in match statements. This is a simplification of an actual
case that happened in practice.

1)
let f i a =
  match i, a with
  | true, `A -> `B
  | false, x -> x

fails with
File "foo.ml", line 4, characters 16-17:
Error: This expression has type [< `A ]
       but an expression was expected of type [> `B ]
       The first variant type does not allow tag(s) `B

2) changing false to _
let f i a =
  match i, a with
  | true, `A -> `B
  | _, x -> x

this succeeds with
val f : bool -> ([> `A | `B ] as 'a) -> 'a

3) changing x in (1) to _ , and using a on the right side
let f i a =
  match i, a with
  | true, `A -> `B
  | false, _ -> a

this fails in the same way as (1)

4) finally adding another case to match statement
let f i a =
  match i, a with
  | true, `A -> `B
  | false, x -> x
  | true, x -> x

this succeeds with the same type as (2)


So it seems there is some interaction between type inference and
exhaustivnest of the match statements.

Can someone shed some light on what is going on here?