Add note and a test to show the prefix rule for path subsuming

Author: noti0na1

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

@@ -123,6 +123,12 @@ trait CaptureRef extends TypeProxy, ValueType:
                 this.subsumes(ypre)
                 || this.match
                     case x @ TermRef(xpre: CaptureRef, _) if x.symbol == y.symbol =>
+                      // To show `{x.f} <:< {y.f}`, it is important to prove `x` and `y`
+                      // are equvalent, which means `x =:= y` in terms for subtyping,
+                      // not just `{x} =:= {y}`.
+                      // It is posible to construct two singleton types `x` and `y`,
+                      // which subumse each other, but are not equal references.
+                      // See `tests/neg-custom-args/captures/path-prefix.scala` for example.
                       withMode(Mode.IgnoreCaptures) {TypeComparer.isSameRef(xpre, ypre)}
                     case _ =>
                       false

tests/neg-custom-args/captures/path-prefix.scala

@@ -0,0 +1,44 @@
+import language.experimental.modularity
+import language.experimental.captureChecking
+import caps.Capability
+
+class F:
+  val f: AnyRef^ = ???
+
+case class B(tracked val a: A) extends F, Capability
+
+class A extends F, Capability:
+  val b: B { val a: A.this.type } = B(this)
+
+def test(a: A) =
+  val x: a.b.type = a.b
+  val y: x.a.type = x.a
+  // x and y are two distinct singleton types with following properties:
+  // x =:= a.b
+  // y =:= x.a =:= a.b.a =:= a
+
+  val cx: AnyRef^{x} = ???
+  val cy: AnyRef^{y} = ???
+  val caf: AnyRef^{a.f} = ???
+  val cabf: AnyRef^{a.b.f} = ???
+  val cxf: AnyRef^{x.f} = ???
+  val cyf: AnyRef^{y.f} = ???
+
+  // x and y subsume to each other:
+  // * {x} <:< {y}: the underlying singleton of y is x.a,
+  //   and the underlying singleton of x.a is a,
+  //   which is a prefix for the underlying type of x (a.b),
+  //   hence {x} <:< {y};
+  // * {y} <:< {x}: by underlying singleton of y is x.a, whose prefix is x.
+  // Hence, {x} =:= {y}.
+  val x2y: AnyRef^{y} = cx
+  val y2x: AnyRef^{x} = cy
+
+  val yf2af: AnyRef^{a.f} = cyf
+  val af2yf: AnyRef^{y.f} = caf
+  val xf2abf: AnyRef^{a.b.f} = cxf
+  val abf2xf: AnyRef^{x.f} = cabf
+
+  // Since `x !=:= y`, {x.f} !=:= {y.f}
+  val yf2xf: AnyRef^{x.f} = cyf // error
+  val xf2yf: AnyRef^{y.f} = cxf // error