Использование вариантов GADT в полиморфном составном типе, как в обычных алгебраических вариантах?

Я, конечно, не эксперт по GADT, но это больше похоже на ограничение переменных обычного типа, чем на GADT. flag word и string word — это разные типы, которые не поместятся в один и тот же массив, несмотря ни на что.

Я предполагаю, что вам нужна экзистенциально квантифицированная переменная типа. Если это так, переменная экзистенциального типа должна встречаться только слева от стрелки. Кажется, это работает:

type word =
 | Arg : string -> word
 | Flag : flag -> word

Или, говоря словами руководства:

Переменные становятся экзистенциальными, когда они появляются внутри аргумента конструктора, но не в его возвращаемом типе.

Редактировать: нет, как указывает @octachron в комментарии, это не то, как работают экзистенциальные типы. Вернее, переменные экзистенциального типа, которых в моем примере нет. Причина та же, но я не совсем понимаю, какое свойство GADT требуется здесь и каково, следовательно, решение.

Это не столько ограничение GADT, сколько одно из их желаемых свойств. Когда вы пишете

type _ word =
| Arg : string -> string word
| Flag : flag -> flag word

вы просите средство проверки типов сделать типы Arg _ и Flag _ разными и несовместимыми.

Чтобы мотивировать такое поведение, лучшим примером может быть список со статической длиной:

 type zero = Zero
 type 'a succ = Succ
 type ('elt,'size) nlist =
 | []: ('elt, zero) nlist
 | (::): 'elt * ('elt, 'size) nlist ->  ('elt, 'size succ) nlist

При таком определении значение типа ('n, 's) nlist содержит кодировку своей длины внутри этого типа. Это позволяет написать всего hd функций

  let hd (a::q) = a

Так как наш экзотический тип списка несет свою длину в своем типе, программа проверки типов может выразить тот факт, что hd принимает список только с одним или несколькими аргументами (т. е. тип hd — ('elt,_ succ) nlist -> 'elt). Таким образом, функция hd всегда возвращает значение (при проверке ее типа).

Но это также означает, что проверка типов теперь должна обеспечивать, чтобы функция hd всегда работала. Другими словами, массив смешивания длины разного размера

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

нельзя разрешить проверку типов, поскольку он содержит элемент, для которого функция hd не определена четко, а средство проверки типов, гарантированное нам до hd, всегда будет возвращать успешное значение.

Возвращаясь к вашему примеру, с вашим определением типа вы сделали возможным различать Flag _ и Int _. Таким образом, я могу написать следующую общую функцию

 let empty (Arg _) = ""
 let map_empty = Array.map empty

и ожидайте, что map_empty работает со всеми хорошо типизированными массивами. Но я не могу применить эту функцию к вашему смешанному массиву

 let args = [|
   Arg "hello";
   Flag {name = "foo"; payload = Some "world"};
 |]

Другими словами, этот массив не может быть хорошо типизирован.

Обычный способ справиться с этой ситуацией с помощью GADT — ввести экзистенциальные оболочки (здесь 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 содержит word индекса неизвестного типа, этот индекс скрыт внутри оболочки any_word. В противоположность,

let flag_args = [|
  Flag {name = "zonk"; payload = None};
  Flag {name = "splines"; payload = Some "reticulate"};
|]

flag_args содержит конкретно flag words. string word исключаются системой типов, что является одной из привлекательных сторон GADT. (Если вам это не нужно, GADT вряд ли вам помогут.)