As the title says, Haddock does not respect the required/provided type variable distinction in pattern synonyms: ```hs type A :: Type data A where MkA :: forall k (a ::k) b. ( Show b ) => Proxy a -> b -> A pattern P :: forall . () => forall k (a :: k) b. ( Show b ) => Proxy a -> b -> A pattern P a b = MkA a b ``` Haddock displays the type of the pattern synonym `P` as: ```hs pattern P :: forall k (a :: k) b. () => Show b => Proxy a -> b -> A ``` which is wrong: it brought the existentials to the outside. NB: the only reason for using poly-kinds in this example was to force Haddock to display the `forall`s. Without it, the foralls are omitted entirely, which is also wrong. The bugs are in `Haddock.Convert.synifyPatSynType`: - it clearly moves all type variables into the "universal" (/required) part, - it uses `implicitForAll`, which will try to make the forall implicit if the kinds can be inferred from the variable occurrences. It should not make either forall implicit if there are existential variables. (Note that `implicitForAll` suffers from other bugs, see https://gitlab.haskell.org/ghc/ghc/-/issues/26246#note_629732).