Visible forall in pattern synonyms

GHC Proposals #281 and #402 allow the use of visible forall in data constructors. That is, we should be able to write

data T a where
  MkT :: forall a -> a -> T a

A quite relevant ticket that also mentions this is #18389. But what about pattern synonyms?

pattern P :: forall a -> a -> T a
pattern P a x = MkT a x

The interaction between PatternSynonyms and RequiredTypeArguments simply hasn't been discussed or specified anywhere.

It's a feature that makes sense. If we are able to define data constructor MkT, then we should also be able to define a synonym for it. I don't see any obstacles to implementing this. However, it would be nice to have a real world use case before putting effort into it.