Skip to content

Commit 388d9a8

Browse files
committed
Fixing subtyping of refined types
Refined type subtyping needs to take into account all information that was seen about members of both refined types. This is handled by storing context info in `pendingRefinedBases` and making use of this to selective rebase qualifiers when comparing refined types. Note: This commit fails in pos/collections and dotc/ast, presumably because of bad interaction between the refined subtyping and the "matchingNames" logic (which will go away).
1 parent 099e5a6 commit 388d9a8

File tree

1 file changed

+146
-40
lines changed

1 file changed

+146
-40
lines changed

src/dotty/tools/dotc/core/TypeComparer.scala

Lines changed: 146 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ import Decorators._
88
import StdNames.{nme, tpnme}
99
import collection.mutable
1010
import printing.Disambiguation.disambiguated
11-
import util.{Stats, DotClass}
11+
import util.{Stats, DotClass, SimpleMap}
1212
import config.Config
1313
import config.Printers._
1414

@@ -84,6 +84,8 @@ class TypeComparer(initctx: Context) extends DotClass {
8484
myAnyType
8585
}
8686

87+
// Constraint handling
88+
8789
/** Map that approximates each param in constraint by its lower bound.
8890
* Currently only used for diagnostics.
8991
*/
@@ -264,6 +266,82 @@ class TypeComparer(initctx: Context) extends DotClass {
264266
inst
265267
}
266268

269+
// Keeping track of seen refinements
270+
271+
/** A map from refined names to the refined types in which they occur.
272+
* During the subtype check involving the parent of a refined type,
273+
* the refined name is stored in the map, so that the outermost
274+
* refinements can be retrieved when interpreting a reference to the name.
275+
* The name is associated with a pair of refinements. If the refinedInfo is
276+
* skipped in sub- and super-type at the same time (first clause of
277+
* `compareRefined`, both refinements are stored. If the name only appears
278+
* as a refinement in the sub- or -super-type, the refinement type is stored
279+
* twice as both elements of the pair.
280+
*/
281+
protected var pendingRefinedBases: SimpleMap[Name, Set[(RefinedType, RefinedType)]]
282+
= SimpleMap.Empty
283+
284+
/** Add pending name to `pendingRefinedBases`. */
285+
private def addPendingName(name: Name, rt1: RefinedType, rt2: RefinedType) = {
286+
var s = pendingRefinedBases(name)
287+
if (s == null) s = Set()
288+
pendingRefinedBases = pendingRefinedBases.updated(name, s + ((rt1, rt2)))
289+
}
290+
291+
/** Given a selection of qualifier `qual` with given `name`, return a refined type
292+
* that refines `qual`, or if that fails return `qual` itself.
293+
* @param considerBoth If true consider both lower and upper base of `name` when
294+
* checking for refinement (but always return the lower one)
295+
* @see Type#refines
296+
*/
297+
private def rebaseQual(qual: Type, name: Name, considerBoth: Boolean = false): Type = {
298+
val bases = pendingRefinedBases(name)
299+
if (bases == null) qual
300+
else bases.find {
301+
case (tp1, tp2) =>
302+
(tp1 refines qual) || considerBoth && (tp1 ne tp2) && (tp2 refines qual)
303+
} match {
304+
case Some((base1, _)) => base1
305+
case _ => qual
306+
}
307+
}
308+
309+
/** If the prefix of a named type is `this` (i.e. an instance of type
310+
* `ThisType` or `RefinedThis`), and there is a refinement type R that
311+
* "refines" (transitively contains as its parent) a class reference
312+
* or refinement corresponding to the prefix, return the named type where
313+
* the prefix is replaced by `RefinedThis(R)`. Otherwise return the named type itself.
314+
*/
315+
private def rebase(tp: NamedType): Type = {
316+
def rebaseFrom(prefix: Type): Type = {
317+
rebaseQual(prefix, tp.name, considerBoth = true) match {
318+
case rt: RefinedType if rt ne prefix => tp.derivedSelect(RefinedThis(rt))
319+
case _ => tp
320+
}
321+
}
322+
tp.prefix match {
323+
case RefinedThis(rt) => rebaseFrom(rt)
324+
case ThisType(cls) => rebaseFrom(cls.info)
325+
case _ => tp
326+
}
327+
}
328+
329+
/** If the given refined type is refined further, return the member
330+
* of the refiend name relative to the refining base, otherwise return
331+
* `refinedInfo`.
332+
* TODO: Figure out why cannot simply write
333+
*
334+
* rebaseQual(rt, rt.refinedName).member(rt.refinedName).info
335+
*
336+
* (too much forcing, probably).
337+
*/
338+
def normalizedInfo(rt: RefinedType) = {
339+
val base = rebaseQual(rt, rt.refinedName)
340+
if (base eq rt) rt.refinedInfo else base.member(rt.refinedName).info
341+
}
342+
343+
// Subtype testing `<:<`
344+
267345
def topLevelSubType(tp1: Type, tp2: Type): Boolean = {
268346
if (tp2 eq NoType) return false
269347
if ((tp2 eq tp1) ||
@@ -448,6 +526,11 @@ class TypeComparer(initctx: Context) extends DotClass {
448526
}
449527
}
450528
comparePolyParam
529+
case tp1: RefinedThis =>
530+
tp2 match {
531+
case tp2: RefinedThis if tp1.binder.parent =:= tp2.binder.parent => true
532+
case _ => thirdTry(tp1, tp2)
533+
}
451534
case tp1: BoundType =>
452535
tp1 == tp2 || thirdTry(tp1, tp2)
453536
case tp1: TypeVar =>
@@ -466,30 +549,42 @@ class TypeComparer(initctx: Context) extends DotClass {
466549
thirdTry(tp1, tp2)
467550
}
468551

469-
def secondTryNamed(tp1: NamedType, tp2: Type): Boolean = tp1.info match {
470-
case OrType(tp11, tp12) =>
471-
val sd = tp1.denot.asSingleDenotation
472-
def derivedRef(tp: Type) =
473-
NamedType(tp1.prefix, tp1.name, sd.derivedSingleDenotation(sd.symbol, tp))
474-
secondTry(OrType.make(derivedRef(tp11), derivedRef(tp12)), tp2)
475-
case TypeBounds(lo1, hi1) =>
476-
if ((tp1.symbol is GADTFlexType) && !isSubTypeWhenFrozen(hi1, tp2))
477-
trySetType(tp1, TypeBounds(lo1, hi1 & tp2))
478-
else if (lo1 eq hi1) isSubType(hi1, tp2)
552+
def secondTryNamed(tp1: NamedType, tp2: Type): Boolean = {
553+
def tryRebase2nd = {
554+
val tp1rebased = rebase(tp1)
555+
if (tp1rebased ne tp1) isSubType(tp1rebased, tp2)
479556
else thirdTry(tp1, tp2)
480-
case _ =>
481-
thirdTry(tp1, tp2)
557+
}
558+
tp1.info match {
559+
case OrType(tp11, tp12) =>
560+
val sd = tp1.denot.asSingleDenotation
561+
def derivedRef(tp: Type) =
562+
NamedType(tp1.prefix, tp1.name, sd.derivedSingleDenotation(sd.symbol, tp))
563+
secondTry(OrType.make(derivedRef(tp11), derivedRef(tp12)), tp2)
564+
case TypeBounds(lo1, hi1) =>
565+
if ((tp1.symbol is GADTFlexType) && !isSubTypeWhenFrozen(hi1, tp2))
566+
trySetType(tp1, TypeBounds(lo1, hi1 & tp2))
567+
else if (lo1 eq hi1) isSubType(hi1, tp2)
568+
else tryRebase2nd
569+
case _ =>
570+
tryRebase2nd
571+
}
482572
}
483573

484574
def thirdTry(tp1: Type, tp2: Type): Boolean = tp2 match {
485575
case tp2: NamedType =>
576+
def tryRebase3rd = {
577+
val tp2rebased = rebase(tp2)
578+
if (tp2rebased ne tp2) isSubType(tp1, tp2rebased)
579+
else fourthTry(tp1, tp2)
580+
}
486581
def compareNamed: Boolean = tp2.info match {
487582
case TypeBounds(lo2, hi2) =>
488583
if ((tp2.symbol is GADTFlexType) && !isSubTypeWhenFrozen(tp1, lo2))
489584
trySetType(tp2, TypeBounds(lo2 | tp1, hi2))
490585
else
491586
((frozenConstraint || !isCappable(tp1)) && isSubType(tp1, lo2)
492-
|| fourthTry(tp1, tp2))
587+
|| tryRebase3rd)
493588

494589
case _ =>
495590
val cls2 = tp2.symbol
@@ -499,43 +594,36 @@ class TypeComparer(initctx: Context) extends DotClass {
499594
if ( cls2 == defn.SingletonClass && tp1.isStable
500595
|| cls2 == defn.NotNullClass && tp1.isNotNull) return true
501596
}
502-
fourthTry(tp1, tp2)
597+
tryRebase3rd
503598
}
504599
compareNamed
505600
case tp2 @ RefinedType(parent2, name2) =>
506-
def matchRefinements(tp1: Type, tp2: Type, seen: Set[Name]): Type = tp1 match {
507-
case tp1 @ RefinedType(parent1, name1) if !(seen contains name1) =>
508-
tp2 match {
509-
case tp2 @ RefinedType(parent2, name2) if nameMatches(name1, name2, tp1, tp2) =>
510-
if (isSubType(tp1.refinedInfo, tp2.refinedInfo))
511-
matchRefinements(parent1, parent2, seen + name1)
512-
else NoType
513-
case _ => tp2
514-
}
515-
case _ => tp2
516-
}
517-
def compareRefined: Boolean =
518-
if (defn.hkTraits contains parent2.typeSymbol) isSubTypeHK(tp1, tp2)
519-
else tp1.widen match {
520-
case tp1 @ RefinedType(parent1, name1) if nameMatches(name1, name2, tp1, tp2) =>
521-
// optimized case; all info on tp1.name2 is in refinement tp1.refinedInfo.
522-
isSubType(tp1.refinedInfo, tp2.refinedInfo) && {
523-
val ancestor2 = matchRefinements(parent1, parent2, Set.empty + name1)
524-
ancestor2.exists && isSubType(tp1, ancestor2)
601+
def compareRefined: Boolean = tp1.widen match {
602+
case tp1 @ RefinedType(parent1, name1)
603+
if nameMatches(name1, name2, tp1, tp2) =>
604+
// optimized case; all info on tp1.name1 is in refinement tp1.refinedInfo.
605+
isSubType(normalizedInfo(tp1), tp2.refinedInfo) && {
606+
val saved = pendingRefinedBases
607+
try {
608+
addPendingName(name1, tp1, tp2)
609+
isSubType(parent1, parent2)
610+
}
611+
finally pendingRefinedBases = saved
525612
}
526613
case _ =>
527614
def qualifies(m: SingleDenotation) = isSubType(m.info, tp2.refinedInfo)
528615
def memberMatches(mbr: Denotation): Boolean = mbr match { // inlined hasAltWith for performance
529616
case mbr: SingleDenotation => qualifies(mbr)
530617
case _ => mbr hasAltWith qualifies
531618
}
532-
def hasMatchingMember(name: Name): Boolean = /*>|>*/ ctx.traceIndented(s"hasMatchingMember($name) ${tp1.member(name).info.show}", subtyping) /*<|<*/ (
533-
memberMatches(tp1 member name)
619+
def hasMatchingMember(name: Name): Boolean = /*>|>*/ ctx.traceIndented(s"hasMatchingMember($name) ${tp1.member(name).info.show}", subtyping) /*<|<*/ {
620+
val tp1r = rebaseQual(tp1, name)
621+
( memberMatches(tp1r member name)
534622
||
535623
{ // special case for situations like:
536624
// foo <: C { type T = foo.T }
537625
tp2.refinedInfo match {
538-
case TypeBounds(lo, hi) if lo eq hi => (tp1 select name) =:= lo
626+
case TypeBounds(lo, hi) if lo eq hi => (tp1r select name) =:= lo
539627
case _ => false
540628
}
541629
}
@@ -545,8 +633,17 @@ class TypeComparer(initctx: Context) extends DotClass {
545633
val tparams = tp1.typeParams
546634
idx < tparams.length && hasMatchingMember(tparams(idx).name)
547635
}
548-
)
549-
isSubType(tp1, parent2) && (
636+
)
637+
}
638+
val matchesParent = {
639+
val saved = pendingRefinedBases
640+
try {
641+
addPendingName(name2, tp2, tp2)
642+
isSubType(tp1, parent2)
643+
}
644+
finally pendingRefinedBases = saved
645+
}
646+
matchesParent && (
550647
name2 == nme.WILDCARD
551648
|| hasMatchingMember(name2)
552649
|| fourthTry(tp1, tp2))
@@ -637,7 +734,12 @@ class TypeComparer(initctx: Context) extends DotClass {
637734
}
638735
}
639736
case tp1: RefinedType =>
640-
isNewSubType(tp1.parent, tp2)
737+
val saved = pendingRefinedBases
738+
try {
739+
addPendingName(tp1.refinedName, tp1, tp1)
740+
isNewSubType(tp1.parent, tp2)
741+
}
742+
finally pendingRefinedBases = saved
641743
case AndType(tp11, tp12) =>
642744
isNewSubType(tp11, tp2) || isNewSubType(tp12, tp2)
643745
case _ =>
@@ -754,6 +856,8 @@ class TypeComparer(initctx: Context) extends DotClass {
754856
isSubType(bounds.lo, bounds.hi) &&
755857
{ tr.symbol.changeGADTInfo(bounds); true }
756858

859+
// Tests around `matches`
860+
757861
/** A function implementing `tp1` matches `tp2`. */
758862
final def matchesType(tp1: Type, tp2: Type, alwaysMatchSimple: Boolean): Boolean = tp1 match {
759863
case tp1: MethodType =>
@@ -835,6 +939,8 @@ class TypeComparer(initctx: Context) extends DotClass {
835939
(poly1.paramBounds corresponds poly2.paramBounds)((b1, b2) =>
836940
isSameType(b1, b2.subst(poly2, poly1)))
837941

942+
// Type equality =:=
943+
838944
/** Two types are the same if are mutual subtypes of each other */
839945
def isSameType(tp1: Type, tp2: Type): Boolean =
840946
if (tp1 eq NoType) false

0 commit comments

Comments
 (0)