[Smaug123]

"Generalised algebraic data type". Pattern-matching on a GADT not only gives you information about the term that was in the datatype, but also about a type that was in the datatype.

For an ADT that doesn't need the power of GADTs: pattern-matching on a List<'a> gives you either an Empty or a Cons(x, xs), where you know up front before you do the pattern-match that x and xs are of type 'a and List<'a>.

For a GADT that is not an ADT: pattern-matching on an Expression might give you "Const(a) where a is an int", or "Equal(a, b) where a, b are bools", etc. Without doing the pattern-match, you can't necessarily tell what types you've ended up with.