Three capture checking fixes

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

@@ -15,6 +15,7 @@ import printing.Texts.*
 import util.{SimpleIdentitySet, Property}
 import util.common.alwaysTrue
 import scala.collection.mutable
+import config.Config.ccAllowUnsoundMaps
 
 /** A class for capture sets. Capture sets can be constants or variables.
  * Capture sets support inclusion constraints <:< where <:< is subcapturing.
@@ -183,9 +184,26 @@ sealed abstract class CaptureSet extends Showable:
  else Const(elems.filter(p))
  else Filtered(asVar, p)
 
- /** capture set obtained by applying `f` to all elements of the current capture set
+ /** Capture set obtained by applying `tm` to all elements of the current capture set
  * and joining the results. If the current capture set is a variable, the same
  * transformation is applied to all future additions of new elements.
+ *
+ * Note: We have a problem how we handle the situation where we have a mapped set
+ *
+ * cs2 = tm(cs1)
+ *
+ * and then the propagation solver adds a new element `x` to `cs2`. What do we
+ * know in this case about `cs1`? We can answer this question in a sound way only
+ * if `tm` is a bijection on capture references or it is idempotent on capture references.
+ * (see definition in IdempotentCapRefMap).
+ * If `tm` is a bijection we know that `tm^-1(x)` must be in `cs1`. If `tm` is idempotent
+ * one possible solution is that `x` is in `cs1`, which is what we assume in this case.
+ * That strategy is sound but not complete.
+ *
+ * If `tm` is some other map, we don't know how to handle this case. For now,
+ * we simply refuse to handle other maps. If they do need to be handled,
+ * `OtherMapped` provides some approximation to a solution, but it is neither
+ * sound nor complete.
  */
  def map(tm: TypeMap)(using Context): CaptureSet = tm match
  case tm: BiTypeMap =>
@@ -194,12 +212,15 @@ sealed abstract class CaptureSet extends Showable:
  if mappedElems == elems then this
  else Const(mappedElems)
  else BiMapped(asVar, tm, mappedElems)
+ case tm: IdentityCaptRefMap => this
  case _ =>
  val mapped = mapRefs(elems, tm, tm.variance)
  if isConst then
  if mapped.isConst && mapped.elems == elems then this
  else mapped
- else Mapped(asVar, tm, tm.variance, mapped)
+ else tm match
+ case tm: IdempotentCaptRefMap => Mapped(asVar, tm, tm.variance, mapped)
+ case _ if ccAllowUnsoundMaps => OtherMapped(asVar, tm, tm.variance, mapped)
 
  def substParams(tl: BindingType, to: List[Type])(using Context) =
  map(Substituters.SubstParamsMap(tl, to))
@@ -390,29 +411,26 @@ object CaptureSet:
  end DerivedVar
 
  /** A variable that changes when `source` changes, where all additional new elements are mapped
- * using ∪ { f(x) | x <- elems }
+ * using ∪ { f(x) | x <- elems }.
  */
  class Mapped private[CaptureSet]
  (val source: Var, tm: TypeMap, variance: Int, initial: CaptureSet)(using @constructorOnly ctx: Context)
  extends DerivedVar(initial.elems):
  addSub(initial)
  val stack = if debugSets then (new Throwable).getStackTrace().nn.take(20) else null
 
- private def whereCreated(using Context): String =
- if stack == null then ""
- else i"""
- |Stack trace of variable creation:"
- |${stack.mkString("\n")}"""
-
  override def addNewElems(newElems: Refs, origin: CaptureSet)(using Context, VarState): CompareResult =
+ addNewElemsImpl(newElems: Refs, origin: CaptureSet)
+ .andAlso(if origin ne source then source.tryInclude(newElems, this) else CompareResult.OK)
+ // `tm` is assumed idempotent, propagate back elems from image set.
+ // This is sound, since we know that for `r in newElems: tm(r) = r`, hence
+ // `r` is _one_ possible solution in `source` that would make an `r` appear in this set.
+ // It's not necessarily the only possible solultion, so the scheme is incomplete.
+
+ protected def addNewElemsImpl(newElems: Refs, origin: CaptureSet)(using Context, VarState): CompareResult =
  val added =
- if origin eq source then
- mapRefs(newElems, tm, variance)
- else
- if variance <= 0 && !origin.isConst && (origin ne initial) then
- report.warning(i"trying to add elems ${CaptureSet(newElems)} from unrecognized source $origin of mapped set $this$whereCreated")
- return CompareResult.fail(this)
- Const(newElems)
+ if origin eq source then mapRefs(newElems, tm, variance)
+ else Const(newElems)
  super.addNewElems(added.elems, origin)
  .andAlso {
  if added.isConst then CompareResult.OK
@@ -430,7 +448,34 @@ object CaptureSet:
  override def toString = s"Mapped$id($source, elems = $elems)"
  end Mapped
 
- class BiMapped private[CaptureSet]
+
+ /** Should be avoided as much as possible:
+ * A mapped set that uses neither a BiTypeMap nor an idempotent type map.
+ * In that case there's no much we can do.
+ * The patch does not propagate added elements back to source and rejects adding
+ * elements from variable sources in contra- and non-variant positions. In essence,
+ * we approximate types resulting from such maps by returning a possible super type
+ * from the actual type.
+ */
+ final class OtherMapped private[CaptureSet]
+ (source: Var, tm: TypeMap, variance: Int, initial: CaptureSet)(using @constructorOnly ctx: Context)
+ extends Mapped(source, tm, variance, initial):
+
+ private def whereCreated(using Context): String =
+ if stack == null then ""
+ else i"""
+ |Stack trace of variable creation:"
+ |${stack.mkString("\n")}"""
+
+ override def addNewElems(newElems: Refs, origin: CaptureSet)(using Context, VarState): CompareResult =
+ if variance <= 0 && !origin.isConst && (origin ne initial) && (origin ne source) then
+ report.warning(i"trying to add elems ${CaptureSet(newElems)} from unrecognized source $origin of mapped set $this$whereCreated")
+ CompareResult.fail(this)
+ else
+ addNewElemsImpl(newElems, origin)
+ end OtherMapped
+
+ final class BiMapped private[CaptureSet]
  (val source: Var, bimap: BiTypeMap, initialElems: Refs)(using @constructorOnly ctx: Context)
  extends DerivedVar(initialElems):
 
@@ -499,6 +544,15 @@ object CaptureSet:
  case _ =>
  false
 
+ /** A TypeMap with the property that every capture reference in the image
+ * of the map is mapped to itself. I.e. for all capture references r1, r2,
+ * if M(r1) == r2 then M(r2) == r2.
+ */
+ trait IdempotentCaptRefMap extends TypeMap
+
+ /** A TypeMap that is the identity on capture references */
+ trait IdentityCaptRefMap extends TypeMap
+
  type CompareResult = CompareResult.Type
 
  /** None = ok, Some(cs) = failure since not a subset of cs */
@@ -509,8 +563,8 @@ object CaptureSet:
  extension (result: Type)
  def isOK: Boolean = result eq OK
  def blocking: CaptureSet = result
- def show: String = if result.isOK then "OK" else result.toString
- def andAlso(op: Context ?=> Type)(using Context): Type = if result.isOK then op else result
+ def show(using Context): String = if result.isOK then "OK" else i"$result"
+ inline def andAlso(op: Context ?=> Type)(using Context): Type = if result.isOK then op else result
 
  class VarState:
  private val elemsMap: util.EqHashMap[Var, Refs] = new util.EqHashMap

compiler/src/dotty/tools/dotc/cc/Setup.scala

@@ -9,6 +9,7 @@ import Types.*, StdNames.*
 import config.Printers.capt
 import ast.tpd
 import transform.Recheck.*
+import CaptureSet.IdentityCaptRefMap
 
 class Setup(
  preRecheckPhase: DenotTransformer,

compiler/src/dotty/tools/dotc/config/Config.scala

@@ -231,4 +231,10 @@ object Config {
  * If false, print them in the form `T @retains(c)`.
  */
  inline val printCaptureSetsAsPrefix = true
+
+ /** If true, allow mappping capture set variables under -Ycc with maps that are neither
+ * bijective nor idempotent. We currently do now know how to do this correctly in all
+ * cases, though.
+ */
+ inline val ccAllowUnsoundMaps = false
 }

compiler/src/dotty/tools/dotc/core/Substituters.scala

@@ -1,6 +1,8 @@
-package dotty.tools.dotc.core
+package dotty.tools.dotc
+package core
 
 import Types._, Symbols._, Contexts._
+import cc.CaptureSet.IdempotentCaptRefMap
 
 /** Substitution operations on types. See the corresponding `subst` and
  * `substThis` methods on class Type for an explanation.
@@ -191,11 +193,11 @@ object Substituters:
  def apply(tp: Type): Type = substRecThis(tp, from, to, this)(using mapCtx)
  }
 
- final class SubstParamMap(from: ParamRef, to: Type)(using Context) extends DeepTypeMap {
+ final class SubstParamMap(from: ParamRef, to: Type)(using Context) extends DeepTypeMap, IdempotentCaptRefMap {
  def apply(tp: Type): Type = substParam(tp, from, to, this)(using mapCtx)
  }
 
- final class SubstParamsMap(from: BindingType, to: List[Type])(using Context) extends DeepTypeMap {
+ final class SubstParamsMap(from: BindingType, to: List[Type])(using Context) extends DeepTypeMap, IdempotentCaptRefMap {
  def apply(tp: Type): Type = substParams(tp, from, to, this)(using mapCtx)
  }
 

compiler/src/dotty/tools/dotc/core/TypeApplications.scala

@@ -11,6 +11,7 @@ import util.Stats._
 import Names._
 import Flags.Module
 import dotty.tools.dotc.config.Config
+import cc.CaptureSet.IdentityCaptRefMap
 
 object TypeApplications {
 

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

@@ -772,8 +772,17 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
  false
  }
  compareTypeBounds
- case CapturingType(parent2, _, _) =>
- recur(tp1, parent2) || fourthTry
+ case CapturingType(parent2, refs2, _) =>
+ def compareCaptured =
+ val refs1 = tp1.captureSet
+ try
+ if refs1.isAlwaysEmpty then recur(tp1, parent2)
+ else subCaptures(refs1, refs2, frozenConstraint).isOK
+ && recur(tp1.widen.stripCapturing, parent2)
+ catch case ex: AssertionError =>
+ println(i"assertion failed while compare captured $tp1 <:< $tp2")
+ throw ex
+ compareCaptured || fourthTry
  case tp2: AnnotatedType if tp2.isRefining =>
  (tp1.derivesAnnotWith(tp2.annot.sameAnnotation) || tp1.isBottomType) &&
  recur(tp1, tp2.parent)

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}
-import CaptureSet.CompareResult
+import CaptureSet.{CompareResult, IdempotentCaptRefMap, IdentityCaptRefMap}
 
 import scala.annotation.internal.sharable
 import scala.annotation.threadUnsafe
@@ -56,7 +56,7 @@ object TypeOps:
  }
 
  /** The TypeMap handling the asSeenFrom */
- class AsSeenFromMap(pre: Type, cls: Symbol)(using Context) extends ApproximatingTypeMap {
+ class AsSeenFromMap(pre: Type, cls: Symbol)(using Context) extends ApproximatingTypeMap, IdempotentCaptRefMap {
  /** Set to true when the result of `apply` was approximated to avoid an unstable prefix. */
  var approximated: Boolean = false
 
@@ -192,7 +192,7 @@ object TypeOps:
  }
  }
 
- class SimplifyMap(using Context) extends TypeMap {
+ class SimplifyMap(using Context) extends IdentityCaptRefMap {
  def apply(tp: Type): Type = simplify(tp, this)
  }
 
@@ -426,7 +426,7 @@ object TypeOps:
  }
 
  /** An approximating map that drops NamedTypes matching `toAvoid` and wildcard types. */
- abstract class AvoidMap(using Context) extends AvoidWildcardsMap:
+ abstract class AvoidMap(using Context) extends AvoidWildcardsMap, IdempotentCaptRefMap:
  @threadUnsafe lazy val localParamRefs = util.HashSet[Type]()
 
  def toAvoid(tp: NamedType): Boolean

compiler/src/dotty/tools/dotc/core/Types.scala

@@ -36,7 +36,7 @@ import config.Printers.{core, typr, matchTypes}
 import reporting.{trace, Message}
 import java.lang.ref.WeakReference
 import cc.{CapturingType, CaptureSet, derivedCapturingType, retainedElems, isBoxedCapturing, CapturingKind, EventuallyCapturingType}
-import CaptureSet.CompareResult
+import CaptureSet.{CompareResult, IdempotentCaptRefMap, IdentityCaptRefMap}
 
 import scala.annotation.internal.sharable
 import scala.annotation.threadUnsafe
@@ -3686,7 +3686,7 @@ object Types {
 
  override def resultType(using Context): Type =
  if (dependencyStatus == FalseDeps) { // dealias all false dependencies
- val dealiasMap = new TypeMap {
+ val dealiasMap = new TypeMap with IdentityCaptRefMap {
  def apply(tp: Type) = tp match {
  case tp @ TypeRef(pre, _) =>
  tp.info match {
@@ -3799,22 +3799,12 @@ object Types {
  /** The least supertype of `resultType` that does not contain parameter dependencies */
  def nonDependentResultApprox(using Context): Type =
  if isResultDependent then
- val dropDependencies = new ApproximatingTypeMap {
+ val dropDependencies = new ApproximatingTypeMap with IdempotentCaptRefMap {
  def apply(tp: Type) = tp match {
  case tp @ TermParamRef(`thisLambdaType`, _) =>
  range(defn.NothingType, atVariance(1)(apply(tp.underlying)))
  case CapturingType(parent, refs, boxed) =>
- val parent1 = this(parent)
- val elems1 = refs.elems.filter {
- case tp @ TermParamRef(`thisLambdaType`, _) => false
- case _ => true
- }
- if elems1.size == refs.elems.size then
- derivedCapturingType(tp, parent1, refs)
- else
- range(
- CapturingType(parent1, CaptureSet(elems1), boxed),
- CapturingType(parent1, CaptureSet.universal, boxed))
+ mapOver(tp)
  case AnnotatedType(parent, ann) if ann.refersToParamOf(thisLambdaType) =>
  val parent1 = mapOver(parent)
  if ann.symbol == defn.RetainsAnnot || ann.symbol == defn.RetainsByNameAnnot then

compiler/src/dotty/tools/dotc/reporting/messages.scala

@@ -25,6 +25,7 @@ import ast.Trees._
 import ast.untpd
 import ast.tpd
 import transform.SymUtils._
+import cc.CaptureSet.IdentityCaptRefMap
 
 /** Messages
  * ========
@@ -250,7 +251,7 @@ import transform.SymUtils._
  // the type mismatch on the bounds instead of the original TypeParamRefs, since
  // these are usually easier to analyze. We exclude F-bounds since these would
  // lead to a recursive infinite expansion.
- object reported extends TypeMap:
+ object reported extends TypeMap, IdentityCaptRefMap:
  def setVariance(v: Int) = variance = v
  val constraint = mapCtx.typerState.constraint
  var fbounded = false

compiler/src/dotty/tools/dotc/typer/CheckCaptures.scala

@@ -15,7 +15,7 @@ import transform.SymUtils.*
 import transform.{Recheck, PreRecheck}
 import Recheck.*
 import scala.collection.mutable
-import CaptureSet.withCaptureSetsExplained
+import CaptureSet.{withCaptureSetsExplained, IdempotentCaptRefMap}
 import StdNames.nme
 import reporting.trace
 
@@ -40,7 +40,7 @@ object CheckCaptures:
  def isOpen = !captured.isAlwaysEmpty && !isBoxed
 
  final class SubstParamsMap(from: BindingType, to: List[Type])(using Context)
- extends ApproximatingTypeMap:
+ extends ApproximatingTypeMap, IdempotentCaptRefMap:
  def apply(tp: Type): Type = tp match
  case tp: ParamRef =>
  if tp.binder == from then to(tp.paramNum) else tp
@@ -408,17 +408,18 @@ class CheckCaptures extends Recheck, SymTransformer:
  tree.symbol.info
  case _ =>
  NoType
- if typeToCheck.exists then
- typeToCheck.widenDealias match
- case wtp @ CapturingType(parent, refs, _) =>
- refs.disallowRootCapability { () =>
- val kind = if tree.isInstanceOf[ValDef] then "mutable variable" else "expression"
- report.error(
- em"""The $kind's type $wtp is not allowed to capture the root capability `*`.
- |This usually means that a capability persists longer than its allowed lifetime.""",
- tree.srcPos)
- }
- case _ =>
+ def checkNotUniversal(tp: Type): Unit = tp.widenDealias match
+ case wtp @ CapturingType(parent, refs, _) =>
+ refs.disallowRootCapability { () =>
+ val kind = if tree.isInstanceOf[ValDef] then "mutable variable" else "expression"
+ report.error(
+ em"""The $kind's type $wtp is not allowed to capture the root capability `*`.
+ |This usually means that a capability persists longer than its allowed lifetime.""",
+ tree.srcPos)
+ }
+ checkNotUniversal(parent)
+ case _ =>
+ checkNotUniversal(typeToCheck)
  super.recheckFinish(tpe, tree, pt)
 
  /** This method implements the rule outlined in #14390: