On: GADTs Meet Their Match [pdf]

[ufo]

Yes, the alternative to GADTs is to just let the compiler give you warnings. For example, if you have a pattern matching over a list that you know is never empty you will write something like

    -- gives error at runtime if list is empty
    case mylist of
      (x:xs) -> dostuff
      []     -> error "impossible"

or

    -- missing case in pattern match gives 
    -- error at runtime and a compiler warning
    case mylist of
      (x:xs) -> dostuff

What GADTs let you do is enrich your types with extra information so you can write incomplete pattern matches and prove that they will never fail so the compiler won't show you any spurious warnings.

Its the old tradeoff between static and dynamic typing - more static guarantees vs more simplicity and flexibility.