I'm a bit lost here. The proposal talks about unidirectional pattern synonyms, but the very first example given is:

patttern MP x y = x@(Just y)

Which is a bidirectional pattern synonym. Should this be patttern MP x y <- x@(Just y) instead, or did you really intend to talk about bidirectional pattern synonyms?

Also, what would happen if the user attempted to match on MP like so?

f (MP Nothing v) = e

Is this case ever reachable?

Sorry, I don't understand what's proposed at all. With proposals that are for syntactic sugar, Simon usually asks the proposer to give the translation/desugaring. There is no straightforward use case shown; only an awkward/degenerate case, per Trac #9793.

If I write

patttern MP x y = x@(Just y)

then what would be an unproblematic use of pattern MP? (And as @RyanGlScott says, if it's intended as bidirectional, give an example in each direction.)

The Language Report for as-patterns has

apat  → var[@apat]

So in using MP, the only thing I'm allowed as first argument is a bare var(?) It's not just that

(Just z)@(Just v) is a jolly funny pattern.

It's an illegal pattern.

Afterthought: This also explains Ryan's

f (MP Nothing v) = e    -- ==>
f (Nothing@(Just v)) = e

is not just unreachable, but illegal.

Re-reading the proposal's

But the semantics of pattern synonyms are NOT simply macro-expansion ...

Well, OK so those are illegal as-patterns but pattern synonyms wouldn't generate them as such. I think the Language Report has a sensible/simple syntactic-based rule to stop you writing code that's semantically pointless or even downright bewildering. Allowing non-var arguments to pattern synonyms in as-var positions means the syntax rule is in effect:

apat  → apat[@apat]

And that would allow patterns like

(Just z)@(Just v)               -- pointless: duplication
Nothing@(Just v)                -- pointless: unreachable
(Just z)@x                      -- pointless: write as   x@(Just v)
(Just (Left w@(u, 5)))@(Just v) -- yer wot?

Can we combine as-patterns with record syntax in pattern synonyms? This just seems weird (perhaps I'm not squinting hard enough):

pattern MP2{ x, y } = x@(Just y)

And I think @RyanGlScott's first comment is right we can't allow even explicit bi-directionals:

pattern MP3 x y <- x@(Just y)  where
  MP3 x y = x                  -- ugh! silently ignore y

pattern MP4 x y <- x @(Just y)  where
  MP4 x y = if x == (Just y) then x else error "inconsistent expressions for pattern synonym"

That error message is going to bewilder end-users: we're trying to make life easier for them.

Then I'm dubious about the claim

• A slab of code can simply be deleted from the compiler.

We'll be able to remove one fussy restriction:

• The rhs of a pattern synonym cannot include an as-pattern. (not currently documented)

But need to support a slew of fussier restrictions:

• as-patterns are OK on rhs of unidirectional patterns;
• not allowed on rhs of bidirectional patterns;
• not allowed with explicitly bidirectional patterns;
• maybe: not allowed with record syntax.

Plus we really need to police the use of the pattern synonym in pattern matching:

• must use bare var for arguments to the constructor that are as-var s
  (and we aren't going to tell you which are the as-var s: refer to your pattern-supplier's docos)

Should this be patttern MP x y <- x@(Just y) instead, or did you really intend to talk about bidirectional pattern synonyms?

Silly me. The proposal is only about unidirectional pattern synonyms. Sorry. Fixed.

Also, what would happen if the user attempted to match on MP like so?

f (MP Nothing v) = e

Just follow the rules I gave. Match the argument v against the RHS of the pattern synonym x@(Just y). Maybe that fails; if so the match fails. Maybe it succeeds, binding x to Just v2 and y to v2. Now match the value of x (namely Just v2) against Nothing. That fails, so the overall match fails. So yes, the rules say that this pattern will never match.

With proposals that are for syntactic sugar, Simon usually asks the proposer to give the translation/desugaring

Quite right. But this is NOT a proposal about syntactic sugar. As the paper explains (in Section 5) a simple-minded syntactic expansion doesn't work. That's why I give the semantics in exactly the same way that the Haskell report explains the semantics of matching.

If I write

patttern MP x y = x@(Just y)

then what would be an unproblematic use of pattern MP?
Response:

f (MP p True) = e

THis would match arguments of form (Just True) and bind p to Just True.

So in using MP, the only thing I'm allowed as first argument is a bare var(?) It's not just that (Just z)@(Just v) is a jolly funny pattern. It's an illegal pattern.
Correct. In the "side note" I speculate that we could make it legal; but that would be a separate proposal. It'd be technically-unproblematic, but of doubtful benefit.
Allowing non-var arguments to pattern synonyms in as-var positions means the syntax rule is in effect:

apat  → apat[@apat]

Correct. And I am not proposing that. Indeed I am not proposing any change to the syntax of patterns. I'm only proposing to lift a restriction that GHC imposes, even though the user manual explicitly says the restriction does not exist.

Can we combine as-patterns with record syntax in pattern synonyms? This just seems weird (perhaps I'm not squinting hard enough):

pattern MP2{ x, y } <- x@(Just y)

(I switched to unidirectional, since that's what the proposal is about.) Yes, that's absolutely fine. For example, I could say

f (MP { y=False, x=p }) = ...

This pattern woudl match values of form (Just False) binding p to False. There are no exceptions here.

as-patterns not allowed on rhs of bidirectional patterns;

There are a whole slew of such patterns not allowed in teh RHS of bidirectonal pattern synonyms (e.g. view patterns), and as-patterns is already in that list. I do not propse any change there.

maybe: not allowed with record syntax.

No, they are fine with record syntax.

must use bare var for arguments to the constructor that are as-var s

No, I do not propose such a restriction

not allowed with explicitly bidirectional patterns;

No, I do not propose such a restriction.

TL;DR: I'm just proposing to LIFT a restriction, one that takes user-manual-space to document; code to implement; and offers no benefits. I'm not proposing to add any new restrictions. I'm not claiming that it's terribly useful, just that its simpler to have fewer restrictions, and simple, uniform rules.

Thanks @simonpj . The trouble is: all your arguments are from the point of view of the compiler-writer, and somewhat from the pattern-writer. But the idea behind pattern synonyms is to make life easier for the pattern-user (and maybe a bit of implementation-hiding).

I'm not claiming that it's terribly useful,

I'm claiming it is counter-useful for the pattern-user. Particularly not banning (or at least warning) using non-var arguments in as-var positions (which allows a pattern that will never match); also allowing explicitly bi-directional as-patterns. And probably confusing: the user sees two arguments which are in fact correlated (must be correlated in an expression), but in an opaque way.

user-manual-space to document

I'm already up for documenting some of the fussy restrictions around pattern synonyms, as you request here. I'll volunteer to also document that as-patterns are allowed, but probably useful chiefly for perplexing users.

But the idea behind pattern synonyms is to make life easier for the pattern-user

I agree. And that is why I wanted to eliminate special cases from the user manual, and give simple, uniform rules that always work. I don't mind writing code in the compiler that benefits users. This code, in my opinion, does not.

But let's see what others say!

@simonpj, the discussion ebbed down. Do you want to submit it to the committee? Does the proposal need more work?

Am I correct in the following (under this proposal):

pattern And x y = x@y

-- I can now do:
f :: A -> B
f (x <- view1 `And` y <- view2) = …
-- I just created and-patterns!

So if this goes through, may it be worth making @ a pattern conjunction at the same time? To limit surprises for pattern-writers?

At any rate, to the pattern user it will be mostly invisible that an @ has been used in the pattern definition. So from where I stand, I don't see the objections raised so far as being on solid ground, though maybe I'm missing something.

@aspiwack, yes you are right. As the "side note" in the proposal says, a logical development would to be allow p1@p2 in pattern syntax -- an and-pattern -- for arbitrary p1 and p2. I'm only not proposing that here because it's a larger change. But it makes total sense, especially if we adopt or-patterns!

See Trac #9793

I've revised the proposal a bit, and have submitted it to the committee.