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

Reduce dummy ranges. #189

Merged
merged 7 commits into from
Sep 10, 2024
Merged

Reduce dummy ranges. #189

merged 7 commits into from
Sep 10, 2024

Conversation

gebner
Copy link
Contributor

@gebner gebner commented Aug 31, 2024

Commit b3c446d improved the ranges of the instantiate implicits error message (thank you @nikswamy) , but there are still cases where the range is the whole declaration.

It turns out that this happens because we often set the range of a term to be the dummy range, which then causes the range to be defaulted to the whole declaration. Properly setting the range of a term requires an explicit call to set_range which is easy to forget.

This PR adds sensible default ranges in the tm_pureapp etc. constructors, to ensure that we do not generate dummy ranges in the first place. Nullary constructors for fvars etc. still produce dummy ranges; we can't guess the range from the arguments there and specifying it everywhere is a lot of churn.

See testcase for an example where this PR improves an error message range.

@mtzguido
Copy link
Member

Thanks Gabriel, I tried it out and it did improve an error I had. I merged master and regen'd the snapshot (hopefully correctfully).

Merging.

@mtzguido mtzguido merged commit 700336c into main Sep 10, 2024
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants