Check anonymous functions with fresh results for consume conditions

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

@@ -863,20 +863,23 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
           case _ =>
 
     /** If `tpe` appears as a (result-) type of a definition, treat its
-     *  hidden set minus its explicitly declared footprint as consumed.
-     *  If `tpe` appears as an argument to a consume parameter, treat
+     *  hidden set of locally owned LocalCaps minus its explicitly declared footprint
+     *  as consumed. If `tpe` appears as an argument to a consume parameter, treat
      *  its footprint as consumed.
      */
     def checkLegalRefs() = role match
       case TypeRole.Result(sym, _) =>
-        if !sym.isAnonymousFunction // we don't check return types of anonymous functions
-            && !sym.is(Case)        // We don't check so far binders in patterns since they
-                                    // have inferred universal types. TODO come back to this;
-                                    // either infer more precise types for such binders or
-                                    // "see through them" when we look at hidden sets.
+        if !sym.is(Case)  // We don't check so far binders in patterns since they
+                          // have inferred universal types. TODO come back to this;
+                          // either infer more precise types for such binders or
+                          // "see through them" when we look at hidden sets.
         then
-          val refs = tpe.deepCaptureSet.elems
-          val refsStar = refs.transHiddenSet
+          var refs = tpe.deepCaptureSet.elems
+          val refsCaps = refs.filter: elem =>
+            elem.core match
+              case core: LocalCap => core.ccOwner.isContainedIn(sym)
+              case _ => false
+          val refsStar = refsCaps.transHiddenSet
           val toCheck = refsStar.directFootprint.nonPeaks.deduct(refs.directFootprint.nonPeaks)
           def descr = i"${role.description} $tpe hides"
           checkConsumedRefs(toCheck, tpe, role, descr, pos)
@@ -1015,8 +1018,8 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
        && !isUnsafeAssumeSeparate(tree.rhs)
        && !isCoverageLiftedTemp(tree)
     then
+      capt.println(i"sep check def $sym: ${tree.tpt.nuType} with ${spanCaptures(tree.tpt).transHiddenSet.directFootprint}")
       checkType(tree.tpt, sym)
-      capt.println(i"sep check def $sym: ${tree.tpt} with ${spanCaptures(tree.tpt).transHiddenSet.directFootprint}")
       pushDef(tree, spanCaptures(tree.tpt).transHiddenSet.deductSymRefs(sym))
 
   def inSection[T](op: => T)(using Context): T =

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

@@ -54,7 +54,7 @@ object ccConfig:
 
   /** Not used currently. Handy for trying out new features */
   def newScheme(using ctx: Context): Boolean =
-    Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.9`)
+    Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.10`)
 
   /** Allow @use annotations */
   def allowUse(using Context): Boolean =

tests/neg-custom-args/captures/lambda-fresh-2.check

@@ -0,0 +1,36 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lambda-fresh-2.scala:20:29 -------------------------------
+20 |  val a: () => Ref^{fresh} = () => f1  // error
+   |                             ^^^^^^^^
+   |Found:    () ->{f1.rd} Ref^{any}
+   |Required: () => Ref^{fresh}
+   |
+   |Note that capability `any` cannot flow into capture set {fresh²}
+   |because `fresh²`, which is existentially bound in Ref^{fresh³}, cannot subsume `any`.
+   |
+   |where:    =>     refers to a root capability in the type of value a
+   |          any    is a root capability classified as Unscoped created in anonymous function of type (): Ref^{any} when instantiating expected result type Ref^{fresh} of function literal
+   |          fresh  is a root capability associated with the result type of (): Ref^{fresh}
+   |          fresh² is a root capability associated with the result type of (): Ref^{any}
+   |          fresh³ is the root capability caps.fresh
+   |
+   | longer explanation available when compiling with `-explain`
+-- Error: tests/neg-custom-args/captures/lambda-fresh-2.scala:12:36 ----------------------------------------------------
+12 |  val a: () => File^{fresh} = () => f1  // error
+   |                                    ^
+   |Separation failure: anonymous function of type (): File^{fresh}'s inferred result type File^ hides non-local value f1
+-- Error: tests/neg-custom-args/captures/lambda-fresh-2.scala:14:11 ----------------------------------------------------
+14 |  def g(): File^ = f3  // error
+   |           ^^^^^
+   |           Separation failure: method g's result type File^ hides non-local value f3
+-- Error: tests/neg-custom-args/captures/lambda-fresh-2.scala:22:11 ----------------------------------------------------
+22 |  def g(): Ref^ = f3  // error
+   |           ^^^^
+   |           Separation failure: method g's result type Ref^ hides non-local value f3
+-- Error: tests/neg-custom-args/captures/lambda-fresh-2.scala:28:35 ----------------------------------------------------
+28 |  val a: () => One^{fresh} = () => f1  // error
+   |                                   ^
+   |Separation failure: anonymous function of type (): One^{fresh}'s inferred result type One^ hides non-local value f1
+-- Error: tests/neg-custom-args/captures/lambda-fresh-2.scala:30:11 ----------------------------------------------------
+30 |  def g(): One^ = f3  // error
+   |           ^^^^
+   |           Separation failure: method g's result type One^ hides non-local value f3

tests/neg-custom-args/captures/lambda-fresh-2.scala

@@ -0,0 +1,38 @@
+import caps.*
+
+class Ref extends Mutable
+class One extends ExclusiveCapability
+class Sha extends SharedCapability
+class File
+
+def test() =
+  val f1: File^ = File()
+  val f2: File^ = File()
+  val f3: File^ = File()
+  val a: () => File^{fresh} = () => f1  // error
+  val b: () => File^ = () => f2  // ok
+  def g(): File^ = f3  // error
+
+def test1() =
+  val f1 = Ref()
+  val f2 = Ref()
+  val f3 = Ref()
+  val a: () => Ref^{fresh} = () => f1  // error
+  val b: () => Ref^ = () => f2  // ok
+  def g(): Ref^ = f3  // error
+
+def test2() =
+  val f1 = One()
+  val f2 = One()
+  val f3 = One()
+  val a: () => One^{fresh} = () => f1  // error
+  val b: () => One^ = () => f2  // ok
+  def g(): One^ = f3  // error
+
+def test3() =
+  val f1 = Sha()
+  val f2 = Sha()
+  val f3 = Sha()
+  val a: () => Sha^{fresh} = () => f1  // ok, SharedCapabilities are excluded from frhsness checking
+  val b: () => Sha^ = () => f2  // ok
+  def g(): Sha^ = f3  // ok, SharedCapabilities are excluded from frhsness checking

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

@@ -84,6 +84,16 @@
    |              ^^^^^^^^^^
    |              Separation failure: value next's type () => Unit hides parameter xs.
    |              The parameter needs to be annotated with consume to allow this.
+-- Error: tests/neg-custom-args/captures/reaches.scala:67:40 -----------------------------------------------------------
+67 |  val id: (x: File^) -> File^{fresh} = x => x // error
+   |                                        ^
+   |Separation failure: anonymous function of type (x: File^): File^{fresh}'s inferred result type File^ hides parameter x.
+   |The parameter needs to be annotated with consume to allow this.
+-- Error: tests/neg-custom-args/captures/reaches.scala:68:36 -----------------------------------------------------------
+68 |  val id2: File^ -> File^{fresh} = x => x // error
+   |                                    ^
+   |Separation failure: anonymous function of type (x: File^): File^{fresh}'s inferred result type File^ hides parameter x.
+   |The parameter needs to be annotated with consume to allow this.
 -- Error: tests/neg-custom-args/captures/reaches.scala:88:28 -----------------------------------------------------------
 88 |  ps.map((x, y) => compose1(x, y)) // error // error // error
    |                            ^

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

@@ -64,8 +64,8 @@ def attack2 =
     f1
 
 def attack3 =
-  val id: (x: File^) -> File^{fresh} = x => x // was error, now OK
-  val id2: File^ -> File^{fresh} = x => x // now also OK
+  val id: (x: File^) -> File^{fresh} = x => x // error
+  val id2: File^ -> File^{fresh} = x => x // error
 
   val leaked = usingFile[File^{id*}]: f =>
     val f1: File^{id*} = id(f)   // error

tests/neg-custom-args/captures/scoped-caps-global.scala

@@ -19,7 +19,7 @@ def test(io: Object^): Unit =
 
   val h: S -> B^ = ???
   val _: (x: S) -> B^{fresh} = h          // error: direct conversion fails
-  val _: (x: S) -> B^{fresh} = (x: S) => h(x)  // eta expansion is ok
+  val _: (x: S) -> B^{fresh} = (x: S) => h(x)  // error: eta expansion also fails since `h` is non-local
 
   val h2: S -> S = ???
   val _: (x: S) -> S^{fresh} = h2               // direct conversion OK for shared S

tests/neg-custom-args/captures/scoped-caps.check

@@ -94,3 +94,7 @@
    |          any² is a root capability in the type of value _$16
    |
    | longer explanation available when compiling with `-explain`
+-- Error: tests/neg-custom-args/captures/scoped-caps.scala:20:36 -------------------------------------------------------
+20 |  val _: (x: S) -> B^{fresh} = (x: S) => h(x)  // error: eta expansion also fails since `h` is non-local
+   |                                    ^
+   |Separation failure: anonymous function of type (x: S^): B^{fresh}'s inferred result type B^ hides non-local value h

tests/neg-custom-args/captures/scoped-caps.scala

@@ -17,7 +17,7 @@ def test(io: Object^): Unit =
 
   val h: S -> B^ = ???
   val _: (x: S) -> B^{fresh} = h          // error: direct conversion fails
-  val _: (x: S) -> B^{fresh} = (x: S) => h(x)  // eta expansion is ok
+  val _: (x: S) -> B^{fresh} = (x: S) => h(x)  // error: eta expansion also fails since `h` is non-local
 
   val h2: S -> S = ???
   val _: (x: S) -> S^{fresh} = h2               // direct conversion OK for shared S