Fix unsoundness in APPLY and SELECT rules (#24159)

We have to specially treat the case where the result contains a
ResultCap. In that case
no improvement is allowed, even if the alternative capture set is empty.

Based on #24155

Author: odersky

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

@@ -1252,14 +1252,11 @@ object Capabilities:
   def toResultInResults(sym: Symbol, fail: Message => Unit, keepAliases: Boolean = false)(tp: Type)(using Context): Type =
     val m = new TypeMap with FollowAliasesMap:
       def apply(t: Type): Type = t match
-        case AnnotatedType(parent @ defn.RefinedFunctionOf(mt), ann) if ann.symbol == defn.InferredDepFunAnnot =>
-          val mt1 = mapOver(mt).asInstanceOf[MethodType]
-          if mt1 ne mt then mt1.toFunctionType(alwaysDependent = true)
-          else parent
-        case defn.RefinedFunctionOf(mt) =>
-          val mt1 = apply(mt)
-          if mt1 ne mt then mt1.toFunctionType(alwaysDependent = true)
-          else t
+        case rt @ defn.RefinedFunctionOf(mt) =>
+          rt.derivedRefinedType(refinedInfo =
+            if rt.isInstanceOf[InferredRefinedType]
+            then mapOver(mt)
+            else apply(mt))
         case t: MethodType if variance > 0 && t.marksExistentialScope =>
           val t1 = mapOver(t).asInstanceOf[MethodType]
           t1.derivedLambdaType(resType = toResult(t1.resType, t1, fail))

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

@@ -732,19 +732,26 @@ class CheckCaptures extends Recheck, SymTransformer:
                 |since its capture set ${qualType.captureSet} is read-only""",
             tree.srcPos)
 
-      val selType = mapResultRoots(recheckSelection(tree, qualType, name, disambiguate), tree.symbol)
+      val origSelType = recheckSelection(tree, qualType, name, disambiguate)
+      val selType = mapResultRoots(origSelType, tree.symbol)
       val selWiden = selType.widen
 
+      def capturesResult = origSelType.widenSingleton match
+        case ExprType(resType) => resType.captureSet.containsResultCapability
+        case _ => false
+
       // Don't apply the rule
       //   - on the LHS of assignments, or
       //   - if the qualifier or selection type is boxed, or
-      //   - the selection is either a trackable capture reference or a pure type
+      //   - the selection is either a trackable capture reference or a pure type, or
+      //   - if the selection is of a parameterless method capturing a result cap
       if noWiden(selType, pt)
           || qualType.isBoxedCapturing
           || selType.isBoxedCapturing
           || selWiden.isBoxedCapturing
           || selType.isTrackableRef
           || selWiden.captureSet.isAlwaysEmpty
+          || capturesResult
       then
         selType
       else
@@ -819,9 +826,8 @@ class CheckCaptures extends Recheck, SymTransformer:
      */
     protected override
     def recheckApplication(tree: Apply, qualType: Type, funType: MethodType, argTypes: List[Type])(using Context): Type =
-      val appType = resultToFresh(
-        super.recheckApplication(tree, qualType, funType, argTypes),
-        Origin.ResultInstance(funType, tree.symbol))
+      val resultType = super.recheckApplication(tree, qualType, funType, argTypes)
+      val appType = resultToFresh(resultType, Origin.ResultInstance(funType, tree.symbol))
       val qualCaptures = qualType.captureSet
       val argCaptures =
         for (argType, formal) <- argTypes.lazyZip(funType.paramInfos) yield
@@ -830,6 +836,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         case appType @ CapturingType(appType1, refs)
         if qualType.exists
             && !tree.fun.symbol.isConstructor
+            && !resultType.captureSet.containsResultCapability
             && qualCaptures.mightSubcapture(refs)
             && argCaptures.forall(_.mightSubcapture(refs)) =>
           val callCaptures = argCaptures.foldLeft(qualCaptures)(_ ++ _)

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

@@ -193,11 +193,12 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
           case AppliedType(`tycon`, args0) => args0.last ne args.last
           case _ => false
         if expand then
-          val fn = depFun(
+          val (fn: RefinedType) = depFun(
             args.init, args.last,
             isContextual = defn.isContextFunctionClass(tycon.classSymbol))
               .showing(i"add function refinement $tp ($tycon, ${args.init}, ${args.last}) --> $result", capt)
-          AnnotatedType(fn, Annotation(defn.InferredDepFunAnnot, util.Spans.NoSpan))
+            .runtimeChecked
+          RefinedType.inferred(fn.parent, fn.refinedName, fn.refinedInfo)
         else tp
       case _ => tp
 

compiler/src/dotty/tools/dotc/core/Types.scala

@@ -3268,12 +3268,14 @@ object Types extends TypeUtils {
 
     def checkInst(using Context): this.type = this // debug hook
 
+    def newLikeThis(parent: Type, refinedName: Name, refinedInfo: Type)(using Context): Type =
+      RefinedType(parent, refinedName, refinedInfo)
+
     final def derivedRefinedType
         (parent: Type = this.parent, refinedName: Name = this.refinedName, refinedInfo: Type = this.refinedInfo)
         (using Context): Type =
       if ((parent eq this.parent) && (refinedName eq this.refinedName) && (refinedInfo eq this.refinedInfo)) this
-      else if isPrecise then RefinedType.precise(parent, refinedName, refinedInfo)
-      else RefinedType(parent, refinedName, refinedInfo)
+      else newLikeThis(parent, refinedName, refinedInfo)
 
     /** Add this refinement to `parent`, provided `refinedName` is a member of `parent`. */
     def wrapIfMember(parent: Type)(using Context): Type =
@@ -3308,6 +3310,17 @@ object Types extends TypeUtils {
   class PreciseRefinedType(parent: Type, refinedName: Name, refinedInfo: Type)
   extends RefinedType(parent, refinedName, refinedInfo):
     override def isPrecise = true
+    override def newLikeThis(parent: Type, refinedName: Name, refinedInfo: Type)(using Context): Type =
+      PreciseRefinedType(parent, refinedName, refinedInfo)
+
+  /** Used for refined function types created at cc/Setup that come from original
+   *  generic function types. Function types of this class don't get their result
+   *  captures mapped from FreshCaps to ResultCaps with toResult.
+   */
+  class InferredRefinedType(parent: Type, refinedName: Name, refinedInfo: Type)
+  extends RefinedType(parent, refinedName, refinedInfo):
+    override def newLikeThis(parent: Type, refinedName: Name, refinedInfo: Type)(using Context): Type =
+      InferredRefinedType(parent, refinedName, refinedInfo)
 
   object RefinedType {
     @tailrec def make(parent: Type, names: List[Name], infos: List[Type])(using Context): Type =
@@ -3322,6 +3335,10 @@ object Types extends TypeUtils {
     def precise(parent: Type, name: Name, info: Type)(using Context): RefinedType =
       assert(!ctx.erasedTypes)
       unique(new PreciseRefinedType(parent, name, info)).checkInst
+
+    def inferred(parent: Type, name: Name, info: Type)(using Context): RefinedType =
+      assert(!ctx.erasedTypes)
+      unique(new InferredRefinedType(parent, name, info)).checkInst
   }
 
   /** A recursive type. Instances should be constructed via the companion object.

library/src/scala/collection/immutable/LazyListIterable.scala

@@ -311,7 +311,7 @@ final class LazyListIterable[+A] private (lazyState: LazyListIterable.EmptyMarke
         throw new RuntimeException(
           "LazyListIterable evaluation depends on its own result (self-reference); see docs for more info")
 
-      val fun = _tail.asInstanceOf[() ->{this} LazyListIterable[A]^]
+      val fun = _tail.asInstanceOf[() ->{this} LazyListIterable[A]^{this}]
       _tail = MidEvaluation
       val l =
         // `fun` returns a LazyListIterable that represents the state (head/tail) of `this`. We call `l.evaluated` to ensure

tests/neg-custom-args/captures/apply-fresh.check

@@ -0,0 +1,31 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/apply-fresh.scala:17:15 ----------------------------------
+17 |  val _: Ref = x // error
+   |               ^
+   |               Found:    (x : Ref^)
+   |               Required: Ref
+   |
+   |               Note that capability cap is not included in capture set {}.
+   |
+   |               where:    ^ and cap refer to a fresh root capability in the type of value x
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/apply-fresh.scala:21:15 ----------------------------------
+21 |  val _: Ref = y // error
+   |               ^
+   |               Found:    (y : Ref^)
+   |               Required: Ref
+   |
+   |               Note that capability cap is not included in capture set {}.
+   |
+   |               where:    ^ and cap refer to a fresh root capability in the type of value y
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/apply-fresh.scala:25:15 ----------------------------------
+25 |  val _: Ref = z // error
+   |               ^
+   |               Found:    (z : Ref^{bar.newRef})
+   |               Required: Ref
+   |
+   |               Note that capability bar.newRef is not included in capture set {}.
+   |
+   | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/apply-fresh.scala

@@ -0,0 +1,25 @@
+object Test
+
+class Ref
+
+class Foo:
+  def newRef: Ref^ = Ref()
+
+class Bar:
+  val newRef: Ref^ = Ref()
+
+def newRef: Ref^ = Ref()
+
+def test =
+
+  val f = () => newRef
+  val x = f()
+  val _: Ref = x // error
+
+  val foo = Foo()
+  val y = foo.newRef
+  val _: Ref = y // error
+
+  val bar = Bar()
+  val z = bar.newRef
+  val _: Ref = z // error

tests/neg-custom-args/captures/capt-depfun.check

@@ -1,11 +1,12 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt-depfun.scala:11:43 ----------------------------------
 11 |  val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error
    |                                         ^^^^^^^
-   |                                         Found:    Str^{} ->{ac, y, z} Str^{y, z}
-   |                                         Required: Str^{y, z} => Str^{y, z}
+   |Found:    Str^{} => Str^{y, z}
+   |Required: Str^{y, z} =>² Str^{y, z}
    |
-   |                                         Note that capability y is not included in capture set {}.
+   |Note that capability y is not included in capture set {}.
    |
-   |                                         where:    => refers to a fresh root capability in the type of value dc
+   |where:    =>  refers to a fresh root capability created in value dc when instantiating method apply's type (x: C^): Str^{x} =>³ Str^{x}
+   |          =>² refers to a fresh root capability in the type of value dc
    |
    | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/caseclass/Test_2.scala

@@ -22,4 +22,4 @@ def test(c: C) =
 
   val y4 = y3 match
     case Ref(xx) => xx
-  val y4c: () ->{y3} Unit = y4
+  val y4c: () ->{y3} Unit = y4 // error

tests/neg-custom-args/captures/cc-existential-conformance.check

@@ -1,60 +1,56 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:8:24 --------------------
 8 |  val y: A -> Fun[B^] = x // error
   |                        ^
-  |                   Found:    (x : A -> (x²: A) -> B^)
-  |                   Required: A -> A -> B^²
+  |                  Found:    (x : A -> (x²: A) -> B^)
+  |                  Required: A -> A -> B^²
   |
-  |                   Note that capability cap is not included in capture set {cap²}
-  |                   because cap is not visible from cap² in value y.
+  |                  Note that capability cap is not included in capture set {cap²}
+  |                  because cap is not visible from cap² in value y.
   |
-  |                   where:    ^ and cap   refer to a root capability associated with the result type of (x²: A): B^
-  |                             ^² and cap² refer to a fresh root capability in the type of value y
-  |                             x           is a value in method test
-  |                             x²          is a reference to a value parameter
+  |                  where:    ^           refers to a root capability associated with the result type of (x²: A): B^
+  |                            ^² and cap² refer to a fresh root capability in the type of value y
+  |                            cap         is the universal root capability
+  |                            x           is a value in method test
+  |                            x²          is a reference to a value parameter
   |
   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:9:29 --------------------
 9 |  val z: A -> (x: A) -> B^ = y // error
   |                             ^
-  |                      Found:    A -> A -> B^{y*}
-  |                      Required: A -> (x: A) -> B^
+  |                           Found:    A -> A -> B^{y*}
+  |                           Required: A -> (x: A) -> B^
   |
-  |                      Note that capability y* is not included in capture set {cap}.
+  |                           Note that capability y* is not included in capture set {cap}.
   |
-  |                      Note that the existential capture root in B^²
-  |                      cannot subsume the capability y* since that capability is not a `Sharable` capability..
-  |
-  |                      where:    ^ and cap refer to a root capability associated with the result type of (x: A): B^
-  |                                ^²        refers to the universal root capability
+  |                           where:    ^   refers to a root capability associated with the result type of (x: A): B^
+  |                                     cap is the universal root capability
   |
   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:13:19 -------------------
 13 |  val y: Fun[B^] = x // error
    |                   ^
-   |                 Found:    (x : (x²: A) -> B^)
-   |                 Required: A -> B^²
+   |                Found:    (x : (x²: A) -> B^)
+   |                Required: A -> B^²
    |
-   |                 Note that capability cap is not included in capture set {cap²}
-   |                 because cap is not visible from cap² in value y.
+   |                Note that capability cap is not included in capture set {cap²}
+   |                because cap is not visible from cap² in value y.
    |
-   |                 where:    ^ and cap   refer to a root capability associated with the result type of (x²: A): B^
-   |                           ^² and cap² refer to a fresh root capability in the type of value y
-   |                           x           is a value in method test2
-   |                           x²          is a reference to a value parameter
+   |                where:    ^           refers to a root capability associated with the result type of (x²: A): B^
+   |                          ^² and cap² refer to a fresh root capability in the type of value y
+   |                          cap         is the universal root capability
+   |                          x           is a value in method test2
+   |                          x²          is a reference to a value parameter
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:14:24 -------------------
 14 |  val z: (x: A) -> B^ = y // error
    |                        ^
-   |                    Found:    A -> B^{y*}
-   |                    Required: (x: A) -> B^
-   |
-   |                    Note that capability y* is not included in capture set {cap}.
+   |                        Found:    A -> B^{y*}
+   |                        Required: (x: A) -> B^
    |
-   |                    Note that the existential capture root in B^²
-   |                    cannot subsume the capability y* since that capability is not a `Sharable` capability..
+   |                        Note that capability y* is not included in capture set {cap}.
    |
-   |                    where:    ^ and cap refer to a root capability associated with the result type of (x: A): B^
-   |                              ^²        refers to the universal root capability
+   |                        where:    ^   refers to a root capability associated with the result type of (x: A): B^
+   |                                  cap is the universal root capability
    |
    | longer explanation available when compiling with `-explain`