Fix levelOK when root.Result variables are added to capture set variables.

The check was not working properly before, which meant that problems went undetected.
To make things work again, we need two additional fixes

 - A more detailed treatment of result mapping for inferred types. In these, we map
   root.Fresh to root.Result only if the original inferred type was dependent.
   AppliedType functions are also mapped to RefinedType functions in setup, but this
   should not count for fresh to result mappings.
 - A fix in the Fresh to Result mapping of parameterless defs.

Author: odersky

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

@@ -183,7 +183,7 @@ sealed abstract class CaptureSet extends Showable:
    */
   def accountsFor(x: CaptureRef)(using ctx: Context)(using vs: VarState = VarState.Separate): Boolean =
 
-    def debugInfo(using Context) = i"$this accountsFor $x, which has capture set ${x.captureSetOfInfo}"
+    def debugInfo(using Context) = i"$this accountsFor $x"
 
     def test(using Context) = reporting.trace(debugInfo):
       elems.exists(_.subsumes(x))
@@ -353,7 +353,14 @@ sealed abstract class CaptureSet extends Showable:
 
   /** Invoke handler if this set has (or later aquires) the root capability `cap` */
   def disallowRootCapability(handler: () => Context ?=> Unit)(using Context): this.type =
-    if containsRootCapability then handler()
+    val hasRoot =
+      if ccConfig.newScheme then
+        elems.exists: elem =>
+          val elem1 = elem.stripReadOnly
+          elem1.isCap || elem1.isResultRoot
+      else
+        containsRootCapability
+    if hasRoot then handler()
     this
 
   /** Invoke handler on the elements to ensure wellformedness of the capture set.
@@ -499,7 +506,7 @@ object CaptureSet:
       ccs.varId += 1
       ccs.varId
 
-    //assert(id != 40)
+    //assert(id != 8, this)
 
     /** A variable is solved if it is aproximated to a from-then-on constant set.
      *  Interpretation:
@@ -529,7 +536,7 @@ object CaptureSet:
     /** A handler to be invoked if the root reference `cap` is added to this set */
     var rootAddedHandler: () => Context ?=> Unit = () => ()
 
-    private[CaptureSet] var noUniversal = false
+    private[CaptureSet] var universalOK = true
 
     /** A handler to be invoked when new elems are added to this set */
     var newElemAddedHandler: CaptureRef => Context ?=> Unit = _ => ()
@@ -600,33 +607,38 @@ object CaptureSet:
             case _ => foldOver(b, t)
       find(false, binder)
 
-    // TODO: Also track allowable TermParamRefs and root.Results in capture sets
-    private def levelOK(elem: CaptureRef)(using Context): Boolean =
-      if elem.isRootCapability then
-        !noUniversal
-      else elem match
-        case elem @ root.Result(mt) =>
-          !noUniversal && isPartOf(mt.resType)
-        case elem: TermRef if level.isDefined =>
-          elem.prefix match
-            case prefix: CaptureRef =>
-              levelOK(prefix)
-            case _ =>
-              ccState.symLevel(elem.symbol) <= level
-        case elem: ThisType if level.isDefined =>
-          ccState.symLevel(elem.cls).nextInner <= level
-        case elem: ParamRef if !this.isInstanceOf[BiMapped] =>
-          isPartOf(elem.binder.resType)
-          || {
-            capt.println(
-              i"""LEVEL ERROR $elem for $this
-                 |elem binder = ${elem.binder}""")
+    private def levelOK(elem: CaptureRef)(using Context): Boolean = elem match
+      case elem @ root.Fresh(_) =>
+        if ccConfig.newScheme then
+          if !level.isDefined || ccState.symLevel(elem.ccOwner) <= level then true
+          else
+            println(i"LEVEL ERROR $elem cannot be included in $this of $owner")
             false
-          }
-        case QualifiedCapability(elem1) =>
-          levelOK(elem1)
-        case _ =>
-          true
+        else universalOK
+      case elem @ root.Result(mt) =>
+        universalOK && (this.isInstanceOf[BiMapped] || isPartOf(mt.resType))
+      case elem: TermRef if elem.isCap =>
+        universalOK
+      case elem: TermRef if level.isDefined =>
+        elem.prefix match
+          case prefix: CaptureRef =>
+            levelOK(prefix)
+          case _ =>
+            ccState.symLevel(elem.symbol) <= level
+      case elem: ThisType if level.isDefined =>
+        ccState.symLevel(elem.cls).nextInner <= level
+      case elem: ParamRef if !this.isInstanceOf[BiMapped] =>
+        isPartOf(elem.binder.resType)
+        || {
+          capt.println(
+            i"""LEVEL ERROR $elem for $this
+                |elem binder = ${elem.binder}""")
+          false
+        }
+      case QualifiedCapability(elem1) =>
+        levelOK(elem1)
+      case _ =>
+        true
 
     def addDependent(cs: CaptureSet)(using Context, VarState): CompareResult =
       if (cs eq this) || cs.isUniversal || isConst then
@@ -638,7 +650,7 @@ object CaptureSet:
         CompareResult.Fail(this :: Nil)
 
     override def disallowRootCapability(handler: () => Context ?=> Unit)(using Context): this.type =
-      noUniversal = true
+      universalOK = false
       rootAddedHandler = handler
       super.disallowRootCapability(handler)
 

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

@@ -211,9 +211,11 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
           case AppliedType(`tycon`, args0) => args0.last ne args.last
           case _ => false
         if expand then
-          depFun(args.init, args.last,
+          val fn = 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))
         else tp
       case _ => tp
 

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

@@ -13,7 +13,6 @@ import NameKinds.ExistentialBinderName
 import NameOps.isImpureFunction
 import reporting.Message
 import util.{SimpleIdentitySet, EqHashMap}
-import util.Spans.NoSpan
 import ast.tpd
 import annotation.constructorOnly
 
@@ -355,29 +354,38 @@ object root:
     toVar(tp)
   end toResult
 
-  /** Map global roots in function results to result roots */
-  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)
-        if mt1 ne mt then mt1.toFunctionType(alwaysDependent = true)
-        else t
-      case t: MethodType if variance > 0 && t.marksExistentialScope =>
-        val t1 = mapOver(t).asInstanceOf[MethodType]
-        t1.derivedLambdaType(resType = toResult(t1.resType, t1, fail))
-      case CapturingType(parent, refs) =>
-        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)
-          else mapFollowingAliases(t)
-        catch case ex: AssertionError =>
-          println(i"error while mapping $t")
-          throw ex
+  /** Map global roots in function results to result roots. Also,
+   *  map roots in the types of parameterless def methods.
+   */
+  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 t: MethodType if variance > 0 && t.marksExistentialScope =>
+          val t1 = mapOver(t).asInstanceOf[MethodType]
+          t1.derivedLambdaType(resType = toResult(t1.resType, t1, fail))
+        case CapturingType(parent, refs) =>
+          t.derivedCapturingType(this(parent), refs)
+        case t: (LazyRef | TypeVar) =>
+          mapConserveSuper(t)
+        case _ =>
+          try
+            if keepAliases then mapOver(t)
+            else mapFollowingAliases(t)
+          catch case ex: AssertionError =>
+            println(i"error while mapping $t")
+            throw ex
+    m(tp) match
+      case tp1: ExprType if sym.is(Method, butNot = Accessor) =>
+        tp1.derivedExprType(toResult(tp1.resType, tp1, fail))
+      case tp1 => tp1
   end toResultInResults
 
 end root

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

@@ -1038,6 +1038,7 @@ class Definitions {
   @tu lazy val DeprecatedInheritanceAnnot: ClassSymbol = requiredClass("scala.deprecatedInheritance")
   @tu lazy val ImplicitAmbiguousAnnot: ClassSymbol = requiredClass("scala.annotation.implicitAmbiguous")
   @tu lazy val ImplicitNotFoundAnnot: ClassSymbol = requiredClass("scala.annotation.implicitNotFound")
+  @tu lazy val InferredDepFunAnnot: ClassSymbol = requiredClass("scala.caps.internal.inferredDepFun")
   @tu lazy val InlineParamAnnot: ClassSymbol = requiredClass("scala.annotation.internal.InlineParam")
   @tu lazy val IntoAnnot: ClassSymbol = requiredClass("scala.annotation.into")
   @tu lazy val IntoParamAnnot: ClassSymbol = requiredClass("scala.annotation.internal.$into")

library/src/scala/caps/package.scala

@@ -122,6 +122,14 @@ object internal:
    */
   final class rootCapability extends annotation.StaticAnnotation
 
+  /** An annotation used internally to mark a function type that was
+   *  converted to a dependent function type during setup of inferred types.
+   *  Such function types should not map roots to result variables.
+   */
+  final class inferredDepFun extends annotation.StaticAnnotation
+
+end internal
+
 @experimental
 object unsafe:
   /**

tests/neg-custom-args/captures/capt-capability.scala

@@ -0,0 +1,9 @@
+import caps.{Capability, SharedCapability}
+
+def foo() =
+  val x: SharedCapability = ???
+
+  val z3 =
+    if x == null then (y: Unit) => x else (y: Unit) => new Capability() {} // error
+
+

tests/neg-custom-args/captures/class-level-attack.scala

@@ -0,0 +1,25 @@
+import language.experimental.captureChecking
+import caps.*
+
+class IO
+
+class Ref[X](init: X):
+  var x = init
+  def get: X = x
+  def put(y: X): Unit = x = y
+
+class C(io: IO^):
+  val r: Ref[IO^] = Ref[IO^](io) // error:
+    //Type variable X of constructor Ref cannot be instantiated to box IO^ since
+    //that type captures the root capability `cap`.
+    // where: ^ refers to the universal root capability
+  val r2: Ref[IO^] = Ref(io) // error:
+    //Error: Ref[IO^{io}] does not conform to Ref[IO^] (since Refs are invariant)
+  def set(x: IO^) = r.put(x)
+
+def outer(outerio: IO^) =
+  val c = C(outerio)
+  def test(innerio: IO^) =
+    c.set(innerio)
+
+

tests/pos-custom-args/captures/capt-capability.scala

@@ -1,4 +1,4 @@
-import caps.Capability
+import caps.{Capability, SharedCapability}
 
 def f1(c: Capability): () ->{c} c.type = () => c // ok
 
@@ -14,15 +14,18 @@ def f3: Int =
   x
 
 def foo() =
-  val x: Capability = ???
+  val x: SharedCapability = ???
   val y: Capability = x
   val x2: () ->{x} Capability = ???
   val y2: () ->{x} Capability = x2
 
   val z1: () => Capability = f1(x)
   def h[X](a: X)(b: X) = a
 
-  val z2 =
-    if x == null then () => x else () => new Capability() {}
+  val z2: (y: Unit) ->{x} Capability^ =
+    if x == null then (y: Unit) => x else (y: Unit) => new Capability() {}
+  // z2's type cannot be inferred, see neg test
+  //val z3 =
+  //  if x == null then (y: Unit) => x else (y: Unit) => new Capability() {}
   val _ = x
 

tests/pos-custom-args/captures/rinaudo.scala

@@ -0,0 +1,12 @@
+import language.experimental.captureChecking
+import caps.*
+
+trait FileSystem extends Capability:
+  def print(msg: String): Unit
+
+class Logger(using fs: FileSystem):
+    def info(msg: String): Unit = fs.print(msg)
+
+def log(msg: String): FileSystem ?-> Unit =
+  val l = new Logger
+  l.info(msg)