Fix apply rule

compiler/src/dotty/tools/dotc/ast/untpd.scala

@@ -523,7 +523,10 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {
   def rootDot(name: Name)(implicit src: SourceFile): Select = Select(Ident(nme.ROOTPKG), name)
   def scalaDot(name: Name)(implicit src: SourceFile): Select = Select(rootDot(nme.scala), name)
   def scalaAnnotationDot(name: Name)(using SourceFile): Select = Select(scalaDot(nme.annotation), name)
+  def scalaAnnotationInternalDot(name: Name)(using SourceFile): Select = Select(scalaAnnotationDot(nme.internal), name)
   def scalaRuntimeDot(name: Name)(using SourceFile): Select = Select(scalaDot(nme.runtime), name)
+  def scalaCapsDot(name: Name)(using SourceFile): Select = Select(scalaDot(nme.caps), name)
+  def scalaCapsInternalDot(name: Name)(using SourceFile): Select = Select(scalaCapsDot(nme.internal), name)
   def scalaUnit(implicit src: SourceFile): Select = scalaDot(tpnme.Unit)
   def scalaAny(implicit src: SourceFile): Select = scalaDot(tpnme.Any)
 
@@ -553,16 +556,16 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {
     Annotated(parent, annot)
 
   def makeReachAnnot()(using Context): Tree =
-    New(ref(defn.ReachCapabilityAnnot.typeRef), Nil :: Nil)
+    New(scalaAnnotationInternalDot(tpnme.reachCapability), Nil :: Nil)
 
   def makeReadOnlyAnnot()(using Context): Tree =
-    New(ref(defn.ReadOnlyCapabilityAnnot.typeRef), Nil :: Nil)
+    New(scalaAnnotationInternalDot(tpnme.readOnlyCapability), Nil :: Nil)
 
   def makeOnlyAnnot(qid: Tree)(using Context) =
-    New(AppliedTypeTree(ref(defn.OnlyCapabilityAnnot.typeRef), qid :: Nil), Nil :: Nil)
+    New(AppliedTypeTree(scalaAnnotationInternalDot(tpnme.onlyCapability), qid :: Nil), Nil :: Nil)
 
   def makeConsumeAnnot()(using Context): Tree =
-    New(ref(defn.ConsumeAnnot.typeRef), Nil :: Nil)
+    New(scalaCapsInternalDot(tpnme.consume), Nil :: Nil)
 
   def makeConstructor(tparams: List[TypeDef], vparamss: List[List[ValDef]], rhs: Tree = EmptyTree)(using Context): DefDef =
     DefDef(nme.CONSTRUCTOR, joinParams(tparams, vparamss), TypeTree(), rhs)

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

@@ -87,6 +87,8 @@ class CCState:
 
   private var collapseFresh: Boolean = false
 
+  private var discardUses: Boolean = false
+
 object CCState:
 
   /** If we are currently in capture checking or setup, and `mt` is a method
@@ -137,4 +139,16 @@ object CCState:
   /** Should all FreshCap instances be treated as equal to GlobalCap? */
   def collapseFresh(using Context): Boolean = ccState.collapseFresh
 
+  /** Run `op` but suppress all recording of uses in `markFree` */
+   inline def withDiscardedUses[T](op: => T)(using Context): T =
+    if isCaptureCheckingOrSetup then
+      val ccs = ccState
+      val saved = ccs.discardUses
+      ccs.discardUses = true
+      try op finally ccs.discardUses = saved
+    else op
+
+  /** Should uses not be recorded in markFree? */
+  def discardUses(using Context): Boolean = ccState.discardUses
+
 end CCState

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

@@ -130,8 +130,8 @@ object CheckCaptures:
                 |A classifier class is a class extending `caps.Capability` and directly extending `caps.Classifier`.""",
             ann.srcPos)
         check(ref)
-      case tpe =>
-        report.error(em"$elem: $tpe is not a legal element of a capture set", ann.srcPos)
+      case elem =>
+        report.error(em"$elem is not a legal element of a capture set", ann.srcPos)
     ann.retainedSet.retainedElementsRaw.foreach(check)
 
   /** Disallow bad roots anywhere in type `tp``.
@@ -574,7 +574,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           	// Under deferredReaches, don't propagate out of methods inside terms.
           	// The use set of these methods will be charged when that method is called.
 
-      if !cs.isAlwaysEmpty then
+      if !cs.isAlwaysEmpty && !CCState.discardUses then
         recur(cs, curEnv, null)
         if addUseInfo then useInfos += ((tree, cs, curEnv))
     end markFree
@@ -783,6 +783,9 @@ class CheckCaptures extends Recheck, SymTransformer:
           else argType0.widen.stripCapturing
         capt.println(i"rechecking unsafeAssumePure of $arg with $pt: $argType")
         super.recheckFinish(argType, tree, pt)
+      else if meth == defn.Caps_unsafeDiscardUses then
+        val arg :: Nil = tree.args: @unchecked
+        withDiscardedUses(recheck(arg, pt))
       else
         val res = super.recheckApply(tree, pt)
         includeCallCaptures(meth, res, tree)
@@ -837,6 +840,8 @@ class CheckCaptures extends Recheck, SymTransformer:
       appType match
         case appType @ CapturingType(appType1, refs)
         if qualType.exists
+            && !qualType.isBoxedCapturing
+            && !resultType.isBoxedCapturing
             && !tree.fun.symbol.isConstructor
             && !resultType.captureSet.containsResultCapability
             && qualCaptures.mightSubcapture(refs)

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

@@ -1026,6 +1026,7 @@ class Definitions {
     @tu lazy val CapsUnsafeModule: Symbol = requiredModule("scala.caps.unsafe")
     @tu lazy val Caps_unsafeAssumePure: Symbol = CapsUnsafeModule.requiredMethod("unsafeAssumePure")
     @tu lazy val Caps_unsafeAssumeSeparate: Symbol = CapsUnsafeModule.requiredMethod("unsafeAssumeSeparate")
+    @tu lazy val Caps_unsafeDiscardUses: Symbol = CapsUnsafeModule.requiredMethod("unsafeDiscardUses")
     @tu lazy val Caps_unsafeErasedValue: Symbol = CapsUnsafeModule.requiredMethod("unsafeErasedValue")
     @tu lazy val Caps_ContainsTrait: TypeSymbol = CapsModule.requiredType("Contains")
     @tu lazy val Caps_ContainsModule: Symbol = requiredModule("scala.caps.Contains")

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

@@ -573,6 +573,7 @@ object StdNames {
     val ofDim: N                = "ofDim"
     val on: N                   = "on"
     val only: N                 = "only"
+    val onlyCapability: N       = "onlyCapability"
     val opaque: N               = "opaque"
     val open: N                 = "open"
     val ordinal: N              = "ordinal"
@@ -591,6 +592,8 @@ object StdNames {
     val productPrefix: N        = "productPrefix"
     val quotes : N              = "quotes"
     val raw_ : N                = "raw"
+    val reachCapability: N      = "reachCapability"
+    val readOnlyCapability: N   = "readOnlyCapability"
     val rd: N                   = "rd"
     val refl: N                 = "refl"
     val reflect: N              = "reflect"

library/src/scala/caps/package.scala

@@ -208,6 +208,9 @@ object unsafe:
    */
   def unsafeAssumeSeparate(op: Any): op.type = op
 
+  /** A wrapper around code for which uses go unrecorded */
+  def unsafeDiscardUses(op: Any): op.type = op
+
   /** An unsafe variant of erasedValue that can be used as an escape hatch. Unlike the
    *  user-accessible compiletime.erasedValue, this version is assumed
    *  to be a pure expression, hence capability safe. But there is no proof

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

@@ -1264,13 +1264,26 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
     if (it.hasNext) eagerCons(it.next(), newLL(eagerHeadFromIterator(it)))
     else Empty
 
+  // TODO This should be (xss: (collection.Iterable[A]^)*)
   override def concat[A](xss: collection.Iterable[A]*): LazyListIterable[A] =
     if (xss.knownSize == 0) empty
     else newLL(eagerHeadConcatIterators(xss.iterator))
 
-  private def eagerHeadConcatIterators[A](it: Iterator[collection.Iterable[A]^]^): LazyListIterable[A]^{it} =
-    if (!it.hasNext) Empty
-    else eagerHeadPrependIterator(it.next().iterator)(eagerHeadConcatIterators(it))
+  /* TODO This should be:
+  private def eagerHeadConcatIterators[A](it: Iterator[collection.Iterable[A]^]^): LazyListIterable[A]^{it*} =
+    if !it.hasNext then Empty
+    else
+      eagerHeadPrependIterator
+          (caps.unsafe.unsafeDiscardUses(it.next()).iterator)
+          (eagerHeadConcatIterators(it))
+  */
+
+  private def eagerHeadConcatIterators[A](it: Iterator[collection.Iterable[A]]^): LazyListIterable[A]^{it} =
+    if !it.hasNext then Empty
+    else
+      eagerHeadPrependIterator
+          (it.next().iterator)
+          (eagerHeadConcatIterators(it))
 
   /** An infinite LazyListIterable that repeatedly applies a given function to a start value.
     *

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

@@ -0,0 +1,46 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/apply-rule.scala:3:19 ------------------------------------
+3 |  val _: () -> A = x // error
+  |                   ^
+  |                   Found:    (x : () ->{s*} A^{})
+  |                   Required: () -> A
+  |
+  |                   Note that capability s* is not included in capture set {}.
+  |
+  | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/apply-rule.scala:5:19 ------------------------------------
+5 |  val _: () -> A = y // error
+  |                   ^
+  |                   Found:    (y : () ->{s*} A^{})
+  |                   Required: () -> A
+  |
+  |                   Note that capability s* is not included in capture set {}.
+  |
+  | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/apply-rule.scala:9:19 ------------------------------------
+9 |  val _: () -> A = x // error
+  |                   ^
+  |                   Found:    (x : () ->{C} A^{})
+  |                   Required: () -> A
+  |
+  |                   Note that capability C is not included in capture set {}.
+  |
+  | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/apply-rule.scala:11:19 -----------------------------------
+11 |  val _: () -> A = y // error
+   |                   ^
+   |                   Found:    (y : () ->{C} A^{})
+   |                   Required: () -> A
+   |
+   |                   Note that capability C is not included in capture set {}.
+   |
+   | longer explanation available when compiling with `-explain`
+-- Error: tests/neg-custom-args/captures/apply-rule.scala:2:11 ---------------------------------------------------------
+2 |  val x = s(0) // error
+  |          ^^^^
+  |          Local reach capability s* leaks into capture scope of method select.
+  |          You could try to abstract the capabilities referred to by s* in a capset variable.
+-- Error: tests/neg-custom-args/captures/apply-rule.scala:4:12 ---------------------------------------------------------
+4 |  val y = s.head // error
+  |          ^^^^^^
+  |          Local reach capability s* leaks into capture scope of method select.
+  |          You could try to abstract the capabilities referred to by s* in a capset variable.

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

@@ -0,0 +1,16 @@
+def select[A](s: Seq[() => A]) =
+  val x = s(0) // error
+  val _: () -> A = x // error
+  val y = s.head // error
+  val _: () -> A = y // error
+
+def select2[A, C^](s: Seq[() ->{C} A]) =
+  val x = s(0)
+  val _: () -> A = x // error
+  val y = s.head
+  val _: () -> A = y // error
+
+
+
+
+

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

@@ -0,0 +1,12 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/nicolas1.scala:10:2 --------------------------------------
+10 |  val all: Seq[Rand ?->{head, tail*} A] = head +: tail // error
+   |  ^
+   |  Found:    (contextual$1: Rand^'s1) ?->{head, tail*} A^'s2
+   |  Required: (Rand^) ?->{head} A
+   |
+   |  Note that capability tail* is not included in capture set {head}.
+   |
+   |  where:    ^ refers to the universal root capability
+11 |  all(nextInt(all.length))
+   |
+   | longer explanation available when compiling with `-explain`

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

@@ -0,0 +1,11 @@
+import caps.*
+
+trait Rand extends SharedCapability:
+  def range(min: Int, max: Int): Int
+
+def nextInt(max: Int): Rand ?-> Int =
+  r ?=> r.range(0, max)
+
+def oneOf[A](head: Rand ?=> A, tail: (Rand ?=> A)*): Rand ?->{head} A =
+  val all: Seq[Rand ?->{head, tail*} A] = head +: tail // error
+  all(nextInt(all.length))

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

@@ -0,0 +1,2 @@
+def test(c: Object^) =
+  val x: () -> Unit = caps.unsafe.unsafeDiscardUses(() => println(c))