Introduce precise refined types

They don't need an intersection when computing member types. Previously we did that
for augmented constructor types through the refinedOverride annotation. But that does
not apply to RefinedTypes with capset variables created in Setup. That's why we
still needed withCollapsedFresh to avoid non-sensical types in intersections.

Author: odersky

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

@@ -467,8 +467,7 @@ extension (tp: Type)
     acc(false, tp)
 
   def refinedOverride(name: Name, rinfo: Type)(using Context): Type =
-    RefinedType(tp, name,
-      AnnotatedType(rinfo, Annotation(defn.RefineOverrideAnnot, util.Spans.NoSpan)))
+    RefinedType.precise(tp, name, rinfo)
 
   def dropUseAndConsumeAnnots(using Context): Type =
     tp.dropAnnot(defn.UseAnnot).dropAnnot(defn.ConsumeAnnot)

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

@@ -358,7 +358,8 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
     if shared.isEmpty then i"${CaptureSet(shared)}"
     else shared.nth(0) match
       case fresh: FreshCap =>
-        if fresh.hiddenSet.owner.exists then i"{$fresh of ${fresh.hiddenSet.owner}}" else i"$fresh"
+        val where = if ctx.settings.YccVerbose.value then "" else i" of ${fresh.ccOwnerStr}"
+        i"{$fresh$where}"
       case _ =>
         i"${CaptureSet(shared)}"
 
@@ -574,9 +575,9 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
           case Select(This(_), _) => tree
           case Select(prefix, _) => pathRoot(prefix)
           case _ => tree
-          
+
         val rootSym = pathRoot(tree).symbol
-        
+
         def findClashing(prevDefs: List[DefInfo]): Option[DefInfo] = prevDefs match
           case prevDef :: prevDefs1 =>
             if prevDef.symbol == rootSym then Some(prevDef)

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

@@ -273,7 +273,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
                 then
                   val getterType =
                     mapInferred(inCaptureRefinement = true)(tp.memberInfo(getter)).strippedDealias
-                  RefinedType(core, getter.name,
+                  RefinedType.precise(core, getter.name,
                       CapturingType(getterType,
                         CaptureSet.ProperVar(ctx.owner, isRefining = true)))
                     .showing(i"add capture refinement $tp --> $result", capt)

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

@@ -1086,7 +1086,6 @@ class Definitions {
   @tu lazy val UseAnnot: ClassSymbol = requiredClass("scala.caps.use")
   @tu lazy val ReserveAnnot: ClassSymbol = requiredClass("scala.caps.reserve")
   @tu lazy val ConsumeAnnot: ClassSymbol = requiredClass("scala.caps.internal.consume")
-  @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")
   @tu lazy val BeanGetterMetaAnnot: ClassSymbol = requiredClass("scala.annotation.meta.beanGetter")
@@ -1130,7 +1129,7 @@ class Definitions {
 
   // Set of annotations that are not printed in types except under -Yprint-debug
   @tu lazy val SilentAnnots: Set[Symbol] =
-    Set(InlineParamAnnot, ErasedParamAnnot, RefineOverrideAnnot, SilentIntoAnnot, UseAnnot, ConsumeAnnot)
+    Set(InlineParamAnnot, ErasedParamAnnot, SilentIntoAnnot, UseAnnot, ConsumeAnnot)
 
   // A list of annotations that are commonly used to indicate that a field/method argument or return
   // type is not null. These annotations are used by the nullification logic in JavaNullInterop to

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

@@ -914,12 +914,10 @@ object Types extends TypeUtils {
           pdenot.asSingleDenotation.derivedSingleDenotation(pdenot.symbol, jointInfo)
         }
         else
-          val overridingRefinement = rinfo match
-            case AnnotatedType(rinfo1, ann) if ann.symbol == defn.RefineOverrideAnnot => rinfo1
-            case _ if pdenot.symbol.is(Tracked) => rinfo
-            case _ => NoType
-          if overridingRefinement.exists then
-            pdenot.asSingleDenotation.derivedSingleDenotation(pdenot.symbol, overridingRefinement)
+          val overridingRefinement =
+            tp.isPrecise || pdenot.symbol.is(Tracked)
+          if overridingRefinement then
+            pdenot.asSingleDenotation.derivedSingleDenotation(pdenot.symbol, rinfo)
           else
             val isRefinedMethod = rinfo.isInstanceOf[MethodOrPoly]
             val joint = CCState.withCollapsedFresh:
@@ -3259,6 +3257,12 @@ object Types extends TypeUtils {
     else assert(refinedInfo.isInstanceOf[TypeType], this)
     assert(!refinedName.is(NameKinds.ExpandedName), this)
 
+    /** If true we know that refinedInfo is always more precise than the info for
+     *  field `refinedName` in parent, so no type intersection needs to be computed
+     *  for the type of this field.
+     */
+    def isPrecise: Boolean = false
+
     override def underlying(using Context): Type = parent
 
     private def badInst =
@@ -3270,6 +3274,7 @@ object Types extends TypeUtils {
         (parent: Type = this.parent, refinedName: Name = this.refinedName, refinedInfo: Type = this.refinedInfo)
         (using Context): Type =
       if ((parent eq this.parent) && (refinedName eq this.refinedName) && (refinedInfo eq this.refinedInfo)) this
+      else if isPrecise then RefinedType.precise(parent, refinedName, refinedInfo)
       else RefinedType(parent, refinedName, refinedInfo)
 
     /** Add this refinement to `parent`, provided `refinedName` is a member of `parent`. */
@@ -3302,6 +3307,10 @@ object Types extends TypeUtils {
   class CachedRefinedType(parent: Type, refinedName: Name, refinedInfo: Type)
   extends RefinedType(parent, refinedName, refinedInfo)
 
+  class PreciseRefinedType(parent: Type, refinedName: Name, refinedInfo: Type)
+  extends RefinedType(parent, refinedName, refinedInfo):
+    override def isPrecise = true
+
   object RefinedType {
     @tailrec def make(parent: Type, names: List[Name], infos: List[Type])(using Context): Type =
       if (names.isEmpty) parent
@@ -3311,6 +3320,10 @@ object Types extends TypeUtils {
       assert(!ctx.erasedTypes)
       unique(new CachedRefinedType(parent, name, info)).checkInst
     }
+
+    def precise(parent: Type, name: Name, info: Type)(using Context): RefinedType =
+      assert(!ctx.erasedTypes)
+      unique(new PreciseRefinedType(parent, name, info)).checkInst
   }
 
   /** A recursive type. Instances should be constructed via the companion object.

library/src/scala/caps/package.scala

@@ -145,6 +145,7 @@ object internal:
    *  info from the parent type, so no intersection needs to be formed.
    *  This could be useful for tracked parameters as well.
    */
+  @deprecated
   final class refineOverride extends annotation.StaticAnnotation
 
   /** An annotation used internally for root capability wrappers of `cap` that

tests/neg-custom-args/captures/sep-pairs-unboxed.check

@@ -45,29 +45,27 @@
    |  Hidden footprint of current argument  : {two.fst}
    |  Capture set of second argument        : {two*}
    |  Footprint set of second argument      : {two*}
-   |  The two sets overlap at               : {two.cap of class Pair}
+   |  The two sets overlap at               : {cap of a new instance of class Pair}
    |
    |where:    ^  refers to a fresh root capability classified as Mutable in the type of value fst
    |          ^² refers to a fresh root capability classified as Mutable created in value twisted when checking argument to parameter fst of constructor PairPair
--- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:47:24 -------------------------------------------------
+-- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:47:33 -------------------------------------------------
 47 |  val twisted = swapped(two, two.snd) // error
-   |                        ^^^
-   |Separation failure: argument of type  (two : Pair{val fst: Ref^; val snd: Ref^²}^³)
+   |                             ^^^^^^^
+   |Separation failure: argument of type  (two.snd : Ref^)
    |to method swapped: (@consume x: Pair^, @consume y: Ref^): PairPair^
-   |corresponds to capture-polymorphic formal parameter x of type  Pair^⁴
-   |and hides capabilities  {two}.
-   |Some of these overlap with the captures of the second argument with type  (two.snd : Ref^).
+   |corresponds to capture-polymorphic formal parameter y of type  Ref^²
+   |and hides capabilities  {two.snd}.
+   |Some of these overlap with the captures of the first argument with type  (two : Pair{val fst: Ref^; val snd: Ref^}^).
    |
-   |  Hidden set of current argument        : {two}
-   |  Hidden footprint of current argument  : {two}
-   |  Capture set of second argument        : {two.snd}
-   |  Footprint set of second argument      : {two.snd}
-   |  The two sets overlap at               : {two.snd}
+   |  Hidden set of current argument        : {two.snd}
+   |  Hidden footprint of current argument  : {two.snd}
+   |  Capture set of first argument         : {two*}
+   |  Footprint set of first argument       : {two*}
+   |  The two sets overlap at               : {cap of a new instance of class Pair}
    |
-   |where:    ^  refers to a fresh root capability classified as Mutable in the type of value fst
-   |          ^² refers to a fresh root capability classified as Mutable in the type of value snd
-   |          ^³ refers to a fresh root capability in the type of value two
-   |          ^⁴ refers to a fresh root capability created in value twisted when checking argument to parameter x of method swapped
+   |where:    ^  refers to a fresh root capability classified as Mutable in the type of value snd
+   |          ^² refers to a fresh root capability classified as Mutable created in value twisted when checking argument to parameter y of method swapped
 -- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:58:26 -------------------------------------------------
 58 |  val twoOther = Pair(two.fst, two.snd)  // error // error
    |                      ^^^^^^^