type annotations for GADTs

[Ganesh Sittampalam]

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
-------------- next part --------------
{-# OPTIONS_GHC -fglasgow-exts #-}

module GADT where

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