Skip to content

Commit

Permalink
Add note and a test to show the prefix rule for path subsuming
Browse files Browse the repository at this point in the history
  • Loading branch information
noti0na1 committed Oct 29, 2024
1 parent 1b0634a commit f16d565
Show file tree
Hide file tree
Showing 2 changed files with 50 additions and 0 deletions.
6 changes: 6 additions & 0 deletions compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
44 changes: 44 additions & 0 deletions tests/neg-custom-args/captures/path-prefix.scala
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit f16d565

Please sign in to comment.