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: [EMAIL PROTECTED]
[mailto:glasgow-haskell-bugs-
| [EMAIL PROTECTED] On Behalf Of Ganesh Sittampalam
| Sent: 29 September 2005 11:40
| To: [email protected]
| 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
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
