Skip to content

Fresh level checking bypassed for inferred lambda arguments #23431

Closed
@Linyxus

Description

@Linyxus

Compiler version

main

Minimized code

import language.experimental.captureChecking
trait IO
def withIO(op: IO^ => Unit): Unit = ???
def test(): Unit =
  withIO: io1 =>
    var myIO: IO^ = io1
    def setIO(io: IO^): Unit =
      myIO = io  // error, level mismatch
    withIO(setIO)
    withIO: (io2: IO^) =>
      myIO = io2  // error, level mismatch
    withIO: io3 =>
      myIO = io3  // should be error too, but ok

Output

[info] running (fork) dotty.tools.dotc.Main -d /Users/linyxus/Workspace/dotty/compiler/../out/default-last-scalac-out.jar -classpath /Users/linyxus/Library/Caches/Coursier/v1/https/repo1.maven.org/maven2/org/scala-lang/scala-library/2.13.16/scala-library-2.13.16.jar:/Users/linyxus/Workspace/dotty/library/../out/bootstrap/scala3-library-bootstrapped/scala-3.7.3-RC1-bin-SNAPSHOT-nonbootstrapped/scala3-library_3-3.7.3-RC1-bin-SNAPSHOT.jar -color:never issues/cc-var-level.scala
-- [E007] Type Mismatch Error: issues/cc-var-level.scala:8:13 --------------------------------------------------------------------------------------------------------------------------
8 |      myIO = io  // error, level mismatch
  |             ^^
  |             Found:    (io : IO^)
  |             Required: IO^²
  |
  |             where:    ^  refers to a fresh root capability in the type of parameter io
  |                       ^² refers to a fresh root capability in the type of variable myIO
  |
  | longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: issues/cc-var-level.scala:11:13 -------------------------------------------------------------------------------------------------------------------------
11 |      myIO = io2  // error, level mismatch
   |             ^^^
   |             Found:    (io2 : IO^)
   |             Required: IO^²
   |
   |             where:    ^  refers to a fresh root capability in the type of parameter io2
   |                       ^² refers to a fresh root capability in the type of variable myIO
   |
   | longer explanation available when compiling with `-explain`
2 errors found

Expectation

Should be error for all three cases since they are morally equivalent.

Metadata

Metadata

Assignees

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions