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

В последнее время я играл с GADT и задавался вопросом, может ли кто-нибудь указать мне в правильном направлении, чтобы научиться печатать это так, чтобы оно скомпилировалось, если это возможно, или я слишком усложняю вещи.

Я видел здесь несколько других ответов на сопоставление с образцом GADT, но, похоже, это немного другое.

Я видел, как это делается для представления типа без возможных значений:

module Nothing = {
  type t =
    | Nothing(t);
};

Поэтому я хотел использовать его, чтобы заблокировать этот тип Exit.t, чтобы у меня был тип Exit.t ('a, Nothing.t) для представления случая Success, фиксирующего тот факт, что нет восстанавливаемого значения Failure.

module Exit = {
  type t('a, 'e) =
    | Success('a): t('a, Nothing.t)
    | Failure('e): t(Nothing.t, 'e);

Это казалось нормальным, пока я не попытался написать для него функцию flatMap.

  let flatMap: ('a => t('a1, 'e), t('a, 'e)) => t('a1, 'e) = (f, exit) =>
    switch (exit) {
    | Success(a) => f(a)
    | Failure(_) as e => e
    };
};

Как есть, он подразумевает, что тип Exit.t всегда будет Exit.t (Nothing.t, Nothing.t), что, как я понимаю, поскольку тип в случае Failure установит для первого типа значение Nothing, а в случае Success будет установите для второго типа значение Nothing.

Я попробовал одну вещь, которую знаю, - сделать некоторые из этих типов локальными с помощью type a. Я пробовал type a a1 e и type a e оставить 'a1, но, похоже, мне просто не удалось уловить идею.