Using GADTs for typed subsetting of your language

One use case for GADTs (as a special case of dependent types) is to form a typed subset of your host language.  One creates an EDSL called Expr a, where a is a type of the language (say this language is Haskell).  Values of types Expr a are the abstract syntax trees of expressions of type a from your host language.  This is just a special case of embedding a typed language into your host language: in this case the typed language is a subset of your host language.