On 10/19/05, oleg@pobox.com
I never argued about convenience of GADTs. They can be quite handy when dealing with existentials: GADT embody a safe cast and so spare us form writing the boring casting code ourselves. And perhaps this is the only compelling case for GADTs.
Speaking about casts, I was playing with using GADTs to create a non-extensible version of Data.Typeable and Data.Dynamic. I wonder if it's possible to write such a thing without GADTs (and unsafeCoerce, which is used in Data.Dynamic, IIRC). BTW, being non-extensible has some benefits, for example, I feel a bit uneasy when I use full blown Dynamics in Haskell (not that I do it that often). See code in the attachment. It has some functions which I didn't find in Data.Dynamics, actually one function: withDyn :: Dyn -> (forall a. Typed a => a -> b) -> b Best regards Tomasz