Re: [Caml-list] GADT+polymorphic variants quirk

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

Let us just say that using polymorphic variant or object types as
indices of GADTs are not explicitly supported. In your case, it seems
that the problem is that unification including abstract rows does not
work correctly. This can be classified as a (known) bug, but it is not clear yet
when we will fix it.
I would suggest avoid using polymorphic variants here, using rather
a simple encoding:

   type whole = Whole
   type general = General

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

This should avoid these problems without any real loss of expressivity.

Jacques Garrigue

On 2016/12/28 05:04, Anton Bachin wrote:
> 
> 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