Always use adapted type in withDenotation #16901
Merged
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.
When creating a NamedType with a given overloaded denotation, make sure that the type has a Name as designator. This prevents accidentally overwriting a more precise symbolic TermRef that refers to one specific alternative of the denotation.
This might be enough to fix #16884.
EDIT: It wasn't enough but the second commit 46e82dd should fix it. The second commit never overwrites in
withDenot
. It can do that because we fixinfoDependsOnPrefix
to work correctly for abstract types that are refined in a self type. It turned out that previously we needed some TypeRefs to keep their Name designators because that way we would recompute their info with amember
operation. If these TypeRefs had a symbol designator they would be recomputed wrongly bysymd.current
infromDesignator
because the precedinginfoDependsOnPrefix
test was faulty.It would be great if we could maintain the general invariant that NamedTypes with overloaded denotations always have names as designators. But that looks very hard when we take into account that we need to update named types to new runs. A type might have a single denotation in one round and an overloaded one in the next.