I was reading the explanation of GADTs on the wikihttp://en.wikibooks.org/wiki/Haskell/GADT , and but can't make any sense of the examples. Sure I understand what a GADT is, but I'm looking for practical examples, and the ones on the wiki seem to show what you *cannot* do with them... For example, the article gives an alternative approach to the safeHead function (see code below) But now that does not work either, since Cons x y never evaluates to MarkedList x Safe, so safeHead (Cons 1 Nil) will give a type error... Am I missing something or is this wikibook just confusing? Does anybody have good links to examples of GADTs? Yampa surely seems a good example, but it's a bit too advanced. data NotSafe data Safe data MarkedList :: * -> * -> * where Nil :: MarkedList t NotSafe Cons :: t -> MarkedList t y -> MarkedList t z safeHead :: MarkedList x Safe -> x safeHead (Cons x _) = x silly 0 = Nil silly 1 = Cons () Nil silly n = Cons () $ silly (n-1)