Tighten subsume rules for existentials

 1. cap no longer subsumes existential variables
 2. existential variables don't subsume other existential variables

Still open: Existential variables should only subsume other capabilties if these
are sharable capabilities.

Author: odersky

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

@@ -584,15 +584,6 @@ extension (tp: Type)
     case tp: ThisType => tp.cls.ccLevel.nextInner
     case _ => undefinedLevel
 
-  /** Is this a method or function that has `other` as its direct or indirect result
-   *  type?
-   */
-  def hasSuffix(other: MethodType)(using Context): Boolean =
-    (tp eq other) || tp.match
-      case defn.RefinedFunctionOf(mt) => mt.hasSuffix(other)
-      case mt: MethodType => mt.resType.hasSuffix(other)
-      case _ => false
-
 extension (tp: MethodType)
   /** A method marks an existential scope unless it is the prefix of a curried method */
   def marksExistentialScope(using Context): Boolean =

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

@@ -264,11 +264,10 @@ trait CaptureRef extends TypeProxy, ValueType:
         || !y.stripReadOnly.isCap && !yIsExistential && canAddHidden && vs.addHidden(hidden, y)
       case Existential.Vble(binder) =>
         y.stripReadOnly match
-          case Existential.Vble(binder1) => binder1.hasSuffix(binder)
-            .showing(i"cmp existential $binder maxSubsumes $binder1 = $result", capt)
+          case Existential.Vble(binder1) => false
           case _ => true
       case _ =>
-        this.isCap /*&& !yIsExistential*/ && canAddHidden && vs != VarState.HardSeparate
+        this.isCap && !yIsExistential && canAddHidden && vs != VarState.HardSeparate
         || y.match
             case ReadOnlyCapability(y1) => this.stripReadOnly.maxSubsumes(y1, canAddHidden)
             case _ => false

tests/neg-custom-args/captures/unsound-reach-3.scala

@@ -10,15 +10,15 @@ def withFile[R](path: String)(op: File^ => R): R = ???
 trait Foo[+X]:
   def use(@consume x: File^): X
 class Bar extends Foo[File^]: // error
-  def use(@consume x: File^): File^ = x
+  def use(@consume x: File^): File^ = x // error override
 
 def bad(): Unit =
   val backdoor: Foo[File^] = new Bar // error (follow-on, since the parent Foo[File^] of bar is illegal).
   val boom: Foo[File^{backdoor*}] = backdoor
 
   var escaped: File^{backdoor*} = null
   withFile("hello.txt"): f =>
-    escaped = boom.use(f) // error
-      // boom.use: (x: File^) -> File^{backdoor*}, it is a selection so reach capabilities are allowed
+    escaped = boom.use(f) // error: separation
+      // was boom.use: (x: File^) -> File^{backdoor*}, it is a selection so reach capabilities are allowed
       // f: File^, so there is no reach capabilities
 

tests/neg-custom-args/captures/unsound-reach-4.check

@@ -13,7 +13,7 @@
 -- [E164] Declaration Error: tests/neg-custom-args/captures/unsound-reach-4.scala:17:6 ---------------------------------
 17 |  def use(@consume x: F): File^ = x // error @consume override
    |      ^
-   |error overriding method use in trait Foo of type (x: File^): box File^;
-   |  method use of type (x: File^): File^ has a parameter x with different @consume status than the corresponding parameter in the overridden definition
+   |      error overriding method use in trait Foo of type (x: File^): box File^;
+   |        method use of type (x: File^): File^ has incompatible type
    |
    | longer explanation available when compiling with `-explain`