Сопоставление с образцом в GADT не удается

Краткий ответ заключается в том, что GADT делают систему типов слишком выразительной, чтобы ее можно было полностью вывести. Например, в вашем случае следующие функции являются общими (иначе говоря, они обрабатывают все возможные значения своего ввода

let one = (One) => None
let two = (Two) => None

Вы можете проверить их общее количество, добавив пункт явного опровержения в синтаксисе OCaml (синтаксис Reason еще не обновлен, чтобы включить их):

let one = function
| One -> None
| _ -> .

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

Следовательно, вам нужно сообщить средству проверки типов, что вы собираетесь сопоставить значение типа t(a) для любого a, это необходимо сделать с локально абстрактными типами:

let x (type a, (x:t(a))) = switch(x){
| One => None
| Two => None
}

С помощью этой локально абстрактной аннотации средство проверки типов знает, что не предполагается заменять эту переменную a конкретным типом глобально (иначе говоря, он должен учитывать, что локально a является некоторым неизвестным абстрактным типом), но он может уточнить его локально при сопоставлении с GADT .

Строго говоря, аннотация нужна только на выкройке, поэтому вы можете написать

let x (type a) = fun
| (One:t(a)) => None
| Two => None

Обратите внимание, что для рекурсивных функций с GADT вам может потребоваться использовать полные явно полиморфные локально абстрактные обозначения типов:

type t(_) =
| Int(int): t(int)
| Equal(t('a),t('a)):t(bool)

let rec eval: type any. t(any) => any = fun
| Int(n) => n
| Equal(x,y) => eval(x) = eval(y)

где разница в том, что eval рекурсивно полиморфен. См. https://caml.inria.fr/pub/docs/manual-ocaml-4.09/polymorphism.html#sec60.

РЕДАКТИРОВАТЬ: аннотирование возвращаемого типа

Другая аннотация, которая часто требуется, чтобы избежать ужасного «этот тип выйдет за пределы своей области действия», - это добавить аннотацию при выходе из сопоставления с образцом. Типичным примером может служить функция:

let zero (type a, (x:t(a)) = switch (x){
| One => 0
| Two => 0.
}

Здесь есть двусмысленность, потому что внутри ветви One проверка типов знает, что int=a, но, покидая этот контекст, он должен выбрать одну или другую сторону уравнения. (В этом конкретном случае, оставленный на собственном устройстве, проверка типов решает, что (0: int) является более логичным выводом, потому что 0 является целым числом, и этот тип никоим образом не контактировал с локально абстрактным типом a.)

Этой неоднозначности можно избежать, используя явную аннотацию, либо локально

let zero (type a, (x:t(a))) = switch (x){
| One => ( 0 : a )
| Two => ( 0. : a )
}

или в целом функция

let zero (type a): t(a) => a = fun
| One => 0
| Two => 0.

Кто-то, вероятно, скоро придет и даст правильное объяснение, но краткий ответ заключается в том, что вам нужно использовать локально абстрактный тип вместо переменной типа.

let x: type a. t(a) => option(a) =
  fun
  | One => None
  | Two => None;

Почему? Что ж, для меня это все еще загадка, особенно в этом случае, когда это всего лишь фантомный тип и никакие фактические значения типа не задействованы. Но я подозреваю, что это частично объясняется этим абзацем (или следующим) из руководства:

Вывод типа для GADT, как известно, сложен. Это связано с тем, что некоторые типы могут стать неоднозначными при выходе из ветки. Например, в приведенном выше случае Int, n может иметь тип int или a, и они не эквивалентны за пределами этой ветви. В первом приближении вывод типа всегда будет работать, если сопоставление с образцом аннотировано типами, не содержащими переменных свободного типа (как для проверяемого, так и для возвращаемого типа). Так обстоит дело в приведенном выше примере благодаря аннотации типа, содержащей только локально абстрактные типы.