Internal parser error using syntax rules

[foones]

The following snippet produces an internal (__IMPOSSIBLE__) parser error at src/full/Agda/Syntax/Concrete/Operators/Parser.hs:114:77 in Agda-2.6.2.1. I have tried it in a slightly older version (Agda-2.6.1) with similar results:

postulate X : Set
postulate Π : (X → X) → X
syntax Π  (λ A → B) = Π A , B
syntax Π' (λ A → B) = Π' A , B 
Π' : (X → X) → X
(Π' α , P α) = (Π α , P α)

[nad]

One cannot use lambda abstractions as patterns (excluding dot patterns), but the error message should be better.

[andreasabel]

The error is raised here (second __IMPOSSIBLE__):

agda/src/full/Agda/Syntax/Concrete/Operators/Parser.hs

Lines 109 to 118 in 798be60

	unExprView = \case
	LocalV x -> IdentP x
	AppV e1 e2 -> AppP e1 e2
	OpAppV d ns es -> let ess :: [NamedArg Pattern]
	ess = (fmap . fmap . fmap)
	(\case
	Placeholder{} -> __IMPOSSIBLE__
	NoPlaceholder _ x -> fromOrdinary __IMPOSSIBLE__ x)
	es
	in OpAppP (fuseRange d ess) d ns ess

This never worked properly, there is an internal error all the way back to 2.4.2.6 (and probably further).

[andreasabel]

(Removed from 2.6.2.2 as it does not pick cleanly.)