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

Panic when showing module contents with pattern synonym #5551

Closed
laMudri opened this issue Sep 9, 2021 · 1 comment · Fixed by #6126
Closed

Panic when showing module contents with pattern synonym #5551

laMudri opened this issue Sep 9, 2021 · 1 comment · Fixed by #6126
Assignees
@jespercockx
Labels
internal-error Concerning internal errors of Agda pattern-synonyms type: bug Issues and pull requests about actual bugs
Milestone
2.6.3

Comments

@laMudri
Copy link

laMudri commented Sep 9, 2021

Pressing C-c C-o (agda2-module-contents-maybe-toplevel) on the hole produces a panic. Agda version 2.6.2

module Scratch where

module Foo where
  pattern pat x = x

foo : Set
foo = {!Foo!}
/sharedhome/home/james/Documents/agda/Scratch.agda:7,7-14
Panic: Unbound name: Scratch.Foo.pat[0,2,6]@ModuleNameHash
10507650244568858286
when retrieving the contents of a module
@gallais gallais added internal-error Concerning internal errors of Agda pattern-synonyms type: bug Issues and pull requests about actual bugs labels Sep 10, 2021
@andreasabel
Copy link
Member

@laMudri : I dimly remember there was a code sprint on pattern synonyms at a recent Agda Meeting. Part of this was to make pattern synonyms proper declarations. This would likely also fix the OP. Atm, pattern synonyms live in their own structure rather than in the signature with all other declarations.

@jespercockx jespercockx added this to the 2.6.3 milestone Aug 23, 2022
@jespercockx jespercockx mentioned this issue Aug 23, 2022
Closed
@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#5551 ] Filter out names without a definition from module c…
4a0d9ae 
…ontents
jespercockx added a commit to jespercockx/agda that referenced this issue Sep 23, 2022
@jespercockx
[ fix agda#5551 ] Filter out names without a definition from module c…
2e877e6 
…ontents
@jespercockx jespercockx linked a pull request Sep 23, 2022 that will close this issue
Fix for issue #5551 #6126
Merged
jespercockx added a commit that referenced this issue Sep 26, 2022
@jespercockx
[ fix #5551 ] Filter out names without a definition from module contents
44024e6
@andreasabel andreasabel mentioned this issue Oct 24, 2022
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@jespercockx jespercockx

Labels
internal-error Concerning internal errors of Agda pattern-synonyms 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 issue #5551 jespercockx/agda
4 participants
@gallais @andreasabel @jespercockx @laMudri