I think it is a bug.
It also works with silly type annotations:
doy :: Y X a b -> Y X a b
doy (Y (X :: foo)(X :: bar)) = Y X X
Looks like something smart is happening in the Pattern Annotation rule.
Arthur
On 29-sep-05, at 12:40, Ganesh Sittampalam wrote:
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<GADT.hs>_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@xxxxxxxxxxx
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
| 