GADT

The key point about GADTs is that pattern matching causes type refinement. – GHC User Guide

An example GADT:

data Query result where 
  Query_NotesByTag :: Tag -> Query [Note]
  Query_AllTags :: Query [Tag]

Pattern matching on the GADT constructor causes type refinement. For example, pattern matching on the constructor Query_NotesByTag refines the type (of the query result) to [Note]. GADTs are extremely useful for this purpose, something that cannot be achieved with regular ADTs (algebraic data types).

gadt