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

Agsy/Auto panics with -r in the presence of a pattern synonym #5828

Closed
kindaro opened this issue Mar 11, 2022 · 3 comments · Fixed by #6127
Closed

Agsy/Auto panics with -r in the presence of a pattern synonym #5828

kindaro opened this issue Mar 11, 2022 · 3 comments · Fixed by #6127
Assignees
@jespercockx
Labels
auto Issues to do with the Auto proof search (Mimer, Agsy) internal-error Concerning internal errors of Agda scope Issues relating to scope checking type: bug Issues and pull requests about actual bugs
Milestone
2.6.3

Comments

@kindaro
Copy link

kindaro commented Mar 11, 2022

See:

module x where

data X : Set
  where x : X

pattern y = x

theorem : X
theorem = {-r }0

(You will need to erase the hole and make a new one in the same place for Agda to understand what you mean.)

If you try to fill the hole with automatic proof search, you will see an error like this:

Panic: Unbound name: x.y[0,6]@ModuleNameHash 15504699851561257075

Without -r, the hole is automatically filled with y.

I am on Agda 2.6.3 built recently from source.
@andreasabel andreasabel added scope Issues relating to scope checking auto Issues to do with the Auto proof search (Mimer, Agsy) internal-error Concerning internal errors of Agda type: bug Issues and pull requests about actual bugs labels Mar 12, 2022
@andreasabel
Copy link
Member

Thanks for reporting, @kindaro. Auto has no maintainer, so there is little hope this is going to be fixed...

@kindaro
Copy link
Author

kindaro commented Mar 13, 2022

Wow well good to know. I am learning Agda yet so I cannot solve this myself but maybe some time later I could!

@jespercockx
Copy link
Member

This might be the same problem as #5551, so not a problem with auto itself after all.

@jespercockx jespercockx added this to the 2.6.3 milestone Aug 23, 2022
@jespercockx jespercockx self-assigned this Aug 23, 2022
jespercockx added a commit to jespercockx/agda that referenced this issue Sep 23, 2022
@jespercockx
[ fix agda#5828 ] Replace some calls to getConstInfo by the (safer)…
3387653 
… `getConstInfo'`
@jespercockx jespercockx linked a pull request Sep 23, 2022 that will close this issue
Fix for #5828 #6127
Merged
jespercockx added a commit that referenced this issue Sep 24, 2022
@jespercockx
[ fix #5828 ] Replace some calls to getConstInfo by the (safer) `ge…
c7733c0 
…tConstInfo'`
@andreasabel andreasabel mentioned this issue Oct 24, 2022
Closed
@andreasabel andreasabel changed the title Panic when trying to automatically fill a hole with -r in the presence of a pattern synonym. Agsy/Auto panics with -r in the presence of a pattern synonym Oct 24, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@jespercockx jespercockx

Labels
auto Issues to do with the Auto proof search (Mimer, Agsy) internal-error Concerning internal errors of Agda scope Issues relating to scope checking type: bug Issues and pull requests about actual bugs
Projects
None yet
Milestone
2.6.3
Development

Successfully merging a pull request may close this issue.

Fix for #5828 jespercockx/agda
3 participants
@andreasabel @kindaro @jespercockx