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

Postpone irrelevant/incoherent instance selection using the same logic as overlap #7373

Draft
wants to merge 3 commits into
base: master
Choose a base branch
from

Conversation

ncfavier
Copy link
Member

@ncfavier ncfavier commented Jul 14, 2024

Fixes the1lab/1lab#407 and another similar bug.

This is still in the spirit of using overlapOk as a heuristic for "we now have a list of 'good enough' candidates that would all be equally suitable (save for additional constraints that do not mention the goal type), so we can proceed to thin down the list by applying overlap rules or picking an arbitrary candidate". The heuristic is not perfect but this can be remedied with --backtracking-instance-search; for example removing the INCOHERENT pragma from Issue7364.agda still fails as it always has.

Note that the Number-Nat nonsense in the test cases is required to trigger the bugs, as these are scheduling-sensitive issues.

@ncfavier ncfavier requested a review from plt-amy July 14, 2024 21:36
@ncfavier ncfavier marked this pull request as draft July 14, 2024 22:02
Extracted from a failure in the stdlib.
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.

Another irrelevant instance search bug
1 participant