bug in GADT typechecking

Hello ghc folks,

The following GADT program fails to typecheck, although I think it really
should be fine, so I'm reporting this as a bug.  I'm sorry, but I haven't
been able to simplify the foo function any more without causing the error
to go away.  :(

> {-# 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............   ^^^^^^^^

It's a strange bug, and is quite an inconvenience.  Could this be a result
of the wobbly types used for GADTs? It seems to me that this is a pretty
dead safe bit of code--after all (PP x) and (Lis (U x)) have precisely the
same type!

I get the following error:

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'

when running with

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

using the ghc compiler in debian sarge.
-- 
David Roundy
http://www.darcs.net