Re: bug in GADT typechecking

> > {-# OPTIONS_GHC -fglasgow-exts #-}
> > module Main where
> > 
> > data Foo a b where
> >     Foo :: Int -> Foo a b
> > 
> > data Patch a b where
> >     PP :: Foo a b -> Patch a b
> >     Lis :: PL a b -> Patch a b
> > 
> > data PL a b where
> >     U :: Patch a b -> PL a b
> >     Nil :: PL x x
> >     (:-) :: PL c d -> PL d e -> PL c e
> > 
> > data Pair alpha omega where
> >     (:.) :: Patch a i -> Patch i o -> Pair a o
> > 
> > foo :: Pair a b -> Maybe (Pair a b)
> > foo (Lis (U x :- y) :. Lis Nil) = Just (PP x :. Lis y)
> 
>                                           ^^^^
> 
> Oddly enough, the code *does* typecheck if we change the above line to
> 
> foo (Lis (U a :- b) :. Lis Nil) = Just (Lis (U a) :. Lis b)
> 
> which differs only in here............   ^^^^^^^^

Looks to me as if ghc is right to complain. PP takes a Foo, but U takes
a Patch. Therefore the x that's matched on the lhs is a Patch, not a Foo.

> test.lhs:27:44:
>     Couldn't match `Foo a b' against `Patch a1 d'
>       Expected type: Foo a b
>       Inferred type: Patch a1 d
>     In the first argument of `PP', namely `x'
>     In the first argument of `(:.)', namely `PP x'

> Glasgow Haskell Compiler, Version 6.4, for Haskell 98, compiled by GHC 
> version 6.4

FWIW, same error with ghc-6.5 from a few weeks ago.

Cheers,
  Andres