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.

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

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
Labels
internal-error Concerning internal errors of Agda pattern-synonyms type: bug Issues and pull requests about actual bugs
Milestone

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
internal-error Concerning internal errors of Agda pattern-synonyms type: bug Issues and pull requests about actual bugs
Projects
None yet
Development

Successfully merging a pull request may close this issue.

4 participants