Pattern synonyms and GADTs in GHC 8.0.1

[Emil Axelsson]

I have a problem where a pattern synonym doesn't provide the expected 
type refinement in GHC 8.0.1.

> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE PatternSynonyms #-}
>
> data Exp a
>   where
>     Num :: (Eq a, Num a) => a -> Exp a
>     Add :: (Eq a, Num a) => Exp a -> Exp a -> Exp a
>
> pattern NumP a = Num a
>
> pattern AddP :: (Num a, Eq a) => Exp a -> Exp a -> Exp a
> pattern AddP a b = Add a b
>
> simplifyP :: Exp a -> Exp a
> simplifyP (AddP a (NumP 0)) = a
> simplifyP a                 = a

This gives the error

     • No instance for (Eq a) arising from a pattern
       Possible fix:
         add (Eq a) to the context of
           the type signature for:
             simplifyP :: Exp a -> Exp a
     • In the pattern: AddP a (NumP 0)
       In an equation for ‘simplifyP’: simplifyP (AddP a (NumP 0)) = a

If I remove the type signature for `AddP`, the code goes through. 
Unfortunately, in my real code I need the type signature in order to 
resolve overloading.

GHC 7.10 didn't have this problem.

Is this a bug?

/ Emil