[Caml-list] strange type inference for polymorphic variants

["Török Edwin" <edwin+ml-ocaml@etorok.net>]

Hi,

If I use a polymorphic variant in a match case that has a _ branch then I get an "interesting" type inferred,
 for example: [< `A of a | `B of a > `A ], instead of: [< `A of a | `B of a ].
To make it work I have to list all possibilities instead of _, _.

I always use `A with a parameter of type a, it seems strange that OCaml would infer `A without a parameter.
Also the inferred type ([< `A of a | `B of a > `A ]) does actually accept both [`A of a] and [`B of a] as input,
and doesn't accept `A without a parameter, so what is the difference between the inferred type and the one I wrote in the signature
([< `A of a | `B of a])?

Here is some simplified code that fails to compile:

$ ocaml
        OCaml version 4.00.1

# type a = string * string;;
type a = string * string
# module Bad3 : sig
  val copy: [< `A of a | `B of a ] -> [< `A of a | `C of a] -> unit
end = struct
  let generic (a: [< `A of a | `B of a]) (b: [< `A of a | `C of a]) = ()
  let specific a b = false
  let copy a b = match a, b with
  | `A x, `A y ->
      if not (specific (`A x) (`A y)) then
        generic a b
  | _, _ ->
      generic a b
end;;
Error: Signature mismatch:
       ...
       Values do not match:
         val copy :
           [< `A of a | `B of a > `A ] -> [< `A of a | `C of a > `A ] -> unit
       is not included in
         val copy : [< `A of a | `B of a ] -> [< `A of a | `C of a ] -> unit


And here is some code that works:
module OK : sig
  val copy: [< `A of a | `B of a ] -> [< `A of a | `C of a] -> unit
end = struct
  let generic (a: [< `A of a | `B of a]) (b: [< `A of a | `C of a]) = ()
  let specific a b = false
  let copy a b = match a, b with
    | `A x, `A y when specific (`A x) (`A y) -> ()
    | (`A _ | `B _), (`A _ | `C _ ) ->
      generic a b
end;;

Here are a few other ways to write the same code which result in an error:
module Bad1: sig
  val test: [< `A of a | `B of a ] -> [< `A of a | `C of a] -> unit
end = struct
  let generic (a: [< `A of a | `B of a]) (b: [< `A of a | `C of a]) = ()
  let specific (a: [`A of a]) (b:[`A of a]) = false
  let test a b =
    let use_specific = match a, b with
      | `A x, `A y -> specific (`A x) (`A y)
      | _, _ -> false in
    if not use_specific then
      generic a b;;
end;;

module Bad2 : sig
  val copy: [< `A of a | `B of a ] -> [< `A of a | `C of a] -> unit
end = struct
  let generic (a: [< `A of a | `B of a]) (b: [< `A of a | `C of a]) = ()
  let specific (a: [`A of a]) (b:[`A of a]) = false
  let copy a b = match a, b with
    | `A x, `A y when specific (`A x) (`A y) ->
        ()
    | _, _ ->
        generic a b
end;;

Best regards,
--Edwin