With an implicit forall, the code does type check.
So to recap. Explicit/implicit forall doesn't seem to matter here (both compile, both work):
pattern Justy :: a -> Maybe a pattern Justy x = Just x
pattern Justy2 :: forall a. a -> Maybe a pattern Justy2 x = Just x
(The docos for Pattern Synonyms don't give any examples with explicit `forall`; neither do they discuss whether it makes a difference. I'm inclined to say don't bother with outermost `forall`.) But it does matter here:
data Some where Some :: a -> Some
pattern Any :: a -> Some pattern Any x = Some x
pattern Any2 :: forall a. a -> Some pattern Any2 x = Some x
pattern Any3 :: (forall a. a) -> Some pattern Any3 x = Some x
`Any` is accepted; `Any2` and `Any3` are rejected with a type mismatch/rigid tyvar message per your o.p. (I'm not surprised `Any3` is rejected.) The message complains about the binding line, not the signature. If you don't give a signature for `Any`, we get (with `-fprint-explicit-foralls`) `Any :: forall {a}. a -> Some`, which is the same as for `Justy, Justy2 :: forall {a}. a -> Maybe a` mutatis mutandis. As to 'working', I presume your actual code doesn't merely have an existential for `Some`(?) but rather a constraint. Otherwise pattern-matching with `(Any x)` or with `(Some x)` you can't do anything with the `x` on RHS. Your o.p. asked
Is there a way around it, or is this a missing feature?
What feature would you like that you think is "missing"? Do you think a pattern's explicit `forall` for an existential data constructor should do something different vs for a regular datatype? This could just be a stray loose end that nobody anticipated with Pattern Synonyms.