GHC Proposals [#281](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst) and [#402](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0402-gadt-syntax.rst) allow the use of visible forall in data constructors. That is, we should be able to write ```haskell 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? ```haskell 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.