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

Inferred type is too general for high order operator with tuple parameter #1167

Closed
bugarela opened this issue Sep 19, 2023 · 1 comment · Fixed by #1409
Closed

Inferred type is too general for high order operator with tuple parameter #1167

bugarela opened this issue Sep 19, 2023 · 1 comment · Fixed by #1409
Assignees
Labels
bug Something isn't working typechecker Type checker for Quint

Comments

@bugarela
Copy link
Collaborator

bugarela commented Sep 19, 2023

For some reason, the inferred type for optionSum is too general here:

poll.options.listForall(option =>
val optionKey = option._1
// FIXME(#1167): Type annotation below is a workaround, inferred type is too general
val optionSum: int = option._2
// `ballots` only contains entries if there are > 0 votes.
optionSum > 0 implies and {
summed_ballots.keys().contains(optionKey),
summed_ballots.get(optionKey) == optionSum
}
)

Symptoms:

@bugarela
Copy link
Collaborator Author

The quantification fix I'm working on will fix this issue 🎉

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working typechecker Type checker for Quint
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant