Skip to content

Commit a84fbb1

Browse files
committed
Use a pending set to detect infinite recursion.
Instead of having an ad hoc criteria on type parameters' bounds. This makes sense, because the spec wants a finite derivation tree for the provablyDisjoint relation. If we hit the same pair of types in the tree, that branch of the exploration will not lead to a finite subtree.
1 parent 12e74ac commit a84fbb1

File tree

1 file changed

+42
-71
lines changed

1 file changed

+42
-71
lines changed

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

Lines changed: 42 additions & 71 deletions
Original file line numberDiff line numberDiff line change
@@ -2800,12 +2800,12 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
28002800
* property that in all possible contexts, the same match type expression
28012801
* is either stuck or reduces to the same case.
28022802
*/
2803-
def provablyDisjoint(tp1: Type, tp2: Type)(using Context): Boolean = trace(i"provable disjoint $tp1, $tp2", matchTypes) {
2804-
// println(s"provablyDisjoint(${tp1.show}, ${tp2.show})")
2803+
def provablyDisjoint(tp1: Type, tp2: Type)(using Context): Boolean =
2804+
provablyDisjoint(tp1, tp2, null)
28052805

2806-
def isEnumValue(ref: TermRef): Boolean =
2807-
val sym = ref.termSymbol
2808-
sym.isAllOf(EnumCase, butNot=JavaDefined)
2806+
def provablyDisjoint(tp1: Type, tp2: Type, pending: util.HashSet[(Type, Type)] | Null)(
2807+
using Context): Boolean = trace(i"provable disjoint $tp1, $tp2", matchTypes) {
2808+
// println(s"provablyDisjoint(${tp1.show}, ${tp2.show})")
28092809

28102810
@scala.annotation.tailrec
28112811
def disjointnessBoundary(tp: Type): Type = tp match
@@ -2823,7 +2823,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
28232823
case tp @ AppliedType(tycon: TypeRef, _) if tycon.symbol.isClass =>
28242824
tp
28252825
case tp: TermRef =>
2826-
if isEnumValue(tp) then tp
2826+
val isEnumValue = tp.termSymbol.isAllOf(EnumCase, butNot = JavaDefined)
2827+
if isEnumValue then tp
28272828
else
28282829
val optGadtBounds = gadtBounds(tp.symbol)
28292830
if optGadtBounds != null then disjointnessBoundary(optGadtBounds.hi)
@@ -2841,17 +2842,21 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
28412842
end disjointnessBoundary
28422843

28432844
(disjointnessBoundary(tp1), disjointnessBoundary(tp2)) match
2845+
// Infinite recursion detection
2846+
case pair if pending != null && pending.contains(pair) =>
2847+
false
2848+
28442849
// Cases where there is an intersection or union on the right
28452850
case (tp1, tp2: OrType) =>
2846-
provablyDisjoint(tp1, tp2.tp1) && provablyDisjoint(tp1, tp2.tp2)
2851+
provablyDisjoint(tp1, tp2.tp1, pending) && provablyDisjoint(tp1, tp2.tp2, pending)
28472852
case (tp1, tp2: AndType) =>
2848-
provablyDisjoint(tp1, tp2.tp1) || provablyDisjoint(tp1, tp2.tp2)
2853+
provablyDisjoint(tp1, tp2.tp1, pending) || provablyDisjoint(tp1, tp2.tp2, pending)
28492854

28502855
// Cases where there is an intersection or union on the left but not on the right
28512856
case (tp1: OrType, tp2) =>
2852-
provablyDisjoint(tp1.tp1, tp2) && provablyDisjoint(tp1.tp2, tp2)
2857+
provablyDisjoint(tp1.tp1, tp2, pending) && provablyDisjoint(tp1.tp2, tp2, pending)
28532858
case (tp1: AndType, tp2) =>
2854-
provablyDisjoint(tp1.tp1, tp2) || provablyDisjoint(tp1.tp2, tp2)
2859+
provablyDisjoint(tp1.tp1, tp2, pending) || provablyDisjoint(tp1.tp2, tp2, pending)
28552860

28562861
/* Cases where both are unique values (enum cases or constant types)
28572862
*
@@ -2888,18 +2893,18 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
28882893
*
28892894
* Regardless, we do not look at prefixes.
28902895
*/
2891-
case (tp1, tp2) =>
2896+
case tpPair @ (tp1, tp2) =>
28922897
val cls1 = tp1.classSymbol.asClass
28932898
val cls2 = tp2.classSymbol.asClass
28942899

2895-
def isBaseTypeWithDisjointArguments(baseClass: ClassSymbol): Boolean =
2900+
def isBaseTypeWithDisjointArguments(baseClass: ClassSymbol, pending: util.HashSet[(Type, Type)]): Boolean =
28962901
if baseClass.typeParams.isEmpty then
28972902
// A common mono base class can never be disjoint thanks to type params
28982903
false
28992904
else
29002905
(tp1.baseType(baseClass), tp2.baseType(baseClass)) match
29012906
case (AppliedType(tycon1, args1), AppliedType(tycon2, args2)) =>
2902-
provablyDisjointTypeArgs(baseClass, args1, args2)
2907+
provablyDisjointTypeArgs(baseClass, args1, args2, pending)
29032908
case _ =>
29042909
false
29052910
end isBaseTypeWithDisjointArguments
@@ -2922,16 +2927,22 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
29222927
* We exclude any base class that is an ancestor of one of the other base classes:
29232928
* they are useless, since anything discovered at their level would also be discovered at
29242929
* the level of the descendant common base class.
2925-
* Moreover, we have to do this to prevent infinite recursion with curiously-recursive
2926-
* superclasses: for example `class Seq[A] extends SeqOps[A, Seq[A]]`.
29272930
*/
2931+
val innerPending =
2932+
if pending != null then pending
2933+
else util.HashSet[(Type, Type)]()
2934+
innerPending += tpPair
2935+
29282936
val cls2BaseClassSet = SymDenotations.BaseClassSet(cls2.classDenot.baseClasses)
29292937
val commonBaseClasses = cls1.classDenot.baseClasses.filter(cls2BaseClassSet.contains(_))
29302938
def isAncestorOfOtherBaseClass(cls: ClassSymbol): Boolean =
29312939
commonBaseClasses.exists(other => (other ne cls) && other.derivesFrom(cls))
2932-
commonBaseClasses.exists { baseClass =>
2933-
!isAncestorOfOtherBaseClass(baseClass) && isBaseTypeWithDisjointArguments(baseClass)
2940+
val result = commonBaseClasses.exists { baseClass =>
2941+
!isAncestorOfOtherBaseClass(baseClass) && isBaseTypeWithDisjointArguments(baseClass, innerPending)
29342942
}
2943+
2944+
innerPending -= tpPair
2945+
result
29352946
end existsCommonBaseTypeWithDisjointArguments
29362947

29372948
provablyDisjointClasses(cls1, cls2)
@@ -2941,7 +2952,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
29412952

29422953
private def provablyDisjointClasses(cls1: Symbol, cls2: Symbol)(using Context): Boolean =
29432954
def isDecomposable(cls: Symbol): Boolean =
2944-
cls.is(Sealed) && !cls.hasAnonymousChild
2955+
cls.is(Sealed) && !cls.hasAnonymousChild
29452956

29462957
def decompose(cls: Symbol): List[Symbol] =
29472958
cls.children.map { child =>
@@ -2979,7 +2990,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
29792990
false
29802991
end provablyDisjointClasses
29812992

2982-
private def provablyDisjointTypeArgs(cls: ClassSymbol, args1: List[Type], args2: List[Type])(using Context): Boolean =
2993+
private def provablyDisjointTypeArgs(cls: ClassSymbol, args1: List[Type], args2: List[Type], pending: util.HashSet[(Type, Type)])(using Context): Boolean =
29832994
def fullyInstantiated(tp: Type): Boolean = new TypeAccumulator[Boolean] {
29842995
override def apply(x: Boolean, t: Type) =
29852996
x && {
@@ -2993,11 +3004,11 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
29933004

29943005
// It is possible to conclude that two types applied are disjoint by
29953006
// looking at covariant type parameters if the said type parameters
2996-
// are disjoin and correspond to fields.
3007+
// are disjoint and correspond to fields.
29973008
// (Type parameter disjointness is not enough by itself as it could
29983009
// lead to incorrect conclusions for phantom type parameters).
2999-
def covariantDisjoint(tp1: Type, tp2: Type): Boolean =
3000-
provablyDisjoint(tp1, tp2)
3010+
def covariantDisjoint(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean =
3011+
provablyDisjoint(tp1, tp2, pending) && typeparamCorrespondsToField(cls.appliedRef, tparam)
30013012

30023013
// In the invariant case, we also use a stronger notion of disjointness:
30033014
// we consider fully instantiated types not equal wrt =:= to be disjoint
@@ -3008,66 +3019,26 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
30083019
// Note that this is currently a theoretical concern since Dotty
30093020
// doesn't have type tags, meaning that users cannot write patterns
30103021
// that do type tests on higher kinded types.
3011-
def invariantDisjoint(tp1: Type, tp2: Type): Boolean =
3012-
provablyDisjoint(tp1, tp2) ||
3022+
def invariantDisjoint(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean =
3023+
provablyDisjoint(tp1, tp2, pending) ||
30133024
!isSameType(tp1, tp2) &&
30143025
fullyInstantiated(tp1) && // We can only trust a "no" from `isSameType` when
30153026
fullyInstantiated(tp2) // both `tp1` and `tp2` are fully instantiated.
30163027

30173028
args1.lazyZip(args2).lazyZip(cls.typeParams).exists {
30183029
(arg1, arg2, tparam) =>
3019-
val v = typeParamVarianceStatusForDisjointness(cls, tparam)
3020-
if (v.is(Covariant))
3021-
covariantDisjoint(arg1, arg2)
3022-
else if (v.is(Contravariant))
3030+
val v = tparam.paramVarianceSign
3031+
if (v > 0)
3032+
covariantDisjoint(arg1, arg2, tparam)
3033+
else if (v < 0)
3034+
// Contravariant case: a value where this type parameter is
3035+
// instantiated to `Any` belongs to both types.
30233036
false
30243037
else
3025-
invariantDisjoint(arg1, arg2)
3038+
invariantDisjoint(arg1, arg2, tparam)
30263039
}
30273040
end provablyDisjointTypeArgs
30283041

3029-
/** The "variance status" of the given type parameter for the purpose of deciding disjointness.
3030-
*
3031-
* The variance status of a type parameter is its variance if it is "usable for deciding disjointness",
3032-
* and `Contravariant` otherwise.
3033-
*
3034-
* - `Contravariant` means that it is not usable.
3035-
* - `Covariant` means that it is usable and requires type arguments to be provably disjoint.
3036-
* - `Invariant` means that it is usable and requires type arguments be either a) provably disjoint
3037-
* or b) not equivalent and fully defined.
3038-
*
3039-
* A contravariant type parameter is never usable for deciding disjointness.
3040-
* We can always instantiate them to their upper bound to find a common type.
3041-
*
3042-
* An invariant type parameter is usable if its bounds do not depend on the prefix.
3043-
*
3044-
* A covariant type parameter is usable if its bounds do not depend on the prefix *and*
3045-
* it corresponds to a field.
3046-
* (Type parameter disjointness is not enough by itself as it could lead to
3047-
* incorrect conclusions for phantom type parameters.)
3048-
*/
3049-
private def typeParamVarianceStatusForDisjointness(cls: ClassSymbol, tparam: TypeSymbol)(using Context): Variance =
3050-
// Should this be cached in `tparam` or its denotation?
3051-
3052-
if tparam.is(Contravariant) then
3053-
Contravariant
3054-
else
3055-
val boundsDependOnPrefix = new TypeAccumulator[Boolean] {
3056-
override def apply(x: Boolean, t: Type): Boolean =
3057-
x || (t match {
3058-
case t: ThisType => true
3059-
case _ => foldOver(false, t)
3060-
})
3061-
}.apply(false, tparam.info)
3062-
3063-
if boundsDependOnPrefix then
3064-
Contravariant
3065-
else if tparam.is(Covariant) && !typeparamCorrespondsToField(cls.appliedRef, tparam) then
3066-
Contravariant
3067-
else
3068-
tparam.variance
3069-
end typeParamVarianceStatusForDisjointness
3070-
30713042
protected def explainingTypeComparer = ExplainingTypeComparer(comparerContext)
30723043
protected def trackingTypeComparer = TrackingTypeComparer(comparerContext)
30733044

0 commit comments

Comments
 (0)