Fix capture checking of dependent functions (#16264)

Fixes #15921.

Capture checking can be unsound for dependent functions. Minimized
example:

```scala
trait Cap { def use(): Unit }

def main() = {
  val f: (io: {*} Cap) -> {} () -> Unit =
    io => () => io.use()  // should be an error

  val g: ({*} Cap) -> {} () -> Unit =
    io => () => io.use()  // error, as expected
}
```
In the above example, we issue an error for `g`, but not for `f`, which
is unsound.

The root cause of this issue is that in the `Typer` phase, we only
create `InferredTypeTree` for the result type of function values when
the expected type of the function literal is non-dependent; and later
during `Setup` of the capture checking phase, we only create capture set
variables and update the information of function symbols when its result
type tree is an `InferredTypeTree`.

To be more specific, the function literal `io => () => io.use()` in both
`f` and `g` would be expaneded into the following tree in `Typer`:
```scala
def $anonfun(io: {*} Cap): {} () -> Unit = 
  {
    {
      def $anonfun(): Unit = 
        {
          io.use()
        }
      closure($anonfun)
    }
  }
closure($anonfun)
```
For `g`, where the expected type of the function literal is
non-dependent, we would create capture set variables in `Setup` for the
return type `{} () -> Unit` and update the symbol info of the outer
`$anonfun`. For `f`, we would not do these things because `{} () ->
Unit` is not an `InferredTypeTree`.

This PR fixes this issue by typing the `DependentTypeTree` as an
`InferredTypeTree` in the typer.

~Currently, although this PR fixes the soundness problem, it brings
completeness issues, where sometimes we propagate the universal
capability to some capture sets incorrectly, which prevents some
positive test cases from being accepted. I am still investigating this
issue and thus mark this PR as a draft for now.~

The completeness problem is fixed by two additional refinements:
- preciser propagation of captured references through mapped instance
(see
[dd88672](dd88672)),
- healing ill-formed type parameter capture sets (see
[0e7d33a](0e7d33a)).

compiler/src/dotty/tools/dotc/cc/CaptureSet.scala

@@ -546,7 +546,7 @@ object CaptureSet:
           else CompareResult.fail(this)
         }
         .andAlso {
-          if (origin ne source) && mapIsIdempotent then
+          if (origin ne source) && (origin ne initial) && mapIsIdempotent then
             // `tm` is idempotent, propagate back elems from image set.
             // This is sound, since we know that for `r in newElems: tm(r) = r`, hence
             // `r` is _one_ possible solution in `source` that would make an `r` appear in this set.

compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala

@@ -606,11 +606,28 @@ class CheckCaptures extends Recheck, SymTransformer:
 
     /** Massage `actual` and `expected` types using the methods below before checking conformance */
     override def checkConformsExpr(actual: Type, expected: Type, tree: Tree)(using Context): Unit =
-      val expected1 = addOuterRefs(expected, actual)
+      val expected1 = alignDependentFunction(addOuterRefs(expected, actual), actual.stripCapturing)
       val actual1 = adaptBoxed(actual, expected1, tree.srcPos)
       //println(i"check conforms $actual1 <<< $expected1")
       super.checkConformsExpr(actual1, expected1, tree)
 
+    private def toDepFun(args: List[Type], resultType: Type, isContextual: Boolean, isErased: Boolean)(using Context): Type =
+      MethodType.companion(isContextual = isContextual, isErased = isErased)(args, resultType)
+        .toFunctionType(isJava = false, alwaysDependent = true)
+
+    /** Turn `expected` into a dependent function when `actual` is dependent. */
+    private def alignDependentFunction(expected: Type, actual: Type)(using Context): Type =
+      def recur(expected: Type): Type = expected.dealias match
+        case expected @ CapturingType(eparent, refs) =>
+          CapturingType(recur(eparent), refs, boxed = expected.isBoxed)
+        case expected @ defn.FunctionOf(args, resultType, isContextual, isErased)
+          if defn.isNonRefinedFunction(expected) && defn.isFunctionType(actual) && !defn.isNonRefinedFunction(actual) =>
+          val expected1 = toDepFun(args, resultType, isContextual, isErased)
+          expected1
+        case _ =>
+          expected
+      recur(expected)
+
     /** For the expected type, implement the rule outlined in #14390:
      *   - when checking an expression `a: Ca Ta` against an expected type `Ce Te`,
      *   - where the capture set `Ce` contains Cls.this,
@@ -875,12 +892,79 @@ class CheckCaptures extends Recheck, SymTransformer:
           capt.println(i"checked $root with $selfType")
     end checkSelfTypes
 
+    /** Heal ill-formed capture sets in the type parameter.
+     *
+     *  We can push parameter refs into a capture set in type parameters
+     *  that this type parameter can't see.
+     *  For example, when capture checking the following expression:
+     *
+     *    def usingLogFile[T](op: (f: {*} File) => T): T = ...
+     *
+     *    usingLogFile[box ?1 () -> Unit] { (f: {*} File) => () => { f.write(0) } }
+     *
+     *  We may propagate `f` into ?1, making ?1 ill-formed.
+     *  This also causes soundness issues, since `f` in ?1 should be widened to `*`,
+     *  giving rise to an error that `*` cannot be included in a boxed capture set.
+     *
+     *  To solve this, we still allow ?1 to capture parameter refs like `f`, but
+     *  compensate this by pushing the widened capture set of `f` into ?1.
+     *  This solves the soundness issue caused by the ill-formness of ?1.
+     */
+    private def healTypeParam(tree: Tree)(using Context): Unit =
+      val checker = new TypeTraverser:
+        private def isAllowed(ref: CaptureRef): Boolean = ref match
+          case ref: TermParamRef => allowed.contains(ref)
+          case _ => true
+
+        // Widen the given term parameter refs x₁ : C₁ S₁ , ⋯ , xₙ : Cₙ Sₙ to their capture sets C₁ , ⋯ , Cₙ.
+        //
+        // If in these capture sets there are any capture references that are term parameter references we should avoid,
+        // we will widen them recursively.
+        private def widenParamRefs(refs: List[TermParamRef]): List[CaptureSet] =
+          @scala.annotation.tailrec
+          def recur(todos: List[TermParamRef], acc: List[CaptureSet]): List[CaptureSet] =
+            todos match
+              case Nil => acc
+              case ref :: rem =>
+                val cs = ref.captureSetOfInfo
+                val nextAcc = cs.filter(isAllowed(_)) :: acc
+                val nextRem: List[TermParamRef] = (cs.elems.toList.filter(!isAllowed(_)) ++ rem).asInstanceOf
+                recur(nextRem, nextAcc)
+          recur(refs, Nil)
+
+        private def healCaptureSet(cs: CaptureSet): Unit =
+          val toInclude = widenParamRefs(cs.elems.toList.filter(!isAllowed(_)).asInstanceOf)
+          toInclude.foreach(checkSubset(_, cs, tree.srcPos))
+
+        private var allowed: SimpleIdentitySet[TermParamRef] = SimpleIdentitySet.empty
+
+        def traverse(tp: Type) =
+          tp match
+            case CapturingType(parent, refs) =>
+              healCaptureSet(refs)
+              traverse(parent)
+            case tp @ RefinedType(parent, rname, rinfo: MethodType) if defn.isFunctionType(tp) =>
+              traverse(rinfo)
+            case tp: TermLambda =>
+              val saved = allowed
+              try
+                tp.paramRefs.foreach(allowed += _)
+                traverseChildren(tp)
+              finally allowed = saved
+            case _ =>
+              traverseChildren(tp)
+
+      if tree.isInstanceOf[InferredTypeTree] then
+        checker.traverse(tree.knownType)
+    end healTypeParam
+
     /** Perform the following kinds of checks
      *   - Check all explicitly written capturing types for well-formedness using `checkWellFormedPost`.
      *   - Check that externally visible `val`s or `def`s have empty capture sets. If not,
      *     suggest an explicit type. This is so that separate compilation (where external
      *     symbols have empty capture sets) gives the same results as joint compilation.
      *   - Check that arguments of TypeApplys and AppliedTypes conform to their bounds.
+     *   - Heal ill-formed capture sets of type parameters. See `healTypeParam`.
      */
     def postCheck(unit: tpd.Tree)(using Context): Unit =
       unit.foreachSubTree {
@@ -933,6 +1017,8 @@ class CheckCaptures extends Recheck, SymTransformer:
               }
               checkBounds(normArgs, tl)
             case _ =>
+
+          args.foreach(healTypeParam(_))
         case _ =>
       }
       if !ctx.reporter.errorsReported then

compiler/src/dotty/tools/dotc/typer/Typer.scala

@@ -2938,7 +2938,7 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
           case tree: untpd.TypedSplice => typedTypedSplice(tree)
           case tree: untpd.UnApply => typedUnApply(tree, pt)
           case tree: untpd.Tuple => typedTuple(tree, pt)
-          case tree: untpd.DependentTypeTree => completeTypeTree(untpd.TypeTree(), pt, tree)
+          case tree: untpd.DependentTypeTree => completeTypeTree(untpd.InferredTypeTree(), pt, tree)
           case tree: untpd.InfixOp => typedInfixOp(tree, pt)
           case tree: untpd.ParsedTry => typedTry(tree, pt)
           case tree @ untpd.PostfixOp(qual, Ident(nme.WILDCARD)) => typedAsFunction(tree, pt)

tests/pos-custom-args/captures/boxmap.scala → tests/neg-custom-args/boxmap.scala

@@ -15,5 +15,7 @@ def lazymap[A <: Top, B <: Top](b: Box[A])(f: A => B): {f} (() -> Box[B]) =
 def test[A <: Top, B <: Top] =
   def lazymap[A <: Top, B <: Top](b: Box[A])(f: A => B) =
     () => b[Box[B]]((x: A) => box(f(x)))
-  val x: (b: Box[A]) -> (f: A => B) -> (() -> Box[B]) = lazymap[A, B]
+  val x0: (b: Box[A]) -> (f: A => B) -> (() -> Box[B]) = lazymap[A, B]  // error
+  val x: (b: Box[A]) -> (f: A => B) -> {b, f} (() -> Box[B]) = lazymap[A, B]  // works
+  val y: (b: Box[A]) -> (f: A => B) -> {*} (() -> Box[B]) = lazymap[A, B]  // works
   ()

tests/neg-custom-args/captures/byname.check

@@ -8,7 +8,7 @@
 10 |  h(f2()) // error
    |    ^^^^
    |    Found:    {cap1} (x$0: Int) -> Int
-   |    Required: {cap2} Int -> Int
+   |    Required: {cap2} (x$0: Int) -> Int
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/byname.scala:19:5 ----------------------------------------

tests/neg-custom-args/captures/cc-depfun.scala

@@ -0,0 +1,9 @@
+trait Cap { def use(): Unit }
+
+def main() = {
+  val f: (io: {*} Cap) -> {} () -> Unit =
+    io => () => io.use()  // error
+
+  val g: ({*} Cap) -> {} () -> Unit =
+    io => () => io.use()  // error
+}

tests/neg-custom-args/captures/heal-tparam-cs.scala

@@ -0,0 +1,33 @@
+import language.experimental.captureChecking
+
+trait Cap { def use(): Unit }
+
+def localCap[T](op: (cap: {*} Cap) => T): T = ???
+
+def main(io: {*} Cap, net: {*} Cap): Unit = {
+  val test1 = localCap { cap => // error
+    () => { cap.use() }
+  }
+
+  val test2: (cap: {*} Cap) -> {cap} () -> Unit =
+    localCap { cap =>  // should work
+      (cap1: {*} Cap) => () => { cap1.use() }
+    }
+
+  val test3: (cap: {io} Cap) -> {io} () -> Unit =
+    localCap { cap =>  // should work
+      (cap1: {io} Cap) => () => { cap1.use() }
+    }
+
+  val test4: (cap: {io} Cap) -> {net} () -> Unit =
+    localCap { cap =>  // error
+      (cap1: {io} Cap) => () => { cap1.use() }
+    }
+
+  def localCap2[T](op: (cap: {io} Cap) => T): T = ???
+
+  val test5: {io} () -> Unit =
+    localCap2 { cap =>  // ok
+      () => { cap.use() }
+    }
+}

tests/neg-custom-args/captures/i15921.scala

@@ -0,0 +1,12 @@
+trait Stream { def close(): Unit = (); def write(x: Any): Unit = () }
+
+object Test {
+  def usingLogFile[T](op: (c: {*} Stream) => T): T =
+    val logFile = new Stream { }
+    val result = op(logFile)
+    logFile.close()
+    result
+
+  val later = usingLogFile { f => () => f.write(0) } // error
+  later()   // writing to closed file!
+}

tests/neg-custom-args/captures/try.check

@@ -2,7 +2,7 @@
 23 |  val a = handle[Exception, CanThrow[Exception]] { // error
    |                                                 ^
    |                                                 Found:    ? ({*} CT[Exception]) -> CanThrow[Exception]
-   |                                                 Required: CanThrow[Exception] => box {*} CT[Exception]
+   |                                                 Required: {*} CanThrow[Exception] -> box {*} CT[Exception]
 24 |    (x: CanThrow[Exception]) => x
 25 |  }{
    |
@@ -11,11 +11,25 @@
 29 |  val b = handle[Exception, () -> Nothing] {  // error
    |                                           ^
    |                                           Found:    ? (x: {*} CT[Exception]) -> {x} () -> Nothing
-   |                                           Required: CanThrow[Exception] => () -> Nothing
+   |                                           Required: {*} (x$0: CanThrow[Exception]) -> () -> Nothing
 30 |    (x: CanThrow[Exception]) => () => raise(new Exception)(using x)
 31 |  } {
    |
    | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:52:2 -------------------------------------------
+47 |val global: () -> Int = handle {
+48 |  (x: CanThrow[Exception]) =>
+49 |    () =>
+50 |      raise(new Exception)(using x)
+51 |      22
+52 |} {  // error
+   |                        ^
+   |                        Found:    {x$0} () -> Int
+   |                        Required: () -> Int
+53 |  (ex: Exception) => () => 22
+54 |}
+   |
+   | longer explanation available when compiling with `-explain`
 -- Error: tests/neg-custom-args/captures/try.scala:40:4 ----------------------------------------------------------------
 35 |  val xx = handle {
 36 |    (x: CanThrow[Exception]) =>
@@ -24,19 +38,7 @@
 39 |        22
 40 |  } {  // error
    |           ^
-   |           The expression's type box {*} () -> Int is not allowed to capture the root capability `*`.
+   |           The expression's type box {x$0, *} () -> Int is not allowed to capture the root capability `*`.
    |           This usually means that a capability persists longer than its allowed lifetime.
 41 |    (ex: Exception) => () => 22
 42 |  }
--- Error: tests/neg-custom-args/captures/try.scala:52:2 ----------------------------------------------------------------
-47 |val global = handle {
-48 |  (x: CanThrow[Exception]) =>
-49 |    () =>
-50 |      raise(new Exception)(using x)
-51 |      22
-52 |} {  // error
-   |             ^
-   |             The expression's type box {*} () -> Int is not allowed to capture the root capability `*`.
-   |             This usually means that a capability persists longer than its allowed lifetime.
-53 |  (ex: Exception) => () => 22
-54 |}

tests/neg-custom-args/captures/try.scala

@@ -44,11 +44,11 @@ def test =
   yy // OK
 
 
-val global = handle {
+val global: () -> Int = handle {
   (x: CanThrow[Exception]) =>
     () =>
       raise(new Exception)(using x)
       22
 } {  // error
   (ex: Exception) => () => 22
-}
+}

tests/neg-custom-args/captures/usingLogFile.check

@@ -1,13 +1,3 @@
--- Error: tests/neg-custom-args/captures/usingLogFile.scala:23:27 ------------------------------------------------------
-23 |  val later = usingLogFile { f => () => f.write(0) } // error
-   |                           ^^^^^^^^^^^^^^^^^^^^^^^^^
-   |                           {f} () -> Unit cannot be box-converted to box ? () -> Unit
-   |                           since one of their capture sets contains the root capability `*`
--- Error: tests/neg-custom-args/captures/usingLogFile.scala:29:9 -------------------------------------------------------
-29 |  later2.x()  // error
-   |  ^^^^^^^^
-   |  The expression's type box {*} () -> Unit is not allowed to capture the root capability `*`.
-   |  This usually means that a capability persists longer than its allowed lifetime.
 -- Error: tests/neg-custom-args/captures/usingLogFile.scala:33:2 -------------------------------------------------------
 33 |  later3() // error
    |  ^^^^^^
@@ -18,18 +8,32 @@
    |  ^^^^^^^^
    |  The expression's type box {*} () -> Unit is not allowed to capture the root capability `*`.
    |  This usually means that a capability persists longer than its allowed lifetime.
--- Error: tests/neg-custom-args/captures/usingLogFile.scala:47:27 ------------------------------------------------------
+-- Error: tests/neg-custom-args/captures/usingLogFile.scala:23:6 -------------------------------------------------------
+23 |  val later = usingLogFile { f => () => f.write(0) } // error
+   |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |  Non-local value later cannot have an inferred type
+   |  {x$0} () -> Unit
+   |  with non-empty capture set {x$0}.
+   |  The type needs to be declared explicitly.
+-- Error: tests/neg-custom-args/captures/usingLogFile.scala:29:9 -------------------------------------------------------
+29 |  later2.x()  // error
+   |  ^^^^^^^^
+   |  The expression's type box {x$0, *} () -> Unit is not allowed to capture the root capability `*`.
+   |  This usually means that a capability persists longer than its allowed lifetime.
+-- Error: tests/neg-custom-args/captures/usingLogFile.scala:47:6 -------------------------------------------------------
 47 |  val later = usingLogFile { f => () => f.write(0) } // error
-   |                           ^^^^^^^^^^^^^^^^^^^^^^^^^
-   |                           {f} () -> Unit cannot be box-converted to box ? () -> Unit
-   |                           since one of their capture sets contains the root capability `*`
--- Error: tests/neg-custom-args/captures/usingLogFile.scala:62:33 ------------------------------------------------------
+   |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |  Non-local value later cannot have an inferred type
+   |  {x$0} () -> Unit
+   |  with non-empty capture set {x$0}.
+   |  The type needs to be declared explicitly.
+-- Error: tests/neg-custom-args/captures/usingLogFile.scala:62:25 ------------------------------------------------------
 62 |    val later = usingFile("out", f => (y: Int) => xs.foreach(x => f.write(x + y))) // error
-   |                                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-   |                                 {f} (x$0: Int) -> Unit cannot be box-converted to box ? (x$0: Int) -> Unit
-   |                                 since one of their capture sets contains the root capability `*`
--- Error: tests/neg-custom-args/captures/usingLogFile.scala:71:37 ------------------------------------------------------
+   |                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |        The expression's type box {x$0, *} (x$0: Int) -> Unit is not allowed to capture the root capability `*`.
+   |        This usually means that a capability persists longer than its allowed lifetime.
+-- Error: tests/neg-custom-args/captures/usingLogFile.scala:71:25 ------------------------------------------------------
 71 |    val later = usingFile("logfile", usingLogger(_, l => () => l.log("test"))) // error
-   |                                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-   |                                     {_$1} () -> Unit cannot be box-converted to box ? () -> Unit
-   |                                     since one of their capture sets contains the root capability `*`
+   |                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |                The expression's type box {x$0, *} () -> Unit is not allowed to capture the root capability `*`.
+   |                This usually means that a capability persists longer than its allowed lifetime.

tests/neg-custom-args/captures/vars.check

@@ -25,7 +25,7 @@
 -- Error: tests/neg-custom-args/captures/vars.scala:32:8 ---------------------------------------------------------------
 32 |  local { cap3 => // error
    |  ^
-   |  The expression's type box {*} (x$0: String) -> String is not allowed to capture the root capability `*`.
+   |  The expression's type box {x$0, *} (x$0: String) -> String is not allowed to capture the root capability `*`.
    |  This usually means that a capability persists longer than its allowed lifetime.
 33 |    def g(x: String): String = if cap3 == cap3 then "" else "a"
 34 |    g