From 3cd94b4049d84d32464d695c753e1b1770a34c89 Mon Sep 17 00:00:00 2001 From: Dale Wijnand Date: Fri, 31 Jan 2025 14:18:56 +0000 Subject: [PATCH 1/3] Avoid inf recursion in provablyDisjointClasses --- .../dotty/tools/dotc/core/TypeComparer.scala | 20 ++++++++++++----- tests/pos/i22266.scala | 22 +++++++++++++++++++ 2 files changed, 37 insertions(+), 5 deletions(-) create mode 100644 tests/pos/i22266.scala diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 6d21143a71ed..ff55f92a4a82 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -3201,14 +3201,15 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling result end existsCommonBaseTypeWithDisjointArguments - provablyDisjointClasses(cls1, cls2) + provablyDisjointClasses(cls1, cls2, seen = null) || existsCommonBaseTypeWithDisjointArguments end match } - private def provablyDisjointClasses(cls1: Symbol, cls2: Symbol)(using Context): Boolean = + private def provablyDisjointClasses(cls1: Symbol, cls2: Symbol, seen: util.HashSet[Symbol] | Null)(using Context): Boolean = def isDecomposable(cls: Symbol): Boolean = - cls.is(Sealed) && !cls.hasAnonymousChild + if seen != null && seen.contains(cls) then false + else cls.is(Sealed) && !cls.hasAnonymousChild def decompose(cls: Symbol): List[Symbol] = cls.children.flatMap { child => @@ -3217,6 +3218,13 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling else child :: Nil }.filter(child => child.exists && child != cls) + inline def seeing(inline cls: Symbol)(inline thunk: util.HashSet[Symbol] => Boolean) = + val seen1 = if seen == null then new util.HashSet[Symbol] else seen + try + seen1 += cls + thunk(seen1) + finally seen1 -= cls + def eitherDerivesFromOther(cls1: Symbol, cls2: Symbol): Boolean = cls1.derivesFrom(cls2) || cls2.derivesFrom(cls1) @@ -3239,9 +3247,11 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling // instantiations of `cls1` (terms of the form `new cls1`) are not // of type `tp2`. Therefore, we can safely decompose `cls1` using // `.children`, even if `cls1` is non abstract. - decompose(cls1).forall(x => provablyDisjointClasses(x, cls2)) + seeing(cls1): seen1 => + decompose(cls1).forall(x => provablyDisjointClasses(x, cls2, seen1)) else if (isDecomposable(cls2)) - decompose(cls2).forall(x => provablyDisjointClasses(cls1, x)) + seeing(cls2): seen1 => + decompose(cls2).forall(x => provablyDisjointClasses(cls1, x, seen1)) else false end provablyDisjointClasses diff --git a/tests/pos/i22266.scala b/tests/pos/i22266.scala new file mode 100644 index 000000000000..2ecdf9492a93 --- /dev/null +++ b/tests/pos/i22266.scala @@ -0,0 +1,22 @@ +sealed trait NonPolygon +sealed trait Polygon + +sealed trait SymmetryAspect +sealed trait RotationalSymmetry extends SymmetryAspect +sealed trait MaybeRotationalSymmetry extends SymmetryAspect + +enum Shape: + case Circle extends Shape with NonPolygon with RotationalSymmetry + case Triangle extends Shape with Polygon with MaybeRotationalSymmetry + case Square extends Shape with Polygon with RotationalSymmetry + +object Shape: + + def hasPolygon( + rotationalSyms: Vector[Shape & RotationalSymmetry], + maybeSyms: Vector[Shape & MaybeRotationalSymmetry] + ): Boolean = + val all = rotationalSyms.concat(maybeSyms) + all.exists: + case _: Polygon => true + case _ => false From 04f6fc3893404bfc8c87395d2daa5601b7672fe9 Mon Sep 17 00:00:00 2001 From: Dale Wijnand Date: Fri, 31 Jan 2025 15:19:02 +0000 Subject: [PATCH 2/3] Avoid early widening enum val symbols in provablyDisjointClasses --- .../dotty/tools/dotc/core/TypeComparer.scala | 31 +++++++------------ tests/pos/i22266.unenum.scala | 22 +++++++++++++ tests/warn/i21860.unenum.scala | 2 +- 3 files changed, 34 insertions(+), 21 deletions(-) create mode 100644 tests/pos/i22266.unenum.scala diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index ff55f92a4a82..7ef4e2ba47bc 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -3201,35 +3201,28 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling result end existsCommonBaseTypeWithDisjointArguments - provablyDisjointClasses(cls1, cls2, seen = null) + provablyDisjointClasses(cls1, cls2) || existsCommonBaseTypeWithDisjointArguments end match } - private def provablyDisjointClasses(cls1: Symbol, cls2: Symbol, seen: util.HashSet[Symbol] | Null)(using Context): Boolean = + private def provablyDisjointClasses(cls1: Symbol, cls2: Symbol)(using Context): Boolean = def isDecomposable(cls: Symbol): Boolean = - if seen != null && seen.contains(cls) then false - else cls.is(Sealed) && !cls.hasAnonymousChild + cls.is(Sealed) && !cls.hasAnonymousChild def decompose(cls: Symbol): List[Symbol] = - cls.children.flatMap { child => + cls.children.map: child => if child.isTerm then - child.info.classSymbols // allow enum vals to be decomposed to their enum class (then filtered out) and any mixins - else child :: Nil - }.filter(child => child.exists && child != cls) - - inline def seeing(inline cls: Symbol)(inline thunk: util.HashSet[Symbol] => Boolean) = - val seen1 = if seen == null then new util.HashSet[Symbol] else seen - try - seen1 += cls - thunk(seen1) - finally seen1 -= cls + child.info.classSymbol.orElse(child) + else child + .filter(child => child.exists && child != cls) def eitherDerivesFromOther(cls1: Symbol, cls2: Symbol): Boolean = cls1.derivesFrom(cls2) || cls2.derivesFrom(cls1) def smallestNonTraitBase(cls: Symbol): Symbol = - cls.asClass.baseClasses.find(!_.is(Trait)).get + val classes = if cls.isClass then cls.asClass.baseClasses else cls.info.classSymbols + classes.find(!_.is(Trait)).get if (eitherDerivesFromOther(cls1, cls2)) false @@ -3247,11 +3240,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling // instantiations of `cls1` (terms of the form `new cls1`) are not // of type `tp2`. Therefore, we can safely decompose `cls1` using // `.children`, even if `cls1` is non abstract. - seeing(cls1): seen1 => - decompose(cls1).forall(x => provablyDisjointClasses(x, cls2, seen1)) + decompose(cls1).forall(x => provablyDisjointClasses(x, cls2)) else if (isDecomposable(cls2)) - seeing(cls2): seen1 => - decompose(cls2).forall(x => provablyDisjointClasses(cls1, x, seen1)) + decompose(cls2).forall(x => provablyDisjointClasses(cls1, x)) else false end provablyDisjointClasses diff --git a/tests/pos/i22266.unenum.scala b/tests/pos/i22266.unenum.scala new file mode 100644 index 000000000000..e7529b7edabe --- /dev/null +++ b/tests/pos/i22266.unenum.scala @@ -0,0 +1,22 @@ +sealed trait NonPolygon +sealed trait Polygon + +sealed trait SymmetryAspect +sealed trait RotationalSymmetry extends SymmetryAspect +sealed trait MaybeRotationalSymmetry extends SymmetryAspect + +sealed abstract class Shape + +object Shape: + case object Circle extends Shape with NonPolygon with RotationalSymmetry + case object Triangle extends Shape with Polygon with MaybeRotationalSymmetry + case object Square extends Shape with Polygon with RotationalSymmetry + + def hasPolygon( + rotationalSyms: Vector[Shape & RotationalSymmetry], + maybeSyms: Vector[Shape & MaybeRotationalSymmetry] + ): Boolean = + val all = rotationalSyms.concat(maybeSyms) + all.exists: + case _: Polygon => true + case _ => false diff --git a/tests/warn/i21860.unenum.scala b/tests/warn/i21860.unenum.scala index 7335e1b6851d..e4b282e35e76 100644 --- a/tests/warn/i21860.unenum.scala +++ b/tests/warn/i21860.unenum.scala @@ -3,7 +3,7 @@ sealed trait Corners { self: Figure => } sealed abstract class Shape extends Figure object Shape: - case object Triange extends Shape with Corners + case object Triangle extends Shape with Corners case object Square extends Shape with Corners case object Circle extends Shape case object Ellipsis extends Shape From 4cd2a97a1c74a1eb3408e128fa4166eb1d0899f7 Mon Sep 17 00:00:00 2001 From: Dale Wijnand Date: Mon, 3 Feb 2025 11:40:29 +0000 Subject: [PATCH 3/3] Document enum value changes in provablyDisjointClasses --- .../dotty/tools/dotc/core/TypeComparer.scala | 21 ++++++++++++++++--- docs/_spec/03-types.md | 2 +- 2 files changed, 19 insertions(+), 4 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 7ef4e2ba47bc..cc0471d40213 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -2983,11 +2983,11 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling * * 1. Single inheritance of classes * 2. Final classes cannot be extended - * 3. ConstantTypes with distinct values are non intersecting - * 4. TermRefs with distinct values are non intersecting + * 3. ConstantTypes with distinct values are non-intersecting + * 4. TermRefs with distinct values are non-intersecting * 5. There is no value of type Nothing * - * Note on soundness: the correctness of match types relies on on the + * Note on soundness: the correctness of match types relies on the * property that in all possible contexts, the same match type expression * is either stuck or reduces to the same case. * @@ -3206,6 +3206,11 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling end match } + /** Are `cls1` and `cls1` provablyDisjoint classes, i.e., is `cls1 ⋔ cls2` true? + * + * Note that "class" where includes traits, module classes, and (in the recursive case) + * enum value term symbols. + */ private def provablyDisjointClasses(cls1: Symbol, cls2: Symbol)(using Context): Boolean = def isDecomposable(cls: Symbol): Boolean = cls.is(Sealed) && !cls.hasAnonymousChild @@ -3213,6 +3218,16 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling def decompose(cls: Symbol): List[Symbol] = cls.children.map: child => if child.isTerm then + // Enum vals with mixins, such as in i21860 or i22266, + // don't have a single class symbol. + // So instead of decomposing to NoSymbol + // (which leads to erroneously considering an enum type + // as disjoint from one of the mixin, eg. i21860.scala), + // or instead of decomposing to all the class symbols of + // the enum value (which leads to other mixins being decomposed, + // and infinite recursion, eg. i22266), + // we decompose to the enum value term symbol, and handle + // that within the rest of provablyDisjointClasses. child.info.classSymbol.orElse(child) else child .filter(child => child.exists && child != cls) diff --git a/docs/_spec/03-types.md b/docs/_spec/03-types.md index 4b1293258495..5d4e205aace9 100644 --- a/docs/_spec/03-types.md +++ b/docs/_spec/03-types.md @@ -1071,7 +1071,7 @@ The following properties hold about ´⌈X⌉´ (we have paper proofs for those) The "lower-bound rule" states that ´S <: T´ if ´T = q.X´ and ´q.X´ is a non-class type designator and ´S <: L´ where ´L´ is the lower bound of the underlying type definition of ´q.X´". That rule is known to break transitivy of subtyping in Scala already. -Second, we define the relation ´⋔´ on *classes* (including traits and hidden classes of objects) as: +Second, we define the relation ´⋔´ on *classes* (including traits, hidden classes of objects, and enum terms) as: - ´C ⋔ D´ if `´C ∉´ baseClasses´(D)´` and ´D´ is `final` - ´C ⋔ D´ if `´D ∉´ baseClasses´(C)´` and ´C´ is `final`