Fix root treatment of parameterless methods

 - Map cap to Result in their original types (was Fresh before)
 - Map Result to Fresh on access

Author: odersky

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

@@ -1162,7 +1162,8 @@ object CaptureSet:
     def unify(root1: root.Result, root2: root.Result)(using Context): Boolean =
       (root1, root2) match
         case (root1 @ root.Result(binder1), root2 @ root.Result(binder2))
-        if (binder1 eq binder2)
+        if ((binder1 eq binder2)
+            || binder1.isInstanceOf[ExprType] && binder2.isInstanceOf[ExprType])
           && (root1.rootAnnot.originalBinder ne root2.rootAnnot.originalBinder)
           && eqResultMap(root1) == null
           && eqResultMap(root2) == null

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

@@ -556,6 +556,16 @@ class CheckCaptures extends Recheck, SymTransformer:
         if sym.exists && curEnv.isOpen then
           markFree(capturedVars(sym).filter(isRetained), tree)
 
+    /** If `tp` (possibly after widening singletons) is an ExprType
+     *  of a parameterless method, map Result instances in it to Fresh instances
+     */
+    def mapResultRoots(tp: Type, sym: Symbol)(using Context): Type =
+      tp.widenSingleton match
+        case tp: ExprType if sym.is(Method) =>
+          root.resultToFresh(tp, root.Origin.ResultInstance(tp, sym))
+        case _ =>
+          tp
+
     /** Under the sealed policy, disallow the root capability in type arguments.
      *  Type arguments come either from a TypeApply node or from an AppliedType
      *  which represents a trait parent in a template.
@@ -618,7 +628,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         if pathRef.derivesFrom(defn.Caps_Mutable) && pt.isValueType && !pt.isMutableType then
           pathRef = pathRef.readOnly
         markFree(sym, pathRef, tree)
-      super.recheckIdent(tree, pt)
+      mapResultRoots(super.recheckIdent(tree, pt), tree.symbol)
 
     /** The expected type for the qualifier of a selection. If the selection
      *  could be part of a capability path or is a a read-only method, we return
@@ -665,7 +675,7 @@ class CheckCaptures extends Recheck, SymTransformer:
                 |since its capture set ${qualType.captureSet} is read-only""",
             tree.srcPos)
 
-      val selType = recheckSelection(tree, qualType, name, disambiguate)
+      val selType = mapResultRoots(recheckSelection(tree, qualType, name, disambiguate), tree.symbol)
       val selWiden = selType.widen
 
       // Don't apply the rule

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

@@ -323,7 +323,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
 
     try
       val tp1 = mapInferred(refine = true)(tp)
-      val tp2 = root.toResultInResults(_ => assert(false))(tp1)
+      val tp2 = root.toResultInResults(NoSymbol, _ => assert(false))(tp1)
       if tp2 ne tp then capt.println(i"expanded inferred in ${ctx.owner}: $tp  -->  $tp1  -->  $tp2")
       tp2
     catch case ex: AssertionError =>
@@ -458,7 +458,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
 
     def transform(tp: Type): Type =
       val tp1 = toCapturing(tp)
-      val tp2 = root.toResultInResults(fail, toCapturing.keepFunAliases)(tp1)
+      val tp2 = root.toResultInResults(sym, fail, toCapturing.keepFunAliases)(tp1)
       val snd = if toCapturing.keepFunAliases then "" else " 2nd time"
       if tp2 ne tp then capt.println(i"expanded explicit$snd in ${ctx.owner}: $tp  -->  $tp1  -->  $tp2")
       tp2
@@ -648,7 +648,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
 
             val paramSymss = sym.paramSymss
             def newInfo(using Context) = // will be run in this or next phase
-              root.toResultInResults(report.error(_, tree.srcPos)):
+              root.toResultInResults(sym, report.error(_, tree.srcPos)):
                 if sym.is(Method) then
                   paramsToCap(methodType(paramSymss, localReturnType))
                 else tree.tpt.nuType

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

@@ -110,7 +110,7 @@ object root:
         ""
 
   enum Kind:
-    case Result(binder: MethodType)
+    case Result(binder: MethodicType)
     case Fresh(hidden: CaptureSet.HiddenSet)(val origin: Origin)
     case Global
 
@@ -134,14 +134,14 @@ object root:
       ccs.rootId += 1
       ccs.rootId
 
-    //assert(id != 4)
+    //assert(id != 4, kind)
 
     override def symbol(using Context) = defn.RootCapabilityAnnot
     override def tree(using Context) = New(symbol.typeRef, Nil)
     override def derivedAnnotation(tree: Tree)(using Context): Annotation = this
 
     private var myOriginalKind = kind
-    def originalBinder: MethodType = myOriginalKind.asInstanceOf[Kind.Result].binder
+    def originalBinder: MethodicType = myOriginalKind.asInstanceOf[Kind.Result].binder
 
     def derivedAnnotation(binder: MethodType)(using Context): Annotation = kind match
       case Kind.Result(b) if b ne binder =>
@@ -198,13 +198,13 @@ object root:
   type Result = AnnotatedType
 
   object Result:
-    def apply(binder: MethodType)(using Context): Result =
+    def apply(binder: MethodicType)(using Context): Result =
       val hiddenSet = CaptureSet.HiddenSet(NoSymbol)
       val res = AnnotatedType(cap, Annot(Kind.Result(binder)))
       hiddenSet.owningCap = res
       res
 
-    def unapply(tp: Result)(using Context): Option[MethodType] = tp.annot match
+    def unapply(tp: Result)(using Context): Option[MethodicType] = tp.annot match
       case Annot(Kind.Result(binder)) => Some(binder)
       case _ => None
   end Result
@@ -298,7 +298,7 @@ object root:
    *  variable bound by `mt`.
    *  Stop at function or method types since these have been mapped before.
    */
-  def toResult(tp: Type, mt: MethodType, fail: Message => Unit)(using Context): Type =
+  def toResult(tp: Type, mt: MethodicType, fail: Message => Unit)(using Context): Type =
 
     abstract class CapMap extends BiTypeMap:
       override def mapOver(t: Type): Type = t match
@@ -356,7 +356,7 @@ object root:
   end toResult
 
   /** Map global roots in function results to result roots */
-  def toResultInResults(fail: Message => Unit, keepAliases: Boolean = false)(using Context): TypeMap = new TypeMap with FollowAliasesMap:
+  def toResultInResults(sym: Symbol, fail: Message => Unit, keepAliases: Boolean = false)(using Context): TypeMap = new TypeMap with FollowAliasesMap:
     def apply(t: Type): Type = t match
       case defn.RefinedFunctionOf(mt) =>
         val mt1 = apply(mt)
@@ -369,6 +369,8 @@ object root:
         t.derivedCapturingType(this(parent), refs)
       case t: (LazyRef | TypeVar) =>
         mapConserveSuper(t)
+      case t: ExprType if sym.is(Method, butNot = Accessor) =>
+        t.derivedExprType(toResult(t.resType, t, fail))
       case _ =>
         try
           if keepAliases then mapOver(t)

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

@@ -3721,7 +3721,8 @@ object Types extends TypeUtils {
   // is that most poly types are cyclic via poly params,
   // and therefore two different poly types would never be equal.
 
-  trait MethodicType extends TermType
+  trait MethodicType extends TermType:
+    def resType: Type
 
   /** A by-name parameter type of the form `=> T`, or the type of a method with no parameter list. */
   abstract case class ExprType(resType: Type)
@@ -4279,7 +4280,7 @@ object Types extends TypeUtils {
                       ps.get(elemName) match
                         case Some(elemRef) => assert(elemRef eq elem, i"bad $mt")
                         case _ =>
-                    case root.Result(binder) if binder ne mt =>
+                    case root.Result(binder: MethodType) if binder ne mt =>
                       assert(binder.paramNames.toList != mt.paramNames.toList, i"bad $mt")
                     case _ =>
               checkRefs(refs)

scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala

@@ -25,7 +25,7 @@ import scala.runtime.Statics
 import language.experimental.captureChecking
 import annotation.unchecked.uncheckedCaptures
 import caps.cap
-import caps.unsafe.{unsafeAssumeSeparate, untrackedCaptures}
+import caps.unsafe.{unsafeAssumeSeparate, unsafeAssumePure, untrackedCaptures}
 
 /**  This class implements an immutable linked list. We call it "lazy"
   *  because it computes its elements only when they are needed.
@@ -989,7 +989,12 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
 
   private sealed trait State[+A] extends Serializable {
     def head: A
-    def tail: LazyListIterable[A]^
+    def tail: LazyListIterable[A]/*^*/
+      // should be ^ but this fails checking. The problem is that
+      // the ^ in LazyListIterable[A]^ is treated as a result reference.
+      // But then it cannot be subsumed by
+      //   val tail: LazyListIterable[A]^
+      // in class State.Cons.
   }
 
   private object State {
@@ -1000,14 +1005,15 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
     }
 
     @SerialVersionUID(3L)
-    final class Cons[A](val head: A, val tail: LazyListIterable[A]^) extends State[A]
+    final class Cons[A](val head: A, val tail: LazyListIterable[A]/*^*/) extends State[A]
   }
 
   /** Creates a new LazyListIterable. */
   @inline private def newLL[A](state: => State[A]^): LazyListIterable[A]^{state} = new LazyListIterable[A](() => state)
 
   /** Creates a new State.Cons. */
-  @inline private def sCons[A](hd: A, tl: LazyListIterable[A]^): State[A]^{tl} = new State.Cons[A](hd, tl)
+  @inline private def sCons[A](hd: A, tl: LazyListIterable[A]^): State[A]^{tl} =
+    new State.Cons[A](hd, tl.unsafeAssumePure)
 
   private val anyToMarker: Any => Any = _ => Statics.pfMarker
 

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

@@ -19,14 +19,14 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15772.scala:35:34 ---------------------------------------
 35 |  val boxed2 : Observe[C]^ = box2(c) // error
    |                                  ^
-   |                                  Found:    box C^
-   |                                  Required: box C{val arg: C^?}^?
+   |Found:    box C^
+   |Required: box C{val arg: C^?}^?
    |
-   |                                  where:    ^ refers to a fresh root capability in the result type of method c
+   |where:    ^ refers to a fresh root capability created in value boxed2 when instantiating method c's type -> C^{cap}
    |
    |
-   |                                  Note that the universal capability `cap`
-   |                                  cannot be included in capture set ?
+   |Note that the universal capability `cap`
+   |cannot be included in capture set ?
    |
    | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15772.scala:46:2 ----------------------------------------

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

@@ -0,0 +1,10 @@
+-- [E164] Declaration Error: tests/neg-custom-args/captures/lazyListState.scala:12:39 ----------------------------------
+12 |  final class Cons[A](val head: A, val tail: LazyListIterable[A]^) extends State[A] // error
+   |                                       ^
+   |                 error overriding method tail in trait State of type -> LazyListIterable[A]^{cap};
+   |                   value tail of type LazyListIterable[A]^ has incompatible type
+   |
+   |                 where:    ^   refers to a fresh root capability in the type of value tail
+   |                           cap is a root capability associated with the result type of -> LazyListIterable[A²]^²
+   |
+   | longer explanation available when compiling with `-explain`

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

@@ -0,0 +1,13 @@
+class LazyListIterable[+A]
+
+private sealed trait State[+A]:
+  def head: A
+  def tail: LazyListIterable[A]^
+
+private object State:
+  object Empty extends State[Nothing]:
+    def head: Nothing = throw new NoSuchElementException("head of empty lazy list")
+    def tail: LazyListIterable[Nothing] = throw new UnsupportedOperationException("tail of empty lazy list")
+
+  final class Cons[A](val head: A, val tail: LazyListIterable[A]^) extends State[A] // error
+

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

@@ -37,8 +37,8 @@
 22 |  def tail: LazyList[Nothing]^ = ???  // error overriding
    |      ^
    |      error overriding method tail in class LazyList of type -> lazylists.LazyList[Nothing];
-   |        method tail of type -> lazylists.LazyList[Nothing]^ has incompatible type
+   |        method tail of type -> lazylists.LazyList[Nothing]^{cap} has incompatible type
    |
-   |      where:    ^ refers to a fresh root capability in the result type of method tail
+   |      where:    cap is a root capability associated with the result type of -> lazylists.LazyList[Nothing]^
    |
    | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/linear-buffer.check

@@ -8,11 +8,6 @@
   |             ^^^^^^^^^^^^^
   |         Separation failure: method bar's result type BadBuffer[T]^ hides non-local this of class class BadBuffer.
   |         The access must be in a @consume method to allow this.
--- Error: tests/neg-custom-args/captures/linear-buffer.scala:6:9 -------------------------------------------------------
-6 |  def foo = // error
-  |         ^
-  |Separation failure: method foo's inferred result type BadBuffer[box T^{}]^ hides non-local this of class class BadBuffer.
-  |The access must be in a @consume method to allow this.
 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:19:17 -----------------------------------------------------
 19 |  val buf3 = app(buf, 3) // error
    |                 ^^^

tests/neg-custom-args/captures/linear-buffer.scala

@@ -3,7 +3,7 @@ import language.experimental.captureChecking
 
 class BadBuffer[T] extends Mutable:
   mut def append(x: T): BadBuffer[T]^ = this // error
-  def foo = // error
+  def foo =
     def bar: BadBuffer[T]^ = this // error
     bar
 

tests/neg-custom-args/captures/sep-use2.check

@@ -20,31 +20,13 @@
    |          ^^^^^^^
    |          Separation failure: method cc's result type Object^ hides non-local parameter c
 -- Error: tests/neg-custom-args/captures/sep-use2.scala:18:6 -----------------------------------------------------------
-18 |    { f(cc) } // error // error
+18 |    { f(cc) } // error
    |      ^
    |      Separation failure: Illegal access to {c} which is hidden by the previous definition
    |      of method cc with result type Object^.
    |      This type hides capabilities  {c}
    |
    |      where:    ^ refers to a fresh root capability in the result type of method cc
--- Error: tests/neg-custom-args/captures/sep-use2.scala:18:8 -----------------------------------------------------------
-18 |    { f(cc) } // error // error
-   |        ^^
-   |Separation failure: argument of type  (cc : -> Object^)
-   |to a function of type (x: Object^) ->{c} Object^
-   |corresponds to capture-polymorphic formal parameter x of type  Object^²
-   |and hides capabilities  {cap, c}.
-   |Some of these overlap with the captures of the function prefix.
-   |
-   |  Hidden set of current argument        : {cap, c}
-   |  Hidden footprint of current argument  : {c}
-   |  Capture set of function prefix        : {f}
-   |  Footprint set of function prefix      : {f, c}
-   |  The two sets overlap at               : {c}
-   |
-   |where:    ^   refers to a fresh root capability in the result type of method cc
-   |          ^²  refers to a fresh root capability created in value x1 when checking argument to parameter x of method apply
-   |          cap is a fresh root capability in the result type of method cc
 -- Error: tests/neg-custom-args/captures/sep-use2.scala:20:6 -----------------------------------------------------------
 20 |    { f(c) } // error // error
    |      ^

tests/neg-custom-args/captures/sep-use2.scala

@@ -15,7 +15,7 @@ def test1(@consume c: Object^, f: (x: Object^) => Object^) =
 def test2(@consume c: Object^, f: (x: Object^) ->{c} Object^) =
   def cc: Object^ = c // error
   val x1 =
-    { f(cc) } // error // error
+    { f(cc) } // error
   val x4: Object^ = // ^ hides just c, since the Object^ in the result of `f` is existential
     { f(c) } // error // error
 

tests/neg-custom-args/captures/unsound-reach-6.check

@@ -25,4 +25,4 @@
 -- Error: tests/neg-custom-args/captures/unsound-reach-6.scala:19:14 ---------------------------------------------------
 19 |    val z = f(ys)  // error @consume failure
    |              ^^
-   |Separation failure: argument to @consume parameter with type (ys : -> List[box () ->{io} Unit]) refers to non-local parameter io
+   |Separation failure: argument to @consume parameter with type List[box () ->{io} Unit] refers to non-local parameter io