First stab at useless checking

Several TODOs need follow-up

Author: odersky

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

@@ -99,9 +99,17 @@ extension (tp: Type)
     case AnnotatedType(tp1, ann) if tp1.derivesFrom(defn.Caps_CapSet) && ann.symbol.isRetains =>
       ann.tree.retainedSet.retainedElementsRaw
     case tp =>
-      // Nothing is a special type to represent the empty set
-      if tp.isNothingType then Nil
-      else tp :: Nil // should be checked by wellformedness
+      tp.dealiasKeepAnnots match
+        case tp: TypeRef if tp.symbol == defn.Caps_CapSet =>
+          // This can happen in cases where we try to type an eta expansion `$x => f($x)`
+          // from a polymorphic target type using capture sets. In that case the parameter type
+          // of $x is not treated as inferred is approximated to CapSet. An example is
+          // capset-problem.scala. We handle these cases by appromxating to the empty set.
+          Nil
+        case _ =>
+          // Nothing is a special type to represent the empty set
+          if tp.isNothingType then Nil
+          else tp :: Nil // should be checked by wellformedness
 
   /** A list of capabilities of a retained set. */
   def retainedElements(using Context): List[Capability] =
@@ -571,18 +579,30 @@ extension (sym: Symbol)
   def hasTrackedParts(using Context): Boolean =
     !CaptureSet.ofTypeDeeply(sym.info).isAlwaysEmpty
 
-  /** `sym` itself or its info is annotated @use or it is a type parameter with a matching
-   *  @use-annotated term parameter that contains `sym` in its deep capture set.
+  /** Until 3.7:
+   *    `sym` itself or its info is annotated @use or it is a type parameter with a matching
+   *    @use-annotated term parameter that contains `sym` in its deep capture set.
+   *  From 3.8:
+   *    `sym` is a capset parameter without a `@reserve` annotation that
+   *      - belongs to a class in a class, or
+   *      - belongs to a method where it appears in a the deep capture set of a following term parameter of the same method.
    */
   def isUseParam(using Context): Boolean =
     sym.hasAnnotation(defn.UseAnnot)
     || sym.info.hasAnnotation(defn.UseAnnot)
     || sym.is(TypeParam)
-        && sym.owner.rawParamss.nestedExists: param =>
-            param.is(TermParam) && param.hasAnnotation(defn.UseAnnot)
-            && param.info.deepCaptureSet.elems.exists:
-                case c: TypeRef => c.symbol == sym
-                case _ => false
+        && !sym.info.hasAnnotation(defn.ReserveAnnot)
+        && (sym.owner.isClass
+            || sym.owner.rawParamss.nestedExists: param =>
+                param.is(TermParam)
+                && (!ccConfig.allowUse || param.hasAnnotation(defn.UseAnnot))
+                && param.info.deepCaptureSet.elems.exists:
+                    case c: TypeRef => c.symbol == sym
+                    case _ => false
+            || {
+              //println(i"not is use param $sym")
+              false
+            })
 
   /** `sym` or its info is annotated with `@consume`. */
   def isConsumeParam(using Context): Boolean =

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

@@ -1802,6 +1802,7 @@ class CheckCaptures extends Recheck, SymTransformer:
 
             checkAnnot(defn.UseAnnot)
             checkAnnot(defn.ConsumeAnnot)
+            checkAnnot(defn.ReserveAnnot)
       end OverridingPairsCheckerCC
 
       def traverse(t: Tree)(using Context) =

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

@@ -752,7 +752,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
     end postProcess
 
     /** Check that @use and @consume annotations only appear on parameters and not on
-     *  anonymous function parameters
+     *  anonymous function parameters. Check that @use annotations don't appear
+     *  at all from 3.8 on.
      */
     def checkProperUseOrConsume(tree: Tree)(using Context): Unit = tree match
       case tree: MemberDef =>
@@ -766,11 +767,22 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
               && !(sym.is(Method) && sym.owner.isClass)
             then
               report.error(
-                em"""@consume cannot be used here. Only memeber methods and their term parameters
+                em"""@consume cannot be used here. Only member methods and their term parameters
                     |can have @consume annotations.""",
                 tree.srcPos)
           else if annotCls == defn.UseAnnot then
-            if !isMethodParam then
+            if !ccConfig.allowUse then
+              if sym.is(TypeParam) then
+                report.error(
+                  em"""@use is redundant here and should no longer be written explicitly.
+                      |Capset variables are always implicitly used, unless they are annotated with @caps.preserve.""",
+                  tree.srcPos)
+              else
+                report.error(
+                  em"""@use is no longer supported. Instead of @use you can introduce capset
+                      |variables for the polymorphic parts of parameter types.""",
+                  tree.srcPos)
+            else if !isMethodParam then
               report.error(
                 em"@use cannot be used here. Only method parameters can have @use annotations.",
                 tree.srcPos)

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

@@ -50,12 +50,11 @@ object ccConfig:
   def useFreshLevels(using Context): Boolean =
     Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`)
 
-  /** If true, turn on separation checking */
-  def useSepChecks(using Context): Boolean =
-    Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.8`)
-
   /** Not used currently. Handy for trying out new features */
   def newScheme(using ctx: Context): Boolean =
     Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`)
 
+  def allowUse(using Context): Boolean =
+    Feature.sourceVersion.stable.isAtMost(SourceVersion.`3.7`)
+
 end ccConfig

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

@@ -1074,8 +1074,9 @@ class Definitions {
   @tu lazy val UncheckedVarianceAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedVariance")
   @tu lazy val UncheckedCapturesAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedCaptures")
   @tu lazy val UntrackedCapturesAnnot: ClassSymbol = requiredClass("scala.caps.unsafe.untrackedCaptures")
-  @tu lazy val UseAnnot:  ClassSymbol = requiredClass("scala.caps.use")
-  @tu lazy val ConsumeAnnot:  ClassSymbol = requiredClass("scala.caps.consume")
+  @tu lazy val UseAnnot: ClassSymbol = requiredClass("scala.caps.use")
+  @tu lazy val ConsumeAnnot: ClassSymbol = requiredClass("scala.caps.consume")
+  @tu lazy val ReserveAnnot: ClassSymbol = requiredClass("scala.caps.reserve")
   @tu lazy val RefineOverrideAnnot:  ClassSymbol = requiredClass("scala.caps.internal.refineOverride")
   @tu lazy val VolatileAnnot: ClassSymbol = requiredClass("scala.volatile")
   @tu lazy val LanguageFeatureMetaAnnot: ClassSymbol = requiredClass("scala.annotation.meta.languageFeature")
@@ -1476,7 +1477,7 @@ class Definitions {
   def patchStdLibClass(denot: ClassDenotation)(using Context): Unit =
     // Do not patch the stdlib files if we explicitly disable it
     // This is only to be used during the migration of the stdlib
-    if ctx.settings.YnoStdlibPatches.value then 
+    if ctx.settings.YnoStdlibPatches.value then
       return
 
     def patch2(denot: ClassDenotation, patchCls: Symbol): Unit =
@@ -2111,8 +2112,9 @@ class Definitions {
     CapsModule, CapsModule.moduleClass, PureClass,
     Caps_Capability, // TODO: Remove when Capability is stabilized
     RequiresCapabilityAnnot,
-    captureRoot, Caps_CapSet, Caps_ContainsTrait, Caps_ContainsModule, Caps_ContainsModule.moduleClass, UseAnnot,
-    Caps_Mutable, Caps_Sharable, Caps_Control, Caps_Classifier, ConsumeAnnot,
+    captureRoot, Caps_CapSet, Caps_ContainsTrait, Caps_ContainsModule, Caps_ContainsModule.moduleClass,
+    Caps_Mutable, Caps_Sharable, Caps_Control, Caps_Classifier,
+    ConsumeAnnot, UseAnnot, ReserveAnnot,
     CapsUnsafeModule, CapsUnsafeModule.moduleClass,
     CapsInternalModule, CapsInternalModule.moduleClass,
     RetainsAnnot, RetainsCapAnnot, RetainsByNameAnnot)

compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala

@@ -137,6 +137,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
     keywordText("erased ").provided(isErased)
     ~ specialAnnotText(defn.UseAnnot, arg)
     ~ specialAnnotText(defn.ConsumeAnnot, arg)
+    ~ specialAnnotText(defn.ReserveAnnot, arg)
     ~ homogenizeArg(arg).match
         case arg: TypeBounds => "?" ~ toText(arg)
         case arg => toText(arg)

compiler/src/dotty/tools/dotc/typer/Typer.scala

@@ -602,7 +602,11 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
   def typedIdent(tree: untpd.Ident, pt: Type)(using Context): Tree =
     record("typedIdent")
     val name = tree.name
-    def kind = if (name.isTermName) "" else "type "
+    def kind =
+      if name.isTermName then
+        if ctx.mode.is(Mode.InCaptureSet) then "capability "
+        else ""
+      else "type "
     typr.println(s"typed ident $kind$name in ${ctx.owner}")
     if ctx.mode.is(Mode.Pattern) then
       if name == nme.WILDCARD then

library/src/scala/caps/package.scala

@@ -70,15 +70,25 @@ object Contains:
   @experimental
   given containsImpl[C >: CapSet <: CapSet @retainsCap, R <: Singleton]: Contains[C, R]()
 
-/** An annotation on parameters `x` stating that the method's body makes
- *  use of the reach capability `x*`. Consequently, when calling the method
- *  we need to charge the deep capture set of the actual argiment to the
+/** An annotation on capset parameters `C` stating that the method's body does not
+ *  have `C` in its use-set. `C` might be accessed under a box in the method
+ *  or in the result type of the method. Consequently, when calling the method
+ *  we do not need to charge the capture set of the actual argiment to the
  *  environment.
  *
  *  Note: This should go into annotations. For now it is here, so that we
  *  can experiment with it quickly between minor releases
  */
 @experimental
+final class reserve extends annotation.StaticAnnotation
+
+/** Allowed only for source versions up to 3.7:
+ *  An annotation on parameters `x` stating that the method's body makes
+ *  use of the reach capability `x*`. Consequently, when calling the method
+ *  we need to charge the deep capture set of the actual argiment to the
+ *  environment.
+ */
+@experimental
 final class use extends annotation.StaticAnnotation
 
 /** An annotations on parameters and update methods.