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

Not in scope error instead of missing type signature error #4150

Open
andreasabel opened this issue Oct 21, 2019 · 2 comments
Open

Not in scope error instead of missing type signature error #4150

andreasabel opened this issue Oct 21, 2019 · 2 comments
Assignees
@andreasabel
Labels
regression in 2.5.4 Regression that first appeared in Agda 2.5.4 scope Issues relating to scope checking ux: error reporting Issues to do with how Agda reports errors
Milestone
icebox

Comments

@andreasabel
Copy link
Member 

mutual
  record Foo : Set where
    field
      A : Set
      B : A → F A  -- Not in scope: F
  F A = Set

Up to 2.5.3, Agda reported

...:6,3-6
Missing type signature for left hand side F A

Since 2.5.4, the error has gotten worse:

Not in scope:
  F at ...:5,15-16
@andreasabel andreasabel added ux: error reporting Issues to do with how Agda reports errors scope Issues relating to scope checking regression in 2.5.4 Regression that first appeared in Agda 2.5.4 labels Oct 21, 2019
@andreasabel andreasabel added this to the 2.6.1 milestone Oct 21, 2019
@jespercockx jespercockx modified the milestones: 2.6.1, 2.6.2 Dec 1, 2019
@UlfNorell
Copy link
Member

Most likely due to fix of #2576 where you wanted a "duplicate definition" error instead of missing type signature. This would be the dual case where you prefer the error from the nicifier.

@jespercockx
Copy link
Member

@andreasabel did you have time to look at this yet?

@andreasabel andreasabel modified the milestones: 2.6.2, icebox May 8, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@andreasabel andreasabel

Labels
regression in 2.5.4 Regression that first appeared in Agda 2.5.4 scope Issues relating to scope checking ux: error reporting Issues to do with how Agda reports errors
Projects
None yet
Milestone
icebox
Development

No branches or pull requests
3 participants
@UlfNorell @andreasabel @jespercockx