Argthtjtr

Let's say I have this simple variant-type:

type flag = {

  name: string;

  payload: string option;

}



type word =

 | Arg of string

 | Flag of flag



let args = [|

  Arg "hello";

  Flag {name = "foo"; payload = Some "world"};

|]

If, however, I want to add GADT-constraints to that word type,

type _ word =

 | Arg : string -> string word

 | Flag : flag -> flag word

… the compiler can no longer infer a general type for the members of args:

Line 12, 3:

  This expression has type flag word

       but an expression was expected of type string word

       Type flag is not compatible with type string

Is this simply a limitation of GADTs?

I'm certainly no expert on GADTs, but this seems more like a limitation of ordinary type variables than of GADTs. flag word and string word are distinct types that won't fit into the same array no matter what.

I assume what you want is an existentially quantified type variable. If so the existential type variable should only occur on the left side of the arrow. This seems to work:

type word =

 | Arg : string -> word

 | Flag : flag -> word

Or in the words of the manual:

Variables are made existential when they appear inside a constructor’s argument, but not in its return type.

Edit: Nope, as @octachron points out in a comment, this is not how existential types work. Or rather existential type variables, of which there are none in my example. The cause is the same, but I'm not entirely clear on what property of a GADT is desired here and what therefore the solution would be.

It is not so much a limitation of GADTs than one of their desired properties. When you write

type _ word =

| Arg : string -> string word

| Flag : flag -> flag word

you are asking the typechecker to make the type of Arg _ and Flag _ different and incompatible.

To motivate this behavior, a better example might be a list with a static length:

 type zero = Zero

 type 'a succ = Succ

 type ('elt,'size) nlist =

 | : ('elt, zero) nlist

 | (::): 'elt * ('elt, 'size) nlist ->  ('elt, 'size succ) nlist

With this definition a value of type ('n, 's) nlist carries an encoding of its length inside this type. This makes it possible to write a total hd function

  let hd (a::q) = a

Since our exotic list type carries its length in its type, the typechecker can express the fact that hd only accepts list with one or more argument (i.e. the type of hd is
('elt,_ succ) nlist -> 'elt). Thus the function hd always returns (when its type checks).

But this also means that the type checker must now enforce than the function hd always works. In other words, an array mixing length of different size

  [| ; [1]; [1;2] |]

cannot be allowed to type-check because it contains element for which the hd function is not well-defined and the type checker guaranteed to us earlier than hd will always return a successful value.

Returning to your example, with your type definition, you have made it possible to discriminate between Flag _ and Int _. Thus I can write the following total function

 let empty (Arg _) = ""

 let map_empty = Array.map empty

and expect than map_empty works on all well-typed arrays. But I cannot possibly apply this function to your mixed array

 let args = [|

   Arg "hello";

   Flag {name = "foo"; payload = Some "world"};

 |]

In other words, this array cannot be well-typed.

The usual way to handle this situation with GADTs is to introduce existential wrappers (here, any_word):

type flag = {

  name : string;

  payload : string option;

}



type _ word =

  | Arg : string -> string word

  | Flag : flag -> flag word



type any_word = Word : _ word -> any_word [@@unboxed]



let args = [|

  Word (Arg "hello");

  Word (Flag {name = "foo"; payload = Some "world"});

|]

args contains words of unknown type index, that index being hidden inside the any_word wrapper. In contrast,

let flag_args = [|

  Flag {name = "zonk"; payload = None};

  Flag {name = "splines"; payload = Some "reticulate"};

|]

flag_args contains flag words specifically. string words are excluded by the type system, which is one of the attractions of GADTs. (If you don't need this, GADTs are not likely to be helpful.)