Use level checking for Fresh instances (#23101)

This PR changes the way we treat fresh instances. Instead of disallowing
all of them when instantiating type parameters (as well as in a number
of other situations), we allow them but check that inner fresh instances
do not get widened to outer ones. This makes code like this one compile
```scala
class Ref extends Mutable:
  var x = 0
  def get: Int = x
  mut def put(y: Int): Unit = x = y

class Pair[+X, +Y](val fst: X, val snd: Y)

def twoRefs1(): Pair[Ref^, Ref^] =
  Pair(Ref(), Ref())
```
Previously, that would not work since the `X` and `Y` variables of
`Pair` would be instantiated to `Ref^`, which was not allowed.

The PR also implements lots of improvements to error diagnostics.

 - We now disambiguate different instances of `^`, `cap`, or `=>`.
 - We explain for each such instances what it represents exactly.
- We also turn this on for override errors (not necessarily limited to
capture checking).

Author: odersky

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

@@ -118,6 +118,8 @@ class CCState:
 
   private var capIsRoot: Boolean = false
 
+  private var ignoreFreshLevels: Boolean = false
+
 object CCState:
 
   opaque type Level = Int
@@ -162,4 +164,20 @@ object CCState:
   /** Is `caps.cap` a root capability that is allowed to subsume other capabilities? */
   def capIsRoot(using Context): Boolean = ccState.capIsRoot
 
+  /** Run `op` under the assumption that all root.Fresh instances are equal.
+   *  Needed to make override checking of types containing fresh work.
+   *  Asserted in override checking, tested in maxSubsumes.
+   *  Is this sound? Test case is neg-custom-args/captures/leaked-curried.scala.
+   */
+  inline def ignoringFreshLevels[T](op: => T)(using Context): T =
+    if isCaptureCheckingOrSetup then
+      val ccs = ccState
+      val saved = ccs.ignoreFreshLevels
+      ccs.ignoreFreshLevels = true
+      try op finally ccs.ignoreFreshLevels = saved
+    else op
+
+  /** Should all root.Fresh instances be treated equal? */
+  def ignoreFreshLevels(using Context): Boolean = ccState.ignoreFreshLevels
+
 end CCState

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

@@ -4,20 +4,18 @@ package cc
 
 import core.*
 import Types.*, Symbols.*, Contexts.*, Annotations.*, Flags.*
-import Names.TermName
+import Names.{Name, TermName}
 import ast.{tpd, untpd}
 import Decorators.*, NameOps.*
 import config.Printers.capt
 import util.Property.Key
 import tpd.*
+import Annotations.Annotation
 import CaptureSet.VarState
 
 /** Attachment key for capturing type trees */
 private val Captures: Key[CaptureSet] = Key()
 
-/** Context property to print root.Fresh(...) as "fresh" instead of "cap" */
-val PrintFresh: Key[Unit] = Key()
-
 /** Are we at checkCaptures phase? */
 def isCaptureChecking(using Context): Boolean =
   ctx.phaseId == Phases.checkCapturesPhase.id
@@ -465,7 +463,9 @@ extension (tp: Type)
             if args.forall(_.isAlwaysPure) then
               // Also map existentials in results to reach capabilities if all
               // preceding arguments are known to be always pure
-              t.derivedFunctionOrMethod(args, apply(root.resultToFresh(res)))
+              t.derivedFunctionOrMethod(
+                args,
+                apply(root.resultToFresh(res, root.Origin.ResultInstance(t, NoSymbol))))
             else
               t
           case _ =>
@@ -505,6 +505,10 @@ extension (tp: Type)
     case tp: ThisType => ccState.symLevel(tp.cls).nextInner
     case _ => CCState.undefinedLevel
 
+  def refinedOverride(name: Name, rinfo: Type)(using Context): Type =
+    RefinedType(tp, name,
+      AnnotatedType(rinfo, Annotation(defn.RefineOverrideAnnot, util.Spans.NoSpan)))
+
 extension (tp: MethodType)
   /** A method marks an existential scope unless it is the prefix of a curried method */
   def marksExistentialScope(using Context): Boolean =
@@ -694,6 +698,12 @@ abstract class AnnotatedCapability(annotCls: Context ?=> ClassSymbol):
   protected def unwrappable(using Context): Set[Symbol]
 end AnnotatedCapability
 
+object QualifiedCapability:
+  def unapply(tree: AnnotatedType)(using Context): Option[CaptureRef] = tree match
+    case AnnotatedType(parent: CaptureRef, ann)
+    if defn.capabilityQualifierAnnots.contains(ann.symbol) => Some(parent)
+    case _ => None
+
 /** An extractor for `ref @maybeCapability`, which is used to express
  *  the maybe capability `ref?` as a type.
  */
@@ -792,7 +802,8 @@ abstract class DeepTypeAccumulator[T](using Context) extends TypeAccumulator[T]:
       case AnnotatedType(parent, _) =>
         this(acc, parent)
       case t @ FunctionOrMethod(args, res) =>
-        if args.forall(_.isAlwaysPure) then this(acc, root.resultToFresh(res))
+        if args.forall(_.isAlwaysPure) then
+          this(acc, root.resultToFresh(res, root.Origin.ResultInstance(t, NoSymbol)))
         else acc
       case _ =>
         foldOver(acc, t)

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

@@ -14,7 +14,9 @@ import compiletime.uninitialized
 import StdNames.nme
 import CaptureSet.VarState
 import Annotations.Annotation
+import Flags.*
 import config.Printers.capt
+import CCState.{Level, undefinedLevel}
 
 object CaptureRef:
   opaque type Validity = Int
@@ -106,6 +108,10 @@ trait CaptureRef extends TypeProxy, ValueType:
     case root.Fresh(_) => true
     case _ => false
 
+  final def isResultRoot(using Context): Boolean = this match
+    case root.Result(_) => true
+    case _ => false
+
   /** Is this reference the generic root capability `cap` or a Fresh instance? */
   final def isCapOrFresh(using Context): Boolean = isCap || isFresh
 
@@ -122,6 +128,41 @@ trait CaptureRef extends TypeProxy, ValueType:
   final def isExclusive(using Context): Boolean =
     !isReadOnly && (isRootCapability || captureSetOfInfo.isExclusive)
 
+  /** The owning symbol associated with a capability this is
+   *   - for Fresh capabilities: the owner of the hidden set
+   *   - for TermRefs and TypeRefs: the symbol it refers to
+   *   - for derived and path capabilities: the owner of the underlying capability
+   *   - otherwise NoSymbol
+   */
+  final def ccOwner(using Context): Symbol = this match
+    case root.Fresh(hidden) =>
+      hidden.owner
+    case ref: NamedType =>
+      if ref.isCap then NoSymbol
+      else ref.prefix match
+        case prefix: CaptureRef => prefix.ccOwner
+        case _ => ref.symbol
+    case ref: ThisType =>
+      ref.cls
+    case QualifiedCapability(ref1) =>
+      ref1.ccOwner
+    case _ =>
+      NoSymbol
+
+  /** The symbol that represents the level closest-enclosing ccOwner.
+   *  Symbols representing levels are
+   *   - class symbols, but not inner (non-static) module classes
+   *   - method symbols, but not accessors or constructors
+   */
+  final def levelOwner(using Context): Symbol =
+    def adjust(owner: Symbol): Symbol =
+      if !owner.exists
+        || owner.isClass && (!owner.is(Flags.Module) || owner.isStatic)
+        || owner.is(Flags.Method, butNot = Flags.Accessor) && !owner.isConstructor
+      then owner
+      else adjust(owner.owner)
+    adjust(ccOwner)
+
   // With the support of paths, we don't need to normalize the `TermRef`s anymore.
   // /** Normalize reference so that it can be compared with `eq` for equality */
   // final def normalizedRef(using Context): CaptureRef = this match
@@ -263,11 +304,18 @@ trait CaptureRef extends TypeProxy, ValueType:
       case _ => false
     (this eq y)
     || this.match
-      case root.Fresh(hidden) =>
-        vs.ifNotSeen(this)(hidden.elems.exists(_.subsumes(y)))
-        || !y.stripReadOnly.isCap
+      case x @ root.Fresh(hidden) =>
+        def levelOK =
+          if ccConfig.useFreshLevels && !CCState.ignoreFreshLevels then
+            val yOwner = y.levelOwner
+            yOwner.isStaticOwner || x.ccOwner.isContainedIn(yOwner)
+          else
+            !y.stripReadOnly.isCap
             && !yIsExistential
-            && !y.isInstanceOf[TermParamRef]
+            && !y.isInstanceOf[ParamRef]
+
+        vs.ifNotSeen(this)(hidden.elems.exists(_.subsumes(y)))
+        || levelOK
             && canAddHidden
             && vs.addHidden(hidden, y)
       case x @ root.Result(binder) =>