Trying to understand this GADT typing



Seems I had it wrong about that Nothing.t type and could simplify this anyways.

Hello! I’ve been playing around with GADTs lately and was wondering if anybody could point me in the right direction for learning how to type this so it would compile, if it’s possible, or if I’m overly complicating things.

I’ve seen this type of thing done to represent a type with no possible values:

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

So I wanted to use it to lock down this Exit.t type so I could have a type of Exit.t('a, Nothing.t) to represent the Success case, capturing the fact that there is no recoverable Failure value.

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

This seemed to be okay, until I tried to write a flatMap function for it.

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

As is, it is inferring type Exit.t to always be Exit.t(Nothing.t, Nothing.t) which, I kind of understand since the type in the Failure case would set the first type to Nothing and the Success case would set the second type to Nothing.

I’ve tried the one thing I know, making some of those types local using type a. I’ve tried type a a1 e and type a e leaving 'a1 but I just don’t seem to be able to capture the idea.