fix: Fix various type-system-refresh issues #5712
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
# Conflicts: # Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs
| @@ -512,6 +525,19 @@ bool TryApplyDefaultAdviceFor(PreTypeProxy proxy) { | |||
| return false; | |||
| } | |||
|
|
|||
| bool TryUseCompatibleTypesAsBounds() { | |||
| // if there is a compatible-types constraint "ty ~~ proxy", then decide on the bound "ty :> proxy" | |||
There was a problem hiding this comment.
What is a compatible types constraint, ty ~~ proxy ? If I'm in the code and I read this comment, can I follow links that lead me to a description of these constraints?
There was a problem hiding this comment.
Without a description of what the issues were and how they were resolved, I can't understand the functional changes made in this PR. I'm guessing this PR solves a newly discovered problem that was not discussed in previous documentation, so it would be good to extend the documentation.
keyboardDrummer
approved these changes
Sep 5, 2024
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.
Description
This PR contains various fixes in the new resolver, found while preparing Dafny to switch to
--type-system-refreshas the default.How has this been tested?
These issues that this PR fixes were found when running the test suite with a version of
dafnythat uses--type-system-refresh --general-traits=datatype --general-newtypesby default. However, since not all test files pass with these options, this PR does not change the default options, which also means that the existing tests don't test for the behavior that has been fixed. The purpose of this PR is to get these fixes in as soon as possible (and to make sure they don't break any existing functionality). The full testing will happen in a future PR that changes the default options.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.