Change rules for tracked refinments and tighten intersections

Intersections used the heuristic mightAccountFor instead of the precise accountsFor. Thsi
can lead to a loss of precision and (if unchecked afterwards) also soundness. The fix caused
some tests to fail, which involved tracked parameters.

We now deal with tracked parameters in the same way as parameters that carry a @refineOverride annotation.

Author: odersky

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

@@ -935,7 +935,7 @@ object CaptureSet:
   end Intersection
 
   def elemIntersection(cs1: CaptureSet, cs2: CaptureSet)(using Context): Refs =
-    cs1.elems.filter(cs2.mightAccountFor) ++ cs2.elems.filter(cs1.mightAccountFor)
+    cs1.elems.filter(cs2.accountsFor) ++ cs2.elems.filter(cs1.accountsFor)
 
   /** A capture set variable used to record the references hidden by a Fresh instance,
    *  The elems and deps members are repurposed as follows:

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

@@ -860,10 +860,14 @@ object Types extends TypeUtils {
               pinfo recoverable_& rinfo
           pdenot.asSingleDenotation.derivedSingleDenotation(pdenot.symbol, jointInfo)
         }
-        else rinfo match
-          case AnnotatedType(rinfo1, ann) if ann.symbol == defn.RefineOverrideAnnot =>
-            pdenot.asSingleDenotation.derivedSingleDenotation(pdenot.symbol, rinfo1)
-          case _ =>
+        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)
+          else
             val isRefinedMethod = rinfo.isInstanceOf[MethodOrPoly]
             val joint = pdenot.meet(
               new JointRefDenotation(NoSymbol, rinfo, Period.allInRun(ctx.runId), pre, isRefinedMethod),