Don't allow instantiated ResultCaps to subsume anything

We map them to fresh caps but their hidden sets should not accept new elements.

Author: odersky

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

@@ -1033,7 +1033,13 @@ object Capabilities:
       override def mapCapability(c: Capability, deep: Boolean) = c match
         case c @ ResultCap(binder) =>
           if localBinders.contains(binder) then c // keep bound references
-          else seen.getOrElseUpdate(c, FreshCap(origin)) // map free references to FreshCap
+          else
+            // Create a fresh skolem that does not subsume anything
+            def freshSkolem =
+              val c = FreshCap(origin)
+              c.hiddenSet.markSolved(provisional = false)
+              c
+            seen.getOrElseUpdate(c, freshSkolem) // map free references to FreshCap
         case _ => super.mapCapability(c, deep)
     end subst
 

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

@@ -1206,6 +1206,7 @@ object CaptureSet:
       if alias ne this then alias.add(elem)
       else
         def addToElems() =
+          assert(!isConst)
           includeElem(elem)
           deps.foreach: dep =>
             assert(dep != this)
@@ -1378,8 +1379,10 @@ object CaptureSet:
      *  but the special state VarState.Separate overrides this.
      */
     def addHidden(hidden: HiddenSet, elem: Capability)(using Context): Boolean =
-      hidden.add(elem)(using ctx, this)
-      true
+      if hidden.isConst then false
+      else
+        hidden.add(elem)(using ctx, this)
+        true
 
     /** If root1 and root2 belong to the same binder but have different originalBinders
      *  it means that one of the roots was mapped to the binder of the other by a

tests/neg-custom-args/captures/frozen-result.scala

@@ -0,0 +1,9 @@
+class B
+
+def Test(consume b1: B^, consume b2: B^) =
+  def f(): B^ = B()
+  var x: B^ = f()
+  x = b1 // error separation but should be OK, see #23889
+  var y = f()
+  y = b2 // error
+