From f14c19f64a1ec2f4c21691f450fb96286714ea4c Mon Sep 17 00:00:00 2001 From: odersky Date: Thu, 18 Jul 2024 12:24:14 +0200 Subject: [PATCH] Give some explanation of a capture set was under-approximated --- .../src/dotty/tools/dotc/cc/CaptureOps.scala | 3 ++- .../src/dotty/tools/dotc/cc/CaptureSet.scala | 15 +++++++++--- .../dotty/tools/dotc/cc/CapturingType.scala | 2 +- .../dotty/tools/dotc/cc/CheckCaptures.scala | 23 ++++++++++++++++++- .../captures/class-contra.check | 7 ++++-- .../captures/explain-under-approx.check | 20 ++++++++++++++++ .../captures/explain-under-approx.scala | 17 ++++++++++++++ 7 files changed, 79 insertions(+), 8 deletions(-) create mode 100644 tests/neg-custom-args/captures/explain-under-approx.check create mode 100644 tests/neg-custom-args/captures/explain-under-approx.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index 116b35e34aea..1f19641e3b08 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -244,7 +244,8 @@ 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, frozen = true).isOK + if (cs.isAlwaysEmpty || cs.isConst && cs.subCaptures(tp.captureSet, frozen = true).isOK) + && !cs.keepAlways then tp else tp match case CapturingType(parent, cs1) => parent.capturing(cs1 ++ cs) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index 7b639ee64cdf..690d9b4411aa 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -88,6 +88,8 @@ sealed abstract class CaptureSet extends Showable: final def isUnboxable(using Context) = elems.exists(elem => elem.isRootCapability || Existential.isExistentialVar(elem)) + final def keepAlways: Boolean = this.isInstanceOf[EmptyWithProvenance] + /** 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. @@ -219,7 +221,8 @@ sealed abstract class CaptureSet extends Showable: * `this` and `that` */ def ++ (that: CaptureSet)(using Context): CaptureSet = - if this.subCaptures(that, frozen = true).isOK then that + if this.subCaptures(that, frozen = true).isOK then + if that.isAlwaysEmpty && this.keepAlways then this else that else if that.subCaptures(this, frozen = true).isOK then this else if this.isConst && that.isConst then Const(this.elems ++ that.elems) else Union(this, that) @@ -294,7 +297,7 @@ sealed abstract class CaptureSet extends Showable: case _ => val mapped = mapRefs(elems, tm, tm.variance) if isConst then - if mapped.isConst && mapped.elems == elems then this + if mapped.isConst && mapped.elems == elems && !mapped.keepAlways then this else mapped else Mapped(asVar, tm, tm.variance, mapped) @@ -398,6 +401,12 @@ object CaptureSet: override def toString = elems.toString end Const + case class EmptyWithProvenance(ref: CaptureRef, mapped: Type) extends Const(SimpleIdentitySet.empty): + override def optionalInfo(using Context): String = + if ctx.settings.YccDebug.value + then i" under-approximating the result of mapping $ref to $mapped" + else "" + /** A special capture set that gets added to the types of symbols that were not * themselves capture checked, in order to admit arbitrary corresponding capture * sets in subcapturing comparisons. Similar to platform types for explicit @@ -863,7 +872,7 @@ object CaptureSet: || upper.isConst && upper.elems.size == 1 && upper.elems.contains(r1) || r.derivesFrom(defn.Caps_CapSet) if variance > 0 || isExact then upper - else if variance < 0 then CaptureSet.empty + else if variance < 0 then CaptureSet.EmptyWithProvenance(r, r1) else upper.maybe /** Apply `f` to each element in `xs`, and join result sets with `++` */ diff --git a/compiler/src/dotty/tools/dotc/cc/CapturingType.scala b/compiler/src/dotty/tools/dotc/cc/CapturingType.scala index f859b0d110aa..bb79e52f1060 100644 --- a/compiler/src/dotty/tools/dotc/cc/CapturingType.scala +++ b/compiler/src/dotty/tools/dotc/cc/CapturingType.scala @@ -33,7 +33,7 @@ object CapturingType: * boxing status is the same or if A is boxed. */ def apply(parent: Type, refs: CaptureSet, boxed: Boolean = false)(using Context): Type = - if refs.isAlwaysEmpty then parent + if refs.isAlwaysEmpty && !refs.keepAlways then parent else parent match case parent @ CapturingType(parent1, refs1) if boxed || !parent.isBoxed => apply(parent1, refs ++ refs1, boxed) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 667d91a10330..511c978a8e32 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -990,6 +990,25 @@ class CheckCaptures extends Recheck, SymTransformer: | |Note that ${msg.toString}""" + private def addApproxAddenda(using Context) = + new TypeAccumulator[Addenda]: + def apply(add: Addenda, t: Type) = t match + case CapturingType(t, CaptureSet.EmptyWithProvenance(ref, mapped)) => + /* val (origCore, kind) = original match + case tp @ AnnotatedType(parent, ann) if ann.hasSymbol(defn.ReachCapabilityAnnot) => + (parent, " deep") + case _ => + (original, "")*/ + add ++ new Addenda: + override def toAdd(using Context): List[String] = + i""" + | + |Note that a capability $ref in a capture set appearing in contravariant position + |was mapped to $mapped which is not a capability. Therefore, it was under-approximated to the empty set.""" + :: Nil + case _ => + foldOver(add, t) + /** Massage `actual` and `expected` types before checking conformance. * Massaging is done by the methods following this one: * - align dependent function types and add outer references in the expected type @@ -1015,7 +1034,9 @@ class CheckCaptures extends Recheck, SymTransformer: else capt.println(i"conforms failed for ${tree}: $actual vs $expected") err.typeMismatch(tree.withType(actualBoxed), expected1, - addenda ++ CaptureSet.levelErrors ++ boxErrorAddenda(boxErrors)) + addApproxAddenda( + addenda ++ CaptureSet.levelErrors ++ boxErrorAddenda(boxErrors), + expected1)) actual end checkConformsExpr diff --git a/tests/neg-custom-args/captures/class-contra.check b/tests/neg-custom-args/captures/class-contra.check index 6d4c89f872ad..9fc009ac3d48 100644 --- a/tests/neg-custom-args/captures/class-contra.check +++ b/tests/neg-custom-args/captures/class-contra.check @@ -1,7 +1,10 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/class-contra.scala:12:39 --------------------------------- 12 | def fun(x: K{val f: T^{a}}) = x.setf(a) // error | ^ - | Found: (a : T^{x, y}) - | Required: T + | Found: (a : T^{x, y}) + | Required: T^{} + | + | Note that a capability (K.this.f : T^) in a capture set appearing in contravariant position + | was mapped to (x.f : T^{a}) which is not a capability. Therefore, it was under-approximated to the empty set. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/explain-under-approx.check b/tests/neg-custom-args/captures/explain-under-approx.check new file mode 100644 index 000000000000..2d2b05b4b95a --- /dev/null +++ b/tests/neg-custom-args/captures/explain-under-approx.check @@ -0,0 +1,20 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/explain-under-approx.scala:12:10 ------------------------- +12 | col.add(Future(() => 25)) // error + | ^^^^^^^^^^^^^^^^ + | Found: Future[Int]{val a: (async : Async^)}^{async} + | Required: Future[Int]^{} + | + | Note that a capability Collector.this.futs* in a capture set appearing in contravariant position + | was mapped to col.futs* which is not a capability. Therefore, it was under-approximated to the empty set. + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/explain-under-approx.scala:15:11 ------------------------- +15 | col1.add(Future(() => 25)) // error + | ^^^^^^^^^^^^^^^^ + | Found: Future[Int]{val a: (async : Async^)}^{async} + | Required: Future[Int]^{} + | + | Note that a capability Collector.this.futs* in a capture set appearing in contravariant position + | was mapped to col1.futs* which is not a capability. Therefore, it was under-approximated to the empty set. + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/explain-under-approx.scala b/tests/neg-custom-args/captures/explain-under-approx.scala new file mode 100644 index 000000000000..816465e4af34 --- /dev/null +++ b/tests/neg-custom-args/captures/explain-under-approx.scala @@ -0,0 +1,17 @@ +trait Async extends caps.Capability + +class Future[+T](x: () => T)(using val a: Async) + +class Collector[T](val futs: Seq[Future[T]^]): + def add(fut: Future[T]^{futs*}) = ??? + +def main() = + given async: Async = ??? + val futs = (1 to 20).map(x => Future(() => x)) + val col = Collector(futs) + col.add(Future(() => 25)) // error + val col1: Collector[Int] { val futs: Seq[Future[Int]^{async}] } + = Collector(futs) + col1.add(Future(() => 25)) // error + +