Back in 2020, I created Cubiml, a simple ML-like language that demonstrated how to extend the usual Hindley–Milner type system with subtyping while still having decidable full type inference. One question I got was whether it would be possible to support generalized algebraic data types (GADTs) in Cubiml. I had heard that GADTs break type inference and didn’t see the point, so I didn’t think much of it at the time.

A Generalized Algebraic Data Type (GADT) is a generic ADT where some variants have specific type arguments, e.g.

data Expr a where
  EValue    :: a -> Expr a
  ELessThan :: Expr Int -> Expr Int -> Expr Bool
  EIfElse   :: Expr Bool -> Expr a -> Expr a -> Expr a

The post also mentions existential (existentially-quanitifed) types, which are types with a type variable in some variants which isn’t in the type itself, e.g.

data StringToFrom =
  forall a. StringToFrom (a -> String) (String -> a)

These are often combined like

data Expr a where
  EValue    :: a -> Expr a
  ELessThan :: Expr Int -> Expr Int -> Expr Bool
  EIfElse   :: Expr Bool -> Expr a -> Expr a -> Expr a
  EApply    :: forall a. Expr (a -> b) -> Expr a -> Expr b
  EEquals   :: forall a. Expr a -> Expr a -> Expr Bool

and this breaks Hindley-Milner type inference, an algorithm which is guaranteed to infer every type in a simpler type system, but inferring every type in one with GADTs (specifically, polymorphic recursion) or existential types is undecidable.