[Haskell-cafe] Typeclasses and GADT [Was: Regular Expressions without GADTs]

[Tomasz Zielonka]

On 10/19/05, oleg at pobox.com <oleg at pobox.com> wrote:
> 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