GADT

Foundations for Structured Programming with GADTs. GADTs are Generalized Algebraic Data Types and they allow data constructors to return types of values other than the original type they were given.