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{-# 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
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
