@@ -61,18 +61,19 @@ trait CaptureRef extends TypeProxy, ValueType:
6161 case tp : TermParamRef => tp.underlying.derivesFrom(defn.Caps_Exists )
6262 case _ => false
6363
64- /** Normalize reference so that it can be compared with `eq` for equality */
65- final def normalizedRef (using Context ): CaptureRef = this match
66- case tp @ AnnotatedType (parent : CaptureRef , annot) if tp.isTrackableRef =>
67- tp.derivedAnnotatedType(parent.normalizedRef, annot)
68- case tp : TermRef if tp.isTrackableRef =>
69- tp.symbol.termRef
70- case _ => this
64+ // With the support of pathes, we don't need to normalize the `TermRef`s anymore.
65+ // /** Normalize reference so that it can be compared with `eq` for equality */
66+ // final def normalizedRef(using Context): CaptureRef = this match
67+ // case tp @ AnnotatedType(parent: CaptureRef, annot) if tp.isTrackableRef =>
68+ // tp.derivedAnnotatedType(parent.normalizedRef, annot)
69+ // case tp: TermRef if tp.isTrackableRef =>
70+ // tp.symbol.termRef
71+ // case _ => this
7172
7273 /** The capture set consisting of exactly this reference */
7374 final def singletonCaptureSet (using Context ): CaptureSet .Const =
7475 if mySingletonCaptureSet == null then
75- mySingletonCaptureSet = CaptureSet (this .normalizedRef )
76+ mySingletonCaptureSet = CaptureSet (this )
7677 mySingletonCaptureSet.uncheckedNN
7778
7879 /** The capture set of the type underlying this reference */
@@ -97,27 +98,51 @@ trait CaptureRef extends TypeProxy, ValueType:
9798 * x subsumes y ==> x* subsumes y, x subsumes y?
9899 * x subsumes y ==> x* subsumes y*, x? subsumes y?
99100 * x: x1.type /\ x1 subsumes y ==> x subsumes y
101+ * TODO: Document path cases
100102 */
101103 final def subsumes (y : CaptureRef )(using Context ): Boolean =
104+
105+ def subsumingRefs (x : Type , y : Type ): Boolean = x match
106+ case x : CaptureRef => y match
107+ case y : CaptureRef => x.subsumes(y)
108+ case _ => false
109+ case _ => false
110+
111+ def viaInfo (info : Type )(test : Type => Boolean ): Boolean = info.match
112+ case info : SingletonCaptureRef => test(info)
113+ case info : AndType => viaInfo(info.tp1)(test) || viaInfo(info.tp2)(test)
114+ case info : OrType => viaInfo(info.tp1)(test) && viaInfo(info.tp2)(test)
115+ case _ => false
116+
102117 (this eq y)
103118 || this .isRootCapability
104119 || y.match
105120 case y : TermRef =>
106- (y.prefix eq this )
107- || y.info.match
108- case y1 : SingletonCaptureRef => this .subsumes(y1)
121+ y.prefix.match
122+ case ypre : CaptureRef =>
123+ this .subsumes(ypre)
124+ || this .match
125+ case x @ TermRef (xpre : CaptureRef , _) if x.symbol == y.symbol =>
126+ // To show `{x.f} <:< {y.f}`, it is important to prove `x` and `y`
127+ // are equvalent, which means `x =:= y` in terms of subtyping,
128+ // not just `{x} =:= {y}` in terms of subcapturing.
129+ // It is possible to construct two singleton types `x` and `y`,
130+ // which subsume each other, but are not equal references.
131+ // See `tests/neg-custom-args/captures/path-prefix.scala` for example.
132+ withMode(Mode .IgnoreCaptures ) {TypeComparer .isSameRef(xpre, ypre)}
133+ case _ =>
134+ false
109135 case _ => false
136+ || viaInfo(y.info)(subsumingRefs(this , _))
110137 case MaybeCapability (y1) => this .stripMaybe.subsumes(y1)
111138 case _ => false
112139 || this .match
113140 case ReachCapability (x1) => x1.subsumes(y.stripReach)
114- case x : TermRef =>
115- x.info match
116- case x1 : SingletonCaptureRef => x1.subsumes(y)
117- case _ => false
141+ case x : TermRef => viaInfo(x.info)(subsumingRefs(_, y))
118142 case x : TermParamRef => subsumesExistentially(x, y)
119143 case x : TypeRef => assumedContainsOf(x).contains(y)
120144 case _ => false
145+ end subsumes
121146
122147 def assumedContainsOf (x : TypeRef )(using Context ): SimpleIdentitySet [CaptureRef ] =
123148 CaptureSet .assumedContains.getOrElse(x, SimpleIdentitySet .empty)
0 commit comments