type annotations for GADTs

[Ganesh Sittampalam]

In case it influences your decision re 6.4.2 slightly, it would be quite 
useful for the darcs code base to have a 6.4 release that fixes this, as 
having to put in the extra type annotations is somewhat disruptive.

[Darcs is experimenting with GADTs to help enforce some correctness 
properties in the patch handling code; see 
http://wiki.darcs.net/index.html/GADTPlan for a rough explanation]

Cheers,

Ganesh

On Wed, 12 Oct 2005, Simon Peyton-Jones wrote:

> A palpable bug, thank you.  Now fixed in CVS.  It'll be in 6.4.2 also if
> we ever release that.
>
> Simon
>
> | -----Original Message-----
> | From: glasgow-haskell-bugs-bounces at haskell.org
> [mailto:glasgow-haskell-bugs-
> | bounces at haskell.org] On Behalf Of Ganesh Sittampalam
> | Sent: 29 September 2005 11:40
> | To: glasgow-haskell-bugs at haskell.org
> | Subject: type annotations for GADTs
> |
> | Hi,
> |
> | I found it slightly surprising that the program below (also attached
> as a
> | file) needs the nested type annotations in the place commented. It's
> not
> | really clear whether it's a bug or just a natural consequence of GADT
> | type-checking, but since Simon Marlow also found it surprising it at
> first
> | glance, I thought I'd send it in for comment.
> |
> | The intuitive argument I came up with for why it might be necessary is
> | that each GADT requires some kind of type signature in argument
> position
> | to generalise its type correctly, and the overall signature for doy
> isn't
> | enough to generalise the type of the X arguments.
> |
> | Cheers,
> |
> | Ganesh
> |
> | data X a b where
> |     X :: X a a
> |
> | data Y x a b where
> |     Y :: x a b -> x b c -> Y x a c
> |
> | {- This needs the nested type annotations -}
> | doy :: Y X a b -> Y X a b
> | doy (Y (X :: X a c) (X :: X c b)) = Y X X
> |
> | data YX a b where
> |     YX :: X a b -> X b c -> YX a c
> |
> | {- This version doesn't need them -}
> | doyx :: YX a b -> YX a b
> | doyx (YX X X) = YX X X
>
>