Impredicative instantiation of universally quantified variables in guarded positions fails in pattern synonyms

Consider the following declarations:

data T a b where
  Blah :: forall a b. a -> b -> T a b

mustWork1 :: T (forall a. a -> a) Int -> Int
mustWork1 (Blah f x) = f x

mustWork1 works as it should. Unfortunately this isn't the case for mustWork2.

pattern BlahSyn :: forall a b. () => () => a -> b -> T a b
pattern BlahSyn f x = Blah f x

mustWork2 :: T (forall a. a -> a) Int -> Int
mustWork2 (BlahSyn f x) = f x

Here is the error message for mustWork2:

/Users/artin/Programming/projects/playground/src/Synonym.hs:123:12-22: error: [GHC-83865]
• Couldn't match type: forall a. a -> a
with: Int -> Int
Expected: T (forall a. a -> a) Int
Actual: T (Int -> Int) Int
• In the pattern: BlahSyn f x
In an equation for ‘mustWork2’: mustWork2 (BlahSyn f x) = f x
|
123 | mustWork2 (BlahSyn f x) = f x
|            ^^^^^^^^^^^
Failed, no modules to be reloaded.

@simonpj

@rae