type annotations for GADTs

[Simon Peyton-Jones]

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