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

GADT.hs
Description: Text document

_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@xxxxxxxxxxx
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs