From 58cbdbc83cda1ad93337ea7cd7ce7076fad2658e Mon Sep 17 00:00:00 2001 From: odersky Date: Wed, 21 May 2025 18:05:51 +0200 Subject: [PATCH 1/6] Refactor some descriptions to be more reusable --- .../src/dotty/tools/dotc/cc/Capability.scala | 13 ++++++++ .../src/dotty/tools/dotc/core/SymUtils.scala | 10 ++++++ .../dotty/tools/dotc/reporting/Message.scala | 32 ++++--------------- .../neg-custom-args/sep-tvar-follow.scala | 10 ++++++ 4 files changed, 40 insertions(+), 25 deletions(-) create mode 100644 tests/pending/neg-custom-args/sep-tvar-follow.scala diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index 3a2d122c8e68..808c98149c0c 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -58,6 +58,7 @@ object Capabilities: trait RootCapability extends Capability: val rootId = nextRootId nextRootId += 1 + def descr(using Context): String /** The base trait of all capabilties represented as types */ trait CoreCapability extends TypeProxy, Capability: @@ -120,6 +121,7 @@ object Capabilities: */ @sharable // We override below all operations that access internal capability state object GlobalCap extends RootCapability: + def descr(using Context) = "the universal root capability" override val maybe = Maybe(this) override val readOnly = ReadOnly(this) override def reach = unsupported("cap.reach") @@ -143,6 +145,14 @@ object Capabilities: case that: FreshCap => this eq that case _ => false + def descr(using Context) = + val originStr = origin match + case Origin.InDecl(sym) if sym.exists => + origin.explanation + case _ => + i" created in ${hiddenSet.owner.sanitizedDescription}${origin.explanation}" + i"a fresh root capability$originStr" + object FreshCap: def apply(origin: Origin)(using Context): FreshCap | GlobalCap.type = if ccConfig.useSepChecks then FreshCap(ctx.owner, origin) @@ -225,6 +235,9 @@ object Capabilities: rcap.myOrigin = primary primary.variants += rcap rcap + + def descr(using Context) = + i"a root capability associated with the result type of $binder" end ResultCap /** A trait for references in CaptureSets. These can be NamedTypes, ThisTypes or ParamRefs, diff --git a/compiler/src/dotty/tools/dotc/core/SymUtils.scala b/compiler/src/dotty/tools/dotc/core/SymUtils.scala index 1b83014e5735..209f12fa8b87 100644 --- a/compiler/src/dotty/tools/dotc/core/SymUtils.scala +++ b/compiler/src/dotty/tools/dotc/core/SymUtils.scala @@ -118,6 +118,16 @@ class SymUtils: def isGenericProduct(using Context): Boolean = whyNotGenericProduct.isEmpty + def sanitizedDescription(using Context): String = + if self.isConstructor then + i"constructor of ${self.owner.sanitizedDescription}" + else if self.isAnonymousFunction then + i"anonymous function of type ${self.info}" + else if self.name.toString.contains('$') then + self.owner.sanitizedDescription + else + self.show + /** Is this an old style implicit conversion? * @param directOnly only consider explicitly written methods * @param forImplicitClassOnly only consider methods generated from implicit classes diff --git a/compiler/src/dotty/tools/dotc/reporting/Message.scala b/compiler/src/dotty/tools/dotc/reporting/Message.scala index 25d0c479b8a8..1e313ca749d3 100644 --- a/compiler/src/dotty/tools/dotc/reporting/Message.scala +++ b/compiler/src/dotty/tools/dotc/reporting/Message.scala @@ -53,7 +53,7 @@ object Message: case None => false end Disambiguation - private type Recorded = Symbol | ParamRef | SkolemType | Capability + private type Recorded = Symbol | ParamRef | SkolemType | RootCapability private case class SeenKey(str: String, isType: Boolean) @@ -183,31 +183,11 @@ object Message: s"is a ${ctx.printer.kindString(sym)}${sym.showExtendedLocation}${addendum("bounds", info)}" case tp: SkolemType => s"is an unknown value of type ${tp.widen.show}" - case ref: Capability => + case ref: RootCapability => val relation = if List("^", "=>", "?=>").exists(key.startsWith) then "refers to" else "is" - def ownerStr(owner: Symbol): String = - if owner.isConstructor then - i"constructor of ${ownerStr(owner.owner)}" - else if owner.isAnonymousFunction then - i"anonymous function of type ${owner.info}" - else if owner.name.toString.contains('$') then - ownerStr(owner.owner) - else - owner.show - val descr = - ref match - case GlobalCap => "the universal root capability" - case ref: FreshCap => - val descr = ref.origin match - case origin @ Origin.InDecl(sym) if sym.exists => - origin.explanation - case origin => - i" created in ${ownerStr(ref.hiddenSet.owner)}${origin.explanation}" - i"a fresh root capability$descr" - case ResultCap(binder) => i"a root capability associated with the result type of $binder" - s"$relation $descr" + s"$relation ${ref.descr}" end explanation /** Produce a where clause with explanations for recorded iterms. @@ -274,14 +254,16 @@ object Message: override def toTextCapturing(parent: Type, refs: GeneralCaptureSet, boxText: Text) = refs match case refs: CaptureSet if isUniversalCaptureSet(refs) && !defn.isFunctionType(parent) && !printDebug && seen.isActive => - boxText ~ toTextLocal(parent) ~ seen.record("^", isType = true, refs.elems.nth(0)) + boxText + ~ toTextLocal(parent) + ~ seen.record("^", isType = true, refs.elems.nth(0).asInstanceOf[RootCapability]) case _ => super.toTextCapturing(parent, refs, boxText) override def funMiddleText(isContextual: Boolean, isPure: Boolean, refs: GeneralCaptureSet | Null): Text = refs match case refs: CaptureSet if isUniversalCaptureSet(refs) && seen.isActive => - seen.record(arrow(isContextual, isPure = false), isType = true, refs.elems.nth(0)) + seen.record(arrow(isContextual, isPure = false), isType = true, refs.elems.nth(0).asInstanceOf[RootCapability]) case _ => super.funMiddleText(isContextual, isPure, refs) diff --git a/tests/pending/neg-custom-args/sep-tvar-follow.scala b/tests/pending/neg-custom-args/sep-tvar-follow.scala new file mode 100644 index 000000000000..09ee3a17a054 --- /dev/null +++ b/tests/pending/neg-custom-args/sep-tvar-follow.scala @@ -0,0 +1,10 @@ +import language.experimental.captureChecking +trait Ref +def swap(x1: Ref^, x2: Ref^): Unit = () +def foo(a: Ref^)[X](op: (z: Ref^) -> X^{z}): X^{a} = op(a) +def test1(a: Ref^): Unit = + def bad(x: Ref^)(y: Ref^{a}): Unit = swap(x, y) + val t1 = bad + def t2[X] = foo(a)[X] + val t3 = t2[(y: Ref^{a}) -> Unit](t1) + t3(a) // boom From 97e5316b1618f7f4f98dd16d108b3ab78e3c5e29 Mon Sep 17 00:00:00 2001 From: odersky Date: Fri, 23 May 2025 11:15:03 +0200 Subject: [PATCH 2/6] Implement and use central error notes logic in TypeComparer Needs some adaption for subCaptures tests for now. --- .../src/dotty/tools/dotc/cc/CCState.scala | 20 +----- .../src/dotty/tools/dotc/cc/Capability.scala | 2 +- .../src/dotty/tools/dotc/cc/CaptureOps.scala | 3 - .../src/dotty/tools/dotc/cc/CaptureSet.scala | 16 ++--- .../dotty/tools/dotc/cc/CheckCaptures.scala | 42 ++++++----- .../dotty/tools/dotc/core/TypeComparer.scala | 72 +++++++++++++++++-- .../src/dotty/tools/dotc/typer/Typer.scala | 2 +- .../captures/capt-depfun.check | 4 ++ 8 files changed, 105 insertions(+), 56 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CCState.scala b/compiler/src/dotty/tools/dotc/cc/CCState.scala index 5e0ba4627da3..bdc93c95ad37 100644 --- a/compiler/src/dotty/tools/dotc/cc/CCState.scala +++ b/compiler/src/dotty/tools/dotc/cc/CCState.scala @@ -3,7 +3,7 @@ package dotc package cc import core.* -import CaptureSet.{CompareResult, CompareFailure, VarState} +import CaptureSet.{CompareResult, VarState} import collection.mutable import reporting.Message import Contexts.Context @@ -16,24 +16,6 @@ class CCState: // ------ Error diagnostics ----------------------------- - /** Error reprting notes produces since the last call to `test` */ - var notes: List[ErrorNote] = Nil - - def addNote(note: ErrorNote): Unit = - if !notes.exists(_.getClass == note.getClass) then - notes = note :: notes - - def test(op: => CompareResult): CompareResult = - val saved = notes - notes = Nil - try op match - case res: CompareFailure => res.withNotes(notes) - case res => res - finally notes = saved - - def testOK(op: => Boolean): CompareResult = - test(if op then CompareResult.OK else CompareResult.Fail(Nil)) - /** Warnings relating to upper approximations of capture sets with * existentially bound variables. */ diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index 808c98149c0c..60a1704ff45d 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -558,7 +558,7 @@ object Capabilities: case y: ResultCap => vs.unify(x, y) case _ => y.derivesFromSharedCapability if !result then - ccState.addNote(CaptureSet.ExistentialSubsumesFailure(x, y)) + TypeComparer.addErrorNote(CaptureSet.ExistentialSubsumesFailure(x, y)) result case GlobalCap => y match diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index de54dea83d75..8795c7a9318e 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -41,9 +41,6 @@ def depFun(args: List[Type], resultType: Type, isContextual: Boolean, paramNames /** An exception thrown if a @retains argument is not syntactically a Capability */ class IllegalCaptureRef(tpe: Type)(using Context) extends Exception(tpe.show) -/** A base trait for data producing addenda to error messages */ -trait ErrorNote - /** The currently valid CCState */ def ccState(using Context): CCState = Phases.checkCapturesPhase.asInstanceOf[CheckCaptures].ccState1 diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index eb97d7e1cc6f..4aa11f629b3f 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -16,6 +16,7 @@ import util.{SimpleIdentitySet, Property} import typer.ErrorReporting.Addenda import util.common.alwaysTrue import scala.collection.{mutable, immutable} +import TypeComparer.ErrorNote import CCState.* import TypeOps.AvoidMap import compiletime.uninitialized @@ -242,7 +243,7 @@ sealed abstract class CaptureSet extends Showable: if result.isOK then addDependent(that) else - result.levelError.foreach(ccState.addNote) + result.levelError.foreach(TypeComparer.addErrorNote) varState.rollBack() result //.showing(i"subcaptures $this <:< $that = ${result.show}", capt) @@ -960,6 +961,8 @@ object CaptureSet: //assert(id != 4) + description = i"elements subsumed by $owningCap" + private def aliasRef: FreshCap | Null = if myElems.size == 1 then myElems.nth(0) match @@ -1075,17 +1078,10 @@ object CaptureSet: */ case class ExistentialSubsumesFailure(val ex: ResultCap, val other: Capability) extends ErrorNote - trait CompareFailure: - private var myErrorNotes: List[ErrorNote] = Nil - def errorNotes: List[ErrorNote] = myErrorNotes - def withNotes(notes: List[ErrorNote]): this.type = - myErrorNotes = notes - this - enum CompareResult extends Showable: case OK - case Fail(trace: List[CaptureSet]) extends CompareResult, CompareFailure - case LevelError(cs: CaptureSet, elem: Capability) extends CompareResult, CompareFailure, ErrorNote + case Fail(trace: List[CaptureSet]) extends CompareResult, ErrorNote + case LevelError(cs: CaptureSet, elem: Capability) extends CompareResult, ErrorNote override def toText(printer: Printer): Text = inContext(printer.printerContext): diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index c7e31b7dd6b8..3f299fbe68c1 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -18,7 +18,7 @@ import util.{SimpleIdentitySet, EqHashMap, EqHashSet, SrcPos, Property} import transform.{Recheck, PreRecheck, CapturedVars} import Recheck.* import scala.collection.mutable -import CaptureSet.{withCaptureSetsExplained, CompareResult, CompareFailure, ExistentialSubsumesFailure} +import CaptureSet.{withCaptureSetsExplained, CompareResult, ExistentialSubsumesFailure} import CCState.* import StdNames.nme import NameKinds.{DefaultGetterName, WildcardParamName, UniqueNameKind} @@ -352,11 +352,12 @@ class CheckCaptures extends Recheck, SymTransformer: assert(cs1.subCaptures(cs2).isOK, i"$cs1 is not a subset of $cs2") /** If `res` is not CompareResult.OK, report an error */ - def checkOK(res: CompareResult, prefix: => String, added: Capability | CaptureSet, target: CaptureSet, pos: SrcPos, provenance: => String = "")(using Context): Unit = + def checkOK(res: TypeComparer.CompareResult, prefix: => String, added: Capability | CaptureSet, target: CaptureSet, pos: SrcPos, provenance: => String = "")(using Context): Unit = res match - case res: CompareFailure => + case TypeComparer.CompareResult.Fail(notes) => + val ((res: CompareResult) :: Nil, otherNotes) = notes.partition(_.isInstanceOf[CompareResult]): @unchecked def msg(provisional: Boolean) = - def toAdd: String = errorNotes(res.errorNotes).toAdd.mkString + def toAdd: String = errorNotes(otherNotes).toAdd.mkString def descr: String = val d = res.blocking.description if d.isEmpty then provenance else "" @@ -377,10 +378,19 @@ class CheckCaptures extends Recheck, SymTransformer: report.error(msg(provisional = false), pos) case _ => + def convertResult(op: => CompareResult)(using Context): TypeComparer.CompareResult = + TypeComparer.test: + op match + case res: TypeComparer.ErrorNote => + TypeComparer.addErrorNote(res) + false + case CompareResult.OK => + true + /** Check subcapturing `{elem} <: cs`, report error on failure */ def checkElem(elem: Capability, cs: CaptureSet, pos: SrcPos, provenance: => String = "")(using Context) = checkOK( - ccState.test(elem.singletonCaptureSet.subCaptures(cs)), + convertResult(elem.singletonCaptureSet.subCaptures(cs)), i"$elem cannot be referenced here; it is not", elem, cs, pos, provenance) @@ -388,7 +398,7 @@ class CheckCaptures extends Recheck, SymTransformer: def checkSubset(cs1: CaptureSet, cs2: CaptureSet, pos: SrcPos, provenance: => String = "", cs1description: String = "")(using Context) = checkOK( - ccState.test(cs1.subCaptures(cs2)), + convertResult(cs1.subCaptures(cs2)), if cs1.elems.size == 1 then i"reference ${cs1.elems.nth(0)}$cs1description is not" else i"references $cs1$cs1description are not all", cs1, cs2, pos, provenance) @@ -1272,7 +1282,7 @@ class CheckCaptures extends Recheck, SymTransformer: type BoxErrors = mutable.ListBuffer[Message] | Null - private def errorNotes(notes: List[ErrorNote])(using Context): Addenda = + private def errorNotes(notes: List[TypeComparer.ErrorNote])(using Context): Addenda = if notes.isEmpty then NothingToAdd else new Addenda: override def toAdd(using Context) = notes.map: note => @@ -1336,20 +1346,20 @@ class CheckCaptures extends Recheck, SymTransformer: if actualBoxed eq actual then // Only `addOuterRefs` when there is no box adaptation expected1 = addOuterRefs(expected1, actual, tree.srcPos) - ccState.testOK(isCompatible(actualBoxed, expected1)) match - case CompareResult.OK => - if debugSuccesses then tree match - case Ident(_) => - println(i"SUCCESS $tree for $actual <:< $expected:\n${TypeComparer.explained(_.isSubType(actualBoxed, expected1))}") - case _ => - actualBoxed - case fail: CompareFailure => + TypeComparer.test(isCompatible(actualBoxed, expected1)) match + case TypeComparer.CompareResult.Fail(notes) => capt.println(i"conforms failed for ${tree}: $actual vs $expected") err.typeMismatch(tree.withType(actualBoxed), expected1, addApproxAddenda( - addenda ++ errorNotes(fail.errorNotes), + addenda ++ errorNotes(notes), expected1)) actual + case /*OK*/ _ => + if debugSuccesses then tree match + case Ident(_) => + println(i"SUCCESS $tree for $actual <:< $expected:\n${TypeComparer.explained(_.isSubType(actualBoxed, expected1))}") + case _ => + actualBoxed end checkConformsExpr /** Turn `expected` into a dependent function when `actual` is dependent. */ diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 5ecb0ee01ec0..10db6d9cf133 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -50,12 +50,17 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling opaquesUsed = false recCount = 0 needsGc = false + maxErrorLevel = -1 + errorNotes = Nil if Config.checkTypeComparerReset then checkReset() private var pendingSubTypes: util.MutableSet[(Type, Type)] | Null = null private var recCount = 0 private var monitored = false + private var maxErrorLevel: Int = -1 + private var errorNotes: List[(Int, ErrorNote)] = Nil + private var needsGc = false private var canCompareAtoms: Boolean = true // used for internal consistency checking @@ -148,7 +153,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling def testSubType(tp1: Type, tp2: Type): CompareResult = GADTused = false opaquesUsed = false - if !topLevelSubType(tp1, tp2) then CompareResult.Fail + if !topLevelSubType(tp1, tp2) then CompareResult.Fail(Nil) else if GADTused then CompareResult.OKwithGADTUsed else if opaquesUsed then CompareResult.OKwithOpaquesUsed // we cast on GADTused, so handles if both are used else CompareResult.OK @@ -1584,10 +1589,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling ctx.gadtState.restore(savedGadt) val savedSuccessCount = successCount try - recCount += 1 - if recCount >= Config.LogPendingSubTypesThreshold then monitored = true - val result = if monitored then monitoredIsSubType else firstTry - recCount -= 1 + val result = inNestedLevel: + if recCount >= Config.LogPendingSubTypesThreshold then monitored = true + if monitored then monitoredIsSubType else firstTry if !result then restore() else if recCount == 0 && needsGc then state.gc() @@ -1602,6 +1606,32 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling throw ex } + /** Run `op` in a recursion level (indicated by `recCount`) increased by one. + * This affects when monitoring starts and how error notes are propagated. + * On exit, error notes added at the current level are either + * - promoted to the next outer level (in case of failure), + * - cancelled (in case of success). + */ + inline def inNestedLevel(inline op: Boolean): Boolean = + recCount += 1 + val result = op + recCount -= 1 + if maxErrorLevel > recCount then + if result then + maxErrorLevel = -1 + errorNotes = errorNotes.filterConserve: p => + val (level, note) = p + if level <= recCount then + if level > maxErrorLevel then maxErrorLevel = level + true + else false + else + errorNotes = errorNotes.mapConserve: p => + val (level, note) = p + if level > recCount then (recCount, note) else p + maxErrorLevel = recCount + result + private def nonExprBaseType(tp: Type, cls: Symbol)(using Context): Type = if tp.isInstanceOf[ExprType] then NoType else tp.baseType(cls) @@ -3219,12 +3249,26 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling def reduceMatchWith[T](op: MatchReducer => T)(using Context): T = inSubComparer(matchReducer)(op) + + /** Add given ErrorNote note, provided there is not yet an error note with + * the same class as `note`. + */ + def addErrorNote(note: ErrorNote): Unit = + if errorNotes.forall(_._2.getClass != note.getClass) then + errorNotes = (recCount, note) :: errorNotes + assert(maxErrorLevel <= recCount) + maxErrorLevel = recCount } object TypeComparer { + /** A base trait for data producing addenda to error messages */ + trait ErrorNote + + /** A richer compare result, returned by `testSubType` and `test`. */ enum CompareResult: - case OK, Fail, OKwithGADTUsed, OKwithOpaquesUsed + case OK, OKwithGADTUsed, OKwithOpaquesUsed + case Fail(errorNotes: List[ErrorNote]) /** Class for unification variables used in `natValue`. */ private class AnyConstantType extends UncachedGroundType with ValueType { @@ -3393,6 +3437,22 @@ object TypeComparer { def subCaptures(refs1: CaptureSet, refs2: CaptureSet, vs: CaptureSet.VarState)(using Context): CaptureSet.CompareResult = comparing(_.subCaptures(refs1, refs2, vs)) + + def inNestedLevel(op: => Boolean)(using Context): Boolean = + comparer.inNestedLevel(op) + + def addErrorNote(note: ErrorNote)(using Context): Unit = + comparer.addErrorNote(note) + + /** Run `op` on current type comparer, maping its Boolean result to + * a CompareResult with possible outcomes OK and Fail(...)`. In case + * of failure pass the accumulated errorNotes of this type comparer to + * in the Fail value. + */ + def test(op: => Boolean)(using Context): CompareResult = + comparing: comparer => + if op then CompareResult.OK + else CompareResult.Fail(comparer.errorNotes.map(_._2)) } object MatchReducer: diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala index 3f24f3f8f62b..dd04d6f9478a 100644 --- a/compiler/src/dotty/tools/dotc/typer/Typer.scala +++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala @@ -4581,7 +4581,7 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer tree } else TypeComparer.testSubType(tree.tpe.widenExpr, pt) match - case CompareResult.Fail => + case CompareResult.Fail(_) => wtp match case wtp: MethodType => missingArgs(wtp) case _ => diff --git a/tests/neg-custom-args/captures/capt-depfun.check b/tests/neg-custom-args/captures/capt-depfun.check index a5db4da7a319..28341e0be9cd 100644 --- a/tests/neg-custom-args/captures/capt-depfun.check +++ b/tests/neg-custom-args/captures/capt-depfun.check @@ -6,6 +6,10 @@ | | where: => refers to a fresh root capability in the type of value dc | + | + | Note that the existential capture root in Str^{x} => Str^{x} + | cannot subsume the capability Str^{x}> + | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/capt-depfun.scala:11:24 ------------------------------------------------------- 11 | val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error // error: separatioon From ce78e87ed8903304044babed7941aaef57dea7ac Mon Sep 17 00:00:00 2001 From: odersky Date: Sat, 24 May 2025 14:06:01 +0200 Subject: [PATCH 3/6] Drop CaptureSet.CompareResult Handle everything using error notes --- .../src/dotty/tools/dotc/cc/CCState.scala | 2 +- .../src/dotty/tools/dotc/cc/CaptureOps.scala | 2 +- .../src/dotty/tools/dotc/cc/CaptureSet.scala | 208 ++++++++---------- .../dotty/tools/dotc/cc/CheckCaptures.scala | 31 +-- .../dotty/tools/dotc/core/TypeComparer.scala | 84 ++++--- .../src/dotty/tools/dotc/core/TypeOps.scala | 4 +- .../src/dotty/tools/dotc/core/Types.scala | 2 +- .../captures/capt-depfun.check | 4 - 8 files changed, 165 insertions(+), 172 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CCState.scala b/compiler/src/dotty/tools/dotc/cc/CCState.scala index bdc93c95ad37..5feae257b97e 100644 --- a/compiler/src/dotty/tools/dotc/cc/CCState.scala +++ b/compiler/src/dotty/tools/dotc/cc/CCState.scala @@ -3,7 +3,7 @@ package dotc package cc import core.* -import CaptureSet.{CompareResult, VarState} +import CaptureSet.VarState import collection.mutable import reporting.Message import Contexts.Context diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index 8795c7a9318e..6f86dd20ab44 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -154,7 +154,7 @@ extension (tp: Type) * the two capture sets are combined. */ def capturing(cs: CaptureSet)(using Context): Type = - if (cs.isAlwaysEmpty || cs.isConst && cs.subCaptures(tp.captureSet, VarState.Separate).isOK) + if (cs.isAlwaysEmpty || cs.isConst && cs.subCaptures(tp.captureSet, VarState.Separate)) && !cs.keepAlways then tp else tp match diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index 4aa11f629b3f..fb8d17d2a087 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -114,6 +114,10 @@ sealed abstract class CaptureSet extends Showable: final def keepAlways: Boolean = this.isInstanceOf[EmptyWithProvenance] + def failWith(fail: TypeComparer.ErrorNote)(using Context): false = + TypeComparer.addErrorNote(fail) + false + /** Try to include an element in this capture set. * @param elem The element to be added * @param origin The set that originated the request, or `empty` if the request came from outside. @@ -133,14 +137,17 @@ sealed abstract class CaptureSet extends Showable: * element is not the root capability, try instead to include its underlying * capture set. */ - protected def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): CompareResult = reporting.trace(i"try include $elem in $this # ${maybeId}"): - if accountsFor(elem) then CompareResult.OK - else addNewElem(elem) + protected def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): Boolean = reporting.trace(i"try include $elem in $this # ${maybeId}"): + accountsFor(elem) || addNewElem(elem) /** Try to include all element in `refs` to this capture set. */ - protected final def tryInclude(newElems: Refs, origin: CaptureSet)(using Context, VarState): CompareResult = - (CompareResult.OK /: newElems): (r, elem) => - r.andAlso(tryInclude(elem, origin)) + protected final def tryInclude(newElems: Refs, origin: CaptureSet)(using Context, VarState): Boolean = + TypeComparer.inNestedLevel: + // Run in nested level so that a error notes for a failure here can be + // cancelled in case the whole comparison succeeds. + // We do this here because all nested tryInclude and subCaptures calls go + // through this method. + newElems.forall(tryInclude(_, origin)) /** Add an element to this capture set, assuming it is not already accounted for, * and omitting any mapping or filtering. @@ -149,34 +156,29 @@ sealed abstract class CaptureSet extends Showable: * element is not the root capability, try instead to include its underlying * capture set. */ - protected final def addNewElem(elem: Capability)(using ctx: Context, vs: VarState): CompareResult = - if elem.isTerminalCapability || !vs.isOpen then - addThisElem(elem) - else - addThisElem(elem).orElse: - val underlying = elem.captureSetOfInfo - tryInclude(underlying.elems, this).andAlso: - underlying.addDependent(this) - CompareResult.OK - - /** Add new elements one by one using `addNewElem`, abort on first failure */ - protected final def addNewElems(newElems: Refs)(using Context, VarState): CompareResult = - (CompareResult.OK /: newElems): (r, elem) => - r.andAlso(addNewElem(elem)) + protected final def addNewElem(elem: Capability)(using ctx: Context, vs: VarState): Boolean = + addThisElem(elem) + || !elem.isTerminalCapability + && vs.isOpen + && { + val underlying = elem.captureSetOfInfo + val res = tryInclude(underlying.elems, this) + if res then underlying.addDependent(this) + res + } /** Add a specific element, assuming it is not already accounted for, * and omitting any mapping or filtering, without possibility to backtrack * to the underlying capture set. */ - protected def addThisElem(elem: Capability)(using Context, VarState): CompareResult + protected def addThisElem(elem: Capability)(using Context, VarState): Boolean - protected def addIfHiddenOrFail(elem: Capability)(using ctx: Context, vs: VarState): CompareResult = - if elems.exists(_.maxSubsumes(elem, canAddHidden = true)) - then CompareResult.OK - else CompareResult.Fail(this :: Nil) + protected def addIfHiddenOrFail(elem: Capability)(using ctx: Context, vs: VarState): Boolean = + elems.exists(_.maxSubsumes(elem, canAddHidden = true)) + || failWith(IncludeFailure(this :: Nil)) /** If this is a variable, add `cs` as a dependent set */ - protected def addDependent(cs: CaptureSet)(using Context, VarState): CompareResult + protected def addDependent(cs: CaptureSet)(using Context, VarState): Boolean /** If `cs` is a variable, add this capture set as one of its dependent sets */ protected def addAsDependentTo(cs: CaptureSet)(using Context): this.type = @@ -193,14 +195,15 @@ sealed abstract class CaptureSet extends Showable: i"$this accountsFor $x$suffix" def test(using Context) = reporting.trace(debugInfo): - elems.exists(_.subsumes(x)) - || // Even though subsumes already follows captureSetOfInfo, this is not enough. - // For instance x: C^{y, z}. Then neither y nor z subsumes x but {y, z} accounts for x. - !x.isTerminalCapability - && !x.coreType.derivesFrom(defn.Caps_CapSet) - && !(vs.isSeparating && x.captureSetOfInfo.containsTerminalCapability) - // in VarState.Separate, don't try to widen to cap since that might succeed with {cap} <: {cap} - && x.captureSetOfInfo.subCaptures(this, VarState.Separate).isOK + TypeComparer.noNotes: // Any failures in accountsFor should not lead to error notes + elems.exists(_.subsumes(x)) + || // Even though subsumes already follows captureSetOfInfo, this is not enough. + // For instance x: C^{y, z}. Then neither y nor z subsumes x but {y, z} accounts for x. + !x.isTerminalCapability + && !x.coreType.derivesFrom(defn.Caps_CapSet) + && !(vs.isSeparating && x.captureSetOfInfo.containsTerminalCapability) + // in VarState.Separate, don't try to widen to cap since that might succeed with {cap} <: {cap} + && x.captureSetOfInfo.subCaptures(this, VarState.Separate) comparer match case comparer: ExplainingTypeComparer => comparer.traceIndented(debugInfo)(test) @@ -217,7 +220,8 @@ sealed abstract class CaptureSet extends Showable: def mightAccountFor(x: Capability)(using Context): Boolean = reporting.trace(i"$this mightAccountFor $x, ${x.captureSetOfInfo}?", show = true): CCState.withCollapsedFresh: // OK here since we opportunistically choose an alternative which gets checked later - elems.exists(_.subsumes(x)(using ctx)(using VarState.ClosedUnrecorded)) + TypeComparer.noNotes: + elems.exists(_.subsumes(x)(using ctx)(using VarState.ClosedUnrecorded)) || !x.isTerminalCapability && { val elems = x.captureSetOfInfo.elems @@ -234,34 +238,31 @@ sealed abstract class CaptureSet extends Showable: && !that.elems.forall(this.mightAccountFor) /** The subcapturing test, taking an explicit VarState. */ - final def subCaptures(that: CaptureSet, vs: VarState)(using Context): CompareResult = + final def subCaptures(that: CaptureSet, vs: VarState)(using Context): Boolean = subCaptures(that)(using ctx, vs) /** The subcapturing test, using a given VarState */ - final def subCaptures(that: CaptureSet)(using ctx: Context, vs: VarState = VarState()): CompareResult = - val result = that.tryInclude(elems, this) - if result.isOK then + final def subCaptures(that: CaptureSet)(using ctx: Context, vs: VarState = VarState()): Boolean = + if that.tryInclude(elems, this) then addDependent(that) else - result.levelError.foreach(TypeComparer.addErrorNote) varState.rollBack() - result - //.showing(i"subcaptures $this <:< $that = ${result.show}", capt) + false /** Two capture sets are considered =:= equal if they mutually subcapture each other * in a frozen state. */ def =:= (that: CaptureSet)(using Context): Boolean = - this.subCaptures(that, VarState.Separate).isOK - && that.subCaptures(this, VarState.Separate).isOK + this.subCaptures(that, VarState.Separate) + && that.subCaptures(this, VarState.Separate) /** The smallest capture set (via <:<) that is a superset of both * `this` and `that` */ def ++ (that: CaptureSet)(using Context): CaptureSet = - if this.subCaptures(that, VarState.HardSeparate).isOK then + if this.subCaptures(that, VarState.HardSeparate) then if that.isAlwaysEmpty && this.keepAlways then this else that - else if that.subCaptures(this, VarState.HardSeparate).isOK then this + else if that.subCaptures(this, VarState.HardSeparate) then this else if this.isConst && that.isConst then Const(this.elems ++ that.elems) else Union(this, that) @@ -276,8 +277,8 @@ sealed abstract class CaptureSet extends Showable: /** The largest capture set (via <:<) that is a subset of both `this` and `that` */ def **(that: CaptureSet)(using Context): CaptureSet = - if this.subCaptures(that, VarState.Closed()).isOK then this - else if that.subCaptures(this, VarState.Closed()).isOK then that + if this.subCaptures(that, VarState.Closed()) then this + else if that.subCaptures(this, VarState.Closed()) then that else if this.isConst && that.isConst then Const(elemIntersection(this, that)) else Intersection(this, that) @@ -472,13 +473,15 @@ object CaptureSet: def isAlwaysEmpty(using Context) = elems.isEmpty def isProvisionallySolved(using Context) = false - def addThisElem(elem: Capability)(using Context, VarState): CompareResult = - val res = addIfHiddenOrFail(elem) - if !res.isOK && this.isProvisionallySolved then - println(i"Cannot add $elem to provisionally solved $this") - res + def addThisElem(elem: Capability)(using Context, VarState): Boolean = + addIfHiddenOrFail(elem) + || { + if this.isProvisionallySolved then + capt.println(i"Cannot add $elem to provisionally solved $this") + false + } - def addDependent(cs: CaptureSet)(using Context, VarState) = CompareResult.OK + def addDependent(cs: CaptureSet)(using Context, VarState) = true def upperApprox(origin: CaptureSet)(using Context): CaptureSet = this @@ -505,7 +508,7 @@ object CaptureSet: */ object Fluid extends Const(emptyRefs): override def isAlwaysEmpty(using Context) = false - override def addThisElem(elem: Capability)(using Context, VarState) = CompareResult.OK + override def addThisElem(elem: Capability)(using Context, VarState) = true override def accountsFor(x: Capability)(using Context)(using VarState): Boolean = true override def mightAccountFor(x: Capability)(using Context): Boolean = true override def toString = "" @@ -597,11 +600,11 @@ object CaptureSet: assert(elem.subsumes(elem1), i"Skipped map ${tm.getClass} maps newly added $elem to $elem1 in $this") - final def addThisElem(elem: Capability)(using Context, VarState): CompareResult = + final def addThisElem(elem: Capability)(using Context, VarState): Boolean = if isConst || !recordElemsState() then // Fail if variable is solved or given VarState is frozen addIfHiddenOrFail(elem) else if !levelOK(elem) then - CompareResult.LevelError(this, elem) // or `elem` is not visible at the level of the set. + failWith(LevelError(this, elem)) // or `elem` is not visible at the level of the set. else // id == 108 then assert(false, i"trying to add $elem to $this") assert(elem.isWellformed, elem) @@ -612,14 +615,15 @@ object CaptureSet: newElemAddedHandler(elem) val normElem = if isMaybeSet then elem else elem.stripMaybe // assert(id != 5 || elems.size != 3, this) - val res = (CompareResult.OK /: deps): (r, dep) => - r.andAlso: - reporting.trace(i"forward $normElem from $this # $id to $dep # ${dep.maybeId} of class ${dep.getClass.toString}"): - dep.tryInclude(normElem, this) - if ccConfig.checkSkippedMaps && res.isOK then checkSkippedMaps(elem) - res.orElse: + val res = deps.forall: dep => + reporting.trace(i"forward $normElem from $this # $id to $dep # ${dep.maybeId} of class ${dep.getClass.toString}"): + dep.tryInclude(normElem, this) + if ccConfig.checkSkippedMaps && res then checkSkippedMaps(elem) + if !res then elems -= elem - res.addToTrace(this) + TypeComparer.updateErrorNotes: + case IncludeFailure(trace) => IncludeFailure(this :: trace) + res private def isPartOf(binder: Type)(using Context): Boolean = val find = new TypeAccumulator[Boolean]: @@ -662,14 +666,14 @@ object CaptureSet: case _ => true - def addDependent(cs: CaptureSet)(using Context, VarState): CompareResult = + def addDependent(cs: CaptureSet)(using Context, VarState): Boolean = if (cs eq this) || cs.isUniversal || isConst then - CompareResult.OK + true else if recordDepsState() then deps += cs - CompareResult.OK + true else - CompareResult.Fail(this :: Nil) + failWith(IncludeFailure(this :: Nil)) override def disallowRootCapability(upto: Symbol)(handler: () => Context ?=> Unit)(using Context): this.type = rootLimit = upto @@ -721,7 +725,7 @@ object CaptureSet: //println(i"solving var $this $approx ${approx.isConst} deps = ${deps.toList}") val newElems = approx.elems -- elems given VarState() - if tryInclude(newElems, empty).isOK then + if tryInclude(newElems, empty) then markSolved(provisional = false) /** Mark set as solved and propagate this info to all dependent sets */ @@ -819,13 +823,12 @@ object CaptureSet: (val source: Var, val bimap: BiTypeMap, initialElems: Refs)(using @constructorOnly ctx: Context) extends DerivedVar(source.owner, initialElems): - override def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): CompareResult = + override def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): Boolean = if origin eq source then val mappedElem = bimap.mapCapability(elem) - if accountsFor(mappedElem) then CompareResult.OK - else addNewElem(mappedElem) + accountsFor(mappedElem) || addNewElem(mappedElem) else if accountsFor(elem) then - CompareResult.OK + true else // Propagate backwards to source. The element will be added then by another // forward propagation from source that hits the first branch `if origin eq source then`. @@ -859,17 +862,16 @@ object CaptureSet: (val source: Var, val p: Context ?=> Capability => Boolean)(using @constructorOnly ctx: Context) extends DerivedVar(source.owner, source.elems.filter(p)): - override def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): CompareResult = + override def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): Boolean = if accountsFor(elem) then - CompareResult.OK + true else if origin eq source then - if p(elem) then addNewElem(elem) - else CompareResult.OK + !p(elem) || addNewElem(elem) else // Filtered elements have to be back-propagated to source. // Elements that don't satisfy `p` are not allowed. if p(elem) then source.tryInclude(elem, this) - else CompareResult.Fail(this :: Nil) + else failWith(IncludeFailure(this :: Nil)) override def computeApprox(origin: CaptureSet)(using Context): CaptureSet = if source eq origin then @@ -891,14 +893,14 @@ object CaptureSet: addAsDependentTo(cs1) addAsDependentTo(cs2) - override def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): CompareResult = - if accountsFor(elem) then CompareResult.OK + override def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): Boolean = + if accountsFor(elem) then true else val res = super.tryInclude(elem, origin) // If this is the union of a constant and a variable, // propagate `elem` to the variable part to avoid slack // between the operands and the union. - if res.isOK && (origin ne cs1) && (origin ne cs2) then + if res && (origin ne cs1) && (origin ne cs2) then if cs1.isConst then cs2.tryInclude(elem, origin) else if cs2.isConst then cs1.tryInclude(elem, origin) else res @@ -915,13 +917,12 @@ object CaptureSet: deps += cs1 deps += cs2 - override def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): CompareResult = + override def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): Boolean = val present = if origin eq cs1 then cs2.accountsFor(elem) else if origin eq cs2 then cs1.accountsFor(elem) else true - if present && !accountsFor(elem) then addNewElem(elem) - else CompareResult.OK + !present || accountsFor(elem) || addNewElem(elem) override def computeApprox(origin: CaptureSet)(using Context): CaptureSet = if (origin eq cs1) || (origin eq cs2) then @@ -1065,7 +1066,7 @@ object CaptureSet: case TypeBounds(CapturingType(lo, loRefs), CapturingType(hi, hiRefs)) if lo =:= hi => given VarState() val cs2 = arg2.captureSet - hiRefs.subCaptures(cs2).isOK && cs2.subCaptures(loRefs).isOK + hiRefs.subCaptures(cs2) && cs2.subCaptures(loRefs) case _ => false @@ -1078,48 +1079,25 @@ object CaptureSet: */ case class ExistentialSubsumesFailure(val ex: ResultCap, val other: Capability) extends ErrorNote - enum CompareResult extends Showable: - case OK - case Fail(trace: List[CaptureSet]) extends CompareResult, ErrorNote - case LevelError(cs: CaptureSet, elem: Capability) extends CompareResult, ErrorNote - + sealed abstract class CompareFailure extends ErrorNote, Showable: + override def kind = classOf[CompareFailure] override def toText(printer: Printer): Text = inContext(printer.printerContext): this match - case OK => Str("OK") - case Fail(trace) => + case IncludeFailure(trace) => if ctx.settings.YccDebug.value then printer.toText(trace, ", ") else blocking.show case LevelError(cs: CaptureSet, elem: Capability) => Str(i"($elem at wrong level for $cs at level ${cs.level.toString})") - /** The result is OK */ - def isOK: Boolean = this == OK - /** If not isOK, the blocking capture set */ def blocking: CaptureSet = (this: @unchecked) match - case Fail(cs) => cs.last + case IncludeFailure(cs) => cs.last case LevelError(cs, _) => cs + end CompareFailure - /** Optionally, this result if it is a level error */ - def levelError: Option[LevelError] = this match - case result: LevelError => Some(result) - case _ => None - - inline def andAlso(op: Context ?=> CompareResult)(using Context): CompareResult = - if isOK then op else this - - inline def orElse(op: Context ?=> CompareResult)(using Context): CompareResult = - if isOK then this - else - val alt = op - if alt.isOK then alt - else this - - inline def addToTrace(cs: CaptureSet): CompareResult = this match - case Fail(trace) => Fail(cs :: trace) - case _ => this - end CompareResult + case class IncludeFailure(trace: List[CaptureSet]) extends CompareFailure + case class LevelError(cs: CaptureSet, elem: Capability) extends CompareFailure /** A VarState serves as a snapshot mechanism that can undo * additions of elements or super sets if an operation fails diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 3f299fbe68c1..b08e6937f7d8 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -18,7 +18,7 @@ import util.{SimpleIdentitySet, EqHashMap, EqHashSet, SrcPos, Property} import transform.{Recheck, PreRecheck, CapturedVars} import Recheck.* import scala.collection.mutable -import CaptureSet.{withCaptureSetsExplained, CompareResult, ExistentialSubsumesFailure} +import CaptureSet.{withCaptureSetsExplained, CompareFailure, LevelError, ExistentialSubsumesFailure} import CCState.* import StdNames.nme import NameKinds.{DefaultGetterName, WildcardParamName, UniqueNameKind} @@ -349,13 +349,14 @@ class CheckCaptures extends Recheck, SymTransformer: /** Assert subcapturing `cs1 <: cs2` (available for debugging, otherwise unused) */ def assertSub(cs1: CaptureSet, cs2: CaptureSet)(using Context) = - assert(cs1.subCaptures(cs2).isOK, i"$cs1 is not a subset of $cs2") + assert(cs1.subCaptures(cs2), i"$cs1 is not a subset of $cs2") /** If `res` is not CompareResult.OK, report an error */ def checkOK(res: TypeComparer.CompareResult, prefix: => String, added: Capability | CaptureSet, target: CaptureSet, pos: SrcPos, provenance: => String = "")(using Context): Unit = res match case TypeComparer.CompareResult.Fail(notes) => - val ((res: CompareResult) :: Nil, otherNotes) = notes.partition(_.isInstanceOf[CompareResult]): @unchecked + val ((res: CompareFailure) :: Nil, otherNotes) = + notes.partition(_.isInstanceOf[CompareFailure]): @unchecked def msg(provisional: Boolean) = def toAdd: String = errorNotes(otherNotes).toAdd.mkString def descr: String = @@ -378,19 +379,10 @@ class CheckCaptures extends Recheck, SymTransformer: report.error(msg(provisional = false), pos) case _ => - def convertResult(op: => CompareResult)(using Context): TypeComparer.CompareResult = - TypeComparer.test: - op match - case res: TypeComparer.ErrorNote => - TypeComparer.addErrorNote(res) - false - case CompareResult.OK => - true - /** Check subcapturing `{elem} <: cs`, report error on failure */ def checkElem(elem: Capability, cs: CaptureSet, pos: SrcPos, provenance: => String = "")(using Context) = checkOK( - convertResult(elem.singletonCaptureSet.subCaptures(cs)), + TypeComparer.compareResult(elem.singletonCaptureSet.subCaptures(cs)), i"$elem cannot be referenced here; it is not", elem, cs, pos, provenance) @@ -398,7 +390,7 @@ class CheckCaptures extends Recheck, SymTransformer: def checkSubset(cs1: CaptureSet, cs2: CaptureSet, pos: SrcPos, provenance: => String = "", cs1description: String = "")(using Context) = checkOK( - convertResult(cs1.subCaptures(cs2)), + TypeComparer.compareResult(cs1.subCaptures(cs2)), if cs1.elems.size == 1 then i"reference ${cs1.elems.nth(0)}$cs1description is not" else i"references $cs1$cs1description are not all", cs1, cs2, pos, provenance) @@ -1283,11 +1275,12 @@ class CheckCaptures extends Recheck, SymTransformer: type BoxErrors = mutable.ListBuffer[Message] | Null private def errorNotes(notes: List[TypeComparer.ErrorNote])(using Context): Addenda = - if notes.isEmpty then NothingToAdd + val printableNotes = notes.filter(_.isInstanceOf[LevelError | ExistentialSubsumesFailure]) + if printableNotes.isEmpty then NothingToAdd else new Addenda: - override def toAdd(using Context) = notes.map: note => + override def toAdd(using Context) = printableNotes.map: note => val msg = note match - case CompareResult.LevelError(cs, ref) => + case LevelError(cs, ref) => if ref.core.isCapOrFresh then i"""the universal capability $ref |cannot be included in capture set $cs""" @@ -1346,7 +1339,7 @@ class CheckCaptures extends Recheck, SymTransformer: if actualBoxed eq actual then // Only `addOuterRefs` when there is no box adaptation expected1 = addOuterRefs(expected1, actual, tree.srcPos) - TypeComparer.test(isCompatible(actualBoxed, expected1)) match + TypeComparer.compareResult(isCompatible(actualBoxed, expected1)) match case TypeComparer.CompareResult.Fail(notes) => capt.println(i"conforms failed for ${tree}: $actual vs $expected") err.typeMismatch(tree.withType(actualBoxed), expected1, @@ -1522,7 +1515,7 @@ class CheckCaptures extends Recheck, SymTransformer: val cs = actual.captureSet if covariant then cs ++ leaked else - if !leaked.subCaptures(cs).isOK then + if !leaked.subCaptures(cs) then report.error( em"""$expected cannot be box-converted to ${actual.capturing(leaked)} |since the additional capture set $leaked resulting from box conversion is not allowed in $actual""", tree.srcPos) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 10db6d9cf133..772fea772047 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -59,7 +59,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling private var monitored = false private var maxErrorLevel: Int = -1 - private var errorNotes: List[(Int, ErrorNote)] = Nil + protected var errorNotes: List[(Int, ErrorNote)] = Nil private var needsGc = false @@ -433,7 +433,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling case _ => if isCaptureVarComparison then return CCState.withCapAsRoot: - subCaptures(tp1.captureSet, tp2.captureSet).isOK + subCaptures(tp1.captureSet, tp2.captureSet) if (tp1 eq NothingType) || isBottom(tp1) then return true } @@ -541,7 +541,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling case tp1 @ CapturingType(parent1, refs1) => def compareCapturing = if tp2.isAny then true - else if subCaptures(refs1, tp2.captureSet).isOK && sameBoxed(tp1, tp2, refs1) + else if subCaptures(refs1, tp2.captureSet) && sameBoxed(tp1, tp2, refs1) || !ctx.mode.is(Mode.CheckBoundsOrSelfType) && tp1.isAlwaysPure then val tp2a = @@ -583,7 +583,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling if isCaptureVarComparison then return CCState.withCapAsRoot: - subCaptures(tp1.captureSet, tp2.captureSet).isOK + subCaptures(tp1.captureSet, tp2.captureSet) isSubApproxHi(tp1, info2.lo) && (trustBounds || isSubApproxHi(tp1, info2.hi)) || compareGADT @@ -668,12 +668,12 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling && isSubInfo(info1.resultType, info2.resultType.subst(info2, info1)) case (info1 @ CapturingType(parent1, refs1), info2: Type) if info2.stripCapturing.isInstanceOf[MethodOrPoly] => - subCaptures(refs1, info2.captureSet).isOK && sameBoxed(info1, info2, refs1) + subCaptures(refs1, info2.captureSet) && sameBoxed(info1, info2, refs1) && isSubInfo(parent1, info2) case (info1: Type, CapturingType(parent2, refs2)) if info1.stripCapturing.isInstanceOf[MethodOrPoly] => val refs1 = info1.captureSet - (refs1.isAlwaysEmpty || subCaptures(refs1, refs2).isOK) && sameBoxed(info1, info2, refs1) + (refs1.isAlwaysEmpty || subCaptures(refs1, refs2)) && sameBoxed(info1, info2, refs1) && isSubInfo(info1, parent2) case _ => isSubType(info1, info2) @@ -867,12 +867,12 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling // Eamples where this arises is capt-capibility.scala and function-combinators.scala val singletonOK = tp1 match case tp1: SingletonType - if subCaptures(tp1.underlying.captureSet, refs2, CaptureSet.VarState.Separate).isOK => + if subCaptures(tp1.underlying.captureSet, refs2, CaptureSet.VarState.Separate) => recur(tp1.widen, tp2) case _ => false singletonOK - || subCaptures(refs1, refs2).isOK + || subCaptures(refs1, refs2) && sameBoxed(tp1, tp2, refs1) && (recur(tp1.widen.stripCapturing, parent2) || tp1.isInstanceOf[SingletonType] && recur(tp1, parent2) @@ -2830,7 +2830,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling if frozenConstraint then CaptureSet.VarState.Closed() else CaptureSet.VarState() protected def subCaptures(refs1: CaptureSet, refs2: CaptureSet, - vs: CaptureSet.VarState = makeVarState())(using Context): CaptureSet.CompareResult = + vs: CaptureSet.VarState = makeVarState())(using Context): Boolean = try refs1.subCaptures(refs2, vs) catch case ex: AssertionError => @@ -2843,7 +2843,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling */ protected def sameBoxed(tp1: Type, tp2: Type, refs1: CaptureSet)(using Context): Boolean = (tp1.isBoxedCapturing == tp2.isBoxedCapturing) - || refs1.subCaptures(CaptureSet.empty, makeVarState()).isOK + || refs1.subCaptures(CaptureSet.empty, makeVarState()) // ----------- Diagnostics -------------------------------------------------- @@ -3254,16 +3254,40 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling * the same class as `note`. */ def addErrorNote(note: ErrorNote): Unit = - if errorNotes.forall(_._2.getClass != note.getClass) then + if errorNotes.forall(_._2.kind != note.kind) then errorNotes = (recCount, note) :: errorNotes assert(maxErrorLevel <= recCount) maxErrorLevel = recCount + + private[TypeComparer] inline + def isolated[T](inline op: Boolean, inline mapResult: Boolean => T)(using Context): T = + val savedNotes = errorNotes + val savedLevel = maxErrorLevel + errorNotes = Nil + maxErrorLevel = -1 + try mapResult(op) + finally + errorNotes = savedNotes + maxErrorLevel = savedLevel + + /** Run `op` on current type comparer, maping its Boolean result to + * a CompareResult with possible outcomes OK and Fail(...)`. In case + * of failure pass the accumulated errorNotes of this type comparer to + * in the Fail value. + */ + def compareResult(op: => Boolean)(using Context): CompareResult = + isolated(op, res => + if res then CompareResult.OK else CompareResult.Fail(errorNotes.map(_._2))) } object TypeComparer { /** A base trait for data producing addenda to error messages */ - trait ErrorNote + trait ErrorNote: + /** A disciminating kind. An error note is not added if it has the same kind + * as an already existing error note. + */ + def kind: Class[?] = getClass /** A richer compare result, returned by `testSubType` and `test`. */ enum CompareResult: @@ -3280,7 +3304,6 @@ object TypeComparer { else res match case ClassInfo(_, cls, _, _, _) => cls.showLocated case bounds: TypeBounds => i"type bounds [$bounds]" - case CaptureSet.CompareResult.OK => "OK" case res: printing.Showable => res.show case _ => String.valueOf(res).nn @@ -3435,7 +3458,7 @@ object TypeComparer { def reduceMatchWith[T](op: MatchReducer => T)(using Context): T = comparing(_.reduceMatchWith(op)) - def subCaptures(refs1: CaptureSet, refs2: CaptureSet, vs: CaptureSet.VarState)(using Context): CaptureSet.CompareResult = + def subCaptures(refs1: CaptureSet, refs2: CaptureSet, vs: CaptureSet.VarState)(using Context): Boolean = comparing(_.subCaptures(refs1, refs2, vs)) def inNestedLevel(op: => Boolean)(using Context): Boolean = @@ -3444,15 +3467,16 @@ object TypeComparer { def addErrorNote(note: ErrorNote)(using Context): Unit = comparer.addErrorNote(note) - /** Run `op` on current type comparer, maping its Boolean result to - * a CompareResult with possible outcomes OK and Fail(...)`. In case - * of failure pass the accumulated errorNotes of this type comparer to - * in the Fail value. - */ - def test(op: => Boolean)(using Context): CompareResult = - comparing: comparer => - if op then CompareResult.OK - else CompareResult.Fail(comparer.errorNotes.map(_._2)) + def updateErrorNotes(f: PartialFunction[ErrorNote, ErrorNote])(using Context): Unit = + comparer.errorNotes = comparer.errorNotes.mapConserve: p => + val (level, note) = p + if f.isDefinedAt(note) then (level, f(note)) else p + + def compareResult(op: => Boolean)(using Context): CompareResult = + comparing(_.compareResult(op)) + + inline def noNotes(inline op: Boolean)(using Context): Boolean = + comparer.isolated(op, x => x) } object MatchReducer: @@ -3857,9 +3881,11 @@ class ExplainingTypeComparer(initctx: Context, short: Boolean) extends TypeCompa private val b = new StringBuilder private var lastForwardGoal: String | Null = null - private def appendFailure(x: String) = + private def appendFailure(notes: List[ErrorNote]) = if lastForwardGoal != null then // last was deepest goal that failed - b.append(s" = $x") + b.append(s" = false") + for case note: printing.Showable <- notes do + b.append(i": $note") lastForwardGoal = null override def traceIndented[T](str: String)(op: => T): T = @@ -3875,9 +3901,9 @@ class ExplainingTypeComparer(initctx: Context, short: Boolean) extends TypeCompa if short then res match case false => - appendFailure("false") - case res: CaptureSet.CompareResult if res != CaptureSet.CompareResult.OK => - appendFailure(show(res)) + appendFailure(errorNotes.map(_._2)) + case CompareResult.Fail(notes) => + appendFailure(notes) case _ => b.length = curLength // don't show successful subtraces else @@ -3927,7 +3953,7 @@ class ExplainingTypeComparer(initctx: Context, short: Boolean) extends TypeCompa super.gadtAddBound(sym, b, isUpper) } - override def subCaptures(refs1: CaptureSet, refs2: CaptureSet, vs: CaptureSet.VarState)(using Context): CaptureSet.CompareResult = + override def subCaptures(refs1: CaptureSet, refs2: CaptureSet, vs: CaptureSet.VarState)(using Context): Boolean = traceIndented(i"subcaptures $refs1 <:< $refs2 in ${vs.toString}") { super.subCaptures(refs1, refs2, vs) } diff --git a/compiler/src/dotty/tools/dotc/core/TypeOps.scala b/compiler/src/dotty/tools/dotc/core/TypeOps.scala index efd4c6e83cd2..67c8186c17d1 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeOps.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeOps.scala @@ -19,7 +19,7 @@ import typer.Inferencing.* import typer.IfBottom import reporting.TestingReporter import cc.{CapturingType, derivedCapturingType, CaptureSet, captureSet, isBoxed, isBoxedCapturing} -import CaptureSet.{CompareResult, IdentityCaptRefMap, VarState} +import CaptureSet.{IdentityCaptRefMap, VarState} import scala.annotation.internal.sharable import scala.annotation.threadUnsafe @@ -161,7 +161,7 @@ object TypeOps: TypeComparer.lub(simplify(l, theMap), simplify(r, theMap), isSoft = tp.isSoft) case tp @ CapturingType(parent, refs) => if !ctx.mode.is(Mode.Type) - && refs.subCaptures(parent.captureSet, VarState.Separate).isOK + && refs.subCaptures(parent.captureSet, VarState.Separate) && (tp.isBoxed || !parent.isBoxedCapturing) // fuse types with same boxed status and outer boxed with any type then diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala index 728f742ea1ad..2326abf04ad4 100644 --- a/compiler/src/dotty/tools/dotc/core/Types.scala +++ b/compiler/src/dotty/tools/dotc/core/Types.scala @@ -39,7 +39,7 @@ import reporting.{trace, Message} import java.lang.ref.WeakReference import compiletime.uninitialized import cc.* -import CaptureSet.{CompareResult, IdentityCaptRefMap} +import CaptureSet.IdentityCaptRefMap import Capabilities.* import scala.annotation.internal.sharable diff --git a/tests/neg-custom-args/captures/capt-depfun.check b/tests/neg-custom-args/captures/capt-depfun.check index 28341e0be9cd..a5db4da7a319 100644 --- a/tests/neg-custom-args/captures/capt-depfun.check +++ b/tests/neg-custom-args/captures/capt-depfun.check @@ -6,10 +6,6 @@ | | where: => refers to a fresh root capability in the type of value dc | - | - | Note that the existential capture root in Str^{x} => Str^{x} - | cannot subsume the capability Str^{x}> - | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/capt-depfun.scala:11:24 ------------------------------------------------------- 11 | val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error // error: separatioon From cbd308a255fa3a6b5b4eacfd1ba397b86dfa6a9d Mon Sep 17 00:00:00 2001 From: odersky Date: Sat, 24 May 2025 18:57:00 +0200 Subject: [PATCH 4/6] Unify to have a single error class that refers to a set and an element --- .../src/dotty/tools/dotc/cc/CaptureSet.scala | 52 +++++++++---------- .../dotty/tools/dotc/cc/CheckCaptures.scala | 19 ++++--- 2 files changed, 35 insertions(+), 36 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index fb8d17d2a087..ffdebdbcd8a0 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -175,7 +175,7 @@ sealed abstract class CaptureSet extends Showable: protected def addIfHiddenOrFail(elem: Capability)(using ctx: Context, vs: VarState): Boolean = elems.exists(_.maxSubsumes(elem, canAddHidden = true)) - || failWith(IncludeFailure(this :: Nil)) + || failWith(IncludeFailure(this, elem)) /** If this is a variable, add `cs` as a dependent set */ protected def addDependent(cs: CaptureSet)(using Context, VarState): Boolean @@ -604,7 +604,7 @@ object CaptureSet: if isConst || !recordElemsState() then // Fail if variable is solved or given VarState is frozen addIfHiddenOrFail(elem) else if !levelOK(elem) then - failWith(LevelError(this, elem)) // or `elem` is not visible at the level of the set. + failWith(IncludeFailure(this, elem, levelError = true)) // or `elem` is not visible at the level of the set. else // id == 108 then assert(false, i"trying to add $elem to $this") assert(elem.isWellformed, elem) @@ -622,7 +622,7 @@ object CaptureSet: if !res then elems -= elem TypeComparer.updateErrorNotes: - case IncludeFailure(trace) => IncludeFailure(this :: trace) + case note: IncludeFailure => note.addToTrace(this) res private def isPartOf(binder: Type)(using Context): Boolean = @@ -667,13 +667,10 @@ object CaptureSet: true def addDependent(cs: CaptureSet)(using Context, VarState): Boolean = - if (cs eq this) || cs.isUniversal || isConst then - true - else if recordDepsState() then - deps += cs - true - else - failWith(IncludeFailure(this :: Nil)) + (cs eq this) + || cs.isUniversal + || isConst + || recordDepsState() && { deps += cs; true } override def disallowRootCapability(upto: Symbol)(handler: () => Context ?=> Unit)(using Context): this.type = rootLimit = upto @@ -871,7 +868,7 @@ object CaptureSet: // Filtered elements have to be back-propagated to source. // Elements that don't satisfy `p` are not allowed. if p(elem) then source.tryInclude(elem, this) - else failWith(IncludeFailure(this :: Nil)) + else failWith(IncludeFailure(this, elem)) override def computeApprox(origin: CaptureSet)(using Context): CaptureSet = if source eq origin then @@ -1079,25 +1076,24 @@ object CaptureSet: */ case class ExistentialSubsumesFailure(val ex: ResultCap, val other: Capability) extends ErrorNote - sealed abstract class CompareFailure extends ErrorNote, Showable: - override def kind = classOf[CompareFailure] + case class IncludeFailure(cs: CaptureSet, elem: Capability, levelError: Boolean = false) extends ErrorNote, Showable: + private var myTrace: List[CaptureSet] = cs :: Nil + + def trace: List[CaptureSet] = myTrace + def addToTrace(cs1: CaptureSet) = + val res = IncludeFailure(cs, elem, levelError) + res.myTrace = cs1 :: this.myTrace + res + override def toText(printer: Printer): Text = inContext(printer.printerContext): - this match - case IncludeFailure(trace) => - if ctx.settings.YccDebug.value then printer.toText(trace, ", ") - else blocking.show - case LevelError(cs: CaptureSet, elem: Capability) => - Str(i"($elem at wrong level for $cs at level ${cs.level.toString})") - - /** If not isOK, the blocking capture set */ - def blocking: CaptureSet = (this: @unchecked) match - case IncludeFailure(cs) => cs.last - case LevelError(cs, _) => cs - end CompareFailure - - case class IncludeFailure(trace: List[CaptureSet]) extends CompareFailure - case class LevelError(cs: CaptureSet, elem: Capability) extends CompareFailure + if levelError then + i"($elem at wrong level for $cs at level ${cs.level.toString})" + else + if ctx.settings.YccDebug.value + then i"$elem cannot be included in $trace" + else i"$elem cannot be included in $cs" + end IncludeFailure /** A VarState serves as a snapshot mechanism that can undo * additions of elements or super sets if an operation fails diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index b08e6937f7d8..d095231cc468 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -18,7 +18,7 @@ import util.{SimpleIdentitySet, EqHashMap, EqHashSet, SrcPos, Property} import transform.{Recheck, PreRecheck, CapturedVars} import Recheck.* import scala.collection.mutable -import CaptureSet.{withCaptureSetsExplained, CompareFailure, LevelError, ExistentialSubsumesFailure} +import CaptureSet.{withCaptureSetsExplained, IncludeFailure, ExistentialSubsumesFailure} import CCState.* import StdNames.nme import NameKinds.{DefaultGetterName, WildcardParamName, UniqueNameKind} @@ -355,18 +355,18 @@ class CheckCaptures extends Recheck, SymTransformer: def checkOK(res: TypeComparer.CompareResult, prefix: => String, added: Capability | CaptureSet, target: CaptureSet, pos: SrcPos, provenance: => String = "")(using Context): Unit = res match case TypeComparer.CompareResult.Fail(notes) => - val ((res: CompareFailure) :: Nil, otherNotes) = - notes.partition(_.isInstanceOf[CompareFailure]): @unchecked + val ((res: IncludeFailure) :: Nil, otherNotes) = + notes.partition(_.isInstanceOf[IncludeFailure]): @unchecked def msg(provisional: Boolean) = def toAdd: String = errorNotes(otherNotes).toAdd.mkString def descr: String = - val d = res.blocking.description + val d = res.cs.description if d.isEmpty then provenance else "" def kind = if provisional then "previously estimated\n" else "allowed " - em"$prefix included in the ${kind}capture set ${res.blocking}$descr$toAdd" + em"$prefix included in the ${kind}capture set ${res.cs}$descr$toAdd" target match case target: CaptureSet.Var - if res.blocking.isProvisionallySolved => + if res.cs.isProvisionallySolved => report.warning( msg(provisional = true) .prepend(i"Another capture checking run needs to be scheduled because\n"), @@ -1275,12 +1275,15 @@ class CheckCaptures extends Recheck, SymTransformer: type BoxErrors = mutable.ListBuffer[Message] | Null private def errorNotes(notes: List[TypeComparer.ErrorNote])(using Context): Addenda = - val printableNotes = notes.filter(_.isInstanceOf[LevelError | ExistentialSubsumesFailure]) + val printableNotes = notes.filter: + case IncludeFailure(_, _, true) => true + case _: ExistentialSubsumesFailure => true + case _ => false if printableNotes.isEmpty then NothingToAdd else new Addenda: override def toAdd(using Context) = printableNotes.map: note => val msg = note match - case LevelError(cs, ref) => + case IncludeFailure(cs, ref, _) => if ref.core.isCapOrFresh then i"""the universal capability $ref |cannot be included in capture set $cs""" From 3bc3d2fba89600e2a063a43c183fac11e6b6a359 Mon Sep 17 00:00:00 2001 From: odersky Date: Sun, 25 May 2025 10:11:31 +0200 Subject: [PATCH 5/6] Tweak HiddenSet Avoid var for owningCap --- compiler/src/dotty/tools/dotc/cc/Capability.scala | 4 ++-- compiler/src/dotty/tools/dotc/cc/CaptureSet.scala | 7 +++---- tests/neg-custom-args/captures/scope-extrude-mut.check | 9 +++++++++ tests/neg-custom-args/captures/scope-extrude-mut.scala | 9 +++++++++ 4 files changed, 23 insertions(+), 6 deletions(-) create mode 100644 tests/neg-custom-args/captures/scope-extrude-mut.check create mode 100644 tests/neg-custom-args/captures/scope-extrude-mut.scala diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index 60a1704ff45d..8d668a6d29b7 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -138,8 +138,8 @@ object Capabilities: * for diagnostics */ case class FreshCap private (owner: Symbol, origin: Origin)(using @constructorOnly ctx: Context) extends RootCapability: - val hiddenSet = CaptureSet.HiddenSet(owner) - hiddenSet.owningCap = this + val hiddenSet = CaptureSet.HiddenSet(owner, this: @unchecked) + // fails initialization check without the @unchecked override def equals(that: Any) = that match case that: FreshCap => this eq that diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index ffdebdbcd8a0..b836ca41f290 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -950,16 +950,15 @@ object CaptureSet: * which are already subject through snapshotting and rollbacks in VarState. * It's advantageous if we don't need to deal with other pieces of state there. */ - class HiddenSet(initialOwner: Symbol)(using @constructorOnly ictx: Context) + class HiddenSet(initialOwner: Symbol, val owningCap: FreshCap)(using @constructorOnly ictx: Context) extends Var(initialOwner): - var owningCap: FreshCap = uninitialized // initialized when owning FreshCap is created var givenOwner: Symbol = initialOwner override def owner = givenOwner - //assert(id != 4) + //assert(id != 3) - description = i"elements subsumed by $owningCap" + description = i"of elements subsumed by a fresh cap in $initialOwner" private def aliasRef: FreshCap | Null = if myElems.size == 1 then diff --git a/tests/neg-custom-args/captures/scope-extrude-mut.check b/tests/neg-custom-args/captures/scope-extrude-mut.check new file mode 100644 index 000000000000..1e01ddf834f8 --- /dev/null +++ b/tests/neg-custom-args/captures/scope-extrude-mut.check @@ -0,0 +1,9 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scope-extrude-mut.scala:9:8 ------------------------------ +9 | a = a1 // error + | ^^ + | Found: A^{a1.rd} + | Required: A^ + | + | where: ^ refers to a fresh root capability in the type of variable a + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/scope-extrude-mut.scala b/tests/neg-custom-args/captures/scope-extrude-mut.scala new file mode 100644 index 000000000000..75ff0e11abcb --- /dev/null +++ b/tests/neg-custom-args/captures/scope-extrude-mut.scala @@ -0,0 +1,9 @@ +import language.experimental.captureChecking + +class A extends caps.Mutable + +class B: + private var a: A^ = A() + def b() = + val a1 = A() + a = a1 // error \ No newline at end of file From 4e9ebec7797614fb9283c18f365d3d05c70afcc6 Mon Sep 17 00:00:00 2001 From: odersky Date: Mon, 26 May 2025 11:33:54 +0200 Subject: [PATCH 6/6] Avoid double blank line in front of error notes --- compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala | 1 - .../neg-custom-args/captures/cc-existential-conformance.check | 2 -- tests/neg-custom-args/captures/effect-swaps-explicit.check | 1 - tests/neg-custom-args/captures/effect-swaps.check | 1 - tests/neg-custom-args/captures/erased-methods2.check | 2 -- tests/neg-custom-args/captures/filevar.check | 1 - tests/neg-custom-args/captures/heal-tparam-cs.check | 2 -- tests/neg-custom-args/captures/i15923.check | 1 - tests/neg-custom-args/captures/i15923a.check | 1 - tests/neg-custom-args/captures/i15923b.check | 1 - tests/neg-custom-args/captures/i16226.check | 1 - tests/neg-custom-args/captures/i21614.check | 1 - tests/neg-custom-args/captures/i21920.check | 1 - tests/neg-custom-args/captures/leaking-iterators.check | 1 - tests/neg-custom-args/captures/reaches.check | 1 - tests/neg-custom-args/captures/scoped-caps.check | 3 --- tests/neg-custom-args/captures/simple-using.check | 1 - tests/neg-custom-args/captures/try.check | 2 -- tests/neg-custom-args/captures/usingLogFile.check | 4 ---- tests/neg-custom-args/captures/vars.check | 1 - 20 files changed, 29 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index d095231cc468..1bdd7ce92129 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -1300,7 +1300,6 @@ class CheckCaptures extends Recheck, SymTransformer: i"""the existential capture root in ${ex.originalBinder.resType} |cannot subsume the capability $other$since""" i""" - | |Note that ${msg.toString}""" diff --git a/tests/neg-custom-args/captures/cc-existential-conformance.check b/tests/neg-custom-args/captures/cc-existential-conformance.check index d3236ce642b0..0719fd2787df 100644 --- a/tests/neg-custom-args/captures/cc-existential-conformance.check +++ b/tests/neg-custom-args/captures/cc-existential-conformance.check @@ -19,7 +19,6 @@ | where: ^ refers to a fresh root capability in the type of value y | ^² refers to a root capability associated with the result type of (x: A): B^² | - | | Note that the existential capture root in B^ | cannot subsume the capability cap | @@ -45,7 +44,6 @@ | where: ^ refers to a fresh root capability in the type of value y | ^² refers to a root capability associated with the result type of (x: A): B^² | - | | Note that the existential capture root in B^ | cannot subsume the capability cap | diff --git a/tests/neg-custom-args/captures/effect-swaps-explicit.check b/tests/neg-custom-args/captures/effect-swaps-explicit.check index c7cbb351318a..469a0c6f14a4 100644 --- a/tests/neg-custom-args/captures/effect-swaps-explicit.check +++ b/tests/neg-custom-args/captures/effect-swaps-explicit.check @@ -24,7 +24,6 @@ |where: ?=> refers to a fresh root capability created in method fail4 when checking argument to parameter body of method make | ^ refers to the universal root capability | - | |Note that reference contextual$9.type |cannot be included in outer capture set ? 70 | fr.await.ok diff --git a/tests/neg-custom-args/captures/effect-swaps.check b/tests/neg-custom-args/captures/effect-swaps.check index d30aa0ca3f21..69cedcde2f75 100644 --- a/tests/neg-custom-args/captures/effect-swaps.check +++ b/tests/neg-custom-args/captures/effect-swaps.check @@ -24,7 +24,6 @@ |where: ?=> refers to a fresh root capability created in method fail4 when checking argument to parameter body of method make | cap is the universal root capability | - | |Note that reference contextual$9.type |cannot be included in outer capture set ? 70 | fr.await.ok diff --git a/tests/neg-custom-args/captures/erased-methods2.check b/tests/neg-custom-args/captures/erased-methods2.check index 80d2db450c40..d7cca4635f20 100644 --- a/tests/neg-custom-args/captures/erased-methods2.check +++ b/tests/neg-custom-args/captures/erased-methods2.check @@ -8,7 +8,6 @@ | ?=>² refers to a root capability associated with the result type of (using erased x$1: CT[Ex3]^): (erased x$2: CT[Ex2]^) ?=>² Unit | ^ refers to the universal root capability | - | |Note that the existential capture root in (erased x$2: CT[Ex2]^) ?=> Unit |cannot subsume the capability x$1.type since that capability is not a SharedCapability 21 | ?=> (x$2: CT[Ex2]^) @@ -28,7 +27,6 @@ | ?=>³ refers to a root capability associated with the result type of (using erased x$1: CT[Ex2]^): (erased x$2: CT[Ex1]^) ?=>³ Unit | ^ refers to the universal root capability | - | |Note that the existential capture root in (erased x$1: CT[Ex2]^) ?=> (erased x$2: CT[Ex1]^) ?=> Unit |cannot subsume the capability x$1.type since that capability is not a SharedCapability 32 | ?=> (erased x$2: CT[Ex2]^) diff --git a/tests/neg-custom-args/captures/filevar.check b/tests/neg-custom-args/captures/filevar.check index d0b85408b43a..54f67bce972a 100644 --- a/tests/neg-custom-args/captures/filevar.check +++ b/tests/neg-custom-args/captures/filevar.check @@ -7,7 +7,6 @@ |where: => refers to a root capability associated with the result type of (using l: scala.caps.Capability^{cap.rd}): (f: File^{l}) => Unit | cap is the universal root capability | - | |Note that reference l.type |cannot be included in outer capture set ? of parameter f 16 | val o = Service() diff --git a/tests/neg-custom-args/captures/heal-tparam-cs.check b/tests/neg-custom-args/captures/heal-tparam-cs.check index 10b56d5d6304..0a7c333c9e95 100644 --- a/tests/neg-custom-args/captures/heal-tparam-cs.check +++ b/tests/neg-custom-args/captures/heal-tparam-cs.check @@ -7,7 +7,6 @@ |where: => refers to a fresh root capability created in value test1 when checking argument to parameter op of method localCap | ^ refers to the universal root capability | - | |Note that reference c.type |cannot be included in outer capture set ? 11 | () => { c.use() } @@ -23,7 +22,6 @@ | where: => refers to a root capability associated with the result type of (c: Capp^): () => Unit | ^ refers to the universal root capability | - | | Note that the existential capture root in () => Unit | cannot subsume the capability x$0.type since that capability is not a SharedCapability 16 | (c1: Capp^) => () => { c1.use() } diff --git a/tests/neg-custom-args/captures/i15923.check b/tests/neg-custom-args/captures/i15923.check index e234eb579be2..4d3019f92d7a 100644 --- a/tests/neg-custom-args/captures/i15923.check +++ b/tests/neg-custom-args/captures/i15923.check @@ -8,7 +8,6 @@ | cap is the universal root capability | cap² is a root capability associated with the result type of (x$0: Cap^{lcap}): box Id[box Cap^{cap².rd}]^? | - | |Note that reference .rd |cannot be included in outer capture set ? | diff --git a/tests/neg-custom-args/captures/i15923a.check b/tests/neg-custom-args/captures/i15923a.check index 9664fb7bfdde..1b4ef98aff20 100644 --- a/tests/neg-custom-args/captures/i15923a.check +++ b/tests/neg-custom-args/captures/i15923a.check @@ -9,7 +9,6 @@ | ^ refers to the universal root capability | ^² refers to a root capability associated with the result type of (): box Id[box Cap^²]^? | - | |Note that reference |cannot be included in outer capture set ? | diff --git a/tests/neg-custom-args/captures/i15923b.check b/tests/neg-custom-args/captures/i15923b.check index 38da3dc798a8..eb67188bcc25 100644 --- a/tests/neg-custom-args/captures/i15923b.check +++ b/tests/neg-custom-args/captures/i15923b.check @@ -7,7 +7,6 @@ |where: => refers to a fresh root capability created in value leak when checking argument to parameter op of method withCap | ^ refers to the universal root capability | - | |Note that reference lcap.type |cannot be included in outer capture set ? | diff --git a/tests/neg-custom-args/captures/i16226.check b/tests/neg-custom-args/captures/i16226.check index f3b8666c0eb7..4fb4119fdbef 100644 --- a/tests/neg-custom-args/captures/i16226.check +++ b/tests/neg-custom-args/captures/i16226.check @@ -21,7 +21,6 @@ | =>³ refers to a fresh root capability in the result type of method mapd | ^ refers to a root capability associated with the result type of (ref: LazyRef[A]^{io}, f: A => B): LazyRef[B]^ | - | |Note that the existential capture root in LazyRef[B]^ |cannot subsume the capability f1.type since that capability is not a SharedCapability | diff --git a/tests/neg-custom-args/captures/i21614.check b/tests/neg-custom-args/captures/i21614.check index a24677f0f9d1..5bc01afa4dd0 100644 --- a/tests/neg-custom-args/captures/i21614.check +++ b/tests/neg-custom-args/captures/i21614.check @@ -16,7 +16,6 @@ |where: => refers to a fresh root capability created in method mkLoggers2 when checking argument to parameter f of method map | cap is a root capability associated with the result type of (_$1: box File^{files*}): box Logger{val f: File^{_$1}}^{cap.rd, _$1} | - | |Note that reference .rd |cannot be included in outer capture set ? | diff --git a/tests/neg-custom-args/captures/i21920.check b/tests/neg-custom-args/captures/i21920.check index 301564d23b79..70327a9e413f 100644 --- a/tests/neg-custom-args/captures/i21920.check +++ b/tests/neg-custom-args/captures/i21920.check @@ -7,7 +7,6 @@ |where: => refers to a fresh root capability created in value cell when checking argument to parameter f of method open | ^ refers to the universal root capability | - | |Note that reference |cannot be included in outer capture set ? | diff --git a/tests/neg-custom-args/captures/leaking-iterators.check b/tests/neg-custom-args/captures/leaking-iterators.check index f2731166e53d..a64934c41360 100644 --- a/tests/neg-custom-args/captures/leaking-iterators.check +++ b/tests/neg-custom-args/captures/leaking-iterators.check @@ -7,7 +7,6 @@ |where: => refers to a fresh root capability created in method test when checking argument to parameter op of method usingLogFile | ^ refers to the universal root capability | - | |Note that reference log.type |cannot be included in outer capture set ? 57 | xs.iterator.map: x => diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check index a54bb05b8222..29ed6503f45c 100644 --- a/tests/neg-custom-args/captures/reaches.check +++ b/tests/neg-custom-args/captures/reaches.check @@ -86,7 +86,6 @@ | where: ^ refers to the universal root capability | ^² refers to a root capability associated with the result type of (x: File^): File^² | - | | Note that the existential capture root in File^ | cannot subsume the capability x.type since that capability is not a SharedCapability | diff --git a/tests/neg-custom-args/captures/scoped-caps.check b/tests/neg-custom-args/captures/scoped-caps.check index e35af6b10bb9..b57ff92a8899 100644 --- a/tests/neg-custom-args/captures/scoped-caps.check +++ b/tests/neg-custom-args/captures/scoped-caps.check @@ -19,7 +19,6 @@ | ^² refers to a fresh root capability in the type of value g | ^³ refers to a root capability associated with the result type of (x: A^): B^³ | - | | Note that the existential capture root in B^ | cannot subsume the capability cap | @@ -54,7 +53,6 @@ | where: ^ refers to the universal root capability | ^² refers to a root capability associated with the result type of (x: A^): B^² | - | | Note that the existential capture root in B^ | cannot subsume the capability x.type since that capability is not a SharedCapability | @@ -69,7 +67,6 @@ | ^² refers to a root capability associated with the result type of (x: S^{cap.rd}): B^² | cap is the universal root capability | - | | Note that the existential capture root in B^ | cannot subsume the capability cap | diff --git a/tests/neg-custom-args/captures/simple-using.check b/tests/neg-custom-args/captures/simple-using.check index 6e32260d3322..3f31f6e41dd2 100644 --- a/tests/neg-custom-args/captures/simple-using.check +++ b/tests/neg-custom-args/captures/simple-using.check @@ -7,7 +7,6 @@ |where: => refers to a fresh root capability created in method test when checking argument to parameter op of method usingLogFile | ^ refers to the universal root capability | - | |Note that reference f.type |cannot be included in outer capture set ? | diff --git a/tests/neg-custom-args/captures/try.check b/tests/neg-custom-args/captures/try.check index 7f420872eb25..7d1f2bc7f31d 100644 --- a/tests/neg-custom-args/captures/try.check +++ b/tests/neg-custom-args/captures/try.check @@ -39,7 +39,6 @@ |where: => refers to a fresh root capability created in value xx when checking argument to parameter op of method handle | ^ refers to the universal root capability | - | |Note that reference x.type |cannot be included in outer capture set ? 36 | (x: CanThrow[Exception]) => @@ -58,7 +57,6 @@ |where: => refers to a fresh root capability created in value global when checking argument to parameter op of method handle | ^ refers to the universal root capability | - | |Note that reference x.type |cannot be included in outer capture set ? 48 | (x: CanThrow[Exception]) => diff --git a/tests/neg-custom-args/captures/usingLogFile.check b/tests/neg-custom-args/captures/usingLogFile.check index 86ddcb17312d..04df1e7aeca6 100644 --- a/tests/neg-custom-args/captures/usingLogFile.check +++ b/tests/neg-custom-args/captures/usingLogFile.check @@ -7,7 +7,6 @@ |where: => refers to a fresh root capability created in value later when checking argument to parameter op of method usingLogFile | ^ refers to the universal root capability | - | |Note that reference f.type |cannot be included in outer capture set ? | @@ -21,7 +20,6 @@ |where: => refers to a fresh root capability created in value later2 when checking argument to parameter op of method usingLogFile | ^ refers to the universal root capability | - | |Note that reference f.type |cannot be included in outer capture set ? | @@ -35,7 +33,6 @@ |where: => refers to a fresh root capability created in value later when checking argument to parameter op of method usingFile | ^ refers to the universal root capability | - | |Note that reference f.type |cannot be included in outer capture set ? | @@ -49,7 +46,6 @@ |where: => refers to a fresh root capability created in value later when checking argument to parameter op of method usingFile | ^ refers to the universal root capability | - | |Note that reference _$1.type |cannot be included in outer capture set ? | diff --git a/tests/neg-custom-args/captures/vars.check b/tests/neg-custom-args/captures/vars.check index d8b55afd298c..b6504e5e0029 100644 --- a/tests/neg-custom-args/captures/vars.check +++ b/tests/neg-custom-args/captures/vars.check @@ -27,7 +27,6 @@ | | where: ^ refers to the universal root capability | - | | Note that reference cap3.type | cannot be included in outer capture set ? 37 | def g(x: String): String = if cap3 == cap3 then "" else "a"