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

Fix the type of array.elem and the mantis benchmark #1223

Merged
merged 2 commits into from
Apr 4, 2023

Conversation

yannham
Copy link
Member

@yannham yannham commented Apr 4, 2023

When trying to run the benchmarks on #1220, they were broken.

Beside updating to the latest stdlib changes, I had to fix the type of array.elem which lies, because it's polymorphic but equality isn't actually parametric. This means that sadly, currently some statically typed code can actually fail its contract, because the equality is typed with _a -> _a -> Bool. Maybe it shouldn't. In the meantime, let fix elem, which currently fails on any reasonable usage with a spurious blame error.

@yannham yannham requested review from vkleen, ebresafegaga and dpl0a and removed request for dpl0a April 4, 2023 10:21
@github-actions github-actions bot temporarily deployed to pull request April 4, 2023 10:25 Inactive
Copy link
Contributor

@vkleen vkleen left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's pretty unfortunate, but this seems like a good interim fix. It might be useful to document the failing example in a comment in the stdlib, so people like me don't go around changing everything to forall's in a few months 😅

@yannham
Copy link
Member Author

yannham commented Apr 4, 2023

Addressed in f07ee8.

@yannham yannham added the merge-queue merge on green CI label Apr 4, 2023
@github-actions github-actions bot temporarily deployed to pull request April 4, 2023 14:06 Inactive
@yannham yannham merged commit 3448b93 into master Apr 4, 2023
@yannham yannham deleted the fix/mantis-benchmark branch April 4, 2023 16:00
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
merge-queue merge on green CI
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants