> 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.