Skip to content

Commit 9e6c50f

Browse files
oderskyodersky
committed
More detailed error messages
Now we also report on level and classifier errors when comparing with FreshCaps.
1 parent 62ea27e commit 9e6c50f

17 files changed

+98
-53
lines changed

‎compiler/src/dotty/tools/dotc/cc/Capability.scala

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -156,6 +156,14 @@ object Capabilities:
156156
case that: FreshCap => this eq that
157157
case _ => false
158158

159+
def acceptsLevelOf(ref: Capability)(using Context): Boolean =
160+
if ccConfig.useFreshLevels && !CCState.collapseFresh then
161+
val refOwner = ref.levelOwner
162+
refOwner.isStaticOwner || ccOwner.isContainedIn(refOwner)
163+
else ref.core match
164+
case ResultCap(_) | _: ParamRef => false
165+
case _ => true
166+
159167
def descr(using Context) =
160168
val originStr = origin match
161169
case Origin.InDecl(sym) if sym.exists =>
@@ -681,7 +689,7 @@ object Capabilities:
681689
case _ => true
682690

683691
vs.ifNotSeen(this)(x.hiddenSet.elems.exists(_.subsumes(y)))
684-
|| levelOK
692+
|| x.acceptsLevelOf(y)
685693
&& ( y.tryClassifyAs(x.hiddenSet.classifier)
686694
|| { capt.println(i"$y cannot be classified as $x"); false }
687695
)

‎compiler/src/dotty/tools/dotc/cc/CaptureOps.scala

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -467,7 +467,6 @@ extension (tp: Type)
467467

468468
def classifier(using Context): ClassSymbol =
469469
tp.classSymbols.map(_.classifier).foldLeft(defn.AnyClass)(leastClassifier)
470-
471470
extension (tp: MethodType)
472471
/** A method marks an existential scope unless it is the prefix of a curried method */
473472
def marksExistentialScope(using Context): Boolean =
@@ -599,6 +598,11 @@ extension (sym: Symbol)
599598
if sym.is(Method) && sym.owner.isClass then isReadOnlyMethod
600599
else sym.owner.isInReadOnlyMethod
601600

601+
def qualString(prefix: String)(using Context): String =
602+
if !sym.exists then ""
603+
else if sym.isAnonymousFunction then i" $prefix enclosing function"
604+
else i" $prefix $sym"
605+
602606
extension (tp: AnnotatedType)
603607
/** Is this a boxed capturing type? */
604608
def isBoxed(using Context): Boolean = tp.annot match

‎compiler/src/dotty/tools/dotc/cc/CaptureSet.scala

Lines changed: 38 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -263,7 +263,13 @@ sealed abstract class CaptureSet extends Showable:
263263
*/
264264
def mightAccountFor(x: Capability)(using Context): Boolean =
265265
reporting.trace(i"$this mightAccountFor $x, ${x.captureSetOfInfo}?", show = true):
266-
CCState.withCollapsedFresh: // OK here since we opportunistically choose an alternative which gets checked later
266+
CCState.withCollapsedFresh:
267+
// withCollapsedFresh should be dropped. The problem is that since our level checking
268+
// does not deal with classes well, we get false negatives here. Observed in the line
269+
//
270+
// stateFromIteratorConcatSuffix(it)(flatMapImpl(rest, f).state))))
271+
//
272+
// in cc-lib's LazyListIterable.scala.
267273
TypeComparer.noNotes:
268274
elems.exists(_.subsumes(x)(using ctx)(using VarState.ClosedUnrecorded))
269275
|| !x.isTerminalCapability
@@ -1276,28 +1282,37 @@ object CaptureSet:
12761282
res.myTrace = cs1 :: this.myTrace
12771283
res
12781284

1279-
def description(using Context): String = cs match
1280-
case cs: Var =>
1281-
if !cs.levelOK(elem) then
1282-
val levelStr = elem match
1283-
case ref: TermRef => i", defined in ${ref.symbol.maybeOwner}"
1284-
case _ => ""
1285-
i"""capability ${elem}$levelStr
1286-
|cannot be included in outer capture set $cs"""
1287-
else if !elem.tryClassifyAs(cs.classifier) then
1288-
i"""capability ${elem} is not classified as ${cs.classifier}, therefore it
1289-
|cannot be included in capture set $cs of ${cs.classifier} elements"""
1290-
else if cs.isBadRoot(elem) then
1291-
elem match
1292-
case elem: FreshCap =>
1293-
i"""local capability $elem created in ${elem.ccOwner}
1294-
|cannot be included in outer capture set $cs"""
1295-
case _ =>
1296-
i"universal capability $elem cannot be included in capture set $cs"
1297-
else
1298-
i"capability $elem cannot be included in capture set $cs"
1299-
case _ =>
1300-
i"capability $elem is not included in capture set $cs"
1285+
def description(using Context): String =
1286+
def why =
1287+
val reasons = cs.elems.toList.collect:
1288+
case c: FreshCap if !c.acceptsLevelOf(elem) =>
1289+
i"$elem${elem.levelOwner.qualString("in")} is not visible from $c${c.ccOwner.qualString("in")}"
1290+
case c: FreshCap if !elem.tryClassifyAs(c.hiddenSet.classifier) =>
1291+
i"$c is classified as ${c.hiddenSet.classifier} but $elem is not"
1292+
if reasons.isEmpty then ""
1293+
else reasons.mkString("\nbecause ", "\nand ", "")
1294+
cs match
1295+
case cs: Var =>
1296+
if !cs.levelOK(elem) then
1297+
val levelStr = elem match
1298+
case ref: TermRef => i", defined in ${ref.symbol.maybeOwner}"
1299+
case _ => ""
1300+
i"""capability ${elem}$levelStr
1301+
|cannot be included in outer capture set $cs"""
1302+
else if !elem.tryClassifyAs(cs.classifier) then
1303+
i"""capability ${elem} is not classified as ${cs.classifier}, therefore it
1304+
|cannot be included in capture set $cs of ${cs.classifier} elements"""
1305+
else if cs.isBadRoot(elem) then
1306+
elem match
1307+
case elem: FreshCap =>
1308+
i"""local capability $elem created in ${elem.ccOwner}
1309+
|cannot be included in outer capture set $cs"""
1310+
case _ =>
1311+
i"universal capability $elem cannot be included in capture set $cs"
1312+
else
1313+
i"capability $elem cannot be included in capture set $cs"
1314+
case _ =>
1315+
i"capability $elem is not included in capture set $cs$why"
13011316

13021317
override def toText(printer: Printer): Text =
13031318
inContext(printer.printerContext):

‎compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -67,9 +67,6 @@ object CheckCaptures:
6767
val res = cur
6868
cur = cur.outer
6969
res
70-
71-
def ownerString(using Context): String =
72-
if owner.isAnonymousFunction then "enclosing function" else owner.show
7370
end Env
7471

7572
/** Similar normal substParams, but this is an approximating type map that
@@ -494,7 +491,7 @@ class CheckCaptures extends Recheck, SymTransformer:
494491
CaptureSet.ofType(c1.widen, followResult = true)
495492
capt.println(i"Widen reach $c to $underlying in ${env.owner}")
496493
underlying.disallowRootCapability(NoSymbol): () =>
497-
report.error(em"Local capability $c in ${env.ownerString} cannot have `cap` as underlying capture set", tree.srcPos)
494+
report.error(em"Local capability $c${env.owner.qualString("in")} cannot have `cap` as underlying capture set", tree.srcPos)
498495
recur(underlying, env, lastEnv)
499496

500497
/** Avoid locally defined capability if it is a reach capability or capture set
@@ -548,9 +545,8 @@ class CheckCaptures extends Recheck, SymTransformer:
548545
case ref: NamedType if !ref.symbol.isUseParam =>
549546
val what = if ref.isType then "Capture set parameter" else "Local reach capability"
550547
val owner = ref.symbol.owner
551-
val ownerStr = if owner.isAnonymousFunction then "enclosing function" else owner.show
552548
report.error(
553-
em"""$what $c leaks into capture scope of $ownerStr.
549+
em"""$what $c leaks into capture scope${owner.qualString("of")}.
554550
|To allow this, the ${ref.symbol} should be declared with a @use annotation""", pos)
555551
case _ =>
556552

‎tests/neg-custom-args/captures/cc-existential-conformance.check

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,8 @@
99
| x is a value in method test
1010
| x² is a reference to a value parameter
1111
|
12-
| Note that capability <cap of (x: A): B^> is not included in capture set {cap}.
12+
| Note that capability <cap of (x: A): B^> is not included in capture set {cap}
13+
| because <cap of (x: A): B^> is not visible from cap in value y.
1314
|
1415
| longer explanation available when compiling with `-explain`
1516
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:9:29 --------------------
@@ -34,7 +35,8 @@
3435
| x is a value in method test2
3536
| x² is a reference to a value parameter
3637
|
37-
| Note that capability <cap of (x: A): B^> is not included in capture set {cap}.
38+
| Note that capability <cap of (x: A): B^> is not included in capture set {cap}
39+
| because <cap of (x: A): B^> is not visible from cap in value y.
3840
|
3941
| longer explanation available when compiling with `-explain`
4042
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:14:24 -------------------

‎tests/neg-custom-args/captures/class-level-attack.check

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@
1313
|
1414
| where: ^ refers to a fresh root capability in the type of value r
1515
|
16-
| Note that capability (x : IO^) is not included in capture set {cap}.
16+
| Note that capability (x : IO^) is not included in capture set {cap}
17+
| because (x : IO^) in method set is not visible from cap in value r.
1718
|
1819
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/i16226.check

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,8 @@
99
| =>³ refers to a fresh root capability in the result type of method mapc
1010
| ^ refers to a fresh root capability in the result type of method mapc
1111
|
12-
|Note that capability f1.type is not included in capture set {cap}.
12+
|Note that capability f1.type is not included in capture set {cap}
13+
|because f1.type is not visible from cap in method mapc.
1314
|
1415
| longer explanation available when compiling with `-explain`
1516
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i16226.scala:15:4 ----------------------------------------

‎tests/neg-custom-args/captures/i19330.check

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,8 @@
2020
| where: => refers to a fresh root capability in the type of value bad
2121
| ^ refers to a fresh root capability in the type of value bad
2222
|
23-
| Note that capability cap is not included in capture set {cap}.
23+
| Note that capability cap is not included in capture set {cap}
24+
| because cap in class Bar is not visible from cap in value bad.
2425
|
2526
| longer explanation available when compiling with `-explain`
2627
-- Error: tests/neg-custom-args/captures/i19330.scala:16:14 ------------------------------------------------------------

‎tests/neg-custom-args/captures/i21401.check

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,8 @@
2222
| ^ refers to the universal root capability
2323
| ^² refers to a fresh root capability created in value a when checking argument to parameter op of method usingIO
2424
|
25-
|Note that capability x.type is not included in capture set {cap}.
25+
|Note that capability x.type is not included in capture set {cap}
26+
|because x.type is not visible from cap in value a.
2627
|
2728
| longer explanation available when compiling with `-explain`
2829
-- Error: tests/neg-custom-args/captures/i21401.scala:16:66 ------------------------------------------------------------
@@ -55,6 +56,7 @@
5556
| where: ^ refers to the universal root capability
5657
| ^² refers to a fresh root capability created in value x²
5758
|
58-
| Note that capability x* is not included in capture set {cap}.
59+
| Note that capability x* is not included in capture set {cap}
60+
| because x* is not visible from cap in value x.
5961
|
6062
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/i23431.check

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,8 @@
77
| where: ^ refers to a fresh root capability in the type of parameter io
88
| ^² refers to a fresh root capability in the type of variable myIO
99
|
10-
| Note that capability cap is not included in capture set {cap}.
10+
| Note that capability cap is not included in capture set {cap}
11+
| because cap in method setIO is not visible from cap in variable myIO.
1112
|
1213
| longer explanation available when compiling with `-explain`
1314
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23431.scala:11:13 ---------------------------------------
@@ -19,7 +20,8 @@
1920
| where: ^ refers to a fresh root capability in the type of parameter io2
2021
| ^² refers to a fresh root capability in the type of variable myIO
2122
|
22-
| Note that capability cap is not included in capture set {cap}.
23+
| Note that capability cap is not included in capture set {cap}
24+
| because cap in enclosing function is not visible from cap in variable myIO.
2325
|
2426
| longer explanation available when compiling with `-explain`
2527
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23431.scala:12:12 ---------------------------------------
@@ -31,7 +33,8 @@
3133
|where: => refers to a fresh root capability created in anonymous function of type (io1: IO^): Unit when checking argument to parameter op of method withIO
3234
| ^ refers to the universal root capability
3335
|
34-
|Note that capability cap is not included in capture set {cap}.
36+
|Note that capability cap is not included in capture set {cap}
37+
|because cap in enclosing function is not visible from cap in variable myIO.
3538
13 | myIO = io3
3639
|
3740
| longer explanation available when compiling with `-explain`

0 commit comments

Comments
 (0)