A fix in the core typechecker #3004
Merged
Conversation
This file contains 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
aseemr
commented
Aug 6, 2023
| *) | ||
|
|
||
| [@expect_failure] | ||
| (* |
There was a problem hiding this comment.
This is interesting. The example that was showing failing smt proofs, now works.
There was a problem hiding this comment.
Weird! I noticed the same thing in a completely separate branch, so maybe some dependency got updated? In fact even master does not pass (local) ci for me right now.
There was a problem hiding this comment.
There seems to be a difference between running with --query_stats and without. CI will pass using that flag (this definition will fail as expected). You might need to revert this change to get a green. I'll look to see what causes this.
mtzguido
approved these changes
Aug 6, 2023
|
I have an everest green, merging. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Adding a missing check for expected effect in the case when the expected type is not set.
The fix failed some examples, where the core client wanted a total effect on non-informative types, but core computed a ghost effect (and the cases passed due to the missing check).
To fix those cases, the PR also adds eager promotion so that it computes a total effect in such cases.
The PR also contains a small optimization in inserting hide/reveal coercions. If the expression is
reveal e(resp.hide e), and the context expects an erased (resp. non-erased) type, then instead of making the coercion returnhide (reveal e)(resp.reveal (hide e), we just returne.The last optimization resulted in two failures, one each in
Steel.ST.ArrayandSteel.ST.HigherArray. Since the coerced expression is a little different, tworewritecalls in the libraries (one in each file) had to be tweaked. In general, smt attribute saves us, but these cases were where the coercion was happening in the first argument ofpts_to(see FStarLang/steel#63).