Ignore orphan parameters inside a retains annotation during Ycheck #19684
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.
Fixes #19661.
Cause of the issue
As reported in #19661, the following code triggers an assertation failure during Ycheck:
The failure happens when checking the tree
f(xs)
, whose type isMySet[Int]^{this, PartialFunction[Int, Int]}
. ThecheckNoOrphans
function is invoked onthis
, whose type turns out to be an orphan parameter reference (xs
).We first inspect the tree outputed by
typer
:The problem roots in the signature of the method
f
: in the capture set of its result type, thethis
reference is dangling.How come? It turns out that the
asSeenFrom
map is not working correctly for the typing ofxs.collect
:Instead of replacing
this
withxs
,asSeenFrom
keepsthis
untouched. This is what happened:asSeenFrom
on the method type, theasSeenFrom
map recurses and applies on the annotated type.@retains(this, pf)
), theasSeenFrom
map derives aTreeTypeMap
from itself and uses it to map thetree
of the annotation.this
is properly mapped toxs.type
but the treethis
is never changed (since theTreeTypeMap
is an identity on the structure of trees).To solve this issue, there are (at least) two possibilities:
TypeMap
machineries on annotations to enable it to properly handle these cases. But it is hard: when mapping the capture annotation, we are at a pre-CC phase, so tools for manipulating capture sets are not available. And it is unnecessary: even if we compute these references properly, it gets discarded during CC.@retains
annotation (as opposed to an optimisedCaptureAnnotation
). This feels like a dangerous fix but these@retains
annotations, even if they are ill-formed, is already treated as being unreliable in CC and get rechecked. Also, CC turns these concrete annotations into optimisedCaptureAnnotation
s, which are not ignored by Ycheck.Fix
So this PR implements the second option:
@retains
annotation during Ycheck.CaptureAnnotation
s will not be bypassed.