Skip to content

Iterate where: explanations to fixed point #25851

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
mbovel wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Iterate where: explanations to fixed point #25851

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
94ae04d
Add test for nested type variable explanation
mbovel Apr 17, 2026
d0cf5a6
Iterate where-clause explanations to fixed point
mbovel Apr 17, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
46 changes: 26 additions & 20 deletions compiler/src/dotty/tools/dotc/reporting/Message.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -221,33 +221,39 @@ object Message:
case ref: Capability => ref.isTerminalCapability
}

val toExplain: List[(String, Recorded)] = seen.toList.flatMap { kvs =>
val res: List[(String, Recorded)] = kvs match {
case (key, entry :: Nil) =>
if (needsExplanation(entry)) (key.str, entry) :: Nil else Nil
case (key, entries) =>
for (alt <- entries) yield {
val tickedString = record(key.str, key.isType, alt)
(tickedString, alt)
}
}
res // help the inferencer out
}.sortBy(_._1)
def collectToExplain(): List[(String, Recorded)] =
seen.toList.flatMap { kvs =>
val res: List[(String, Recorded)] = kvs match {
case (key, entry :: Nil) =>
if (needsExplanation(entry)) (key.str, entry) :: Nil else Nil
case (key, entries) =>
for (alt <- entries) yield {
val tickedString = record(key.str, key.isType, alt)
(tickedString, alt)
}
}
res // help the inferencer out
}.sortBy(_._1)

def columnar(parts: List[(String, String)]): List[String] =
lazy val maxLen = parts.map(_._1.length).max
parts.map: (leader, trailer) =>
val variable = hl(leader)
s"""$variable${" " * (maxLen - leader.length)} $trailer"""

// Group keys with the same Recorded entry together. We can't use groupBy here
// since we want to maintain the order in which entries first appear in the
// original list.
val toExplainGrouped: List[(Recorded, List[String])] =
for entry <- toExplain.map(_._2).distinct
yield (entry, for (key, e) <- toExplain if e == entry yield key)
val explainParts = toExplainGrouped.map:
(entry, keys) => (keys.mkString(" and "), explanation(entry, keys))
// Rendering an explanation may record new entries (e.g. a type variable's
// constraint mentioning another type variable). Iterate to a fixed point.
val explained = collection.mutable.LinkedHashMap.empty[Recorded, (List[String], String)]
var prev = -1
while prev != explained.size do
prev = explained.size
val toExplain = collectToExplain()
for entry <- toExplain.map(_._2).distinct if !explained.contains(entry) do
val keys = for (key, e) <- toExplain if e == entry yield key
explained(entry) = (keys, explanation(entry, keys))

val explainParts = explained.values.toList.map:
(keys, expl) => (keys.mkString(" and "), expl)
val explainLines = columnar(explainParts)
if (explainLines.isEmpty) "" else i"where: $explainLines%\n %\n"
end explanations
Expand Down
3 changes: 3 additions & 0 deletions tests/neg-custom-args/captures/boundary-homebrew.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,5 +8,8 @@
|
|where: ^ refers to a root capability created in method test
| any is a root capability created in anonymous function of type (using l1²: boundary.Label[boundary.Label[Int]^²]^²): boundary.Label[Int]^² of parameter parameter l1 of method $anonfun
| ^² refers to the root capability caps.any
| l1 is a parameter in an anonymous function in method test
| l1² is a reference to a value parameter
|
| longer explanation available when compiling with `-explain`
10 changes: 6 additions & 4 deletions tests/neg-custom-args/captures/boundary.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,10 +32,12 @@
|
|Note that capability `any²` cannot flow into capture set {any}.
|
|where: ^ refers to the root capability caps.any
| ^² refers to a root capability classified as Control in the type of value local²
| any is a root capability classified as Control created in object test when checking argument to parameter label of method break
| any² is a root capability classified as Control in the type of value local
|where: ^ refers to the root capability caps.any
| ^² refers to a root capability classified as Control in the type of value local²
| any is a root capability classified as Control created in object test when checking argument to parameter label of method break
| any² is a root capability classified as Control in the type of value local
| local is a value locally defined in object test
| local² is a value locally defined in object test
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/boundary.scala:5:4 ---------------------------------------
Expand Down
7 changes: 7 additions & 0 deletions tests/neg-custom-args/captures/classifiers-secondclass.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,17 +5,24 @@
|of an enclosing function literal with expected type (Int, Int) ->{any.only[Read]} Int.
|
|where: any is a root capability created in anonymous function of type (f²: Levels.File^): Unit when checking argument to parameter op of method parReduce
| ^ refers to the root capability caps.any
| f is a parameter in an anonymous function in method test
| f² is a reference to a value parameter
-- [E223] CaptureChecking Error: tests/neg-custom-args/captures/classifiers-secondclass.scala:54:12 --------------------
54 | f.write(42) // error, the error stems from here
| ^^^^^^^
|Reference `f.write` is not included in the allowed capture set {any.only[Read]}
|of an enclosing function literal with expected type (Int, Int) ->{any.only[Read]} Int.
|
|where: any is a root capability created in anonymous function of type (g: Levels.File^): Unit when checking argument to parameter op of method parReduce
| ^ refers to the root capability caps.any
-- [E223] CaptureChecking Error: tests/neg-custom-args/captures/classifiers-secondclass.scala:57:12 --------------------
57 | g.write(42) // error, the error stems from here
| ^^^^^^^
|Reference `g.write` is not included in the allowed capture set {any.only[Read]}
|of an enclosing function literal with expected type (Int, Int) ->{any.only[Read]} Int.
|
|where: any is a root capability created in anonymous function of type (g²: Levels.File^): Unit when checking argument to parameter op of method parReduce
| ^ refers to the root capability caps.any
| g is a parameter in an anonymous function in method testMulti
| g² is a reference to a value parameter
5 changes: 3 additions & 2 deletions tests/neg-custom-args/captures/freeze-boxes.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,9 @@
|of value a with type Ref^.
|This type hides capabilities {any}
|
|where: ^ refers to a root capability classified as Unscoped in the type of value a
| any is a root capability classified as Unscoped created in value a when instantiating method allocRef's type (): Ref^{fresh}
|where: ^ refers to a root capability classified as Unscoped in the type of value a
| any is a root capability classified as Unscoped created in value a when instantiating method allocRef's type (): Ref^{fresh}
| fresh is a root capability associated with the result type of (): Ref^{fresh}
-- Error: tests/neg-custom-args/captures/freeze-boxes.scala:31:6 -------------------------------------------------------
31 | par(() => a.set(42), () => println(b.get)) // error
| ^^^^^^^^^^^^^^^
Expand Down
16 changes: 9 additions & 7 deletions tests/neg-custom-args/captures/i15772.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,15 +21,17 @@
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15772.scala:35:33 ---------------------------------------
35 | val boxed2 : Observe[C]^ = box2(c) // error
| ^^^^^^^
| Found: (C{val arg: C^}^{any} => Unit) -> Unit
| Required: (C => Unit) =>² Unit
| Found: (C{val arg: C^}^{any} => Unit) -> Unit
| Required: (C => Unit) =>² Unit
|
| Note that capability `any` cannot flow into capture set {}.
| Note that capability `any` cannot flow into capture set {}.
|
| where: => refers to the root capability caps.any
| =>² refers to a root capability in the type of value boxed2
| ^ refers to a root capability in the type of value arg
| any is a root capability created in value boxed2 when instantiating method c's type -> C^{fresh}
| where: => refers to the root capability caps.any
| =>² refers to a root capability in the type of value boxed2
| ^ refers to a root capability in the type of value arg
| any is a root capability created in value boxed2 when instantiating method c's type -> C^{fresh}
| fresh is a root capability associated with the result type of -> C^²
| ^² refers to a root capability in the result type of method c
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15772.scala:46:2 ----------------------------------------
Expand Down
5 changes: 4 additions & 1 deletion tests/neg-custom-args/captures/i15923.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,9 @@
|Found: Id[Cap^{any}]^'s2
|Required: Id[Cap^'s1]^'s3
|
|where: any is a root capability created in anonymous function of type (using lcap: scala.caps.Capability^): Cap^{lcap} ->'s4 Id[Cap^{any}]^'s5 of parameter parameter lcap² of method $anonfun
|where: any is a root capability created in anonymous function of type (using lcap: scala.caps.Capability^): Cap^{lcap} ->'s4 Id[Cap^{any}]^'s5 of parameter parameter lcap² of method $anonfun
| ^ refers to the root capability caps.any
| lcap is a reference to a value parameter
| lcap² is a parameter in an anonymous function in method bar
|
| longer explanation available when compiling with `-explain`
18 changes: 14 additions & 4 deletions tests/neg-custom-args/captures/i16226.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,13 @@
|Note that capability `f1` cannot flow into capture set {any}
|because (f1 : A => B) in an enclosing function is not visible from any in method mapc.
|
|where: => refers to a root capability created in anonymous function of type (ref1²: LazyRef[A]^{io}, f1²: A => B): LazyRef[B]^ of parameter parameter f1 of method $anonfun
| any is a root capability in the result type of method mapc
|where: => refers to a root capability created in anonymous function of type (ref1²: LazyRef[A]^{io}, f1²: A => B): LazyRef[B]^ of parameter parameter f1 of method $anonfun
| any is a root capability in the result type of method mapc
| ^ refers to the root capability caps.any
| f1 is a parameter in an anonymous function in method mapc
| f1² is a reference to a value parameter
| ref1 is a parameter in an anonymous function in method mapc
| ref1² is a reference to a value parameter
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i16226.scala:15:27 ---------------------------------------
Expand All @@ -20,7 +25,12 @@
|Note that capability `f1` cannot flow into capture set {any}
|because (f1 : A => B) in an enclosing function is not visible from any in method mapd.
|
|where: => refers to a root capability created in anonymous function of type (ref1²: LazyRef[A]^{io}, f1²: A => B): LazyRef[B]^ of parameter parameter f1 of method $anonfun
| any is a root capability in the result type of method mapd
|where: => refers to a root capability created in anonymous function of type (ref1²: LazyRef[A]^{io}, f1²: A => B): LazyRef[B]^ of parameter parameter f1 of method $anonfun
| any is a root capability in the result type of method mapd
| ^ refers to the root capability caps.any
| f1 is a parameter in an anonymous function in method mapd
| f1² is a reference to a value parameter
| ref1 is a parameter in an anonymous function in method mapd
| ref1² is a reference to a value parameter
|
| longer explanation available when compiling with `-explain`
3 changes: 3 additions & 0 deletions tests/neg-custom-args/captures/i21401.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,9 @@
|
|where: ^ refers to a root capability created in anonymous function of type (x²: IO^²): IO^² of parameter parameter x of method $anonfun
| any is a root capability created in value a
| ^² refers to the root capability caps.any
| x is a parameter in an anonymous function in method test2
| x² is a reference to a value parameter
|
| longer explanation available when compiling with `-explain`
-- Error: tests/neg-custom-args/captures/i21401.scala:16:66 ------------------------------------------------------------
Expand Down
2 changes: 2 additions & 0 deletions tests/neg-custom-args/captures/i21614.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,8 @@
|
|where: any is a root capability classified as SharedCapability created in anonymous function of type (f²: F): Logger when checking argument to parameter f of constructor Logger
| any² is a root capability classified as SharedCapability in the type of parameter f
| f is a parameter in an anonymous function in method mkLoggers1
| f² is a reference to a value parameter
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:15:12 ---------------------------------------
Expand Down
7 changes: 5 additions & 2 deletions tests/neg-custom-args/captures/i23431.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,8 +33,11 @@
|Note that capability `io3` cannot flow into capture set {any}
|because (io3 : IO^) in an enclosing function is not visible from any in variable myIO.
|
|where: ^ refers to a root capability created in anonymous function of type (io3²: IO^²): Unit of parameter parameter io3 of method $anonfun
| any is a root capability in the type of variable myIO
|where: ^ refers to a root capability created in anonymous function of type (io3²: IO^²): Unit of parameter parameter io3 of method $anonfun
| any is a root capability in the type of variable myIO
| ^² refers to the root capability caps.any
| io3 is a parameter in an anonymous function in method test
| io3² is a reference to a value parameter
|
| longer explanation available when compiling with `-explain`
-- Error: tests/neg-custom-args/captures/i23431.scala:6:14 -------------------------------------------------------------
Expand Down
8 changes: 6 additions & 2 deletions tests/neg-custom-args/captures/indirect-avoid.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,9 @@
|
|Note that capability `any.rd` cannot flow into capture set {}.
|
|where: any is a root capability created in value x1 when instantiating method filterImpl1's type (ll: Test.LL^): Test.LL^{fresh.rd, ll}
|where: any is a root capability created in value x1 when instantiating method filterImpl1's type (ll: Test.LL^): Test.LL^{fresh.rd, ll}
| ^ refers to the root capability caps.any
| fresh is a root capability associated with the result type of (ll: Test.LL^): Test.LL^{fresh.rd, ll}
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/indirect-avoid.scala:32:4 --------------------------------
Expand All @@ -34,4 +36,6 @@
|Fields capturing a root capability need to be given an explicit type unless the capability is already
|subsumed by the computed capability of the enclosing class.
|
|where: any is a root capability created in value x1 when instantiating method filterImpl1's type (ll: Test.LL^): Test.LL^{fresh.rd, ll}
|where: any is a root capability created in value x1 when instantiating method filterImpl1's type (ll: Test.LL^): Test.LL^{fresh.rd, ll}
| ^ refers to the root capability caps.any
| fresh is a root capability associated with the result type of (ll: Test.LL^): Test.LL^{fresh.rd, ll}
3 changes: 3 additions & 0 deletions tests/neg-custom-args/captures/lazyListState.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,5 +6,8 @@
|
| where: ^ refers to a root capability in the type of value tail
| fresh is a root capability associated with the result type of -> LazyListIterable[A²]^²
| A is a type in class Cons
| A² is a type in trait State
| ^² refers to a root capability in the result type of method tail
|
| longer explanation available when compiling with `-explain`
1 change: 1 addition & 0 deletions tests/neg-custom-args/captures/lazylist-global.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,5 +54,6 @@
| method tail of type -> lazylists.LazyList[Nothing]^{fresh} has incompatible type
|
| where: fresh is a root capability associated with the result type of -> lazylists.LazyList[Nothing]^
| ^ refers to a root capability in the result type of method tail
|
| longer explanation available when compiling with `-explain`
1 change: 1 addition & 0 deletions tests/neg-custom-args/captures/lazylist.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,5 +50,6 @@
| method tail of type -> lazylists.LazyList[Nothing]^{fresh} has incompatible type
|
| where: fresh is a root capability associated with the result type of -> lazylists.LazyList[Nothing]^
| ^ refers to a root capability in the result type of method tail
|
| longer explanation available when compiling with `-explain`
3 changes: 2 additions & 1 deletion tests/neg-custom-args/captures/mut-iterator4.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,8 @@
|
|Note that capability `any` cannot flow into capture set {it, f}.
|
|where: any is a root capability created in method mappedIterator when constructing instance Object with (Iterator[U]^{any².rd}) {...}
|where: any is a root capability created in method mappedIterator when constructing instance Object with (Iterator[U]^{any².rd}) {...}
| any² is a root capability created in method mappedIterator
|
22 | def hasNext = it.hasNext
23 | update def next() = f(it.next())
Expand Down
7 changes: 6 additions & 1 deletion tests/neg-custom-args/captures/reaches.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,9 @@
|
|where: ^ refers to a root capability created in anonymous function of type (x²: File^²): File^² of parameter parameter x of method $anonfun
| any is a root capability in the type of value id
| ^² refers to the root capability caps.any
| x is a parameter in an anonymous function in method attack2
| x² is a reference to a value parameter
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:71:27 --------------------------------------
Expand All @@ -51,7 +54,9 @@
|
|Note that capability `any` cannot flow into capture set {id*}.
|
|where: any is a root capability created in value f1 when instantiating function value id's type (x: File^): File^{fresh}
|where: any is a root capability created in value f1 when instantiating function value id's type (x: File^): File^{fresh}
| ^ refers to the root capability caps.any
| fresh is a root capability associated with the result type of (x: File^): File^{fresh}
|
| longer explanation available when compiling with `-explain`
-- Error: tests/neg-custom-args/captures/reaches.scala:39:31 -----------------------------------------------------------
Expand Down
3 changes: 3 additions & 0 deletions tests/neg-custom-args/captures/refine-reach-shallow.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,9 @@
|
|where: ^ refers to a root capability created in anonymous function of type (x²: IO^²): IO^² of parameter parameter x of method $anonfun
| any is a root capability in the type of value f
| ^² refers to the root capability caps.any
| x is a parameter in an anonymous function in method test1
| x² is a reference to a value parameter
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/refine-reach-shallow.scala:10:38 -------------------------
Expand Down
Loading