Skip to content

Commit 3cbf99e

Browse files
committed
[WIP] Fix scala#2874: implement check for expansive cycles
Expansive cycles characterize situations where the class hierarchy of a generic class is potentially infinite. This can lead to nontermination during subtype checks. This PR implements the algorithm in Kennedy, Andrew J., and Benjamin C. Pierce. "On decidability of nominal subtyping with variance." (2006). for detecting (and disallowing) expansive cycles.
1 parent d916343 commit 3cbf99e

File tree

4 files changed

+119
-0
lines changed

4 files changed

+119
-0
lines changed

compiler/src/dotty/tools/dotc/reporting/diagnostic/ErrorMessageID.java

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -96,6 +96,7 @@ public enum ErrorMessageID {
9696
WrongNumberOfParametersID,
9797
DuplicatePrivateProtectedQualifierID,
9898
ExpectedStartOfTopLevelDefinitionID,
99+
TypeParamInExpansiveCycleID,
99100
;
100101

101102
public int errorNumber() {

compiler/src/dotty/tools/dotc/reporting/diagnostic/messages.scala

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1710,4 +1710,38 @@ object messages {
17101710
hl"you have to provide either ${"class"}, ${"trait"}, ${"object"}, or ${"enum"} definitions after qualifiers"
17111711
}
17121712

1713+
case class TypeParamInExpansiveCycle(cinfo: ClassInfo, tparam: Symbol)(implicit ctx: Context)
1714+
extends Message(TypeParamInExpansiveCycleID) {
1715+
1716+
val kind = "Syntax"
1717+
1718+
val msg = hl"type parameter ${tparam.showName} in ${cinfo.classSymbol} is part of an expansive cycle"
1719+
1720+
val explanation =
1721+
hl"""| If a class has a type parameter that is part of an expansive cycle, then a subtype test involving the class
1722+
| might fail to terminate. Expansive cycles are therefore disallowed.
1723+
|
1724+
| For the definition of expansive cycles, see:
1725+
| ${Green("Kennedy, Andrew J., and Benjamin C. Pierce. \"On decidability of nominal subtyping with variance.\" (2006)")}
1726+
|
1727+
| Example
1728+
| In the class definitions:
1729+
|
1730+
| ${"class N[-Z]"}
1731+
| ${"class C[X] extends N[N[C[C[X]]]]"}
1732+
|
1733+
| ${"X"} is part of an expansive cycle. When we try to check ${"C[X] <: N[C[X]]"}, we get the following
1734+
| sequence of subtype tests:
1735+
|
1736+
| ${"C[X] <: N[C[X]]"}
1737+
| ${"N[N[C[C[X]]]] <: N[C[X]]"} (inheritance)
1738+
| ${"C[X] <: N[C[C[X]]]"} (contravariance)
1739+
| ${"N[N[C[C[X]]]} <: N[C[C[X]]]"} (inheritance)
1740+
| ${"C[C[X]] <: N[C[C[X]]]"} (contravariance)
1741+
| ...
1742+
|
1743+
| Notice how the last test is just like the first, but with an additional ${"C"}, which means we will
1744+
| loop forever.
1745+
""".stripMargin
1746+
}
17131747
}

compiler/src/dotty/tools/dotc/typer/Checking.scala

Lines changed: 82 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -707,6 +707,88 @@ trait Checking {
707707
checkNoForwardDependencies(vparams1)
708708
case Nil =>
709709
}
710+
711+
/*** Check that none of the type parameters of a class are part of an expansive cycle.
712+
*
713+
* For the definition of expansive cycles, see Kennedy, Andrew J., and Benjamin C. Pierce.
714+
* "On decidability of nominal subtyping with variance." (2006).
715+
*/
716+
def checkExpansiveCycles(classDef: TypeDef)(implicit ctx: Context): Unit = {
717+
classDef.denot.info match {
718+
case cinfo: ClassInfo =>
719+
cinfo.typeParams foreach {
720+
case tparam: Symbol =>
721+
if (expansiveParams(tparam) contains tparam) {
722+
ctx.error(TypeParamInExpansiveCycle(cinfo, tparam), tparam.pos)
723+
}
724+
case _ =>
725+
}
726+
case _ =>
727+
}
728+
}
729+
730+
/*** A state in the type parameter dependency graph indicates the referenced type parameter and whether we got
731+
* to it through a path that includes at least one expansive edge.
732+
*/
733+
private case class ExpansiveSt(tparam: Symbol, expansive: Boolean)
734+
735+
/*** Calculates the set of type parameters that can be reached from the given type parameter by following a
736+
* path containing at least one expansive edge. The set is calculated via BFS.
737+
*/
738+
private def expansiveParams(tparam: Symbol)(implicit ctx: Context): Set[Symbol] = {
739+
val worklist = mutable.Queue[ExpansiveSt]()
740+
val seen = mutable.Set[ExpansiveSt]()
741+
def enqueue(st: ExpansiveSt): Unit = {
742+
if (!(seen contains st)) {
743+
worklist += st
744+
seen += st
745+
}
746+
}
747+
enqueue(ExpansiveSt(tparam, expansive=false))
748+
while (worklist.nonEmpty) {
749+
val st@ExpansiveSt(fromParam, expansive) = worklist.dequeue()
750+
val findNext = new ExpansiveStAcc(st)
751+
fromParam.owner.info match {
752+
case cinfo: ClassInfo =>
753+
for {
754+
parent <- cinfo.parentsWithArgs
755+
toParams = findNext(List.empty[ExpansiveSt], parent)
756+
toParam <- toParams
757+
} enqueue(toParam)
758+
case _ =>
759+
}
760+
}
761+
Set.empty[Symbol] ++ seen.filter((st) => st.expansive).map((st) => st.tparam)
762+
}
763+
764+
/*** Given a type parameter and a type, finds all refinements in the type that reference the type parameter,
765+
* and whether they do so in an expansive manner.
766+
*/
767+
private class ExpansiveStAcc(state: ExpansiveSt)(implicit ctx: Context) extends TypeAccumulator[List[ExpansiveSt]] {
768+
val ExpansiveSt(tparam, expansive) = state
769+
770+
/** Does the type reference the type parameter somewhere in it? */
771+
def hasReference(typ: Type): Boolean = {
772+
typ.namedPartsWith(_.symbol == tparam).nonEmpty
773+
}
774+
775+
override def apply(acc: List[ExpansiveSt], tp: Type): List[ExpansiveSt] = {
776+
tp match {
777+
case RefinedType(parent, name: TypeName, info) =>
778+
val toParam = parent.typeParamNamed(name)
779+
if (info.typeSymbol == tparam) {
780+
// A non-expansive edge: `tparam` replaces `toParam` directly.
781+
ExpansiveSt(toParam, expansive = expansive) :: acc
782+
} else if (hasReference(info)) {
783+
// An expansive edge: `tparam` is passed as *part* of the argument replacing `toParam`.
784+
this (ExpansiveSt(toParam, expansive = true) :: acc, info)
785+
} else {
786+
acc
787+
}
788+
case _ => foldOver(acc, tp)
789+
}
790+
}
791+
}
710792
}
711793

712794
trait NoChecking extends Checking {

compiler/src/dotty/tools/dotc/typer/Typer.scala

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1429,6 +1429,8 @@ class Typer extends Namer with TypeAssigner with Applications with Implicits wit
14291429
// check value class constraints
14301430
checkDerivedValueClass(cls, body1)
14311431

1432+
checkExpansiveCycles(cdef1)
1433+
14321434
if (ctx.settings.YretainTrees.value) {
14331435
cls.myTree = cdef1
14341436
}

0 commit comments

Comments
 (0)