[Caml-list] GADT+polymorphic variants quirk

[Anton Bachin <antronbachin@gmail.com>]

Hello,

Consider this code for simulating an ad-hoc polymorphic addition
function:

    type whole = [ `Integer ]
    type general = [ whole | `Float ]

    type _ num =
      | I : int -> [> whole ] num
      | F : float -> general num

    module M :
    sig
      val add : ([< general ] as 'a) num -> 'a num -> 'a num
      val to_int : whole num -> int
      val to_float : general num -> float
    end =
    struct
      let add : type a. a num -> a num -> a num = fun a b ->
        match a, b with
        | I n, I m -> I (n + m)
        | F n, I m -> F (n +. float_of_int m)
        | F n, F m -> F (n +. m)
        | _ ->
          (* ----NOTE---- *)
          match b, a with
          | F m, I n -> F (float_of_int n +. m)
          | _ -> assert false

      let to_int : whole num -> int = fun (I n) -> n

      let to_float = function
        | I n -> float_of_int n
        | F n -> n
    end

    let () =
      M.add (I 1) (I 2)  |> M.to_int   |> Printf.printf "%i\n";
      M.add (I 1) (F 2.) |> M.to_float |> Printf.printf "%f\n"

Instead of the nested match expression (marked with (* NOTE *)), I would
have expected to just write

    | I n, F m -> ...

However, if I actually do that, the result is an error on the expression
in the case:

    Error: This expression has type general num
           but an expression was expected of type a num
           Type general = [ `Float | `Integer ] is not compatible with type
             a = [> `Integer ] 
           The second variant type does not allow tag(s) `Float

While the reversed case type-checks successfully. I can imagine why this
would be so, but I want to ask the experts on the mailing list.

Is this a known quirk of the typechecker? A bug? Is there some
alternative syntax I am missing that would allow the I n pattern to be
written first?

Note that there is a way to rewrite the nested match cases to avoid _
and maintain the exhaustiveness check. I wrote them out as above for
clarity. The actual solution I have settled on for now is:

      let add : type a. a num -> a num -> a num = fun a b ->
        match a, b with
        | I n, I m -> I (n + m)
        | F n, I m -> F (n +. float_of_int m)
        | _,   F m ->
          match a with
          | I n -> F (float_of_int n +. m)
          | F n -> F (n +. m)

Best,
Anton


P.S. If interested, the code was for this Stack Overflow question:

    http://stackoverflow.com/questions/41214000

answer:

    http://stackoverflow.com/a/41334879/2482998