type annotations for GADTs

[Arthur Baars]

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 at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs