Skip to content

Make reach refinement shallow - #19171

Merged
Linyxus merged 3 commits into
scala:mainfrom
dotty-staging:refine-reach-shallow
Dec 6, 2023
Merged

Make reach refinement shallow#19171
Linyxus merged 3 commits into
scala:mainfrom
dotty-staging:refine-reach-shallow

Conversation

@Linyxus

@Linyxus Linyxus commented Dec 2, 2023

Copy link
Copy Markdown
Contributor

This is to address the following soundness issue:

trait File
val useFile: [R] -> (path: String) -> (op: File^ -> R) -> R = ???
def main(): Unit =
  val f: [R] -> (path: String) -> (op: File^ -> R) -> R = useFile
  val g: [R] -> (path: String) -> (op: File^{f*} -> R) -> R = f  // should be an error
  val leaked = g[File^{f*}]("test")(f => f)  // boom

try
if variance <= 0 then isFlipped = true
t.dealias match
case t1 @ CapturingType(p, cs) if cs.isUniversal =>

@odersky odersky Dec 3, 2023

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the logic can be simplified a bit by this:

Suggested change
case t1 @ CapturingType(p, cs) if cs.isUniversal =>
case t1 @ CapturingType(p, cs) if cs.isUniversal && !isFlipped =>

@odersky odersky left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Otherwise LGTM

t.dealias match
case t1 @ CapturingType(p, cs) if cs.isUniversal =>
if variance > 0 then
t1.derivedCapturingType(apply(p), if isFlipped then cs else ref.reach.singletonCaptureSet)

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Then you can leave things as they were here.

@odersky odersky assigned Linyxus and unassigned odersky Dec 3, 2023
@Linyxus
Linyxus force-pushed the refine-reach-shallow branch from ce71765 to 64242f4 Compare December 6, 2023 14:04
@Linyxus
Linyxus enabled auto-merge December 6, 2023 14:04
@Linyxus
Linyxus merged commit 86565a4 into scala:main Dec 6, 2023
@Linyxus
Linyxus deleted the refine-reach-shallow branch December 6, 2023 16:35
@Kordyjan Kordyjan added this to the 3.4.0 milestone Dec 20, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants