[ fix ] Improvements and fixes to the coverage checker #3691
+1,009
−183
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
spcfox
changed the title
spcfox
commented
Nov 27, 2025
spcfox
force-pushed
the
fix-coverage-check
branch
3 times, most recently
from
fc0205f to
4abe12c
Compare
Negate `recoverable` and change the order of the clauses. All transformations in this step should preserve behavior
It is now equivalent to `impossibleOK`
…gnal to coverage cheker
I couldn't come up with a test for this, but I'm fairly certain that if it affected any code, that code could be used to construct a proof of false.
It is now equivalent to `impossibleErrOK`
We don't support matching on arrow results because it's a function
spcfox
force-pushed
the
fix-coverage-check
branch
2 times, most recently
from
1e3d06e to
78fb63a
Compare
dunhamsteve
reviewed
Dec 1, 2025
spcfox
force-pushed
the
fix-coverage-check
branch
from
78fb63a to
80447c1
Compare
Matthew-Mosior
approved these changes
Dec 3, 2025
spcfox
force-pushed
the
fix-coverage-check
branch
2 times, most recently
from
340cb5c to
37266ee
Compare
buzden
approved these changes
Dec 4, 2025
Collaborator
buzden
left a comment
buzden
left a comment
There was a problem hiding this comment.
After the last change regarding to the management of Types, I think it's all okay now
Contributor
Author
I’ve found that there’s still an issue with matching on primitive types. I’m already finishing up the fix. matchInt : () -> Void
matchInt Int impossible |
spcfox
force-pushed
the
fix-coverage-check
branch
from
37266ee to
04f8c8c
Compare
Contributor
Author
|
Done! |
dunhamsteve
approved these changes
Dec 4, 2025
Matthew-Mosior
approved these changes
Dec 5, 2025
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Description
Fixes various issues in the coverage checker, primarily those that lead to a proof of false. Also improves the checking of impossible cases (both user-defined and compiler-inferred).
Fixed (reverted) Erased type-casing function seen as total when it's not #3357The fix significantly worsens coverage checking for erased functions. I’ll return to this later.
I do not use the
totalmodifier in tests because coverage should be checked by default.Self-check
CONTRIBUTING.mdand I've updated
CONTRIBUTORS.mdwith my name.implementation, I have updated
CHANGELOG_NEXT.md