Currently all as-patterns are rejected in pattern synonym definitions, to avoid situations like

pattern P x y <- x@(y:_)

since there's no valid reason to be able to then write something like

f [True] False = ...

this would just lead to confusion.

However, I think we could accept as-patterns where the body of the as-pattern doesn't contain any variable bindings that are accessible via the pattern synonym. In other words, this should be OK:

pattern P x <- x@(y:_)

since it's exactly equivalent to

pattern P x <- x@(_:_)

which I don't think is as confusing as the other example.

I haven't really made up my mind yet if these should be bidirectional; but they certainly could be, by just ignoring the body of the as-pattern in the wrapper; so the following two would be equivalent:

pattern P1 x = [x@(y:_)]
pattern P2 x <- [x@(y:_)]
  where
    P2 x = [x]