Required constraints are not inferred for pattern synonyms involving GADTs

Let's say we have the following setup:

{-# LANGUAGE GADTs, PatternSynonyms, ViewPatterns #-}

data T a where
  MkT1 :: a -> T a
  MkT2 :: a -> T (Maybe a)

f :: (Eq a) => a -> a
f = id

Then the following definition works as expected:

pattern P1 x <- MkT1 (f -> x)

with the following inferred type:

λ» :i P1
pattern P1 :: () => Eq t => t -> T t

However, trying to do the same with {{MkT2}} doesn't work:

pattern P2 x <- MkT2 (f -> x)

this results in

Could not deduce (Eq a1) arising from a use of ‘f’
from the context (t ~ Maybe a1)
  bound by a pattern with constructor
             MkT2 :: forall a. a -> T (Maybe a),
           in a pattern synonym declaration

Trac metadata

Trac field	Value
Version
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture