Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Internal error when matching on user syntax with binding #5257

Closed
nguermond opened this issue Mar 4, 2021 · 8 comments
Closed

Internal error when matching on user syntax with binding #5257

nguermond opened this issue Mar 4, 2021 · 8 comments
Labels
bugfix-sprint-candidate internal-error Concerning internal errors of Agda operators Parsing of mixfix operators syntax Bike-shedding of the surface syntax type: bug Issues and pull requests about actual bugs ux: error reporting Issues to do with how Agda reports errors
Milestone
2.6.3

Comments

@nguermond
Copy link

nguermond commented Mar 4, 2021 •
edited by andreasabel
Loading

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 nad added syntax Bike-shedding of the surface syntax type: bug Issues and pull requests about actual bugs labels Mar 4, 2021
@nad nad added this to the 2.6.3 milestone Mar 4, 2021
@nad
Copy link
Contributor

nad commented Mar 4, 2021

The error message should be better.

@andreasabel andreasabel added ux: error reporting Issues to do with how Agda reports errors internal-error Concerning internal errors of Agda operators Parsing of mixfix operators labels Mar 4, 2021
@andreasabel
Copy link
Member

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.

@jespercockx jespercockx mentioned this issue Aug 31, 2022
Closed
@andreasabel andreasabel modified the milestones: 2.6.3, later Aug 31, 2022
@felixwellen
Copy link
Contributor

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
Copy link
Contributor

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

@asr
Copy link
Member

asr commented Nov 11, 2022 •
edited
Loading

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

@felixwellen
Copy link
Contributor

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

@asr
Copy link
Member

asr commented Nov 11, 2022

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

@asr asr modified the milestones: later, 2.6.3 Nov 11, 2022
@andreasabel
Copy link
Member

andreasabel commented Nov 12, 2022 •
edited
Loading

Could have been fixed along with #394 in PR:

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bugfix-sprint-candidate internal-error Concerning internal errors of Agda operators Parsing of mixfix operators syntax Bike-shedding of the surface syntax type: bug Issues and pull requests about actual bugs ux: error reporting Issues to do with how Agda reports errors
Projects
None yet
Milestone
2.6.3
Development

No branches or pull requests
6 participants
@nad @asr @andreasabel @jespercockx @felixwellen @nguermond