Better grouping of explanations in error messages (#24155)

Group explanations that refer to the same Recorded entry with multiple
strings together.

Based on #24154

Author: odersky

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

@@ -205,6 +205,11 @@ object Capabilities:
         hiddenSet.adoptClassifier(cls)
         if freeze then isClassified = true
 
+    def ccOwnerStr(using Context): String =
+      val owner = ccOwner
+      if owner.name == nme.SKOLEM then i"a new instance of ${hiddenSet.owner}"
+      else owner.show
+
     def descr(using Context) =
       val originStr = origin match
         case Origin.InDecl(sym) if sym.exists =>

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

@@ -1089,7 +1089,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")
@@ -1133,7 +1132,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/NamerOps.scala

@@ -52,7 +52,7 @@ object NamerOps:
    */
   def addParamRefinements(resType: Type, paramss: List[List[Symbol]])(using Context): Type =
     paramss.flatten.foldLeft(resType): (rt, param) =>
-      if param.is(Tracked) then RefinedType(rt, param.name, param.termRef)
+      if param.is(Tracked) then RefinedType.precise(rt, param.name, param.termRef)
       else rt
 
   /** Split dependent class refinements off parent type. Add them to `refinements`,

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

@@ -914,12 +914,8 @@ 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)
+          if tp.isPrecise  then
+            pdenot.asSingleDenotation.derivedSingleDenotation(pdenot.symbol, rinfo)
           else
             val isRefinedMethod = rinfo.isInstanceOf[MethodOrPoly]
             val joint = CCState.withCollapsedFresh:
@@ -3259,6 +3255,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 +3272,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 +3305,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 +3318,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.

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

@@ -492,11 +492,13 @@ class PlainPrinter(_ctx: Context) extends Printer {
         if c.hiddenSet.classifier == defn.AnyClass then ""
         else s" classified as ${c.hiddenSet.classifier.name.show}"
       def prefixTxt: Text = c.prefix match
-        case NoPrefix | _: ThisType => ""
+        case NoPrefix => ""
+        case _: ThisType if !ccVerbose => ""
+        case pre: TermRef if !ccVerbose && pre.name == nme.SKOLEM => ""
         case pre: SingletonType => toTextRef(pre) ~ "."
         case pre => toText(pre) ~ "."
       def core: Text =
-        if ccVerbose then s"<fresh$idStr in ${c.ccOwner} hiding " ~ toTextCaptureSet(c.hiddenSet) ~ classified ~ ">"
+        if ccVerbose then s"<fresh$idStr in ${c.ccOwnerStr} hiding " ~ toTextCaptureSet(c.hiddenSet) ~ classified ~ ">"
         else "cap"
       prefixTxt ~ core
     case tp: TypeProxy =>

compiler/src/dotty/tools/dotc/reporting/Message.scala

@@ -142,7 +142,7 @@ object Message:
     end record
 
     /** Create explanation for single `Recorded` type or symbol */
-    private def explanation(entry: AnyRef, key: String)(using Context): String =
+    private def explanation(entry: AnyRef, keys: List[String])(using Context): String =
       def boundStr(bound: Type, default: ClassSymbol, cmp: String) =
         if (bound.isRef(default)) "" else i"$cmp $bound"
 
@@ -178,7 +178,8 @@ object Message:
           s"is an unknown value of type ${tp.widen.show}"
         case ref: RootCapability =>
           val relation =
-            if List("^", "=>", "?=>").exists(key.startsWith) then "refers to"
+            if keys.length > 1 then "refer to"
+            else if List("^", "=>", "?=>").exists(keys(0).startsWith) then "refers to"
             else "is"
           s"$relation ${ref.descr}"
     end explanation
@@ -207,16 +208,20 @@ object Message:
         res // help the inferencer out
       }.sortBy(_._1)
 
-      def columnar(parts: List[(String, String)]): List[String] = {
+      def columnar(parts: List[(String, String)]): List[String] =
         lazy val maxLen = parts.map(_._1.length).max
-        parts.map {
-          case (leader, trailer) =>
-            val variable = hl(leader)
-            s"""$variable${" " * (maxLen - leader.length)} $trailer"""
-        }
-      }
-
-      val explainParts = toExplain.map { case (str, entry) => (str, explanation(entry, str)) }
+        parts.map: (leader, trailer) =>
+          val variable = hl(leader)
+          s"""$variable${" " * (maxLen - leader.length)} $trailer"""
+
+      // Group keys with the same Recorded entry together. We can't use groupBy here
+      // since we want to maintain the order in which entries first appear in the
+      //  original list.
+      val toExplainGrouped: List[(Recorded, List[String])] =
+        for entry <- toExplain.map(_._2).distinct
+        yield (entry, for (key, e) <- toExplain if e == entry yield key)
+      val explainParts = toExplainGrouped.map:
+        (entry, keys) => (keys.mkString(" and "), explanation(entry, keys))
       val explainLines = columnar(explainParts)
       if (explainLines.isEmpty) "" else i"where:    $explainLines%\n          %\n"
     end explanations

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