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).