GADTs allow one to statically enforce stronger program invariants than are otherwise possible in a Hindley-Milner style type system. This post retells the story of how to “roll your own” GADTs using an explicit type of equality constraints. More interestingly, we discuss a particularly versatile definition of type equality in Haskell that can now be transcribed into OCaml due to the recent additio