GADTs are obviously currently a hot topic in functional programming research. Most of the papers focus only on the GADT mechanism (how type checking works etc.). The only example that one usually sees is the "typed evaluator". I am not an expert on this topic, and I'd like to know more about how they would actually be useful in practical programming. For example, I wonder how a parser would look like if it is impossible to construct "wrong" ASTs. Would type checking then effectively take place during parsing? How would a type error in the parsed program be detected and thrown? GADTs are a mechanism for defining more precise types. It helps you make stronger guarantees on an AST structure, which reduces the number of explicit consistency checks you have to perform in code. GADTs are very useful for deriving combinator libraries in the style of John Hughes. Andres Loh shows an embedded DSL for contracts in Haskell using GADTs in Typed Contracts for Functional Programming.