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

Incomplete pattern match for future clause when using scattered match #883

Open
jordancarlin opened this issue Jan 15, 2025 · 2 comments
Open

Comments

@jordancarlin
Copy link
Contributor

#825 introduced a warning for unmatched future clauses in scattered enums. This makes sense when the entire match is written in one place, but probably shouldn't apply for scattered matches. See riscv/sail-riscv#689.

@Alasdair
Copy link
Collaborator

I did consider this situation, and there is an interaction between scattered definitions and the Sail module system that makes this warning still valid, which is that you can have an optional module A define the function clause and an optional module B define the enumeration/union clause it matches on. In this case the <future E clause> part of the warning is a bit misleading because it would really be something more like <E clause from non-required module>.

When you have a modular specification with optional modules, what the type system (and by extension the pattern-completeness checker) are checking is really that any combination of modules work, sort of like parametricity for polymorphic functions - but you also want to be able to check modules separately using just their local definitions and their requirement/imports, so the checker just considers scattered definitions as being 'open' which essentially forces wildcard cases in some places where if you took a global view of all the modules you might be able to reason that a match is actually complete.

Of course it is just a warning, so we could decide in this case to not issue a warning.

@jordancarlin
Copy link
Contributor Author

Hmm. The interaction with the module system is an interesting case that I hadn't considered. It is still unfortunate that we need to add a wildcard match to avoid a warning in cases like this, but maybe it is unavoidable.

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

No branches or pull requests

2 participants