Skip to content

Commit 7ca78b1

Browse files
oderskyodersky
committed
Drop ExistentialSubsumesFailure
Present the information as part of explaining an IncludeFailure instead.
1 parent e570650 commit 7ca78b1

File tree

5 files changed

+51
-69
lines changed

5 files changed

+51
-69
lines changed

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

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -786,12 +786,9 @@ object Capabilities:
786786
&& prefixAllowsAddHidden
787787
&& vs.addHidden(x.hiddenSet, y)
788788
case x: ResultCap =>
789-
val result = y match
789+
y match
790790
case y: ResultCap => vs.unify(x, y)
791791
case _ => y.derivesFromShared
792-
if !result then
793-
TypeComparer.addErrorNote(CaptureSet.ExistentialSubsumesFailure(x, y))
794-
result
795792
case GlobalCap =>
796793
y match
797794
case GlobalCap => true

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

Lines changed: 40 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -1300,20 +1300,6 @@ object CaptureSet:
13001300
/** A TypeMap that is the identity on capabilities */
13011301
trait IdentityCaptRefMap extends TypeMap
13021302

1303-
/** A value of this class is produced and added as a note to ccState
1304-
* when a subsumes check decides that an existential variable `ex` cannot be
1305-
* instantiated to the other capability `other`.
1306-
*/
1307-
case class ExistentialSubsumesFailure(val ex: ResultCap, val other: Capability) extends Note:
1308-
def render(using Context): String =
1309-
def reason =
1310-
if other.isTerminalCapability then ""
1311-
else " since that capability is not a `Sharable` capability"
1312-
i"""
1313-
|
1314-
|Note that the existential capture root in ${ex.originalBinder.resType}
1315-
|cannot subsume the capability $other$reason."""
1316-
13171303
/** Failure indicating that `elem` cannot be included in `cs` */
13181304
case class IncludeFailure(cs: CaptureSet, elem: Capability, levelError: Boolean = false) extends Note, Showable:
13191305
private var myTrace: List[CaptureSet] = cs :: Nil
@@ -1342,44 +1328,47 @@ object CaptureSet:
13421328
|
13431329
|"""
13441330

1345-
def render(using Context): String =
1346-
def why =
1347-
val reasons = cs.elems.toList.collect:
1348-
case c: FreshCap if !c.acceptsLevelOf(elem) =>
1349-
i"$elem${elem.levelOwner.qualString("in")} is not visible from $c${c.ccOwner.qualString("in")}"
1350-
case c: FreshCap if !elem.tryClassifyAs(c.hiddenSet.classifier) =>
1351-
i"$c is classified as ${c.hiddenSet.classifier} but $elem is not"
1352-
if reasons.isEmpty then ""
1353-
else reasons.mkString("\nbecause ", "\nand ", "")
1354-
cs match
1355-
case cs: Var =>
1356-
def ownerStr =
1357-
if !cs.description.isEmpty then "" else cs.owner.qualString("which is owned by")
1358-
if !cs.levelOK(elem) then
1359-
val outlivesStr = elem match
1360-
case ref: TermRef => i"${ref.symbol.maybeOwner.qualString("defined in")} outlives its scope:\n"
1361-
case _ => " outlives its scope: "
1362-
leading:
1363-
i"""Capability ${elem.showAsCapability}${outlivesStr}it leaks into outer capture set $cs$ownerStr"""
1364-
else if !elem.tryClassifyAs(cs.classifier) then
1365-
trailing:
1366-
i"""capability ${elem.showAsCapability} is not classified as ${cs.classifier}, therefore it
1367-
|cannot be included in capture set $cs of ${cs.classifier.name} elements"""
1368-
else if cs.isBadRoot(elem) then
1369-
elem match
1370-
case elem: FreshCap =>
1371-
leading:
1372-
i"""Local capability ${elem.showAsCapability} created in ${elem.ccOwner} outlives its scope:
1373-
|It leaks into outer capture set $cs$ownerStr"""
1374-
case _ =>
1375-
trailing:
1376-
i"universal capability ${elem.showAsCapability} cannot be included in capture set $cs"
1377-
else
1378-
trailing:
1379-
i"capability ${elem.showAsCapability} cannot be included in capture set $cs"
1380-
case _ =>
1331+
def render(using Context): String = cs match
1332+
case cs: Var =>
1333+
def ownerStr =
1334+
if !cs.description.isEmpty then "" else cs.owner.qualString("which is owned by")
1335+
if !cs.levelOK(elem) then
1336+
val outlivesStr = elem match
1337+
case ref: TermRef => i"${ref.symbol.maybeOwner.qualString("defined in")} outlives its scope:\n"
1338+
case _ => " outlives its scope: "
1339+
leading:
1340+
i"""Capability ${elem.showAsCapability}${outlivesStr}it leaks into outer capture set $cs$ownerStr"""
1341+
else if !elem.tryClassifyAs(cs.classifier) then
1342+
trailing:
1343+
i"""capability ${elem.showAsCapability} is not classified as ${cs.classifier}, therefore it
1344+
|cannot be included in capture set $cs of ${cs.classifier.name} elements"""
1345+
else if cs.isBadRoot(elem) then
1346+
elem match
1347+
case elem: FreshCap =>
1348+
leading:
1349+
i"""Local capability ${elem.showAsCapability} created in ${elem.ccOwner} outlives its scope:
1350+
|It leaks into outer capture set $cs$ownerStr"""
1351+
case _ =>
1352+
trailing:
1353+
i"universal capability ${elem.showAsCapability} cannot be included in capture set $cs"
1354+
else
13811355
trailing:
1382-
i"capability ${elem.showAsCapability} is not included in capture set $cs$why"
1356+
i"capability ${elem.showAsCapability} cannot be included in capture set $cs"
1357+
case _ =>
1358+
def why =
1359+
val reasons = cs.elems.toList.collect:
1360+
case c: FreshCap if !c.acceptsLevelOf(elem) =>
1361+
i"$elem${elem.levelOwner.qualString("in")} is not visible from $c${c.ccOwner.qualString("in")}"
1362+
case c: FreshCap if !elem.tryClassifyAs(c.hiddenSet.classifier) =>
1363+
i"$c is classified as ${c.hiddenSet.classifier} but ${elem.showAsCapability} is not"
1364+
case c: ResultCap if !c.subsumes(elem) =>
1365+
val toAdd = if elem.isTerminalCapability then "" else " since that capability is not a SharedCapability"
1366+
i"$c, which is existentially bound in ${c.originalBinder.resType}, cannot subsume ${elem.showAsCapability}$toAdd"
1367+
if reasons.isEmpty then ""
1368+
else reasons.mkString("\nbecause ", "\nand ", "")
1369+
1370+
trailing:
1371+
i"capability ${elem.showAsCapability} is not included in capture set $cs$why"
13831372

13841373
override def toText(printer: Printer): Text =
13851374
inContext(printer.printerContext):

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ import util.chaining.tap
2121
import transform.{Recheck, PreRecheck, CapturedVars}
2222
import Recheck.*
2323
import scala.collection.mutable
24-
import CaptureSet.{withCaptureSetsExplained, IncludeFailure, ExistentialSubsumesFailure, MutAdaptFailure}
24+
import CaptureSet.{withCaptureSetsExplained, IncludeFailure, MutAdaptFailure}
2525
import CCState.*
2626
import StdNames.nme
2727
import NameKinds.{DefaultGetterName, WildcardParamName, UniqueNameKind}

‎tests/neg-custom-args/captures/heal-tparam-cs.check‎

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -15,17 +15,15 @@
1515
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:15:13 -------------------------------
1616
15 | localCap { c => // error
1717
| ^
18-
| Found: (x$0: Capp^'s4) ->'s5 () ->{x$0} Unit
19-
| Required: (c: Capp^) -> () => Unit
18+
|Found: (x$0: Capp^'s4) ->'s5 () ->{x$0} Unit
19+
|Required: (c: Capp^) -> () => Unit
2020
|
21-
| Note that capability x$0 is not included in capture set {cap}.
21+
|Note that capability x$0 is not included in capture set {cap}
22+
|because cap, which is existentially bound in () =>² Unit, cannot subsume x$0 since that capability is not a SharedCapability.
2223
|
23-
| Note that the existential capture root in () =>² Unit
24-
| cannot subsume the capability (x$0 : Capp^'s4) since that capability is not a `Sharable` capability.
25-
|
26-
| where: => refers to a root capability associated with the result type of (c: Capp^): () => Unit
27-
| =>² and ^ refer to the universal root capability
28-
| cap is a root capability associated with the result type of (x$0: Capp^'s4): () ->{x$0} Unit
24+
|where: => refers to a root capability associated with the result type of (c: Capp^): () => Unit
25+
| =>² and ^ refer to the universal root capability
26+
| cap is a root capability associated with the result type of (x$0: Capp^'s4): () ->{x$0} Unit
2927
16 | (c1: Capp^) => () => { c1.use() }
3028
17 | }
3129
|

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

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -22,10 +22,8 @@
2222
| LazyRef[B^'s19]{val elem: () => B^'s20}^{f1, ref1}
2323
|Required: (ref: LazyRef[A]^{io}, f: A =>² B) =>³ LazyRef[B]^
2424
|
25-
|Note that capability f1 is not included in capture set {cap}.
26-
|
27-
|Note that the existential capture root in LazyRef[B]^²
28-
|cannot subsume the capability (f1 : A^'s15 ->'s16 B^'s17) since that capability is not a `Sharable` capability.
25+
|Note that capability f1 is not included in capture set {cap}
26+
|because cap, which is existentially bound in LazyRef[B]^², cannot subsume f1 since that capability is not a SharedCapability.
2927
|
3028
|where: => and cap refer to a root capability associated with the result type of (ref1: LazyRef[A^'s11]{val elem: () ->'s12 A^'s13}^'s14, f1: A^'s15 ->'s16 B^'s17):
3129
| LazyRef[B^'s19]{val elem: () => B^'s20}^{f1, ref1}

0 commit comments

Comments
 (0)