Internal error when matching on user syntax with binding

[nguermond]

When I execute the following (in Agda 2.6.1.2)

data Foo : Set₁ where
  Lam : (a : Set) -> (a -> Foo) -> Foo

syntax Lam a (λ x -> s) = x :: a , s
postulate X : Set
Bar : Foo -> Set
Bar (x :: a , s) = X

I get the following error message

An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/Syntax/Concrete/Operators/Parser.hs:115

I'm not sure whether this is an abusive use of syntax, but reporting anyways because the message tells me to.

[nad]

The error message should be better.

[andreasabel]

The internal error is raised in a pure function:

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

Line 114 in 72e3aac

NoPlaceholder _ x -> fromOrdinary __IMPOSSIBLE__ x)

It was already an internal error in 2.4.2.4 (the oldest Agda I have installed) and could be as old as the syntax feature itself.

[felixwellen]

With latest master, the code above does not produce an internal error, but instead it is now something like:

 /home/felix/agda/test/Fail/Issue5257.agda:7,1-17
Could not parse the left-hand side Bar (x :: a , s)
Operators used in the grammar:
  None
when scope checking the left-hand side Bar (x :: a , s) in the
definition of Bar

[felixwellen]

I think this error message is reasonable enough -> closing.

[asr]

I suggest to cherry-pick the fix into the release-2.6.3 branch and change the milestone to 2.6.3.

[felixwellen]

It currently works on release-2.6.3 and I didn't figure out where it started to work (=give a reasonable error).

[asr]

I was wrong. I thought there was a commit closing the issue.

[andreasabel]

Could have been fixed along with #394 in PR:

• Fixed #394 #5573

This issue can go on the closed issues for milestone 2.6.3. (Was still broken in 2.6.2.2.)