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

Internal error with missing type signature in interleaved mutual type #5638

Closed
phijor opened this issue Nov 9, 2021 · 1 comment
Closed
Assignees
Labels
interleaved mutual regression in 2.6.2 Regression that first appeared in Agda 2.6.2 status: already-fixed status: duplicate Duplicate issue (not in changelog)
Milestone

Comments

@phijor
Copy link

phijor commented Nov 9, 2021

Bug

I mistyped a definition and agda crashed with an internal error.

A minimum working (=crashing) example is:

interleaved mutual
  data Foo where -- note the missing signature `: Set`
      bar : Foo

This produced the following error (pointing here):

Checking min (/tmp/min.agda).
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/Syntax/Concrete/Definitions.hs:851:18 in Agda-2.6.2-5jc1iNTuYyE88p7NRZUfQI:Agda.Syntax.Concrete.Definitions

Without the interleaved mutual block, the above type checks.

Agda version

$ agda --version
Agda version 2.6.2

Related issues

I tried looking for existing issues, maybe this is related to #4881?

@andreasabel andreasabel added interleaved mutual regression in 2.6.2 Regression that first appeared in Agda 2.6.2 labels Nov 16, 2021
@andreasabel andreasabel added this to the 2.6.2.1 milestone Nov 16, 2021
@andreasabel andreasabel self-assigned this Nov 16, 2021
@andreasabel
Copy link
Member

andreasabel commented Nov 16, 2021

Thanks for reporting @phijor!
This is already fixed on master:

The following names are defined but not accompanied by a
declaration: Foo

Looks like a duplicate of #5558.
We close issues once they are fixed on master, so if you want to find related issues, you also have to look through the closed ones...

@andreasabel andreasabel added the status: duplicate Duplicate issue (not in changelog) label Nov 16, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
interleaved mutual regression in 2.6.2 Regression that first appeared in Agda 2.6.2 status: already-fixed status: duplicate Duplicate issue (not in changelog)
Projects
None yet
Development

No branches or pull requests

2 participants