Avoid forming intersections of capture sets on refined type lookup

Author: odersky

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

@@ -1073,7 +1073,7 @@ object CaptureSet:
      *  return whether this was allowed. By default, recording is allowed
      *  but the special state VarState.Separate overrides this.
      */
-    def addHidden(hidden: HiddenSet, elem: CaptureRef): Boolean =
+    def addHidden(hidden: HiddenSet, elem: CaptureRef)(using Context): Boolean =
       elemsMap.get(hidden) match
         case None => elemsMap(hidden) = hidden.elems
         case _ =>
@@ -1112,7 +1112,7 @@ object CaptureSet:
      */
     @sharable
     object Separate extends Closed:
-      override def addHidden(hidden: HiddenSet, elem: CaptureRef): Boolean = false
+      override def addHidden(hidden: HiddenSet, elem: CaptureRef)(using Context): Boolean = false
 
     /** A special state that turns off recording of elements. Used only
      *  in `addSub` to prevent cycles in recordings.
@@ -1122,14 +1122,14 @@ object CaptureSet:
       override def putElems(v: Var, refs: Refs) = true
       override def putDeps(v: Var, deps: Deps) = true
       override def rollBack(): Unit = ()
-      override def addHidden(hidden: HiddenSet, elem: CaptureRef): Boolean = true
+      override def addHidden(hidden: HiddenSet, elem: CaptureRef)(using Context): Boolean = true
 
     /** A closed state that turns off recording of hidden elements (but allows
      *  adding them). Used in `mightAccountFor`.
      */
     @sharable
     private[CaptureSet] object ClosedUnrecorded extends Closed:
-      override def addHidden(hidden: HiddenSet, elem: CaptureRef): Boolean = true
+      override def addHidden(hidden: HiddenSet, elem: CaptureRef)(using Context): Boolean = true
 
   end VarState
 

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

@@ -24,6 +24,7 @@ import StdNames.nme
 import NameKinds.{DefaultGetterName, WildcardParamName, UniqueNameKind}
 import reporting.{trace, Message, OverrideError}
 import Existential.derivedExistentialType
+import Annotations.Annotation
 
 /** The capture checker */
 object CheckCaptures:
@@ -785,7 +786,8 @@ class CheckCaptures extends Recheck, SymTransformer:
         for (getterName, argType) <- mt.paramNames.lazyZip(argTypes) do
           val getter = cls.info.member(getterName).suchThat(_.isRefiningParamAccessor).symbol
           if !getter.is(Private) && getter.hasTrackedParts then
-            refined = RefinedType(refined, getterName, argType.unboxed) // Yichen you might want to check this
+            refined = RefinedType(refined, getterName,
+              AnnotatedType(argType.unboxed, Annotation(defn.RefineOverrideAnnot, util.Spans.NoSpan))) // Yichen you might want to check this
             allCaptures ++= argType.captureSet
         (refined, allCaptures)
 

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

@@ -1071,6 +1071,7 @@ class Definitions {
   @tu lazy val UncheckedCapturesAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedCaptures")
   @tu lazy val UntrackedCapturesAnnot: ClassSymbol = requiredClass("scala.caps.untrackedCaptures")
   @tu lazy val UseAnnot:  ClassSymbol = requiredClass("scala.caps.use")
+  @tu lazy val RefineOverrideAnnot:  ClassSymbol = requiredClass("scala.caps.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")
@@ -1111,6 +1112,10 @@ class Definitions {
   @tu lazy val MetaAnnots: Set[Symbol] =
     NonBeanMetaAnnots + BeanGetterMetaAnnot + BeanSetterMetaAnnot
 
+  // Set of annotations that are not printed in types except under -Yprint-debug
+  @tu lazy val SilentAnnots: Set[Symbol] =
+    Set(InlineParamAnnot, ErasedParamAnnot, RefineOverrideAnnot)
+
   // 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
   // improve the precision of type nullification.

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

@@ -860,21 +860,24 @@ object Types extends TypeUtils {
               pinfo recoverable_& rinfo
           pdenot.asSingleDenotation.derivedSingleDenotation(pdenot.symbol, jointInfo)
         }
-        else
-          val isRefinedMethod = rinfo.isInstanceOf[MethodOrPoly]
-          val joint = pdenot.meet(
-            new JointRefDenotation(NoSymbol, rinfo, Period.allInRun(ctx.runId), pre, isRefinedMethod),
-            pre,
-            safeIntersection = ctx.base.pendingMemberSearches.contains(name))
-          joint match
-            case joint: SingleDenotation
-            if isRefinedMethod
-              && (rinfo <:< joint.info
-                || name == nme.apply && defn.isFunctionType(tp.parent)) =>
-              // use `rinfo` to keep the right parameter names for named args. See i8516.scala.
-              joint.derivedSingleDenotation(joint.symbol, rinfo, pre, isRefinedMethod)
-            case _ =>
-              joint
+        else rinfo match
+          case AnnotatedType(rinfo1, ann) if ann.symbol == defn.RefineOverrideAnnot =>
+            pdenot.asSingleDenotation.derivedSingleDenotation(pdenot.symbol, rinfo1)
+          case _ =>
+            val isRefinedMethod = rinfo.isInstanceOf[MethodOrPoly]
+            val joint = pdenot.meet(
+              new JointRefDenotation(NoSymbol, rinfo, Period.allInRun(ctx.runId), pre, isRefinedMethod),
+              pre,
+              safeIntersection = ctx.base.pendingMemberSearches.contains(name))
+            joint match
+              case joint: SingleDenotation
+              if isRefinedMethod
+                && (rinfo <:< joint.info
+                  || name == nme.apply && defn.isFunctionType(tp.parent)) =>
+                // use `rinfo` to keep the right parameter names for named args. See i8516.scala.
+                joint.derivedSingleDenotation(joint.symbol, rinfo, pre, isRefinedMethod)
+              case _ =>
+                joint
       }
 
       def goApplied(tp: AppliedType, tycon: HKTypeLambda) =

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

@@ -310,8 +310,8 @@ class PlainPrinter(_ctx: Context) extends Printer {
           toTextGlobal(tp.resultType)
         }
       case AnnotatedType(tpe, annot) =>
-        if annot.symbol == defn.InlineParamAnnot || annot.symbol == defn.ErasedParamAnnot
-        then toText(tpe)
+        if defn.SilentAnnots.contains(annot.symbol) && !printDebug then
+          toText(tpe)
         else if (annot.symbol == defn.IntoAnnot || annot.symbol == defn.IntoParamAnnot)
             && !printDebug
         then atPrec(GlobalPrec)( Str("into ") ~ toText(tpe) )

library/src/scala/caps.scala

@@ -70,6 +70,13 @@ import annotation.{experimental, compileTimeOnly, retainsCap}
    */
   final class use extends annotation.StaticAnnotation
 
+  /** An annotation placed on a refinement created by capture checking.
+   *  Refinements with this annotation unconditionally override any
+   *  info vfrom the parent type, so no intersection needs to be formed.
+   *  This could be useful for tracked parameters as well.
+   */
+  final class refineOverride extends annotation.StaticAnnotation
+
   object unsafe:
 
     extension [T](x: T)

scala2-library-cc/src/scala/collection/View.scala

@@ -150,10 +150,8 @@ object View extends IterableFactory[View] {
   object Filter {
     def apply[A](underlying: Iterable[A]^, p: A => Boolean, isFlipped: Boolean): Filter[A]^{underlying, p} =
       underlying match {
-        case filter: Filter[A] if filter.isFlipped == isFlipped =>
+        case filter: Filter[A]^{underlying} if filter.isFlipped == isFlipped =>
           new Filter(filter.underlying, a => filter.p(a) && p(a), isFlipped)
-            .asInstanceOf[Filter[A]^{underlying, p}]
-              // !!! asInstanceOf needed once paths were added, see path-patmat-should-be-pos.scala for minimization
         case _ => new Filter(underlying, p, isFlipped)
       }
   }

tests/neg-custom-args/captures/capt-depfun.check

@@ -0,0 +1,13 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt-depfun.scala:10:43 ----------------------------------
+10 |  val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error // error sepcheck
+   |                                         ^^^^^^^
+   |                                         Found:    Str^{} ->{ac, y, z} Str^{y, z}
+   |                                         Required: Str^{y, z} ->{fresh} Str^{y, z}
+   |
+   | longer explanation available when compiling with `-explain`
+-- Error: tests/neg-custom-args/captures/capt-depfun.scala:10:24 -------------------------------------------------------
+10 |  val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error // error sepcheck
+   |           ^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |           Separation failure: Str^{y, z} => Str^{y, z} captures a root element hiding  {ac, y, z}
+   |           and also refers to  {y, z}.
+   |           The two sets overlap at  {y, z}

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

@@ -1,9 +1,10 @@
 import annotation.retains
+import language.future // sepchecks on
 class C
 type Cap = C @retains(caps.cap)
 class Str
 
 def f(y: Cap, z: Cap) =
   def g(): C @retains(y, z) = ???
   val ac: ((x: Cap) => Str @retains(x) => Str @retains(x)) = ???
-  val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error
+  val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error // error sepcheck

tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala

@@ -452,6 +452,14 @@ object CollectionStrawMan5 {
       this: Filter[A]^{underlying, p} =>
       def iterator: Iterator[A]^{this} = underlying.iterator.filter(p)
     }
+
+    object Filter:
+      def apply[A](underlying: Iterable[A]^, pp: A => Boolean, isFlipped: Boolean): Filter[A]^{underlying, pp} =
+        underlying match
+          case filter: Filter[A]^{underlying} =>
+            new Filter(filter.underlying, a => filter.p(a) && pp(a))
+          case _ => new Filter(underlying, pp)
+
     case class Partition[A](val underlying: Iterable[A]^, p: A => Boolean) {
       self: Partition[A]^{underlying, p} =>