type families + GADT = type unsafety?

[Stefan O'Rear]

On Thu, Sep 27, 2007 at 04:59:49PM +0200, Wolfgang Jeltsch wrote:
> Am Donnerstag, 27. September 2007 15:27 schrieb Roberto Zunino:
> > Roberto Zunino wrote:
> > > (Trac reports "database locked", posting here...)
> >
> > For those interested, here are the follow-ups:
> >
> > http://hackage.haskell.org/trac/ghc/ticket/1723
> >
> > Regards,
> > Zun.
> 
> simonpj writes there:
> > Manuel is about to nuke the old GADT stuff in favour of the new type-family
> > stuff. 
> 
> This doesn’t mean that GADTs are being dropped in favor of type families, does 
> it?

They are being dropped - from the typechecker.  The old syntax will
still work.

data Foo a where
   A :: Foo Int
   B :: Foo Bool


becomes

data Foo a = (a ~ Int) => A | (a ~ Bool) => B

(ignoring the H98 context issue).

Then, in a case statement, traditional GADT refinement reduces to a
special case of equality constraint discharging.  (Simon, does this mean
that non-~ discharging will become subject to GADT-style type annotation
rules?)

Stefan
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: Digital signature
Url : http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20070927/1acfb8f7/attachment.bin