I was reading the explanation of GADTs on the wiki , 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)