diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index c3c743a7c8f5..6a12bb62902d 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -152,10 +152,39 @@ object Capabilities: val hiddenSet = CaptureSet.HiddenSet(owner, this: @unchecked) // fails initialization check without the @unchecked + /** Is this fresh cap (definitely) classified? If that's the case, the + * classifier cannot be changed anymore. + * We need to distinguish `FreshCap`s that can still be classified from + * ones that cannot. Once a `FreshCap` is part of a constant capture set, + * it gets classified by the type that prefixes the set and that classification + * cannot be changed anymore. But other `FreshCap`s are created as members of + * variable sets and then their classification status is open and can be + * constrained further. + */ + private[Capabilities] var isClassified = false + override def equals(that: Any) = that match case that: FreshCap => this eq that case _ => false + /** Is this fresh cap at the right level to be able to subsume `ref`? + */ + def acceptsLevelOf(ref: Capability)(using Context): Boolean = + if ccConfig.useFreshLevels && !CCState.collapseFresh then + val refOwner = ref.levelOwner + refOwner.isStaticOwner || ccOwner.isContainedIn(refOwner) + else ref.core match + case ResultCap(_) | _: ParamRef => false + case _ => true + + /** Classify this FreshCap as `cls`, provided `isClassified` is still false. + * @param freeze Deterermines future `isClassified` state. + */ + def adoptClassifier(cls: ClassSymbol, freeze: Boolean)(using Context): Unit = + if !isClassified then + hiddenSet.adoptClassifier(cls) + if freeze then isClassified = true + def descr(using Context) = val originStr = origin match case Origin.InDecl(sym) if sym.exists => @@ -477,7 +506,7 @@ object Capabilities: def derivesFromCapability(using Context): Boolean = derivesFromCapTrait(defn.Caps_Capability) def derivesFromMutable(using Context): Boolean = derivesFromCapTrait(defn.Caps_Mutable) - def derivesFromSharable(using Context): Boolean = derivesFromCapTrait(defn.Caps_Sharable) + def derivesFromShared(using Context): Boolean = derivesFromCapTrait(defn.Caps_SharedCapability) /** The capture set consisting of exactly this reference */ def singletonCaptureSet(using Context): CaptureSet.Const = @@ -495,7 +524,11 @@ object Capabilities: def isProvisional = this.core match case core: TypeProxy => !core.underlying.exists || core.underlying.isProvisional case _ => false - if !isCaptureChecking || ctx.mode.is(Mode.IgnoreCaptures) || isProvisional then + if !ccConfig.cacheCaptureSetOfInfo + || !isCaptureChecking + || ctx.mode.is(Mode.IgnoreCaptures) + || isProvisional + then myCaptureSet = null else myCaptureSet = computed @@ -524,7 +557,8 @@ object Capabilities: case Reach(_) => captureSetOfInfo.transClassifiers case self: CoreCapability => - joinClassifiers(toClassifiers(self.classifier), captureSetOfInfo.transClassifiers) + if self.derivesFromCapability then toClassifiers(self.classifier) + else captureSetOfInfo.transClassifiers if myClassifiers != UnknownClassifier then classifiersValid == currentId myClassifiers @@ -534,7 +568,8 @@ object Capabilities: cls == defn.AnyClass || this.match case self: FreshCap => - self.hiddenSet.tryClassifyAs(cls) + if self.isClassified then self.hiddenSet.classifier.derivesFrom(cls) + else self.hiddenSet.tryClassifyAs(cls) case self: RootCapability => true case Restricted(_, cls1) => @@ -547,8 +582,8 @@ object Capabilities: case Reach(_) => captureSetOfInfo.tryClassifyAs(cls) case self: CoreCapability => - self.classifier.isSubClass(cls) - && captureSetOfInfo.tryClassifyAs(cls) + if self.derivesFromCapability then self.derivesFrom(cls) + else captureSetOfInfo.tryClassifyAs(cls) def isKnownClassifiedAs(cls: ClassSymbol)(using Context): Boolean = transClassifiers match @@ -677,7 +712,7 @@ object Capabilities: case _ => true vs.ifNotSeen(this)(x.hiddenSet.elems.exists(_.subsumes(y))) - || levelOK + || x.acceptsLevelOf(y) && ( y.tryClassifyAs(x.hiddenSet.classifier) || { capt.println(i"$y cannot be classified as $x"); false } ) @@ -686,7 +721,7 @@ object Capabilities: case x: ResultCap => val result = y match case y: ResultCap => vs.unify(x, y) - case _ => y.derivesFromSharable + case _ => y.derivesFromShared if !result then TypeComparer.addErrorNote(CaptureSet.ExistentialSubsumesFailure(x, y)) result @@ -696,7 +731,7 @@ object Capabilities: case _: ResultCap => false case _: FreshCap if CCState.collapseFresh => true case _ => - y.derivesFromSharable + y.derivesFromShared || canAddHidden && vs != VarState.HardSeparate && CCState.capIsRoot case Restricted(x1, cls) => y.isKnownClassifiedAs(cls) && x1.maxSubsumes(y, canAddHidden) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index cd8615f0f8d5..e759ec2fc2c8 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -378,7 +378,8 @@ extension (tp: Type) def derivesFromCapability(using Context): Boolean = derivesFromCapTrait(defn.Caps_Capability) def derivesFromMutable(using Context): Boolean = derivesFromCapTrait(defn.Caps_Mutable) - def derivesFromSharedCapability(using Context): Boolean = derivesFromCapTrait(defn.Caps_Sharable) + def derivesFromShared(using Context): Boolean = derivesFromCapTrait(defn.Caps_SharedCapability) + def derivesFromExclusive(using Context): Boolean = derivesFromCapTrait(defn.Caps_ExclusiveCapability) /** Drop @retains annotations everywhere */ def dropAllRetains(using Context): Type = // TODO we should drop retains from inferred types before unpickling @@ -401,9 +402,12 @@ extension (tp: Type) if variance <= 0 then t else t.dealias match case t @ CapturingType(p, cs) if cs.containsCapOrFresh => - change = true val reachRef = if cs.isReadOnly then ref.reach.readOnly else ref.reach - t.derivedCapturingType(apply(p), reachRef.singletonCaptureSet) + if reachRef.singletonCaptureSet.mightSubcapture(cs) then + change = true + t.derivedCapturingType(apply(p), reachRef.singletonCaptureSet) + else + t case t @ AnnotatedType(parent, ann) => // Don't map annotations, which includes capture sets t.derivedAnnotatedType(this(parent), ann) @@ -599,6 +603,11 @@ extension (sym: Symbol) if sym.is(Method) && sym.owner.isClass then isReadOnlyMethod else sym.owner.isInReadOnlyMethod + def qualString(prefix: String)(using Context): String = + if !sym.exists then "" + else if sym.isAnonymousFunction then i" $prefix enclosing function" + else i" $prefix $sym" + extension (tp: AnnotatedType) /** Is this a boxed capturing type? */ def isBoxed(using Context): Boolean = tp.annot match @@ -647,7 +656,9 @@ object OnlyCapability: def unapply(tree: AnnotatedType)(using Context): Option[(Type, ClassSymbol)] = tree match case AnnotatedType(parent: Type, ann) if ann.hasSymbol(defn.OnlyCapabilityAnnot) => - Some((parent, ann.tree.tpe.argTypes.head.classSymbol.asClass)) + ann.tree.tpe.argTypes.head.classSymbol match + case cls: ClassSymbol => Some((parent, cls)) + case _ => None case _ => None end OnlyCapability diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index bdb7a774ca51..cb3102679943 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -263,13 +263,19 @@ 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 + CCState.withCollapsedFresh: + // withCollapsedFresh should be dropped. The problem is that since our level checking + // does not deal with classes well, we get false negatives here. Observed in the line + // + // stateFromIteratorConcatSuffix(it)(flatMapImpl(rest, f).state)))) + // + // in cc-lib's LazyListIterable.scala. TypeComparer.noNotes: elems.exists(_.subsumes(x)(using ctx)(using VarState.ClosedUnrecorded)) || !x.isTerminalCapability && { - val elems = x.captureSetOfInfo.elems - !elems.isEmpty && elems.forall(mightAccountFor) + val xelems = x.captureSetOfInfo.elems + !xelems.isEmpty && xelems.forall(mightAccountFor) } /** A more optimistic version of subCaptures used to choose one of two typing rules @@ -436,9 +442,18 @@ sealed abstract class CaptureSet extends Showable: def adoptClassifier(cls: ClassSymbol)(using Context): Unit = for elem <- elems do elem.stripReadOnly match - case fresh: FreshCap => fresh.hiddenSet.adoptClassifier(cls) + case fresh: FreshCap => fresh.adoptClassifier(cls, freeze = isConst) case _ => + /** All capabilities of this set except those Termrefs and FreshCaps that + * are bound by `mt`. + */ + def freeInResult(mt: MethodicType)(using Context): CaptureSet = + filter: + case TermParamRef(binder, _) => binder ne mt + case ResultCap(binder) => binder ne mt + case _ => true + /** A bad root `elem` is inadmissible as a member of this set. What is a bad roots depends * on the value of `rootLimit`. * If the limit is null, all capture roots are good. @@ -611,9 +626,13 @@ object CaptureSet: then i" under-approximating the result of mapping $ref to $mapped" else "" + private def capImpliedByCapability(parent: Type)(using Context): Capability = + if parent.derivesFromExclusive then GlobalCap.readOnly else GlobalCap + /* The same as {cap.rd} but generated implicitly for references of Capability subtypes. */ - case class CSImpliedByCapability() extends Const(SimpleIdentitySet(GlobalCap.readOnly)) + class CSImpliedByCapability(parent: Type)(using @constructorOnly ctx: Context) + extends Const(SimpleIdentitySet(capImpliedByCapability(parent))) /** 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 @@ -692,6 +711,9 @@ object CaptureSet: */ private[CaptureSet] var rootLimit: Symbol | Null = null + def isBadRoot(elem: Capability)(using Context): Boolean = + isBadRoot(rootLimit, elem) + private var myClassifier: ClassSymbol = defn.AnyClass def classifier: ClassSymbol = myClassifier @@ -743,13 +765,14 @@ object CaptureSet: else if !levelOK(elem) then failWith(IncludeFailure(this, elem, levelError = true)) // or `elem` is not visible at the level of the set. else if !elem.tryClassifyAs(classifier) then + //println(i"cannot classify $elem as $classifier, ${elem.asInstanceOf[CoreCapability].classifier}") failWith(IncludeFailure(this, elem)) else // id == 108 then assert(false, i"trying to add $elem to $this") assert(elem.isWellformed, elem) assert(!this.isInstanceOf[HiddenSet] || summon[VarState].isSeparating, summon[VarState]) includeElem(elem) - if isBadRoot(rootLimit, elem) then + if isBadRoot(elem) then rootAddedHandler() val normElem = if isMaybeSet then elem else elem.stripMaybe // assert(id != 5 || elems.size != 3, this) @@ -778,7 +801,7 @@ object CaptureSet: case _ => foldOver(b, t) find(false, binder) - private def levelOK(elem: Capability)(using Context): Boolean = elem match + def levelOK(elem: Capability)(using Context): Boolean = elem match case _: FreshCap => !level.isDefined || ccState.symLevel(elem.ccOwner) <= level @@ -1246,7 +1269,13 @@ object CaptureSet: * when a subsumes check decides that an existential variable `ex` cannot be * instantiated to the other capability `other`. */ - case class ExistentialSubsumesFailure(val ex: ResultCap, val other: Capability) extends ErrorNote + case class ExistentialSubsumesFailure(val ex: ResultCap, val other: Capability) extends ErrorNote: + def description(using Context): String = + def reason = + if other.isTerminalCapability then "" + else " since that capability is not a `Sharable` capability" + i"""the existential capture root in ${ex.originalBinder.resType} + |cannot subsume the capability $other$reason.""" /** Failure indicating that `elem` cannot be included in `cs` */ case class IncludeFailure(cs: CaptureSet, elem: Capability, levelError: Boolean = false) extends ErrorNote, Showable: @@ -1258,6 +1287,38 @@ object CaptureSet: res.myTrace = cs1 :: this.myTrace res + def description(using Context): String = + def why = + val reasons = cs.elems.toList.collect: + case c: FreshCap if !c.acceptsLevelOf(elem) => + i"$elem${elem.levelOwner.qualString("in")} is not visible from $c${c.ccOwner.qualString("in")}" + case c: FreshCap if !elem.tryClassifyAs(c.hiddenSet.classifier) => + i"$c is classified as ${c.hiddenSet.classifier} but $elem is not" + if reasons.isEmpty then "" + else reasons.mkString("\nbecause ", "\nand ", "") + cs match + case cs: Var => + if !cs.levelOK(elem) then + val levelStr = elem match + case ref: TermRef => i", defined in ${ref.symbol.maybeOwner}" + case _ => "" + i"""capability ${elem}$levelStr + |cannot be included in outer capture set $cs""" + else if !elem.tryClassifyAs(cs.classifier) then + i"""capability ${elem} is not classified as ${cs.classifier}, therefore it + |cannot be included in capture set $cs of ${cs.classifier} elements""" + else if cs.isBadRoot(elem) then + elem match + case elem: FreshCap => + i"""local capability $elem created in ${elem.ccOwner} + |cannot be included in outer capture set $cs""" + case _ => + i"universal capability $elem cannot be included in capture set $cs" + else + i"capability $elem cannot be included in capture set $cs" + case _ => + i"capability $elem is not included in capture set $cs$why" + override def toText(printer: Printer): Text = inContext(printer.printerContext): if levelError then @@ -1274,7 +1335,11 @@ object CaptureSet: * @param lo the lower type of the orginal type comparison, or NoType if not known * @param hi the upper type of the orginal type comparison, or NoType if not known */ - case class MutAdaptFailure(cs: CaptureSet, lo: Type = NoType, hi: Type = NoType) extends ErrorNote + case class MutAdaptFailure(cs: CaptureSet, lo: Type = NoType, hi: Type = NoType) extends ErrorNote: + def description(using Context): String = + def ofType(tp: Type) = if tp.exists then i"of the mutable type $tp" else "of a mutable type" + i"""$cs is an exclusive capture set ${ofType(hi)}, + |it cannot subsume a read-only capture set ${ofType(lo)}.""" /** A VarState serves as a snapshot mechanism that can undo * additions of elements or super sets if an operation fails @@ -1487,14 +1552,10 @@ object CaptureSet: // `ref` will not seem subsumed by other capabilities in a `++`. universal case c: CoreCapability => - ofType(c.underlying, followResult = false) + ofType(c.underlying, followResult = true) /** Capture set of a type * @param followResult If true, also include capture sets of function results. - * This mode is currently not used. It could be interesting - * when we change the system so that the capture set of a function - * is the union of the capture sets if its span. - * In this case we should use `followResult = true` in the call in ofInfo above. */ def ofType(tp: Type, followResult: Boolean)(using Context): CaptureSet = def recur(tp: Type): CaptureSet = trace(i"ofType $tp, ${tp.getClass} $followResult", show = true): @@ -1510,13 +1571,9 @@ object CaptureSet: recur(parent) ++ refs case tp @ AnnotatedType(parent, ann) if ann.symbol.isRetains => recur(parent) ++ ann.tree.toCaptureSet - case tpd @ defn.RefinedFunctionOf(rinfo: MethodType) if followResult => + case tpd @ defn.RefinedFunctionOf(rinfo: MethodOrPoly) if followResult => ofType(tpd.parent, followResult = false) // pick up capture set from parent type - ++ recur(rinfo.resType) // add capture set of result - .filter: - case TermParamRef(binder, _) => binder ne rinfo - case ResultCap(binder) => binder ne rinfo - case _ => true + ++ recur(rinfo.resType).freeInResult(rinfo) // add capture set of result case tpd @ AppliedType(tycon, args) => if followResult && defn.isNonRefinedFunction(tpd) then recur(args.last) diff --git a/compiler/src/dotty/tools/dotc/cc/CapturingType.scala b/compiler/src/dotty/tools/dotc/cc/CapturingType.scala index 1cafe295f529..b9545bf39b8b 100644 --- a/compiler/src/dotty/tools/dotc/cc/CapturingType.scala +++ b/compiler/src/dotty/tools/dotc/cc/CapturingType.scala @@ -40,7 +40,6 @@ object CapturingType: apply(parent1, refs ++ refs1, boxed) case _ => if parent.derivesFromMutable then refs.setMutable() - val classifier = parent.classifier refs.adoptClassifier(parent.classifier) AnnotatedType(parent, CaptureAnnotation(refs, boxed)(defn.RetainsAnnot)) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index c0c42bbdb32f..4db8d0920b33 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -67,9 +67,6 @@ object CheckCaptures: val res = cur cur = cur.outer res - - def ownerString(using Context): String = - if owner.isAnonymousFunction then "enclosing function" else owner.show end Env /** Similar normal substParams, but this is an approximating type map that @@ -491,10 +488,10 @@ class CheckCaptures extends Recheck, SymTransformer: case _ => c.core match case c1: RootCapability => c1.singletonCaptureSet case c1: CoreCapability => - CaptureSet.ofType(c1.widen, followResult = false) + CaptureSet.ofType(c1.widen, followResult = true) capt.println(i"Widen reach $c to $underlying in ${env.owner}") underlying.disallowRootCapability(NoSymbol): () => - report.error(em"Local capability $c in ${env.ownerString} cannot have `cap` as underlying capture set", tree.srcPos) + report.error(em"Local capability $c${env.owner.qualString("in")} cannot have `cap` as underlying capture set", tree.srcPos) recur(underlying, env, lastEnv) /** Avoid locally defined capability if it is a reach capability or capture set @@ -548,9 +545,8 @@ class CheckCaptures extends Recheck, SymTransformer: case ref: NamedType if !ref.symbol.isUseParam => val what = if ref.isType then "Capture set parameter" else "Local reach capability" val owner = ref.symbol.owner - val ownerStr = if owner.isAnonymousFunction then "enclosing function" else owner.show report.error( - em"""$what $c leaks into capture scope of $ownerStr. + em"""$what $c leaks into capture scope${owner.qualString("of")}. |To allow this, the ${ref.symbol} should be declared with a @use annotation""", pos) case _ => @@ -704,7 +700,6 @@ class CheckCaptures extends Recheck, SymTransformer: capt.println(i"pick one of $qualType, ${selType.widen}, $qualCs, $selCs ${selWiden.captureSet} in $tree") if qualCs.mightSubcapture(selCs) - //&& !selCs.mightSubcapture(qualCs) && !pt.stripCapturing.isInstanceOf[SingletonType] then selWiden.stripCapturing.capturing(qualCs) @@ -927,28 +922,22 @@ class CheckCaptures extends Recheck, SymTransformer: val paramType = freshToCap(paramTpt.nuType) checkConformsExpr(argType, paramType, param) .showing(i"compared expected closure formal $argType against $param with ${paramTpt.nuType}", capt) - if ccConfig.preTypeClosureResults && !(isEtaExpansion(mdef) && ccConfig.handleEtaExpansionsSpecially) then - // Check whether the closure's result conforms to the expected type - // This constrains parameter types of the closure which can give better - // error messages. - // But if the closure is an eta expanded method reference it's better to not constrain + if !pt.isInstanceOf[RefinedType] + && !(isEtaExpansion(mdef) && ccConfig.handleEtaExpansionsSpecially) + then + // If the closure is not an eta expansion and the expected type is a parametric + // function type, check whether the closure's result conforms to the expected + // result type. This constrains parameter types of the closure which can give better + // error messages. It also prevents mapping fresh to result caps in the closure's + // result type. + // If the closure is an eta expanded method reference it's better to not constrain // its internals early since that would give error messages in generated code // which are less intelligible. An example is the line `a = x` in // neg-custom-args/captures/vars.scala. That's why this code is conditioned. // to apply only to closures that are not eta expansions. assert(paramss1.isEmpty) - val respt0 = pt match - case defn.RefinedFunctionOf(rinfo) => - val paramTypes = params.map(_.asInstanceOf[ValDef].tpt.nuType) - rinfo.instantiate(paramTypes) - case _ => - resType - val respt = resultToFresh(respt0, Origin.LambdaExpected(respt0)) - val res = resultToFresh(mdef.tpt.nuType, Origin.LambdaActual(mdef.tpt.nuType)) - // We need to open existentials here in order not to get vars mixed up in them - // We do the proper check with existentials when we are finished with the closure block. - capt.println(i"pre-check closure $expr of type $res against $respt") - checkConformsExpr(res, respt, expr) + capt.println(i"pre-check closure $expr of type ${mdef.tpt.nuType} against $resType") + checkConformsExpr(mdef.tpt.nuType, resType, expr) case _ => case Nil => @@ -1278,37 +1267,11 @@ 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: - case IncludeFailure(_, _, true) => true - case _: ExistentialSubsumesFailure | _: MutAdaptFailure => true - case _ => false - if printableNotes.isEmpty then NothingToAdd + if notes.isEmpty then NothingToAdd else new Addenda: - override def toAdd(using Context) = printableNotes.map: note => - val msg = note match - case IncludeFailure(cs, ref, _) => - if ref.core.isCapOrFresh then - i"""the universal capability $ref - |cannot be included in capture set $cs""" - else - val levelStr = ref match - case ref: TermRef => i", defined in ${ref.symbol.maybeOwner}" - case _ => "" - i"""reference ${ref}$levelStr - |cannot be included in outer capture set $cs""" - case ExistentialSubsumesFailure(ex, other) => - def since = - if other.isTerminalCapability then "" - else " since that capability is not a `Sharable` capability" - i"""the existential capture root in ${ex.originalBinder.resType} - |cannot subsume the capability $other$since""" - case MutAdaptFailure(cs, lo, hi) => - def ofType(tp: Type) = if tp.exists then i"of the mutable type $tp" else "of a mutable type" - i"""$cs is an exclusive capture set ${ofType(hi)}, - |it cannot subsume a read-only capture set ${ofType(lo)}.""" + override def toAdd(using Context) = notes.map: note => i""" - |Note that ${msg.toString}""" - + |Note that ${note.description}.""" /** Addendas for error messages that show where we have under-approximated by * mapping a a capability in contravariant position to the empty set because @@ -1580,11 +1543,9 @@ class CheckCaptures extends Recheck, SymTransformer: private def improveCaptures(widened: Type, prefix: Type)(using Context): Type = prefix match case ref: Capability if ref.isTracked => widened match - case widened @ CapturingType(p, refs) if ref.singletonCaptureSet.mightSubcapture(refs) => - val improvedCs = - if widened.isBoxed then ref.reach.singletonCaptureSet - else ref.singletonCaptureSet - widened.derivedCapturingType(p, improvedCs) + case widened @ CapturingType(p, refs) + if ref.singletonCaptureSet.mightSubcapture(refs) && !widened.isBoxed => + widened.derivedCapturingType(p, ref.singletonCaptureSet) .showing(i"improve $widened to $result", capt) case _ => widened case _ => widened diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index be71fe82dc72..f5589caf3872 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -186,7 +186,7 @@ object SepCheck: if seen.contains(newElem) then recur(seen, acc, newElems1) else newElem.stripRestricted.stripReadOnly match - case elem: FreshCap => + case elem: FreshCap if !elem.isKnownClassifiedAs(defn.Caps_SharedCapability) => if elem.hiddenSet.deps.isEmpty then recur(seen + newElem, acc + newElem, newElems1) else val superCaps = @@ -612,7 +612,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: val badParams = mutable.ListBuffer[Symbol]() def currentOwner = role.dclSym.orElse(ctx.owner) for hiddenRef <- refsToCheck.deductSymRefs(role.dclSym).deduct(explicitRefs(tpe)) do - if !hiddenRef.derivesFromSharable then + if !hiddenRef.isKnownClassifiedAs(defn.Caps_SharedCapability) then hiddenRef.pathRoot match case ref: TermRef => val refSym = ref.symbol @@ -649,7 +649,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: role match case _: TypeRole.Argument | _: TypeRole.Qualifier => for ref <- refsToCheck do - if !ref.derivesFromSharable then + if !ref.isKnownClassifiedAs(defn.Caps_SharedCapability) then consumed.put(ref, pos) case _ => end checkConsumedRefs diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala index 1a9d86c7d645..2b5b1adb9b31 100644 --- a/compiler/src/dotty/tools/dotc/cc/Setup.scala +++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala @@ -375,14 +375,6 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: else fntpe /** 1. Check that parents of capturing types are not pure. - * 2. Check that types extending caps.Sharable don't have a `cap` in their capture set. - * TODO: Is this enough? - * We need to also track that we cannot get exclusive capabilities in paths - * where some prefix derives from Sharable. Also, can we just - * exclude `cap`, or do we have to extend this to all exclusive capabilties? - * The problem is that we know what is exclusive in general only after capture - * checking, not before. - * But maybe the rules for classification already cover these cases. */ def checkRetainsOK(tp: Type): tp.type = tp match @@ -393,8 +385,6 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: // an explicit result type in the override, the inherited capture set // will be ignored anyway. fail(em"$parent is a pure type, it makes no sense to add a capture set to it") - else if refs.isUniversal && parent.derivesFromSharedCapability then - fail(em"$tp extends Sharable, so it cannot capture `cap`") case _ => tp @@ -410,7 +400,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: then normalizeCaptures(mapOver(t)) match case t1 @ CapturingType(_, _) => t1 - case t1 => CapturingType(t1, CaptureSet.CSImpliedByCapability(), boxed = false) + case t1 => CapturingType(t1, CaptureSet.CSImpliedByCapability(t1), boxed = false) else normalizeCaptures(mapFollowingAliases(t)) def innerApply(t: Type) = diff --git a/compiler/src/dotty/tools/dotc/cc/ccConfig.scala b/compiler/src/dotty/tools/dotc/cc/ccConfig.scala index 4cc2264c12cb..8498760bf649 100644 --- a/compiler/src/dotty/tools/dotc/cc/ccConfig.scala +++ b/compiler/src/dotty/tools/dotc/cc/ccConfig.scala @@ -7,11 +7,8 @@ import config.{Feature, SourceVersion} object ccConfig: - /** If enabled, use a special path in recheckClosure for closures - * to compare the result tpt of the anonymous functon with the expected - * result type. This can narrow the scope of error messages. - */ - inline val preTypeClosureResults = false + /** If enabled, cache capture sets of infos capabilties */ + inline val cacheCaptureSetOfInfo = false /** If this and `preTypeClosureResults` are both enabled, disable `preTypeClosureResults` * for eta expansions. This can improve some error messages. diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala index 8cc5aac942a6..c5dd4662a7b8 100644 --- a/compiler/src/dotty/tools/dotc/core/Definitions.scala +++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala @@ -1003,6 +1003,12 @@ class Definitions { @tu lazy val CapsModule: Symbol = requiredPackage("scala.caps") @tu lazy val captureRoot: TermSymbol = CapsModule.requiredValue("cap") @tu lazy val Caps_Capability: ClassSymbol = requiredClass("scala.caps.Capability") + @tu lazy val Caps_Classifier: ClassSymbol = requiredClass("scala.caps.Classifier") + @tu lazy val Caps_SharedCapability: ClassSymbol = requiredClass("scala.caps.SharedCapability") + @tu lazy val Caps_ExclusiveCapability: ClassSymbol = requiredClass("scala.caps.ExclusiveCapability") + @tu lazy val Caps_Control: ClassSymbol = requiredClass("scala.caps.Control") + @tu lazy val Caps_Mutable: ClassSymbol = requiredClass("scala.caps.Mutable") + @tu lazy val Caps_Read: ClassSymbol = requiredClass("scala.caps.Read") @tu lazy val Caps_CapSet: ClassSymbol = requiredClass("scala.caps.CapSet") @tu lazy val CapsInternalModule: Symbol = requiredModule("scala.caps.internal") @tu lazy val Caps_erasedValue: Symbol = CapsInternalModule.requiredMethod("erasedValue") @@ -1013,10 +1019,6 @@ class Definitions { @tu lazy val Caps_ContainsTrait: TypeSymbol = CapsModule.requiredType("Contains") @tu lazy val Caps_ContainsModule: Symbol = requiredModule("scala.caps.Contains") @tu lazy val Caps_containsImpl: TermSymbol = Caps_ContainsModule.requiredMethod("containsImpl") - @tu lazy val Caps_Mutable: ClassSymbol = requiredClass("scala.caps.Mutable") - @tu lazy val Caps_Sharable: ClassSymbol = requiredClass("scala.caps.Sharable") - @tu lazy val Caps_Control: ClassSymbol = requiredClass("scala.caps.Control") - @tu lazy val Caps_Classifier: ClassSymbol = requiredClass("scala.caps.Classifier") @tu lazy val PureClass: ClassSymbol = requiredClass("scala.Pure") @@ -2110,10 +2112,10 @@ class Definitions { @tu lazy val ccExperimental: Set[Symbol] = Set( CapsModule, CapsModule.moduleClass, PureClass, Caps_Capability, // TODO: Remove when Capability is stabilized + Caps_Classifier, Caps_SharedCapability, Caps_Control, Caps_ExclusiveCapability, Caps_Mutable, Caps_Read, RequiresCapabilityAnnot, captureRoot, Caps_CapSet, Caps_ContainsTrait, Caps_ContainsModule, Caps_ContainsModule.moduleClass, UseAnnot, - Caps_Mutable, Caps_Sharable, Caps_Control, Caps_Classifier, ConsumeAnnot, - CapsUnsafeModule, CapsUnsafeModule.moduleClass, + ConsumeAnnot, CapsUnsafeModule, CapsUnsafeModule.moduleClass, CapsInternalModule, CapsInternalModule.moduleClass, RetainsAnnot, RetainsCapAnnot, RetainsByNameAnnot) diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala index 7f8f8a34c171..ce56bc976ee0 100644 --- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala @@ -3361,6 +3361,9 @@ object TypeComparer { */ def kind: Class[?] = getClass + def description(using Context): String + end ErrorNote + /** A richer compare result, returned by `testSubType` and `test`. */ enum CompareResult: case OK, OKwithGADTUsed, OKwithOpaquesUsed diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala index a6f59d8b2d33..9ca45cb25397 100644 --- a/compiler/src/dotty/tools/dotc/core/Types.scala +++ b/compiler/src/dotty/tools/dotc/core/Types.scala @@ -3743,6 +3743,7 @@ object Types extends TypeUtils { // is that most poly types are cyclic via poly params, // and therefore two different poly types would never be equal. + /** Common base trait of MethodType, PolyType and ExprType */ trait MethodicType extends TermType: def resType: Type diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala index 03bffc65fbc7..437929c79160 100644 --- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala +++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala @@ -284,9 +284,9 @@ class PlainPrinter(_ctx: Context) extends Printer { case tp @ CapturingType(parent, refs) => val boxText: Text = Str("box ") provided tp.isBoxed && ccVerbose if elideCapabilityCaps - && parent.derivesFrom(defn.Caps_Capability) + && parent.derivesFromCapability && refs.containsTerminalCapability - && refs.isReadOnly + && (!parent.derivesFromExclusive || refs.isReadOnly) then toText(parent) else toTextCapturing(parent, refs, boxText) case tp @ RetainingType(parent, refSet) => diff --git a/library/src/scala/caps/package.scala b/library/src/scala/caps/package.scala index 2f466af166e3..3cb0d5a0251c 100644 --- a/library/src/scala/caps/package.scala +++ b/library/src/scala/caps/package.scala @@ -21,9 +21,11 @@ import annotation.{experimental, compileTimeOnly, retainsCap} * is turned on. * But even without capture checking, extending this trait can be useful for documenting the intended purpose * of a class. + * + * Capability has exactly two subtraits: Shared and Exclusive. */ @experimental -trait Capability extends Any +sealed trait Capability extends Any /** A marker trait for classifier capabilities that can appear in `.only` * qualifiers. Capability classes directly extending `Classifier` are treated @@ -36,21 +38,36 @@ trait Classifier @experimental object cap extends Capability -/** Marker trait for classes with methods that requires an exclusive reference. */ +/** Marker trait for capabilities that can be safely shared in a concurrent context. + * During separation checking, shared capabilities are not taken into account. + */ @experimental -trait Mutable extends Capability, Classifier +trait SharedCapability extends Capability, Classifier -/** Marker trait for capabilities that can be safely shared in a concurrent context. - * During separation checking, shared capabilities are not taken into account. - */ @experimental -trait Sharable extends Capability, Classifier +type Shared = SharedCapability + +/** Marker trait for exclusive capabilities that are separation-checked + */ +@experimental +trait ExclusiveCapability extends Capability, Classifier + +@experimental +type Exclusive = ExclusiveCapability /** Base trait for capabilities that capture some continuation or return point in * the stack. Examples are exceptions, labels, Async, CanThrow. */ @experimental -trait Control extends Sharable, Classifier +trait Control extends SharedCapability, Classifier + +/** Marker trait for classes with methods that require an exclusive reference. */ +@experimental +trait Mutable extends ExclusiveCapability, Classifier + +/** Marker trait for classes with reader methods, typically extended by Mutable classes */ +@experimental +trait Read extends Mutable, Classifier /** Carrier trait for capture set type parameters */ @experimental diff --git a/tests/disabled/pos/lazylist.scala b/tests/disabled/pos/lazylist.scala index e56eb484894c..62bb4889eb19 100644 --- a/tests/disabled/pos/lazylist.scala +++ b/tests/disabled/pos/lazylist.scala @@ -34,7 +34,7 @@ object LazyNil extends LazyList[Nothing]: def map[A, B](xs: {*} LazyList[A], f: {*} A => B): {f, xs} LazyList[B] = xs.map(f) -class Cap extends caps.Capability +class Cap extends caps.SharedCapability def test(cap1: Cap, cap2: Cap, cap3: Cap) = def f[T](x: LazyList[T]): LazyList[T] = if cap1 == cap1 then x else LazyNil diff --git a/tests/neg-custom-args/captures/box-adapt-cases.check b/tests/neg-custom-args/captures/box-adapt-cases.check index 330fd196023b..5cbceb1d6c64 100644 --- a/tests/neg-custom-args/captures/box-adapt-cases.check +++ b/tests/neg-custom-args/captures/box-adapt-cases.check @@ -3,6 +3,7 @@ | ^^^^^^^^^^^^^^^^ | Found: (cap: Cap^{io}) ->{io} Int | Required: Cap^{io} -> Int + | Note that capability (io : Cap^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/box-adapt-cases.scala:29:10 ------------------------------ @@ -10,5 +11,6 @@ | ^^^^^^^^^^^^^^^^ | Found: (cap: Cap^?) ->{io, fs} Int | Required: Cap^{io, fs} ->{io} Int + | Note that capability (fs : Cap^) is not included in capture set {io}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/branding.scala b/tests/neg-custom-args/captures/branding.scala index b59677487eb5..9d5ad25e82bc 100644 --- a/tests/neg-custom-args/captures/branding.scala +++ b/tests/neg-custom-args/captures/branding.scala @@ -3,18 +3,18 @@ import caps.* def main() = - trait Channel[T] extends caps.Capability: + trait Channel[T] extends caps.SharedCapability: def send(msg: T): Unit def recv(): T - trait Logger extends caps.Capability: + trait Logger extends caps.SharedCapability: def log(msg: String): Unit // we can close over anything subsumed by the 'trusted' brand capability, but nothing else def runSecure[C^ >: {trusted} <: {trusted}](block: () ->{C} Unit): Unit = block() // This is a 'brand" capability to mark what can be mentioned in trusted code - object trusted extends caps.Capability + object trusted extends caps.SharedCapability val trustedLogger: Logger^{trusted} = ??? val trustedChannel: Channel[String]^{trusted} = ??? diff --git a/tests/neg-custom-args/captures/branding2.scala b/tests/neg-custom-args/captures/branding2.scala index c3091befdc25..f3d2001cf650 100644 --- a/tests/neg-custom-args/captures/branding2.scala +++ b/tests/neg-custom-args/captures/branding2.scala @@ -3,18 +3,18 @@ import caps.* def main() = - trait Channel[T] extends caps.Capability: + trait Channel[T] extends caps.SharedCapability: def send(msg: T): Unit def recv(): T - trait Logger extends caps.Capability: + trait Logger extends caps.SharedCapability: def log(msg: String): Unit // we can close over anything subsumed by the 'trusted' brand capability, but nothing else def runSecure(block: () ->{trusted} Unit): Unit = block() // This is a 'brand" capability to mark what can be mentioned in trusted code - object trusted extends caps.Capability + object trusted extends caps.SharedCapability val trustedLogger: Logger^{trusted} = ??? val trustedChannel: Channel[String]^{trusted} = ??? diff --git a/tests/neg-custom-args/captures/byname.check b/tests/neg-custom-args/captures/byname.check index f3ce717db467..152900a5b29a 100644 --- a/tests/neg-custom-args/captures/byname.check +++ b/tests/neg-custom-args/captures/byname.check @@ -12,12 +12,15 @@ | |where: ?=> refers to a fresh root capability created in method test when checking argument to parameter ff of method h | + |Note that capability (cap1 : Cap) is not included in capture set {cap2}. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/byname.scala:19:5 ---------------------------------------- 19 | h(g()) // error | ^^^ | Found: () ?->{cap2} I^? | Required: () ?->{cap1} I + | Note that capability (cap2 : Cap) is not included in capture set {cap1}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/byname.scala:22:5 ---------------------------------------- @@ -25,5 +28,6 @@ | ^^^^^^^^^ | Found: () ->{cap2} I^? | Required: () ->{cap1} I + | Note that capability (cap2 : Cap) is not included in capture set {cap1}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/byname.scala b/tests/neg-custom-args/captures/byname.scala index dd8fcf1b8818..569814b37185 100644 --- a/tests/neg-custom-args/captures/byname.scala +++ b/tests/neg-custom-args/captures/byname.scala @@ -1,4 +1,4 @@ -class Cap extends caps.Capability +class Cap extends caps.SharedCapability def test(cap1: Cap, cap2: Cap) = def f() = if cap1 == cap1 then g else g diff --git a/tests/neg-custom-args/captures/capt-box-env.scala b/tests/neg-custom-args/captures/capt-box-env.scala index bfe1874d073b..02fe459f67f1 100644 --- a/tests/neg-custom-args/captures/capt-box-env.scala +++ b/tests/neg-custom-args/captures/capt-box-env.scala @@ -1,4 +1,4 @@ -class Cap extends caps.Capability +class Cap extends caps.SharedCapability class Pair[+A, +B](x: A, y: B): def fst: A = x diff --git a/tests/neg-custom-args/captures/capt-box.scala b/tests/neg-custom-args/captures/capt-box.scala index 291882bed36d..0bc1624424c1 100644 --- a/tests/neg-custom-args/captures/capt-box.scala +++ b/tests/neg-custom-args/captures/capt-box.scala @@ -1,4 +1,4 @@ -class Cap extends caps.Capability +class Cap extends caps.SharedCapability def test(x: Cap) = diff --git a/tests/neg-custom-args/captures/capt-capability.scala b/tests/neg-custom-args/captures/capt-capability.scala index 0f293872da25..7813ad8144b8 100644 --- a/tests/neg-custom-args/captures/capt-capability.scala +++ b/tests/neg-custom-args/captures/capt-capability.scala @@ -1,7 +1,7 @@ -import caps.{Capability, Sharable} +import caps.{Capability, SharedCapability} def foo() = - val x: Sharable = ??? + val x: SharedCapability = ??? val z3 = if x == null then (y: Unit) => x else (y: Unit) => new Capability() {} // error diff --git a/tests/neg-custom-args/captures/capt-depfun.check b/tests/neg-custom-args/captures/capt-depfun.check index 369c9915bbe0..ee80bb335d61 100644 --- a/tests/neg-custom-args/captures/capt-depfun.check +++ b/tests/neg-custom-args/captures/capt-depfun.check @@ -6,4 +6,6 @@ | | where: => refers to a fresh root capability in the type of value dc | + | Note that capability (y : C^) is not included in capture set {}. + | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/capt-wf2.scala b/tests/neg-custom-args/captures/capt-wf2.scala index 8bb04a230fdd..30cb5d195805 100644 --- a/tests/neg-custom-args/captures/capt-wf2.scala +++ b/tests/neg-custom-args/captures/capt-wf2.scala @@ -1,4 +1,4 @@ -class C extends caps.Capability +class C extends caps.SharedCapability def test(c: C) = var x: Any^{c} = ??? diff --git a/tests/neg-custom-args/captures/capt1.check b/tests/neg-custom-args/captures/capt1.check index 5c1008190886..dc163dc75f6a 100644 --- a/tests/neg-custom-args/captures/capt1.check +++ b/tests/neg-custom-args/captures/capt1.check @@ -3,6 +3,7 @@ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | Found: () ->{x} C^? | Required: () -> C + | Note that capability (x : C^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:8:2 ------------------------------------------ @@ -10,6 +11,7 @@ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | Found: () ->{x} C^? | Required: Matchable + | Note that capability (x : C^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:15:2 ----------------------------------------- @@ -17,6 +19,7 @@ | ^ | Found: (y: Int) ->{x} Int | Required: Matchable + | Note that capability (x : C^) is not included in capture set {}. 16 | f | | longer explanation available when compiling with `-explain` @@ -25,6 +28,7 @@ | ^ | Found: A^{x} | Required: A + | Note that capability (x : C^) is not included in capture set {}. 23 | def m() = if x == null then y else y 24 | F(22) | @@ -34,6 +38,7 @@ | ^ | Found: A^{x} | Required: A + | Note that capability (x : C^) is not included in capture set {}. 28 | def m() = if x == null then y else y | | longer explanation available when compiling with `-explain` @@ -52,6 +57,8 @@ | |where: ^ refers to a fresh root capability created in value z2 when checking argument to parameter a of method h | + |Note that capability (x : C^) is not included in capture set {}. + | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/capt1.scala:38:13 ------------------------------------------------------------- 38 | val z3 = h[(() -> Cap) @retains[x.type]](() => x)(() => C()) // error diff --git a/tests/neg-custom-args/captures/capture-poly.scala b/tests/neg-custom-args/captures/capture-poly.scala index c0608ad812de..f7decbe5d437 100644 --- a/tests/neg-custom-args/captures/capture-poly.scala +++ b/tests/neg-custom-args/captures/capture-poly.scala @@ -1,6 +1,6 @@ import caps.* -trait Foo extends Capability +trait Foo extends SharedCapability trait CaptureSet: type C^ diff --git a/tests/neg-custom-args/captures/caseclass/Test_2.scala b/tests/neg-custom-args/captures/caseclass/Test_2.scala index 8c13a0d831ef..5d3f9aaa6524 100644 --- a/tests/neg-custom-args/captures/caseclass/Test_2.scala +++ b/tests/neg-custom-args/captures/caseclass/Test_2.scala @@ -1,4 +1,4 @@ -class C extends caps.Capability +class C extends caps.SharedCapability def test(c: C) = val pure: () -> Unit = () => () val impure: () => Unit = pure diff --git a/tests/neg-custom-args/captures/cc-existential-conformance.check b/tests/neg-custom-args/captures/cc-existential-conformance.check index 549e1c0543b5..c73e4c2e1193 100644 --- a/tests/neg-custom-args/captures/cc-existential-conformance.check +++ b/tests/neg-custom-args/captures/cc-existential-conformance.check @@ -9,6 +9,9 @@ | x is a value in method test | x² is a reference to a value parameter | + | Note that capability is not included in capture set {cap} + | because is not visible from cap in value y. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:9:29 -------------------- 9 | val z: A -> (x: A) -> B^ = y // error @@ -18,8 +21,7 @@ | | where: ^ 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 y* since that capability is not a `Sharable` capability + | Note that capability y* is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:13:19 ------------------- @@ -33,6 +35,9 @@ | x is a value in method test2 | x² is a reference to a value parameter | + | Note that capability is not included in capture set {cap} + | because is not visible from cap in value y. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:14:24 ------------------- 14 | val z: (x: A) -> B^ = y // error @@ -42,7 +47,6 @@ | | where: ^ 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 y* since that capability is not a `Sharable` capability + | Note that capability y* is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/cc-glb.check b/tests/neg-custom-args/captures/cc-glb.check index 669cf81a082b..1d978f834175 100644 --- a/tests/neg-custom-args/captures/cc-glb.check +++ b/tests/neg-custom-args/captures/cc-glb.check @@ -3,5 +3,6 @@ | ^^ | Found: (x1 : (Foo[T] & Foo[Any])^{io}) | Required: Foo[T] + | Note that capability (io : Cap^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/cc-poly-1.scala b/tests/neg-custom-args/captures/cc-poly-1.scala index b205b9b25246..a9894fd048a4 100644 --- a/tests/neg-custom-args/captures/cc-poly-1.scala +++ b/tests/neg-custom-args/captures/cc-poly-1.scala @@ -1,9 +1,9 @@ import language.experimental.captureChecking -import caps.{CapSet, Capability} +import caps.{CapSet, SharedCapability} object Test: - class C extends Capability + class C extends SharedCapability class D def f[X^](x: D^{X}): D^{X} = x diff --git a/tests/neg-custom-args/captures/cc-poly-2.check b/tests/neg-custom-args/captures/cc-poly-2.check index 28e0e1863760..0577b4f9d22b 100644 --- a/tests/neg-custom-args/captures/cc-poly-2.check +++ b/tests/neg-custom-args/captures/cc-poly-2.check @@ -6,11 +6,14 @@ | | where: ^ refers to a fresh root capability in the type of value d | + | Note that capability cap is not included in capture set {c1}. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-poly-2.scala:16:20 ------------------------------------ 16 | val _: D^{c1} = x // error | ^ | Found: (x : Test.D^{d}) | Required: Test.D^{c1} + | Note that capability (d : Test.D^) is not included in capture set {c1}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/cc-poly-2.scala b/tests/neg-custom-args/captures/cc-poly-2.scala index 8fb590f4f769..e7ce44f1bea4 100644 --- a/tests/neg-custom-args/captures/cc-poly-2.scala +++ b/tests/neg-custom-args/captures/cc-poly-2.scala @@ -1,9 +1,9 @@ import language.experimental.captureChecking -import caps.{CapSet, Capability} +import caps.{CapSet, SharedCapability} object Test: - class C extends Capability + class C extends SharedCapability class D def f[X^](x: D^{X}): D^{X} = x diff --git a/tests/neg-custom-args/captures/cc-poly-source.scala b/tests/neg-custom-args/captures/cc-poly-source.scala index 915903d670e8..6e67087cbeac 100644 --- a/tests/neg-custom-args/captures/cc-poly-source.scala +++ b/tests/neg-custom-args/captures/cc-poly-source.scala @@ -1,11 +1,11 @@ import language.experimental.captureChecking import annotation.experimental -import caps.{CapSet, Capability} +import caps.{CapSet, SharedCapability} import caps.use @experimental object Test: - class Label //extends Capability + class Label //extends SharedCapability class Listener @@ -30,7 +30,7 @@ import caps.use val listeners = lbls.map(makeListener) // error // we get an error here because we no longer allow contravariant cap // to subsume other capabilities. The problem can be solved by declaring - // Label a Sharable, see cc-poly-source-capability.scala + // Label a SharedCapability, see cc-poly-source-capability.scala val src = Source[{lbls*}] for l <- listeners do src.register(l) diff --git a/tests/neg-custom-args/captures/cc-this-shared.scala b/tests/neg-custom-args/captures/cc-this-shared.scala new file mode 100644 index 000000000000..769bae9b5ee6 --- /dev/null +++ b/tests/neg-custom-args/captures/cc-this-shared.scala @@ -0,0 +1,35 @@ +import caps.consume + +class Cap extends caps.SharedCapability + +def eff(using Cap): Unit = () + +def test(using Cap) = + + class C(val x: () => Int): + val y: C = this // error + + class C2(val x: () => Int): // error + this: C2 => + + class C3: + this: C3 => + val x: Object = this + + class C4(val f: () => Int) extends C3 // error + +// The following is a variation of pos/cc-this.scala +def test2(using @consume cc: Cap) = + + class C(val x: () => Int): + val y: C^ = this + + def f = () => + eff(using cc) + 1 + + def c1 = new C(f) + def c2 = c1 + def c3 = c2.y // was sepcheck error, but OK since we changed to SharedCapability + val c4: C^ = c3 + val _ = c3: C^ diff --git a/tests/neg-custom-args/captures/cc-this.check b/tests/neg-custom-args/captures/cc-this.check index 8e17901d1dcd..85040bbaa0b3 100644 --- a/tests/neg-custom-args/captures/cc-this.check +++ b/tests/neg-custom-args/captures/cc-this.check @@ -3,6 +3,7 @@ | ^^^^ | Found: (C.this : C^{C.this.x}) | Required: C + | Note that capability (C.this.x : () => Int) is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/cc-this.scala:12:15 ----------------------------------------------------------- diff --git a/tests/neg-custom-args/captures/cc-this.scala b/tests/neg-custom-args/captures/cc-this.scala index c64098c8f5b4..d90c0084a14f 100644 --- a/tests/neg-custom-args/captures/cc-this.scala +++ b/tests/neg-custom-args/captures/cc-this.scala @@ -1,6 +1,6 @@ import caps.consume -class Cap extends caps.Capability +class Cap extends caps.ExclusiveCapability def eff(using Cap): Unit = () diff --git a/tests/neg-custom-args/captures/cc-this3.scala b/tests/neg-custom-args/captures/cc-this3.scala index c3d751b12f67..948492eb8c3b 100644 --- a/tests/neg-custom-args/captures/cc-this3.scala +++ b/tests/neg-custom-args/captures/cc-this3.scala @@ -1,5 +1,5 @@ import language.experimental.captureChecking -class Cap extends caps.Capability +class Cap extends caps.SharedCapability def eff(using Cap): Unit = () diff --git a/tests/neg-custom-args/captures/cc-this4.check b/tests/neg-custom-args/captures/cc-this4.check index d97c304a9cd3..4e385b158ce8 100644 --- a/tests/neg-custom-args/captures/cc-this4.check +++ b/tests/neg-custom-args/captures/cc-this4.check @@ -6,4 +6,6 @@ | | where: ^ refers to the universal root capability | + | Note that capability cap is not included in capture set {}. + | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/cc-this5.check b/tests/neg-custom-args/captures/cc-this5.check index a69c482300f8..253ef3985af9 100644 --- a/tests/neg-custom-args/captures/cc-this5.check +++ b/tests/neg-custom-args/captures/cc-this5.check @@ -8,6 +8,7 @@ | ^^^^ | Found: (A.this : A^{c}) | Required: A + | Note that capability (c : Cap) is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E058] Type Mismatch Error: tests/neg-custom-args/captures/cc-this5.scala:7:9 --------------------------------------- diff --git a/tests/neg-custom-args/captures/cc-this5.scala b/tests/neg-custom-args/captures/cc-this5.scala index 4c9a8a706670..811b1e1f8922 100644 --- a/tests/neg-custom-args/captures/cc-this5.scala +++ b/tests/neg-custom-args/captures/cc-this5.scala @@ -1,7 +1,7 @@ class C: val x: C = this -class Cap extends caps.Capability +class Cap extends caps.SharedCapability def foo(c: Cap) = object D extends C: // error diff --git a/tests/neg-custom-args/captures/class-constr.scala b/tests/neg-custom-args/captures/class-constr.scala index 619fa9fa0341..e86263fb0714 100644 --- a/tests/neg-custom-args/captures/class-constr.scala +++ b/tests/neg-custom-args/captures/class-constr.scala @@ -1,6 +1,6 @@ import annotation.{capability, constructorOnly} -class Cap extends caps.Capability +class Cap extends caps.SharedCapability class C(x: Cap, @constructorOnly y: Cap) diff --git a/tests/neg-custom-args/captures/class-contra.check b/tests/neg-custom-args/captures/class-contra.check index 808118bd1795..1c2b7f8e2157 100644 --- a/tests/neg-custom-args/captures/class-contra.check +++ b/tests/neg-custom-args/captures/class-contra.check @@ -3,5 +3,6 @@ | ^ | Found: (a : T^{x, y}) | Required: T^{k.f} + | Note that capability (x : C^) is not included in capture set {k.f}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/class-level-attack.check b/tests/neg-custom-args/captures/class-level-attack.check index a2f60535d86f..9c22c305b1bd 100644 --- a/tests/neg-custom-args/captures/class-level-attack.check +++ b/tests/neg-custom-args/captures/class-level-attack.check @@ -13,4 +13,7 @@ | | where: ^ refers to a fresh root capability in the type of value r | + | Note that capability (x : IO^) is not included in capture set {cap} + | because (x : IO^) in method set is not visible from cap in value r. + | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/classified-inheritance.scala b/tests/neg-custom-args/captures/classified-inheritance.scala index 11f342d314a7..3aef8bd5e35d 100644 --- a/tests/neg-custom-args/captures/classified-inheritance.scala +++ b/tests/neg-custom-args/captures/classified-inheritance.scala @@ -1,6 +1,6 @@ import language.experimental.captureChecking -class C1 extends caps.Control, caps.Sharable // OK +class C1 extends caps.Control, caps.SharedCapability // OK class C2 extends caps.Control, caps.Mutable // error diff --git a/tests/neg-custom-args/captures/classified-wf.scala b/tests/neg-custom-args/captures/classified-wf.scala index 98a61b2d7b7d..40e458e7f61e 100644 --- a/tests/neg-custom-args/captures/classified-wf.scala +++ b/tests/neg-custom-args/captures/classified-wf.scala @@ -1,8 +1,8 @@ import caps.* -class Async extends Capability +class Async extends SharedCapability -class IO extends Capability, Classifier +class IO extends SharedCapability, Classifier def foo(x: Object^{cap.only[Async]}) = ??? // error def bar(x: Object^{cap.only[IO]}) = ??? // ok diff --git a/tests/neg-custom-args/captures/classifiers-secondclass.scala b/tests/neg-custom-args/captures/classifiers-secondclass.scala index c4378df5f9a5..20b898726cfb 100644 --- a/tests/neg-custom-args/captures/classifiers-secondclass.scala +++ b/tests/neg-custom-args/captures/classifiers-secondclass.scala @@ -5,8 +5,8 @@ import caps.* // Test inspired by the "Gentrification Gone too Far?" paper object Levels: - trait Read extends Classifier, Capability - trait ReadWrite extends Classifier, Capability + trait Read extends Classifier, SharedCapability + trait ReadWrite extends Classifier, SharedCapability trait File(val name: String): val r: Read^ diff --git a/tests/neg-custom-args/captures/contracap.check b/tests/neg-custom-args/captures/contracap.check index e2a3e0958674..65af3d27cf1d 100644 --- a/tests/neg-custom-args/captures/contracap.check +++ b/tests/neg-custom-args/captures/contracap.check @@ -1,9 +1,11 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/contracap.scala:15:48 ------------------------------------ 15 | val g: (Ref[Int]^{a}, Ref[Int]^{a}) -> Unit = f // error | ^ - | Found: (f : (Ref[Int]^, Ref[Int]^) -> Unit) - | Required: (Ref[Int]^{a}, Ref[Int]^{a}) -> Unit + | Found: (f : (Ref[Int]^, Ref[Int]^) -> Unit) + | Required: (Ref[Int]^{a}, Ref[Int]^{a}) -> Unit | - | where: ^ refers to the universal root capability + | where: ^ refers to the universal root capability + | + | Note that capability (a : Ref[Int]^) is not included in capture set {cap}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/dcs-tvar.check b/tests/neg-custom-args/captures/dcs-tvar.check index 65fc12f82ba0..9e700c8ab989 100644 --- a/tests/neg-custom-args/captures/dcs-tvar.check +++ b/tests/neg-custom-args/captures/dcs-tvar.check @@ -3,6 +3,7 @@ | ^^^^^^^^^^^^^^^^ | Found: () ->{xs*} Unit | Required: () -> Unit + | Note that capability xs* is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/dcs-tvar.scala:9:2 --------------------------------------- @@ -10,5 +11,6 @@ | ^^^^^^^^^^^^^^^^ | Found: () ->{xs*} Unit | Required: () -> Unit + | Note that capability xs* is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/delayedRunops.check b/tests/neg-custom-args/captures/delayedRunops.check index 5554a32bc10e..8172f8300b91 100644 --- a/tests/neg-custom-args/captures/delayedRunops.check +++ b/tests/neg-custom-args/captures/delayedRunops.check @@ -3,6 +3,7 @@ | ^ | Found: () ->{ops*} Unit | Required: () -> Unit + | Note that capability ops* is not included in capture set {}. 16 | val ops1 = ops 17 | runOps(ops1) | @@ -12,6 +13,7 @@ | ^ | Found: () ->{ops*} Unit | Required: () -> Unit + | Note that capability ops* is not included in capture set {}. 28 | val ops1: List[() ->{ops*} Unit] = ops 29 | runOps(ops1) | diff --git a/tests/neg-custom-args/captures/depfun-reach.check b/tests/neg-custom-args/captures/depfun-reach.check index b6ab88b020ed..446ba4151c9a 100644 --- a/tests/neg-custom-args/captures/depfun-reach.check +++ b/tests/neg-custom-args/captures/depfun-reach.check @@ -6,6 +6,8 @@ | |where: => refers to a fresh root capability created in anonymous function of type (): Unit when checking argument to parameter op of method foreach | + |Note that capability op* cannot be included in capture set {} of value f. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/depfun-reach.scala:19:4 ---------------------------------- 19 | op // error @@ -16,6 +18,8 @@ | where: => refers to a fresh root capability in the type of parameter op | =>² refers to a fresh root capability in the result type of method foo | + | Note that capability cap is not included in capture set {cap}. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/depfun-reach.scala:26:60 --------------------------------- 26 | val b: (xs: List[() ->{io} Unit]) => List[() ->{} Unit] = a // error @@ -26,4 +30,6 @@ | where: => refers to a fresh root capability in the type of value a | =>² refers to a fresh root capability in the type of value b | + | Note that capability cap is not included in capture set {cap}. + | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/effect-swaps-explicit.check b/tests/neg-custom-args/captures/effect-swaps-explicit.check index 04aebe522a1e..4b38fb01d207 100644 --- a/tests/neg-custom-args/captures/effect-swaps-explicit.check +++ b/tests/neg-custom-args/captures/effect-swaps-explicit.check @@ -4,6 +4,7 @@ | ^ | Found: Result.Ok[Future[T^?]^{fr, contextual$1}] | Required: Result[Future[T], Nothing] + | Note that capability (fr : Future[Result[T, E]]^) is not included in capture set {}. 65 | fr.await.ok |-------------------------------------------------------------------------------------------------------------------- |Inline stack trace @@ -23,8 +24,8 @@ |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 ? + |Note that capability contextual$9.type + |cannot be included in outer capture set ?. 70 | fr.await.ok | | longer explanation available when compiling with `-explain` @@ -36,6 +37,8 @@ | |where: ?=> refers to a fresh root capability created in method fail5 when checking argument to parameter body of method make | ^ refers to the universal root capability + | + |Note that capability (fr : Future[Result[T, E]]^) is not included in capture set {}. 74 | Future: fut ?=> 75 | fr.await.ok | diff --git a/tests/neg-custom-args/captures/effect-swaps-explicit.scala b/tests/neg-custom-args/captures/effect-swaps-explicit.scala index 56ab856a7782..54e6bc1f1a34 100644 --- a/tests/neg-custom-args/captures/effect-swaps-explicit.scala +++ b/tests/neg-custom-args/captures/effect-swaps-explicit.scala @@ -2,7 +2,7 @@ object boundary: - final class Label[-T] // extends caps.Capability + final class Label[-T] // extends caps.SharedCapability /** Abort current computation and instead return `value` as the value of * the enclosing `boundary` call that created `label`. @@ -14,7 +14,7 @@ end boundary import boundary.{Label, break} -trait Async extends caps.Sharable +trait Async extends caps.SharedCapability object Async: def blocking[T](body: Async ?=> T): T = ??? diff --git a/tests/neg-custom-args/captures/effect-swaps.check b/tests/neg-custom-args/captures/effect-swaps.check index 1efe26c5182f..25b3247ea161 100644 --- a/tests/neg-custom-args/captures/effect-swaps.check +++ b/tests/neg-custom-args/captures/effect-swaps.check @@ -4,6 +4,7 @@ | ^ | Found: Result.Ok[Future[T^?]^{fr, contextual$1}] | Required: Result[Future[T], Nothing] + | Note that capability (fr : Future[Result[T, E]]^) is not included in capture set {}. 65 | fr.await.ok |-------------------------------------------------------------------------------------------------------------------- |Inline stack trace @@ -18,13 +19,13 @@ 69 | Future: fut ?=> // error, type mismatch | ^ |Found: (contextual$9: boundary.Label[Result[Future[T^?]^?, E^?]^?]^?) ?->{fr, async} Future[T^?]^{fr, contextual$9} - |Required: (boundary.Label[Result[Future[T^?]^?, E^?]]^{cap.rd}) ?=> Future[T^?]^? + |Required: (boundary.Label[Result[Future[T^?]^?, E^?]]^) ?=> Future[T^?]^? | |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 + | ^ refers to the universal root capability | - |Note that reference contextual$9.type - |cannot be included in outer capture set ? + |Note that capability contextual$9.type + |cannot be included in outer capture set ?. 70 | fr.await.ok | | longer explanation available when compiling with `-explain` @@ -32,10 +33,12 @@ 73 | Result.make[Future[T], E]: lbl ?=> // error: type mismatch | ^ |Found: (lbl: boundary.Label[Result[Future[T^?]^?, E^?]^?]^?) ?->{fr, async} Future[T^?]^{fr, lbl} - |Required: (boundary.Label[Result[Future[T], E]]^{cap.rd}) ?=> Future[T] + |Required: (boundary.Label[Result[Future[T], E]]^) ?=> Future[T] | |where: ?=> refers to a fresh root capability created in method fail5 when checking argument to parameter body of method make - | cap is the universal root capability + | ^ refers to the universal root capability + | + |Note that capability (fr : Future[Result[T, E]]^) is not included in capture set {}. 74 | Future: fut ?=> 75 | fr.await.ok | diff --git a/tests/neg-custom-args/captures/effect-swaps.scala b/tests/neg-custom-args/captures/effect-swaps.scala index 27d84d27e556..90f5ffcb5e21 100644 --- a/tests/neg-custom-args/captures/effect-swaps.scala +++ b/tests/neg-custom-args/captures/effect-swaps.scala @@ -2,7 +2,7 @@ object boundary: - final class Label[-T] extends caps.Capability + final class Label[-T] extends caps.SharedCapability /** Abort current computation and instead return `value` as the value of * the enclosing `boundary` call that created `label`. @@ -14,7 +14,7 @@ end boundary import boundary.{Label, break} -trait Async extends caps.Sharable +trait Async extends caps.SharedCapability object Async: def blocking[T](body: Async ?=> T): T = ??? diff --git a/tests/neg-custom-args/captures/erased-methods2.check b/tests/neg-custom-args/captures/erased-methods2.check deleted file mode 100644 index 8e163795f94b..000000000000 --- a/tests/neg-custom-args/captures/erased-methods2.check +++ /dev/null @@ -1,36 +0,0 @@ --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/erased-methods2.scala:20:4 ------------------------------- -20 | = (x$1: CT[Ex3]^) // error - | ^ - |Found: (erased x$1: CT[Ex3]^) ?->? (erased x$2: CT[Ex2]^?) ?->{x$1} Unit - |Required: (erased x$1: CT[Ex3]^) ?=> (erased x$2: CT[Ex2]^) ?=>² Unit - | - |where: ?=> refers to a fresh root capability in the result type of method foo9a - | ?=>² 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 `Sharable` capability -21 | ?=> (x$2: CT[Ex2]^) -22 | ?=> -23 | //given (CT[Ex3]^) = x$1 -24 | Throw(new Ex3) - | - | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/erased-methods2.scala:31:4 ------------------------------- -31 | = (erased x$1: CT[Ex3]^) // error - | ^ - |Found: (erased x$1: CT[Ex3]^) ?->? (erased x$1: CT[Ex2]^?) ?->{x$1} (erased x$2: CT[Ex1]^?) ?->{x$1} Unit - |Required: (erased x$1: CT[Ex3]^) ?=> (erased x$1: CT[Ex2]^) ?=>² (erased x$2: CT[Ex1]^) ?=>³ Unit - | - |where: ?=> refers to a fresh root capability in the result type of method foo10a - | ?=>² refers to a root capability associated with the result type of (using erased x$1: CT[Ex3]^): (erased x$1: CT[Ex2]^) ?=>² (erased x$2: CT[Ex1]^) ?=>³ Unit - | ?=>³ 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 `Sharable` capability -32 | ?=> (erased x$2: CT[Ex2]^) -33 | ?=> (erased x$3: CT[Ex1]^) -34 | ?=> Throw(new Ex3) - | - | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/erased-methods2.scala b/tests/neg-custom-args/captures/erased-methods2.scala index 4eda00d1b4ac..7db94919e578 100644 --- a/tests/neg-custom-args/captures/erased-methods2.scala +++ b/tests/neg-custom-args/captures/erased-methods2.scala @@ -1,3 +1,4 @@ +// was a neg test before import language.experimental.saferExceptions import language.experimental.erasedDefinitions import language.experimental.captureChecking @@ -6,7 +7,7 @@ class Ex1 extends Exception("Ex1") class Ex2 extends Exception("Ex2") class Ex3 extends Exception("Ex3") -class CT[-E <: Exception] extends caps.Capability, compiletime.Erased +class CT[-E <: Exception] extends caps.ExclusiveCapability, compiletime.Erased def Throw[Ex <: Exception](ex: Ex)(using CT[Ex]^): Nothing = ??? diff --git a/tests/neg-custom-args/captures/eta.check b/tests/neg-custom-args/captures/eta.check index 9b74a86d3b49..840c3845b236 100644 --- a/tests/neg-custom-args/captures/eta.check +++ b/tests/neg-custom-args/captures/eta.check @@ -3,12 +3,14 @@ | ^ | Found: (g : () -> A) | Required: () -> Proc^{f} + | Note that capability (f : Proc^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/eta.scala:6:14 ------------------------------------------- 6 | bar( () => f ) // error | ^^^^^^^ | Found: () ->{f} () ->{f} Unit - | Required: () -> () ->? Unit + | Required: () -> () ->{f} Unit + | Note that capability (f : Proc^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/existential-mapping.check b/tests/neg-custom-args/captures/existential-mapping.check index a867be0d8f7a..5813437c53bd 100644 --- a/tests/neg-custom-args/captures/existential-mapping.check +++ b/tests/neg-custom-args/captures/existential-mapping.check @@ -14,6 +14,8 @@ | where: ^ refers to the universal root capability | ^² refers to a root capability associated with the result type of (x: C^): C^² | + | Note that capability is not included in capture set {}. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:12:20 -------------------------- 12 | val _: C^ -> C = x2 // error @@ -23,6 +25,8 @@ | | where: ^ refers to the universal root capability | + | Note that capability x2* is not included in capture set {}. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:15:30 -------------------------- 15 | val _: A^ -> (x: C^) -> C = x3 // error @@ -33,6 +37,8 @@ | where: ^ refers to the universal root capability | ^² refers to a root capability associated with the result type of (x: C^): C^² | + | Note that capability is not included in capture set {}. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:18:25 -------------------------- 18 | val _: A^ -> C^ -> C = x4 // error @@ -42,6 +48,8 @@ | | where: ^ refers to the universal root capability | + | Note that capability x4* is not included in capture set {}. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:21:30 -------------------------- 21 | val _: A^ -> (x: C^) -> C = x5 // error @@ -52,6 +60,8 @@ | where: ^ refers to the universal root capability | ^² refers to a root capability associated with the result type of (x: C^): C^² | + | Note that capability is not included in capture set {}. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:24:30 -------------------------- 24 | val _: A^ -> (x: C^) => C = x6 // error @@ -63,6 +73,8 @@ | ^ refers to the universal root capability | ^² refers to a root capability associated with the result type of (x: C^): C^² | + | Note that capability is not included in capture set {}. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:27:25 -------------------------- 27 | val _: (x: C^) => C = y1 // error @@ -75,6 +87,8 @@ | ^ refers to the universal root capability | ^² refers to a root capability associated with the result type of (x: C^): C^² | + | Note that capability cap is not included in capture set {cap}. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:30:20 -------------------------- 30 | val _: C^ => C = y2 // error @@ -85,6 +99,8 @@ | where: => refers to a fresh root capability in the type of value _$8 | ^ refers to the universal root capability | + | Note that capability y2* is not included in capture set {}. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:33:30 -------------------------- 33 | val _: A^ => (x: C^) => C = y3 // error @@ -97,6 +113,8 @@ | ^ refers to the universal root capability | ^² refers to a root capability associated with the result type of (x: C^): C^² | + | Note that capability is not included in capture set {}. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:36:25 -------------------------- 36 | val _: A^ => C^ => C = y4 // error @@ -108,6 +126,8 @@ | =>² refers to a fresh root capability in the type of value _$10 | ^ refers to the universal root capability | + | Note that capability y4* is not included in capture set {}. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:39:30 -------------------------- 39 | val _: A^ => (x: C^) -> C = y5 // error @@ -120,6 +140,8 @@ | ^ refers to the universal root capability | ^² refers to a root capability associated with the result type of (x: C^): C^² | + | Note that capability cap is not included in capture set {cap}. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:42:30 -------------------------- 42 | val _: A^ => (x: C^) => C = y6 // error @@ -132,4 +154,6 @@ | ^ refers to the universal root capability | ^² refers to a root capability associated with the result type of (x: C^): C^² | + | Note that capability is not included in capture 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 index 816465e4af34..457e0ac3d9a2 100644 --- a/tests/neg-custom-args/captures/explain-under-approx.scala +++ b/tests/neg-custom-args/captures/explain-under-approx.scala @@ -1,4 +1,4 @@ -trait Async extends caps.Capability +trait Async extends caps.SharedCapability class Future[+T](x: () => T)(using val a: Async) diff --git a/tests/neg-custom-args/captures/extending-cap-classes.check b/tests/neg-custom-args/captures/extending-cap-classes.check index fb77546dd8e5..798522638888 100644 --- a/tests/neg-custom-args/captures/extending-cap-classes.check +++ b/tests/neg-custom-args/captures/extending-cap-classes.check @@ -1,19 +1,23 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/extending-cap-classes.scala:7:15 ------------------------- 7 | val x2: C1 = new C2 // error | ^^^^^^ - | Found: C2^{cap.rd} - | Required: C1 + |Found: C2^{cap.rd} + |Required: C1 | - | where: cap is a fresh root capability created in value x2 when constructing Capability instance C2 + |where: cap is a fresh root capability classified as SharedCapability created in value x2 when constructing Capability instance C2 + | + |Note that capability cap.rd is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/extending-cap-classes.scala:8:15 ------------------------- 8 | val x3: C1 = new C3 // error | ^^^^^^ - | Found: C3^{cap.rd} - | Required: C1 + |Found: C3^{cap.rd} + |Required: C1 + | + |where: cap is a fresh root capability classified as SharedCapability created in value x3 when constructing Capability instance C3 | - | where: cap is a fresh root capability created in value x3 when constructing Capability instance C3 + |Note that capability cap.rd is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/extending-cap-classes.scala:13:15 ------------------------ @@ -21,5 +25,6 @@ | ^^ | Found: (y2 : C2) | Required: C1 + | Note that capability cap is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/extending-cap-classes.scala b/tests/neg-custom-args/captures/extending-cap-classes.scala index 6f5a8f48c30a..7f38fd0af488 100644 --- a/tests/neg-custom-args/captures/extending-cap-classes.scala +++ b/tests/neg-custom-args/captures/extending-cap-classes.scala @@ -1,5 +1,5 @@ class C1 -class C2 extends C1, caps.Capability +class C2 extends C1, caps.SharedCapability class C3 extends C2 def test = diff --git a/tests/neg-custom-args/captures/filevar-multi-ios.scala b/tests/neg-custom-args/captures/filevar-multi-ios.scala index f827184a44e8..848d7c268b9c 100644 --- a/tests/neg-custom-args/captures/filevar-multi-ios.scala +++ b/tests/neg-custom-args/captures/filevar-multi-ios.scala @@ -1,7 +1,7 @@ import language.experimental.modularity import compiletime.uninitialized -class IO extends caps.Capability +class IO extends caps.SharedCapability class File: def write(x: String): Unit = ??? diff --git a/tests/neg-custom-args/captures/filevar.check b/tests/neg-custom-args/captures/filevar.check index 54f67bce972a..795b471ecd10 100644 --- a/tests/neg-custom-args/captures/filevar.check +++ b/tests/neg-custom-args/captures/filevar.check @@ -1,14 +1,14 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/filevar.scala:15:12 -------------------------------------- 15 | withFile: f => // error with level checking, was OK under both schemes before | ^ - |Found: (l: scala.caps.Capability^{cap.rd}) ?->? File^? ->? Unit - |Required: (l: scala.caps.Capability^{cap.rd}) ?-> (f: File^{l}) => Unit + |Found: (l: scala.caps.Capability^) ?->? File^? ->? Unit + |Required: (l: scala.caps.Capability^) ?-> (f: File^{l}) => Unit | - |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 + |where: => refers to a root capability associated with the result type of (using l: scala.caps.Capability^): (f: File^{l}) => Unit + | ^ refers to the universal root capability | - |Note that reference l.type - |cannot be included in outer capture set ? of parameter f + |Note that capability l.type + |cannot be included in outer capture set ? of parameter f. 16 | val o = Service() 17 | o.file = f 18 | o.log diff --git a/tests/neg-custom-args/captures/gears-problem.check b/tests/neg-custom-args/captures/gears-problem.check index 0fc5f8c3f163..2cf5d80ad526 100644 --- a/tests/neg-custom-args/captures/gears-problem.check +++ b/tests/neg-custom-args/captures/gears-problem.check @@ -3,6 +3,7 @@ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | Found: Future[T]^{collector.futures*} | Required: Future[T]^{fs*} + | Note that capability collector.futures* is not included in capture set {fs*}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/gears-problem.scala:24:34 -------------------------------- @@ -10,6 +11,7 @@ | ^^^^^ | Found: Future[T^{}]^{collector.futures*} | Required: Future[T]^{fs*} + | Note that capability collector.futures* is not included in capture set {fs*}. | | longer explanation available when compiling with `-explain` there were 4 deprecation warnings; re-run with -deprecation for details diff --git a/tests/neg-custom-args/captures/heal-tparam-cs.check b/tests/neg-custom-args/captures/heal-tparam-cs.check index cfda44733b6e..c696efee626c 100644 --- a/tests/neg-custom-args/captures/heal-tparam-cs.check +++ b/tests/neg-custom-args/captures/heal-tparam-cs.check @@ -7,8 +7,8 @@ |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 ? + |Note that capability c.type + |cannot be included in outer capture set ?. 11 | () => { c.use() } 12 | } | @@ -22,8 +22,7 @@ | 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 `Sharable` capability + | Note that capability x$0.type is not included in capture set {{x$0} Unit>}. 16 | (c1: Capp^) => () => { c1.use() } 17 | } | @@ -33,6 +32,7 @@ | ^ | Found: (x$0: Capp^?) ->? () ->{x$0} Unit | Required: (c: Capp^{io}) -> () ->{net} Unit + | Note that capability x$0.type is not included in capture set {net}. 26 | (c1: Capp^{io}) => () => { c1.use() } 27 | } | @@ -45,13 +45,14 @@ | | where: ^ refers to the universal root capability | + | Note that capability io.type is not included in capture set {}. + | | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:44:4 -------------------------------- +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:44:10 ------------------------------- 44 | io => () => io.use() // error - | ^^^^^^^^^^^^^^^^^^^^ - | Found: (io: Capp^) ->? () ->{io} Unit - | Required: Capp^ -> () -> Unit - | - | where: ^ refers to the universal root capability + | ^^^^^^^^^^^^^^ + | Found: () ->{io} Unit + | Required: () ->? Unit + | Note that capability (io : Capp^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i15772.check b/tests/neg-custom-args/captures/i15772.check index 8c71937090ed..4fbd86815112 100644 --- a/tests/neg-custom-args/captures/i15772.check +++ b/tests/neg-custom-args/captures/i15772.check @@ -29,12 +29,15 @@ | ^ refers to a fresh root capability in the type of value arg | ^² refers to a fresh root capability created in value boxed2 when instantiating method c's type -> C^{cap} | + |Note that capability cap is not included in capture set {}. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15772.scala:46:2 ---------------------------------------- 46 | x: (() -> Unit) // error | ^ | Found: (x : () ->{filesList, sayHello} Unit) | Required: () -> Unit + | Note that capability (filesList : List[File]^{io}) is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/i15772.scala:34:10 ------------------------------------------------------------ diff --git a/tests/neg-custom-args/captures/i15923.check b/tests/neg-custom-args/captures/i15923.check index 9eb930e0f405..ea3349ef2c61 100644 --- a/tests/neg-custom-args/captures/i15923.check +++ b/tests/neg-custom-args/captures/i15923.check @@ -1,14 +1,14 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15923.scala:12:21 --------------------------------------- 12 | val leak = withCap(cap => mkId(cap)) // error | ^^^^^^^^^^^^^^^^ - |Found: (lcap: scala.caps.Capability^{cap.rd}) ?->? Cap^? ->? Id[Cap^?]^? - |Required: (lcap: scala.caps.Capability^{cap.rd}) ?-> Cap^{lcap} => Id[Cap^?]^? + |Found: (lcap: scala.caps.Capability^) ?->? Cap^? ->? Id[Cap^?]^? + |Required: (lcap: scala.caps.Capability^) ?-> Cap^{lcap} => Id[Cap^?]^? | - |where: => refers to a root capability associated with the result type of (using lcap: scala.caps.Capability^{cap.rd}): Cap^{lcap} => Id[Cap^?]^? - | cap is the universal root capability + |where: => refers to a root capability associated with the result type of (using lcap: scala.caps.Capability^): Cap^{lcap} => Id[Cap^?]^? + | ^ refers to the universal root capability | - |Note that reference .rd - |cannot be included in outer capture set ? + |Note that capability + |cannot be included in outer capture set ?. | | longer explanation available when compiling with `-explain` -- Warning: tests/neg-custom-args/captures/i15923.scala:21:56 ---------------------------------------------------------- diff --git a/tests/neg-custom-args/captures/i15923.scala b/tests/neg-custom-args/captures/i15923.scala index 41bfd49e0250..8287be150761 100644 --- a/tests/neg-custom-args/captures/i15923.scala +++ b/tests/neg-custom-args/captures/i15923.scala @@ -12,7 +12,7 @@ def bar() = { val leak = withCap(cap => mkId(cap)) // error } -package test2: +object test2: trait Cap { def use(): Int } type Id[X] = [T] -> (op: X => T) -> T def mkId[X](x: X): Id[X] = [T] => (op: X => T) => op(x) diff --git a/tests/neg-custom-args/captures/i15923a.check b/tests/neg-custom-args/captures/i15923a.check index bc506822275e..6d2156d89a97 100644 --- a/tests/neg-custom-args/captures/i15923a.check +++ b/tests/neg-custom-args/captures/i15923a.check @@ -8,7 +8,7 @@ | =>² refers to a root capability associated with the result type of (lcap: Cap^): () =>² Id[Cap^?]^? | ^ refers to the universal root capability | - |Note that reference - |cannot be included in outer capture set ? + |Note that capability + |cannot be included in outer capture set ?. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i15923b.check b/tests/neg-custom-args/captures/i15923b.check index c7825851a7ef..80e1b3f8b4ba 100644 --- a/tests/neg-custom-args/captures/i15923b.check +++ b/tests/neg-custom-args/captures/i15923b.check @@ -7,7 +7,7 @@ |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 ? + |Note that capability lcap.type + |cannot be included in outer capture set ?. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i16226.check b/tests/neg-custom-args/captures/i16226.check index 1d79d29165dc..e7acc515af2c 100644 --- a/tests/neg-custom-args/captures/i16226.check +++ b/tests/neg-custom-args/captures/i16226.check @@ -9,6 +9,9 @@ | =>³ refers to a fresh root capability in the result type of method mapc | ^ refers to a fresh root capability in the result type of method mapc | + |Note that capability f1.type is not included in capture set {cap} + |because f1.type is not visible from cap in method mapc. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i16226.scala:15:4 ---------------------------------------- 15 | (ref1, f1) => map[A, B](ref1, f1) // error @@ -21,7 +24,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 `Sharable` capability + |Note that capability f1.type is not included in capture set {? A^?}^?, f1: A^? ->? B^?): LazyRef[B^?]{val elem: () => B^?}^{f1, ref1}>}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i16226.scala b/tests/neg-custom-args/captures/i16226.scala index 8e2d91b300ef..b6fc87a1d140 100644 --- a/tests/neg-custom-args/captures/i16226.scala +++ b/tests/neg-custom-args/captures/i16226.scala @@ -1,4 +1,4 @@ -class Cap extends caps.Capability +class Cap extends caps.SharedCapability class LazyRef[T](val elem: () => T): val get: () ->{elem} T = elem diff --git a/tests/neg-custom-args/captures/i16725.scala b/tests/neg-custom-args/captures/i16725.scala index 3422ae537c92..ffa79f72b904 100644 --- a/tests/neg-custom-args/captures/i16725.scala +++ b/tests/neg-custom-args/captures/i16725.scala @@ -1,5 +1,5 @@ import language.experimental.captureChecking -class IO extends caps.Capability: +class IO extends caps.SharedCapability: def brewCoffee(): Unit = ??? def usingIO[T](op: IO => T): T = ??? diff --git a/tests/neg-custom-args/captures/i19330.check b/tests/neg-custom-args/captures/i19330.check index 5a7dc525af4d..044ebd553c07 100644 --- a/tests/neg-custom-args/captures/i19330.check +++ b/tests/neg-custom-args/captures/i19330.check @@ -8,6 +8,7 @@ | ^ | Found: () ->{t} Logger^{t*} | Required: x.T + | Note that capability (t : () => Logger^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i19330.scala:22:22 --------------------------------------- @@ -19,6 +20,9 @@ | where: => refers to a fresh root capability in the type of value bad | ^ refers to a fresh root capability in the type of value bad | + | Note that capability cap is not included in capture set {cap} + | because cap in class Bar is not visible from cap in value bad. + | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/i19330.scala:16:14 ------------------------------------------------------------ 16 | val t: () => Logger^ = () => l // error diff --git a/tests/neg-custom-args/captures/i19470.check b/tests/neg-custom-args/captures/i19470.check index 745018c54c88..d674e8f1c764 100644 --- a/tests/neg-custom-args/captures/i19470.check +++ b/tests/neg-custom-args/captures/i19470.check @@ -3,5 +3,6 @@ | ^^^^^^^^ | Found: Inv[IO^{f?}] | Required: Inv[IO^?]^? + | Note that capability (f : () => IO^) is not included in capture set {f?}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i21313.check b/tests/neg-custom-args/captures/i21313.check index 2a90a1f7aa47..04c5f452bf54 100644 --- a/tests/neg-custom-args/captures/i21313.check +++ b/tests/neg-custom-args/captures/i21313.check @@ -10,4 +10,6 @@ | |where: ^ refers to a fresh root capability created in method test when checking argument to parameter src of method await | + |Note that capability (ac1 : Async^) cannot be included in capture set {ac2} of value src2. + | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i21401.check b/tests/neg-custom-args/captures/i21401.check index 91444d0957e9..bc1a1143239b 100644 --- a/tests/neg-custom-args/captures/i21401.check +++ b/tests/neg-custom-args/captures/i21401.check @@ -22,6 +22,9 @@ | ^ refers to the universal root capability | ^² refers to a fresh root capability created in value a when checking argument to parameter op of method usingIO | + |Note that capability x.type is not included in capture set {cap} + |because x.type is not visible from cap in value a. + | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/i21401.scala:16:66 ------------------------------------------------------------ 16 | val leaked: [R, X <: Boxed[IO^] -> R] -> (op: X) -> R = usingIO[Res](mkRes) // error @@ -53,4 +56,7 @@ | where: ^ refers to the universal root capability | ^² refers to a fresh root capability created in value x² | + | Note that capability x* is not included in capture set {cap} + | because x* is not visible from cap in value x. + | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i21614.check b/tests/neg-custom-args/captures/i21614.check index 9535ce2e5b96..7fdab4b3e043 100644 --- a/tests/neg-custom-args/captures/i21614.check +++ b/tests/neg-custom-args/captures/i21614.check @@ -4,7 +4,9 @@ |Found: (f : F) |Required: File^ | - |where: ^ refers to a fresh root capability created in anonymous function of type (f²: F): Logger when checking argument to parameter f of constructor Logger + |where: ^ refers to a fresh root capability classified as SharedCapability created in anonymous function of type (f²: F): Logger when checking argument to parameter f of constructor Logger + | + |Note that capability cap is not included in capture set {cap}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:15:12 --------------------------------------- @@ -16,7 +18,7 @@ |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: File^?): Logger{val f: File^{_$1}}^{cap.rd, _$1} | - |Note that reference .rd - |cannot be included in outer capture set ? + |Note that capability .rd + |cannot be included in outer capture set ?. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i21614.scala b/tests/neg-custom-args/captures/i21614.scala index f5bab90f543b..c80d65535d14 100644 --- a/tests/neg-custom-args/captures/i21614.scala +++ b/tests/neg-custom-args/captures/i21614.scala @@ -1,12 +1,12 @@ import language.experimental.captureChecking -import caps.Capability +import caps.SharedCapability import caps.use trait List[+T]: def map[U](f: T => U): List[U] -trait File extends Capability -class Logger(f: File^) extends Capability // <- will work if we remove the extends clause +trait File extends SharedCapability +class Logger(f: File^) extends SharedCapability // <- will work if we remove the extends clause def mkLoggers1[F <: File^](@use files: List[F]): List[Logger^] = files.map((f: F) => new Logger(f)) // error, Q: can we make this pass (see #19076)? diff --git a/tests/neg-custom-args/captures/i21620.check b/tests/neg-custom-args/captures/i21620.check index d5be3bab9e73..019ae9623dca 100644 --- a/tests/neg-custom-args/captures/i21620.check +++ b/tests/neg-custom-args/captures/i21620.check @@ -15,6 +15,7 @@ | ^ | Found: (f : () ->{x} () ->{x} Unit) | Required: () -> () ->{x} Unit + | Note that capability (x : C^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21620.scala:20:33 --------------------------------------- @@ -22,5 +23,6 @@ | ^ | Found: (f : () ->{x} () ->{x} Unit) | Required: () -> () ->{x} Unit + | Note that capability (x : C^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i21920.check b/tests/neg-custom-args/captures/i21920.check index 9b3de5548f5b..2b860553c3af 100644 --- a/tests/neg-custom-args/captures/i21920.check +++ b/tests/neg-custom-args/captures/i21920.check @@ -7,7 +7,7 @@ |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 ? + |Note that capability + |cannot be included in outer capture set ?. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i23207.check b/tests/neg-custom-args/captures/i23207.check index 78a5406ce03d..e66b6fb0e285 100644 --- a/tests/neg-custom-args/captures/i23207.check +++ b/tests/neg-custom-args/captures/i23207.check @@ -3,6 +3,7 @@ | ^^^^^ | Found: (box.x : (b : B^{io})^{b}) | Required: A + | Note that capability (io : AnyRef^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23207.scala:18:13 --------------------------------------- @@ -10,6 +11,7 @@ | ^ | Found: (c : B^{b}) | Required: A + | Note that capability (b : B^{io}) is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23207.scala:23:2 ---------------------------------------- @@ -17,6 +19,7 @@ | ^ | Found: A^{io} | Required: A + | Note that capability (io : AnyRef^) is not included in capture set {}. 24 | val hide: AnyRef^{io} = io 25 | val b = new B 26 | val c = b.getBox.x diff --git a/tests/neg-custom-args/captures/i23223.scala b/tests/neg-custom-args/captures/i23223.scala index e606875b840a..f49fd9b40005 100644 --- a/tests/neg-custom-args/captures/i23223.scala +++ b/tests/neg-custom-args/captures/i23223.scala @@ -4,9 +4,9 @@ import caps.* class A: def a: A = this -class B extends A, Capability // error +class B extends A, SharedCapability // error def leak(b: B): A = b.a -class C extends Capability: +class C extends SharedCapability: def c: C^{} = this // error diff --git a/tests/neg-custom-args/captures/i23431.check b/tests/neg-custom-args/captures/i23431.check index 1332c2cf2c79..9d48a8f4e099 100644 --- a/tests/neg-custom-args/captures/i23431.check +++ b/tests/neg-custom-args/captures/i23431.check @@ -7,6 +7,9 @@ | where: ^ refers to a fresh root capability in the type of parameter io | ^² refers to a fresh root capability in the type of variable myIO | + | Note that capability cap is not included in capture set {cap} + | because cap in method setIO is not visible from cap in variable myIO. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23431.scala:11:13 --------------------------------------- 11 | myIO = io2 // error, level mismatch @@ -17,6 +20,9 @@ | where: ^ refers to a fresh root capability in the type of parameter io2 | ^² refers to a fresh root capability in the type of variable myIO | + | Note that capability cap is not included in capture set {cap} + | because cap in enclosing function is not visible from cap in variable myIO. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23431.scala:12:12 --------------------------------------- 12 | withIO: io3 => // error @@ -26,6 +32,9 @@ | |where: => refers to a fresh root capability created in anonymous function of type (io1: IO^): Unit when checking argument to parameter op of method withIO | ^ refers to the universal root capability + | + |Note that capability cap is not included in capture set {cap} + |because cap in enclosing function is not visible from cap in variable myIO. 13 | myIO = io3 | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/inner-classes.scala b/tests/neg-custom-args/captures/inner-classes.scala index fd500e607970..2725e6cd7307 100644 --- a/tests/neg-custom-args/captures/inner-classes.scala +++ b/tests/neg-custom-args/captures/inner-classes.scala @@ -1,6 +1,6 @@ object test: - class FileSystem extends caps.Capability + class FileSystem extends caps.SharedCapability def foo(fs: FileSystem) = diff --git a/tests/neg-custom-args/captures/lazylist.check b/tests/neg-custom-args/captures/lazylist.check index 0959f1a082fb..4bf4f1ac94f9 100644 --- a/tests/neg-custom-args/captures/lazylist.check +++ b/tests/neg-custom-args/captures/lazylist.check @@ -1,8 +1,9 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylist.scala:17:15 ------------------------------------- 17 | def tail = xs() // error | ^^^^ - | Found: lazylists.LazyList[T]^{LazyCons.this.xs} - | Required: lazylists.LazyList[T] + | Found: lazylists.LazyList[T]^{LazyCons.this.xs} + | Required: lazylists.LazyList[T] + | Note that capability (LazyCons.this.xs : () => lazylists.LazyList[T]^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylist.scala:35:29 ------------------------------------- @@ -10,27 +11,31 @@ | ^^^^ | Found: (ref1 : lazylists.LazyCons[Int]{val xs: () ->{cap1} lazylists.LazyList[Int]^{}}^{cap1}) | Required: lazylists.LazyList[Int] + | Note that capability (cap1 : lazylists.CC^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylist.scala:37:36 ------------------------------------- 37 | val ref2c: LazyList[Int]^{ref1} = ref2 // error | ^^^^ - | Found: (ref2 : lazylists.LazyList[Int]^{cap2, ref1}) - | Required: lazylists.LazyList[Int]^{ref1} + | Found: (ref2 : lazylists.LazyList[Int]^{cap2, ref1}) + | Required: lazylists.LazyList[Int]^{ref1} + | Note that capability (cap2 : lazylists.CC^) is not included in capture set {ref1}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylist.scala:39:36 ------------------------------------- 39 | val ref3c: LazyList[Int]^{cap2} = ref3 // error | ^^^^ - | Found: (ref3 : lazylists.LazyList[Int]^{cap2, ref1}) - | Required: lazylists.LazyList[Int]^{cap2} + |Found: (ref3 : lazylists.LazyList[Int]^{cap2, ref1}) + |Required: lazylists.LazyList[Int]^{cap2} + |Note that capability (ref1 : lazylists.LazyCons[Int]{val xs: () ->{cap1} lazylists.LazyList[Int]^{}}^{cap1}) is not included in capture set {cap2}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylist.scala:41:42 ------------------------------------- 41 | val ref4c: LazyList[Int]^{cap1, ref3} = ref4 // error | ^^^^ - | Found: (ref4 : lazylists.LazyList[Int]^{cap3, cap1, cap2}) - | Required: lazylists.LazyList[Int]^{cap1, ref3} + | Found: (ref4 : lazylists.LazyList[Int]^{cap3, cap1, cap2}) + | Required: lazylists.LazyList[Int]^{cap1, ref3} + | Note that capability (cap3 : lazylists.CC^) is not included in capture set {cap1, ref3}. | | longer explanation available when compiling with `-explain` -- [E164] Declaration Error: tests/neg-custom-args/captures/lazylist.scala:22:6 ---------------------------------------- diff --git a/tests/neg-custom-args/captures/lazylists-exceptions.check b/tests/neg-custom-args/captures/lazylists-exceptions.check index 24ba72b1cdad..a60984fac608 100644 --- a/tests/neg-custom-args/captures/lazylists-exceptions.check +++ b/tests/neg-custom-args/captures/lazylists-exceptions.check @@ -1,11 +1,11 @@ -- Error: tests/neg-custom-args/captures/lazylists-exceptions.scala:36:2 ----------------------------------------------- 36 | try // error | ^ - | The result of `try` cannot have type LazyList[Int]^{cap.rd} since + | The result of `try` cannot have type LazyList[Int]^ since | that type captures the root capability `cap`. | This is often caused by a locally generated exception capability leaking as part of its result. | - | where: cap is a fresh root capability classified as Control in the type of given instance canThrow$1 + | where: ^ refers to a fresh root capability classified as Control in the type of given instance canThrow$1 37 | tabulate(10) { i => 38 | if i > 9 then throw Ex1() 39 | i * i diff --git a/tests/neg-custom-args/captures/lazylists1.check b/tests/neg-custom-args/captures/lazylists1.check index 127a0563c3c9..c14568b9600c 100644 --- a/tests/neg-custom-args/captures/lazylists1.check +++ b/tests/neg-custom-args/captures/lazylists1.check @@ -1,7 +1,8 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylists1.scala:25:66 ----------------------------------- 25 | def concat(other: LazyList[A]^{f}): LazyList[A]^{this, f} = ??? : (LazyList[A]^{xs, f}) // error | ^^^^^^^^^^^^^^^^^^^^^^^^^^^ - | Found: LazyList[A]^{xs, f} - | Required: LazyList[A]^{Mapped.this, f} + | Found: LazyList[A]^{xs, f} + | Required: LazyList[A]^{Mapped.this, f} + | Note that capability (xs : LazyList[A]^) is not included in capture set {Mapped.this, f}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/lazylists2.check b/tests/neg-custom-args/captures/lazylists2.check index 720434cb2a2d..1f7fd0e509cb 100644 --- a/tests/neg-custom-args/captures/lazylists2.check +++ b/tests/neg-custom-args/captures/lazylists2.check @@ -3,6 +3,7 @@ | ^ | Found: LazyList[B^?]^{f, xs} | Required: LazyList[B]^{f} + | Note that capability (xs : LazyList[A]^) is not included in capture set {f}. 19 | this: (Mapped^{xs, f}) => 20 | def isEmpty = false 21 | def head: B = f(xs.head) @@ -15,6 +16,7 @@ | ^ | Found: LazyList[B^?]^{f, xs} | Required: LazyList[B]^{xs} + | Note that capability (f : A => B) is not included in capture set {xs}. 28 | this: Mapped^{xs, f} => 29 | def isEmpty = false 30 | def head: B = f(xs.head) @@ -35,6 +37,7 @@ | ^ | Found: LazyList[B^?]^{f, xs} | Required: LazyList[B]^{xs} + | Note that capability (f : A => B) is not included in capture set {xs}. 46 | this: (Mapped^{xs, f}) => 47 | def isEmpty = false 48 | def head: B = f(xs.head) diff --git a/tests/neg-custom-args/captures/lazyref.check b/tests/neg-custom-args/captures/lazyref.check index a8419cb30b12..933b75cabdb8 100644 --- a/tests/neg-custom-args/captures/lazyref.check +++ b/tests/neg-custom-args/captures/lazyref.check @@ -3,27 +3,31 @@ | ^^^^ | Found: (ref1 : LazyRef[Int]{val elem: () ->{cap1} Int}^{cap1}) | Required: LazyRef[Int] + | Note that capability (cap1 : CC^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazyref.scala:22:35 -------------------------------------- 22 | val ref2c: LazyRef[Int]^{cap2} = ref2 // error | ^^^^ - | Found: LazyRef[Int]{val elem: () ->{ref2*} Int}^{ref2} - | Required: LazyRef[Int]^{cap2} + |Found: LazyRef[Int]{val elem: () ->{ref2*} Int}^{ref2} + |Required: LazyRef[Int]^{cap2} + |Note that capability (ref2 : LazyRef[Int]{val elem: () => Int}^{cap2, ref1}) is not included in capture set {cap2}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazyref.scala:24:35 -------------------------------------- 24 | val ref3c: LazyRef[Int]^{ref1} = ref3 // error | ^^^^ - | Found: LazyRef[Int]{val elem: () ->{ref3*} Int}^{ref3} - | Required: LazyRef[Int]^{ref1} + |Found: LazyRef[Int]{val elem: () ->{ref3*} Int}^{ref3} + |Required: LazyRef[Int]^{ref1} + |Note that capability (ref3 : LazyRef[Int]{val elem: () => Int}^{cap2, ref1}) is not included in capture set {ref1}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazyref.scala:30:35 -------------------------------------- 30 | val ref4c: LazyRef[Int]^{cap1} = ref4 // error | ^^^^ - | Found: LazyRef[Int]{val elem: () ->{ref4*} Int}^{ref4} - | Required: LazyRef[Int]^{cap1} + |Found: LazyRef[Int]{val elem: () ->{ref4*} Int}^{ref4} + |Required: LazyRef[Int]^{cap1} + |Note that capability (ref4 : LazyRef[Int]{val elem: () => Int}^{cap2, ref1}) is not included in capture set {cap1}. | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/lazyref.scala:8:24 ------------------------------------------------------------ diff --git a/tests/neg-custom-args/captures/leak-problem-2.check b/tests/neg-custom-args/captures/leak-problem-2.check index 80add5eddd22..5af4d1135454 100644 --- a/tests/neg-custom-args/captures/leak-problem-2.check +++ b/tests/neg-custom-args/captures/leak-problem-2.check @@ -3,5 +3,6 @@ | ^^^^^^^^^^^^^^^^^^^^^ | Found: Source[T^?]^{src1, src2} | Required: Source[T] + | Note that capability (src1 : Source[T]^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/leaked-curried-shared.scala b/tests/neg-custom-args/captures/leaked-curried-shared.scala new file mode 100644 index 000000000000..95d0666e18a1 --- /dev/null +++ b/tests/neg-custom-args/captures/leaked-curried-shared.scala @@ -0,0 +1,20 @@ +trait Cap extends caps.SharedCapability: + def use(): Unit + +def withCap[T](op: (x: Cap) => T): T = ??? + +trait Box: + val get: () ->{} () => Cap + +def main(): Unit = + val leaked = withCap: (io: Cap) => + class Fuzz extends Box, Pure: + self => + val get: () ->{} () ->{io} Cap = + () => () => io // error + class Foo extends Box, Pure: + val get: () ->{} () ->{io} Cap = + () => () => io // error + new Foo + val bad = leaked.get()().use() // using a leaked capability + diff --git a/tests/neg-custom-args/captures/leaked-curried.check b/tests/neg-custom-args/captures/leaked-curried.check index e2327a576070..ff64c979705c 100644 --- a/tests/neg-custom-args/captures/leaked-curried.check +++ b/tests/neg-custom-args/captures/leaked-curried.check @@ -6,3 +6,11 @@ 17 | () => () => io // error | ^^ | reference (io : Cap^) is not included in the allowed capture set {} of the self type of class Foo +-- Error: tests/neg-custom-args/captures/leaked-curried.scala:13:15 ---------------------------------------------------- +13 | val get: () ->{} () ->{io} Cap^ = // error + | ^^^^^^^^^^^^^^^^^^^^^^ + | Separation failure: value get's type () -> () ->{io} Cap^ hides non-local parameter io +-- Error: tests/neg-custom-args/captures/leaked-curried.scala:16:15 ---------------------------------------------------- +16 | val get: () ->{} () ->{io} Cap^ = // error + | ^^^^^^^^^^^^^^^^^^^^^^ + | Separation failure: value get's type () -> () ->{io} Cap^ hides non-local parameter io diff --git a/tests/neg-custom-args/captures/leaked-curried.scala b/tests/neg-custom-args/captures/leaked-curried.scala index 96b8c0254d76..30e0456cb4ea 100644 --- a/tests/neg-custom-args/captures/leaked-curried.scala +++ b/tests/neg-custom-args/captures/leaked-curried.scala @@ -10,10 +10,10 @@ def main(): Unit = val leaked = withCap: (io: Cap^) => class Fuzz extends Box, Pure: self => - val get: () ->{} () ->{io} Cap^ = + val get: () ->{} () ->{io} Cap^ = // error () => () => io // error class Foo extends Box, Pure: - val get: () ->{} () ->{io} Cap^ = + val get: () ->{} () ->{io} Cap^ = // error () => () => io // error new Foo val bad = leaked.get()().use() // using a leaked capability diff --git a/tests/neg-custom-args/captures/leaking-iterators.check b/tests/neg-custom-args/captures/leaking-iterators.check index f4dde1d7f2fd..80461c0496ee 100644 --- a/tests/neg-custom-args/captures/leaking-iterators.check +++ b/tests/neg-custom-args/captures/leaking-iterators.check @@ -7,8 +7,8 @@ |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 ? + |Note that capability log.type + |cannot be included in outer capture set ?. 57 | xs.iterator.map: x => 58 | log.write(x) 59 | x * x diff --git a/tests/neg-custom-args/captures/leaky.check b/tests/neg-custom-args/captures/leaky.check index b5ced771e0f6..57630a636f73 100644 --- a/tests/neg-custom-args/captures/leaky.check +++ b/tests/neg-custom-args/captures/leaky.check @@ -3,6 +3,7 @@ | ^ | Found: test.runnable.Transform{val fun: Any ->{a} Any}^{a} | Required: test.runnable.Transform + | Note that capability (a : test.runnable.A) is not included in capture set {}. 15 | a.print() 16 | () 17 | Transform(f) @@ -13,6 +14,7 @@ | ^ | Found: test.runnable.Transform{val fun: Any ->{a} Any}^{a} | Required: test.runnable.Transform + | Note that capability (a : test.runnable.A) is not included in capture set {}. 21 | a.print() 22 | () 23 | val x = Transform(f) @@ -24,6 +26,7 @@ | ^ | Found: test.runnable.Transform{val fun: Any ->{a} Any}^{a} | Required: test.runnable.Transform + | Note that capability (a : test.runnable.A) is not included in capture set {}. 28 | a.print() 29 | () 30 | val x = Transform.app(f) diff --git a/tests/neg-custom-args/captures/leaky.scala b/tests/neg-custom-args/captures/leaky.scala index b401cab0df63..b614c8e09bdc 100644 --- a/tests/neg-custom-args/captures/leaky.scala +++ b/tests/neg-custom-args/captures/leaky.scala @@ -1,7 +1,7 @@ package test.runnable import language.experimental.captureChecking -case class A() extends caps.Capability: +case class A() extends caps.SharedCapability: def print() = println("leaking...") class Transform(fun: Any => Any): diff --git a/tests/neg-custom-args/captures/levels.check b/tests/neg-custom-args/captures/levels.check index dc8994907634..34f339e57869 100644 --- a/tests/neg-custom-args/captures/levels.check +++ b/tests/neg-custom-args/captures/levels.check @@ -10,5 +10,6 @@ | ^ | Found: (x: String) ->{cap3} String | Required: String -> String + | Note that capability (cap3 : CC^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/lexical-control.scala b/tests/neg-custom-args/captures/lexical-control.scala index 7a38a6a94600..363a070a4759 100644 --- a/tests/neg-custom-args/captures/lexical-control.scala +++ b/tests/neg-custom-args/captures/lexical-control.scala @@ -1,7 +1,7 @@ import language.experimental.captureChecking import caps.* -trait Label extends Capability: +trait Label extends SharedCapability: type Fv^ // the capability set occurring freely in the `block` passed to `boundary` below. def boundary[T, C^](block: Label{type Fv = {C} } ->{C} T): T = ??? // link label and block capture set diff --git a/tests/neg-custom-args/captures/lubs.check b/tests/neg-custom-args/captures/lubs.check index b2eaf6ae6f4e..24f4d2e6546b 100644 --- a/tests/neg-custom-args/captures/lubs.check +++ b/tests/neg-custom-args/captures/lubs.check @@ -3,6 +3,7 @@ | ^^ | Found: (x1 : D^{d1}) | Required: D + | Note that capability (d1 : D^{c1}) is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lubs.scala:18:13 ----------------------------------------- @@ -10,6 +11,7 @@ | ^^ | Found: (x2 : D^{d1}) | Required: D + | Note that capability (d1 : D^{c1}) is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lubs.scala:19:13 ----------------------------------------- @@ -17,5 +19,6 @@ | ^^ | Found: (x3 : D^{d1, d2}) | Required: D + | Note that capability (d1 : D^{c1}) is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/lubs.scala b/tests/neg-custom-args/captures/lubs.scala index 3a2eb59b48b5..dc05984b4f87 100644 --- a/tests/neg-custom-args/captures/lubs.scala +++ b/tests/neg-custom-args/captures/lubs.scala @@ -1,6 +1,6 @@ import java.sql.Date -class C extends caps.Capability +class C extends caps.SharedCapability class D def Test(c1: C, c2: C) = diff --git a/tests/neg-custom-args/captures/nestedclass.check b/tests/neg-custom-args/captures/nestedclass.check index 2987318caf4f..5c4125b30535 100644 --- a/tests/neg-custom-args/captures/nestedclass.check +++ b/tests/neg-custom-args/captures/nestedclass.check @@ -3,5 +3,6 @@ | ^^ | Found: (xs : C^{cap1}) | Required: C + | Note that capability (cap1 : CC^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/outer-var.check b/tests/neg-custom-args/captures/outer-var.check index d6d9067d9d2f..6d4e37022a26 100644 --- a/tests/neg-custom-args/captures/outer-var.check +++ b/tests/neg-custom-args/captures/outer-var.check @@ -8,6 +8,8 @@ | q is a parameter in method inner | q² is a parameter in method test | + | Note that capability cap is not included in capture set {p, q}. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/outer-var.scala:13:9 ------------------------------------- 13 | x = (q: Proc) // error @@ -17,6 +19,8 @@ | | where: => refers to a fresh root capability created in method inner | + | Note that capability cap is not included in capture set {p, q}. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/outer-var.scala:14:9 ------------------------------------- 14 | y = (q: Proc) // error @@ -26,6 +30,8 @@ | | where: => refers to a fresh root capability created in method inner | + | Note that capability cap cannot be included in capture set {p} of variable y. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/outer-var.scala:15:8 ------------------------------------- 15 | y = q // error, was OK under unsealed @@ -35,6 +41,8 @@ | | where: => refers to a fresh root capability in the type of parameter q | + | Note that capability cap cannot be included in capture set {p} of variable y. + | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/outer-var.scala:17:57 --------------------------------------------------------- 17 | var finalizeActions = collection.mutable.ListBuffer[() => Unit]() // error, was OK under unsealed diff --git a/tests/neg-custom-args/captures/path-prefix.scala b/tests/neg-custom-args/captures/path-prefix.scala index af5817636d0b..9312552bc38c 100644 --- a/tests/neg-custom-args/captures/path-prefix.scala +++ b/tests/neg-custom-args/captures/path-prefix.scala @@ -1,13 +1,13 @@ import language.experimental.modularity import language.experimental.captureChecking -import caps.Capability +import caps.SharedCapability class F: val f: AnyRef^ = ??? -case class B(tracked val a: A) extends F, Capability +case class B(tracked val a: A) extends F, SharedCapability -class A extends F, Capability: +class A extends F, SharedCapability: val b: B { val a: A.this.type } = B(this) def test(a: A) = diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check index 70c2b8f2a82b..0868a56d2a18 100644 --- a/tests/neg-custom-args/captures/reaches.check +++ b/tests/neg-custom-args/captures/reaches.check @@ -6,6 +6,8 @@ | |where: => refers to a fresh root capability created in method runAll0 when checking argument to parameter f of method usingFile | ^ refers to the universal root capability + | + |Note that capability cap is not included in capture set {xs*}. 23 | cur = (() => f.write()) :: Nil | | longer explanation available when compiling with `-explain` @@ -17,6 +19,8 @@ | |where: => refers to a fresh root capability created in method runAll1 when checking argument to parameter f of method usingFile | ^ refers to the universal root capability + | + |Note that capability cap cannot be included in capture set {xs*} of value cur. 33 | cur.set: 34 | (() => f.write()) :: Nil | @@ -37,6 +41,9 @@ | where: => refers to the universal root capability | =>² refers to a fresh root capability in the type of value next | + | Note that capability cap is not included in capture set {cap} + | because cap is not visible from cap in value next. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:48:20 -------------------------------------- 48 | cur.set(cur.get.tail: List[Proc]) // error @@ -47,6 +54,9 @@ | where: => refers to the universal root capability | =>² refers to a fresh root capability created in method runAll3 | + | Note that capability cap is not included in capture set {cap} + | because cap is not visible from cap in method runAll3. + | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/reaches.scala:54:51 ----------------------------------------------------------- 54 | val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error @@ -64,6 +74,9 @@ | where: ^ refers to the universal root capability | ^² refers to a fresh root capability in the type of value id | + | Note that capability x.type is not included in capture set {cap} + | because x.type is not visible from cap in value id. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:67:32 -------------------------------------- 67 | val id: (x: File^) -> File^ = x => x // error @@ -74,8 +87,7 @@ | 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 `Sharable` capability + | Note that capability x.type is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:70:38 -------------------------------------- @@ -86,6 +98,8 @@ | |where: => refers to a fresh root capability created in value leaked when checking argument to parameter f of method usingFile | ^ refers to the universal root capability + | + |Note that capability cap is not included in capture set {id*}. 71 | val f1: File^{id*} = id(f) 72 | f1 | @@ -99,6 +113,8 @@ |where: => refers to a fresh root capability created in method mapCompose when checking argument to parameter f of method map | ^ refers to the universal root capability | + |Note that capability ps* cannot be included in capture set {} of value x. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:91:10 -------------------------------------- 91 | ps.map((x, y) => compose1(x, y)) // error @@ -109,9 +125,23 @@ |where: => refers to a fresh root capability created in method mapCompose2 when checking argument to parameter f of method map | ^ refers to the universal root capability | + |Note that capability ps* cannot be included in capture set {} of value x. + | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/reaches.scala:39:31 ----------------------------------------------------------- 39 | val next: () => Unit = cur.head // error | ^^^^^^^^ | Local reach capability xs* leaks into capture scope of method runAll2. | To allow this, the parameter xs should be declared with a @use annotation +-- Error: tests/neg-custom-args/captures/reaches.scala:62:36 ----------------------------------------------------------- +62 | val leaked = usingFile[File^{id*}]: f => // error: separation + | ^ + | Separation failure: Illegal access to cap of value id which is hidden by the previous definition + | of value id with type File^ -> File^². + | This type hides capabilities {cap} + | + | where: ^ refers to the universal root capability + | ^² refers to a fresh root capability in the type of value id + | cap is a fresh root capability created in value id +63 | val f1: File^{id*} = id(f) +64 | f1 diff --git a/tests/neg-custom-args/captures/reaches.scala b/tests/neg-custom-args/captures/reaches.scala index b811b1405590..0d0374cf8d2e 100644 --- a/tests/neg-custom-args/captures/reaches.scala +++ b/tests/neg-custom-args/captures/reaches.scala @@ -59,7 +59,7 @@ def attack2 = val id: File^ -> File^ = x => x // error // val id: File^ -> File^{fresh} - val leaked = usingFile[File^{id*}]: f => // now ok + val leaked = usingFile[File^{id*}]: f => // error: separation val f1: File^{id*} = id(f) f1 diff --git a/tests/neg-custom-args/captures/reaches2.check b/tests/neg-custom-args/captures/reaches2.check index 3ad78fd49eed..e91ea3c3859e 100644 --- a/tests/neg-custom-args/captures/reaches2.check +++ b/tests/neg-custom-args/captures/reaches2.check @@ -2,6 +2,7 @@ 10 | ps.map((x, y) => compose1(x, y)) // error | ^^^^^^^^^^^^^^^^^^^^^^^ | Found: (x$1: (A^? ->{ps*} A^?, A^? ->{ps*} A^?)^?) ->{ps*} A^? ->{ps*} A^? - | Required: ((A ->{ps*} A, A ->{ps*} A)) -> A^? ->? A^? + | Required: ((A ->{ps*} A, A ->{ps*} A)) -> A^? ->{ps*} A^? + | Note that capability ps* is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/readOnly.check b/tests/neg-custom-args/captures/readOnly.check index 46721d3e1627..e212cf2f1a6f 100644 --- a/tests/neg-custom-args/captures/readOnly.check +++ b/tests/neg-custom-args/captures/readOnly.check @@ -3,6 +3,7 @@ | ^^^^ | Found: (getA : () ->{a.rd} Int) | Required: () -> Int + | Note that capability a.rd is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/readOnly.scala:17:23 ------------------------------------- @@ -10,6 +11,7 @@ | ^^^^ | Found: (putA : Int ->{a} Unit) | Required: Int -> Unit + | Note that capability (a : Ref^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/readOnly.scala:20:23 ---------------------------------------------------------- diff --git a/tests/neg-custom-args/captures/real-try.check b/tests/neg-custom-args/captures/real-try.check index c68e82514f24..9663a134a3a1 100644 --- a/tests/neg-custom-args/captures/real-try.check +++ b/tests/neg-custom-args/captures/real-try.check @@ -7,11 +7,11 @@ -- Error: tests/neg-custom-args/captures/real-try.scala:14:2 ----------------------------------------------------------- 14 | try // error | ^ - | The result of `try` cannot have type () ->{cap.rd} Unit since + | The result of `try` cannot have type () => Unit since | that type captures the root capability `cap`. | This is often caused by a locally generated exception capability leaking as part of its result. | - | where: cap is a fresh root capability classified as Control in the type of given instance canThrow$1 + | where: => refers to a fresh root capability classified as Control in the type of given instance canThrow$1 15 | () => foo(1) 16 | catch 17 | case _: Ex1 => ??? @@ -19,11 +19,11 @@ -- Error: tests/neg-custom-args/captures/real-try.scala:20:10 ---------------------------------------------------------- 20 | val x = try // error | ^ - | The result of `try` cannot have type () ->{cap.rd} Unit since - | that type captures the root capability `cap`. - | This is often caused by a locally generated exception capability leaking as part of its result. + | The result of `try` cannot have type () => Unit since + | that type captures the root capability `cap`. + | This is often caused by a locally generated exception capability leaking as part of its result. | - | where: cap is a fresh root capability classified as Control in the type of given instance canThrow$2 + | where: => refers to a fresh root capability classified as Control in the type of given instance canThrow$2 21 | () => foo(1) 22 | catch 23 | case _: Ex1 => ??? @@ -31,11 +31,11 @@ -- Error: tests/neg-custom-args/captures/real-try.scala:26:10 ---------------------------------------------------------- 26 | val y = try // error | ^ - | The result of `try` cannot have type () ->{cap.rd} Cell[Unit]^? since - | that type captures the root capability `cap`. - | This is often caused by a locally generated exception capability leaking as part of its result. + | The result of `try` cannot have type () => Cell[Unit]^? since + | that type captures the root capability `cap`. + | This is often caused by a locally generated exception capability leaking as part of its result. | - | where: cap is a fresh root capability classified as Control in the type of given instance canThrow$3 + | where: => refers to a fresh root capability classified as Control in the type of given instance canThrow$3 27 | () => Cell(foo(1)) 28 | catch 29 | case _: Ex1 => ??? @@ -43,11 +43,11 @@ -- Error: tests/neg-custom-args/captures/real-try.scala:32:10 ---------------------------------------------------------- 32 | val b = try // error | ^ - | The result of `try` cannot have type Cell[() ->{cap.rd} Unit]^? since - | the part () ->{cap.rd} Unit of that type captures the root capability `cap`. - | This is often caused by a locally generated exception capability leaking as part of its result. + | The result of `try` cannot have type Cell[() => Unit]^? since + | the part () => Unit of that type captures the root capability `cap`. + | This is often caused by a locally generated exception capability leaking as part of its result. | - | where: cap is a fresh root capability classified as Control in the type of given instance canThrow$4 + | where: => refers to a fresh root capability classified as Control in the type of given instance canThrow$4 33 | Cell(() => foo(1)) 34 | catch 35 | case _: Ex1 => ??? diff --git a/tests/neg-custom-args/captures/restrict-subsumes.scala b/tests/neg-custom-args/captures/restrict-subsumes.scala index 8bd17f7330a6..71d4df5f06ba 100644 --- a/tests/neg-custom-args/captures/restrict-subsumes.scala +++ b/tests/neg-custom-args/captures/restrict-subsumes.scala @@ -1,7 +1,7 @@ -import caps.{cap, Classifier, Capability} +import caps.{cap, Classifier, SharedCapability} -trait Read extends Capability, Classifier -trait Write extends Capability, Classifier +trait Read extends SharedCapability, Classifier +trait Write extends SharedCapability, Classifier trait A extends Read trait B extends Write diff --git a/tests/neg-custom-args/captures/ro-mut-conformance.check b/tests/neg-custom-args/captures/ro-mut-conformance.check index 9ac0fe2be51e..0f6ce6bfcf58 100644 --- a/tests/neg-custom-args/captures/ro-mut-conformance.check +++ b/tests/neg-custom-args/captures/ro-mut-conformance.check @@ -11,7 +11,6 @@ | | where: ^ refers to a fresh root capability classified as Mutable in the type of value t | - | Note that {cap} is an exclusive capture set of the mutable type Ref^, - | it cannot subsume a read-only capture set of the mutable type (a : Ref). + | Note that capability (a : Ref) is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/scope-extrude-mut.check b/tests/neg-custom-args/captures/scope-extrude-mut.check index fb917d7ceeae..64a17296b7d4 100644 --- a/tests/neg-custom-args/captures/scope-extrude-mut.check +++ b/tests/neg-custom-args/captures/scope-extrude-mut.check @@ -7,4 +7,7 @@ |where: ^ refers to a fresh root capability classified as Mutable created in value a1 when constructing mutable A | ^² refers to a fresh root capability classified as Mutable in the type of variable a | + |Note that capability cap is not included in capture set {cap} + |because cap in method b is not visible from cap in variable a. + | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/scoped-caps.check b/tests/neg-custom-args/captures/scoped-caps.check index 65d9865a393c..d0fbdccd1305 100644 --- a/tests/neg-custom-args/captures/scoped-caps.check +++ b/tests/neg-custom-args/captures/scoped-caps.check @@ -8,6 +8,9 @@ | ^² refers to a root capability associated with the result type of (x: A^): B^² | ^³ refers to a fresh root capability in the type of value g | + | Note that capability is not included in capture set {cap} + | because is not visible from cap in value g. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:9:25 ----------------------------------- 9 | val _: (x: A^) -> B^ = g // error @@ -18,8 +21,7 @@ | 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 g* since that capability is not a `Sharable` capability + | Note that capability g* is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:10:20 ---------------------------------- @@ -32,64 +34,94 @@ | ^² refers to a root capability associated with the result type of (x: A^): B^² | ^³ refers to a fresh root capability in the type of value _$3 | + | Note that capability is not included in capture set {cap} + | because is not visible from cap in value _$3. + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:12:20 ---------------------------------- +12 | val _: A^ -> B^ = x => g(x) // error: g is no longer pure, since it contains the ^ of B + | ^^^^^^^^^ + | Found: (x: A^) ->{g} B^{g*} + | Required: A^ -> B^² + | + | where: ^ refers to the universal root capability + | ^² refers to a fresh root capability in the type of value _$5 + | + | Note that capability (g : A^ -> B^) is not included in capture set {}. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:13:25 ---------------------------------- 13 | val _: (x: A^) -> B^ = x => f(x) // error: existential in B cannot subsume `x` since `x` is not shared | ^^^^^^^^^ - | Found: (x: A^) ->? B^{x} - | Required: (x: A^) -> B^² + | Found: (x: A^) ->? B^{x} + | Required: (x: A^) -> B^² | - | where: ^ refers to the universal root capability - | ^² refers to a root capability associated with the result type of (x: A^): B^² + | 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 `Sharable` capability + | Note that capability x.type is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:16:24 ---------------------------------- 16 | val _: (x: S) -> B^ = h // error: direct conversion fails | ^ - | Found: S^{cap.rd} -> B^{h*} - | Required: (x: S^{cap.rd}) -> B^ + | Found: S^ -> B^{h*} + | Required: (x: S^) -> B^² | - | where: ^ refers to a root capability associated with the result type of (x: S^{cap.rd}): B^ - | cap is the universal root capability + | where: ^ refers to the universal root capability + | ^² refers to a root capability associated with the result type of (x: S^): B^² | - | Note that the existential capture root in B^ - | cannot subsume the capability h* since that capability is not a `Sharable` capability + | Note that capability h* is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:17:24 ---------------------------------- 17 | val _: (x: S) -> B^ = (x: S) => h(x) // error: eta expansion fails | ^^^^^^^^^^^^^^ - | Found: (x: S^{cap.rd}) ->? B^{h*} - | Required: (x: S^{cap.rd}) -> B^ + | Found: (x: S^) ->{h} B^{h*} + | Required: (x: S^) -> B^² | - | where: ^ refers to a root capability associated with the result type of (x: S^{cap.rd}): B^ - | cap is the universal root capability + | where: ^ refers to the universal root capability + | ^² refers to a root capability associated with the result type of (x: S^): B^² | - | Note that the existential capture root in B^ - | cannot subsume the capability h* since that capability is not a `Sharable` capability + | Note that capability (h : S -> B^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:26:19 ---------------------------------- -26 | val _: S -> B^ = j // error - | ^ - | Found: (j : (x: S) -> B^) - | Required: S^{cap.rd} -> B^² +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:21:23 ---------------------------------- +21 | val _: (x: S) -> S = (x: S) => h2(x) // error: eta conversion fails since `h2` is now impure (result type S is a capability) + | ^^^^^^^^^^^^^^^ + | Found: (x: S^) ->{h2} S^{h2*} + | Required: (x: S^) -> S^² | - | where: ^ refers to a root capability associated with the result type of (x: S^{cap.rd}): B^ - | ^² refers to a fresh root capability in the type of value _$13 - | cap is the universal root capability + | where: ^ refers to the universal root capability + | ^² refers to a root capability associated with the result type of (x: S^): S^² + | + | Note that capability (h2 : S -> S) is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:27:19 ---------------------------------- -27 | val _: S -> B^ = x => j(x) // error +27 | val _: S -> B^ = j // error + | ^ + | Found: (j : (x: S) -> B^) + | Required: S^² -> B^³ + | + | where: ^ refers to a root capability associated with the result type of (x: S^²): B^ + | ^² refers to the universal root capability + | ^³ refers to a fresh root capability in the type of value _$14 + | + | Note that capability is not included in capture set {cap} + | because is not visible from cap in value _$14. + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:28:19 ---------------------------------- +28 | val _: S -> B^ = x => j(x) // error | ^^^^^^^^^ - | Found: (x: S^{cap.rd}) ->? B^{x} - | Required: S^{cap.rd} -> B^ + | Found: (x: S^) ->? B^{x} + | Required: S^ -> B^² + | + | where: ^ refers to the universal root capability + | ^² refers to a fresh root capability in the type of value _$15 | - | where: ^ refers to a fresh root capability in the type of value _$14 - | cap is the universal root capability + | Note that capability x.type is not included in capture set {cap} + | because x.type is not visible from cap in value _$15. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/scoped-caps.scala b/tests/neg-custom-args/captures/scoped-caps.scala index 9d11f9f00b7e..128e8c095086 100644 --- a/tests/neg-custom-args/captures/scoped-caps.scala +++ b/tests/neg-custom-args/captures/scoped-caps.scala @@ -1,6 +1,6 @@ class A class B -class S extends caps.Sharable +class S extends caps.SharedCapability def test(io: Object^): Unit = val f: (x: A^) -> B^ = ??? @@ -9,7 +9,7 @@ def test(io: Object^): Unit = val _: (x: A^) -> B^ = g // error val _: A^ -> B^ = f // error val _: A^ -> B^ = g - val _: A^ -> B^ = x => g(x) // now ok, was error: since g is pure, g(x): B^{x} , which does not match B^{fresh} + val _: A^ -> B^ = x => g(x) // error: g is no longer pure, since it contains the ^ of B val _: (x: A^) -> B^ = x => f(x) // error: existential in B cannot subsume `x` since `x` is not shared val h: S -> B^ = ??? @@ -18,7 +18,8 @@ def test(io: Object^): Unit = val h2: S -> S = ??? val _: (x: S) -> S = h2 // direct conversion OK for shared S - val _: (x: S) -> S = (x: S) => h2(x) // eta conversion is also OK + val _: (x: S) -> S = (x: S) => h2(x) // error: eta conversion fails since `h2` is now impure (result type S is a capability) + val _: (x: S) ->{h2} S = (x: S) => h2(x) // eta expansion OK val j: (x: S) -> B^ = ??? val _: (x: S) -> B^ = j diff --git a/tests/neg-custom-args/captures/sep-box.check b/tests/neg-custom-args/captures/sep-box.check index a0fe7340b93b..590c0b01c757 100644 --- a/tests/neg-custom-args/captures/sep-box.check +++ b/tests/neg-custom-args/captures/sep-box.check @@ -1,16 +1,16 @@ -- Error: tests/neg-custom-args/captures/sep-box.scala:41:9 ------------------------------------------------------------ 41 | par(h1.value, h2.value) // error | ^^^^^^^^ - |Separation failure: argument of type Ref^{h1.value*} + |Separation failure: argument of type Ref^{xs*} |to method par: (x: Ref^, y: Ref^): Unit |corresponds to capture-polymorphic formal parameter x of type Ref^ - |and hides capabilities {h1.value*}. - |Some of these overlap with the captures of the second argument with type Ref^{h2.value*}. + |and hides capabilities {xs*}. + |Some of these overlap with the captures of the second argument with type Ref^{xs*}. | - | Hidden set of current argument : {h1.value*} - | Hidden footprint of current argument : {h1.value*, xs*} - | Capture set of second argument : {h2.value*} - | Footprint set of second argument : {h2.value*, xs*} + | Hidden set of current argument : {xs*} + | Hidden footprint of current argument : {xs*} + | Capture set of second argument : {xs*} + | Footprint set of second argument : {xs*} | The two sets overlap at : {xs*} | |where: ^ refers to a fresh root capability classified as Mutable created in method test when checking argument to parameter x of method par diff --git a/tests/neg-custom-args/captures/sep-curried.check b/tests/neg-custom-args/captures/sep-curried.check index 04ca5644bc33..dd0c4d14efa2 100644 --- a/tests/neg-custom-args/captures/sep-curried.check +++ b/tests/neg-custom-args/captures/sep-curried.check @@ -1,10 +1,12 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/sep-curried.scala:48:43 ---------------------------------- 48 | val f: (y: Ref[Int]^{a}) ->{a} Unit = foo(a) // error | ^^^^^^ - | Found: (y: Ref[Int]^) ->{a} Unit - | Required: (y: Ref[Int]^{a}) ->{a} Unit + | Found: (y: Ref[Int]^) ->{a} Unit + | Required: (y: Ref[Int]^{a}) ->{a} Unit | - | where: ^ refers to the universal root capability + | where: ^ refers to the universal root capability + | + | Note that capability (a : Ref[Int]^) is not included in capture set {cap}. | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/sep-curried.scala:16:6 -------------------------------------------------------- diff --git a/tests/neg-custom-args/captures/sep-shared.scala b/tests/neg-custom-args/captures/sep-shared.scala new file mode 100644 index 000000000000..b3509fe37bc6 --- /dev/null +++ b/tests/neg-custom-args/captures/sep-shared.scala @@ -0,0 +1,7 @@ +class E extends caps.ExclusiveCapability +class S extends caps.SharedCapability + +def par(x: E^, y: E^): E = ??? + +def test(x: E^) = par(x, x) // error + diff --git a/tests/neg-custom-args/captures/sep-use2.check b/tests/neg-custom-args/captures/sep-use2.check index 21980d592ef1..d6379639f0bc 100644 --- a/tests/neg-custom-args/captures/sep-use2.check +++ b/tests/neg-custom-args/captures/sep-use2.check @@ -47,15 +47,15 @@ 24 | { f(c) } // error | ^ |Separation failure: argument of type (c : Object^) - |to a function of type Object^ ->{f} Object^{f*} + |to a function of type Object^ ->{c} Object^{f*} |corresponds to capture-polymorphic formal parameter v1 of type Object^² |and hides capabilities {c}. |Some of these overlap with the captures of the function prefix. | | Hidden set of current argument : {c} | Hidden footprint of current argument : {c} - | Capture set of function prefix : {f*} - | Footprint set of function prefix : {f*, c} + | Capture set of function prefix : {c, f*} + | Footprint set of function prefix : {c, f*} | The two sets overlap at : {c} | |where: ^ refers to a fresh root capability in the type of parameter c @@ -69,15 +69,15 @@ 28 | { f(c) } // error | ^ |Separation failure: argument of type (c : Object^) - |to a function of type Object^ ->{f} Object^{f*} + |to a function of type Object^ ->{c} Object^{f*} |corresponds to capture-polymorphic formal parameter v1 of type Object^² |and hides capabilities {c}. |Some of these overlap with the captures of the function prefix. | | Hidden set of current argument : {c} | Hidden footprint of current argument : {c} - | Capture set of function prefix : {f*} - | Footprint set of function prefix : {f*, c} + | Capture set of function prefix : {c, f*} + | Footprint set of function prefix : {c, f*} | The two sets overlap at : {c} | |where: ^ refers to a fresh root capability in the type of parameter c diff --git a/tests/neg-custom-args/captures/shared-capability.check b/tests/neg-custom-args/captures/shared-capability.check index 0c575cd69b78..15355a9fc5b9 100644 --- a/tests/neg-custom-args/captures/shared-capability.check +++ b/tests/neg-custom-args/captures/shared-capability.check @@ -1,6 +1,6 @@ -- Error: tests/neg-custom-args/captures/shared-capability.scala:9:13 -------------------------------------------------- 9 |def test2(a: Async^): Object^ = a // error | ^^^^^^ - | Async^ extends Sharable, so it cannot capture `cap` + | Async^ extends SharedCapability, so it cannot capture `cap` | | where: ^ refers to the universal root capability diff --git a/tests/neg-custom-args/captures/shared-capability.scala b/tests/neg-custom-args/captures/shared-capability.scala deleted file mode 100644 index f10bc6f53444..000000000000 --- a/tests/neg-custom-args/captures/shared-capability.scala +++ /dev/null @@ -1,10 +0,0 @@ - - -import caps.Sharable - -class Async extends Sharable - -def test1(a: Async): Object^ = a // OK - -def test2(a: Async^): Object^ = a // error - diff --git a/tests/neg-custom-args/captures/simple-using.check b/tests/neg-custom-args/captures/simple-using.check index 16ee43bbbe6b..681e83136571 100644 --- a/tests/neg-custom-args/captures/simple-using.check +++ b/tests/neg-custom-args/captures/simple-using.check @@ -7,7 +7,7 @@ |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 ? + |Note that capability f.type + |cannot be included in outer capture set ?. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/spread-problem.check b/tests/neg-custom-args/captures/spread-problem.check index 91022f920486..6f6f169d90e4 100644 --- a/tests/neg-custom-args/captures/spread-problem.check +++ b/tests/neg-custom-args/captures/spread-problem.check @@ -3,6 +3,7 @@ | ^^^^^^^^^^^^^^^^^^^^^^ | Found: Source[T^?]^{src1, src2} | Required: Source[T] + | Note that capability (src1 : Source[T]^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/spread-problem.scala:11:6 -------------------------------- @@ -10,5 +11,6 @@ | ^^^^^^^^^^^^^^^^ | Found: Source[T^?]^{src1, src2} | Required: Source[T] + | Note that capability (src1 : Source[T]^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/test22.scala b/tests/neg-custom-args/captures/test22.scala new file mode 100644 index 000000000000..6b83ac278648 --- /dev/null +++ b/tests/neg-custom-args/captures/test22.scala @@ -0,0 +1,13 @@ +class A +class B +class S extends caps.SharedCapability + +def test(io: Object^): Unit = + val h2: S -> S = ??? + val _: (x: S) -> S = h2 // direct conversion OK for shared S + val _: (x: S) -> S = (x: S) => h2(x) // error: eta conversion fails since `h2` is now impure (result type S is a capability) + val _: (x: S) ->{h2} S = + (x: S) => + val y = h2(x) // eta expansion OK + y + diff --git a/tests/neg-custom-args/captures/try.check b/tests/neg-custom-args/captures/try.check index c470ee13e9ca..1d5434b04010 100644 --- a/tests/neg-custom-args/captures/try.check +++ b/tests/neg-custom-args/captures/try.check @@ -14,6 +14,9 @@ |where: => refers to a fresh root capability created in value a when checking argument to parameter op of method handle | ^ refers to the universal root capability | ^² refers to a fresh root capability created in value a when checking argument to parameter op of method handle + | + |Note that capability x.type is not included in capture set {cap} + |because x.type is not visible from cap in value a. 24 | (x: CanThrow[Exception]) => x 25 | }{ | @@ -26,6 +29,8 @@ | |where: => refers to a fresh root capability created in value b when checking argument to parameter op of method handle | ^ refers to the universal root capability + | + |Note that capability x.type is not included in capture set {}. 30 | (x: CanThrow[Exception]) => () => raise(new Exception)(using x) 31 | } { | @@ -39,8 +44,8 @@ |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 ? + |Note that capability x.type + |cannot be included in outer capture set ?. 36 | (x: CanThrow[Exception]) => 37 | () => 38 | raise(new Exception)(using x) @@ -57,8 +62,8 @@ |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 ? + |Note that capability x.type + |cannot be included in outer capture set ?. 48 | (x: CanThrow[Exception]) => 49 | () => 50 | raise(new Exception)(using x) diff --git a/tests/neg-custom-args/captures/unsound-reach-4.check b/tests/neg-custom-args/captures/unsound-reach-4.check index 576e3c46186b..be216502f3ad 100644 --- a/tests/neg-custom-args/captures/unsound-reach-4.check +++ b/tests/neg-custom-args/captures/unsound-reach-4.check @@ -13,6 +13,9 @@ | | where: ^ refers to a fresh root capability in the type of value backdoor | + | Note that capability cap is not included in capture set {cap} + | because cap is not visible from cap in value backdoor. + | | longer explanation available when compiling with `-explain` -- [E164] Declaration Error: tests/neg-custom-args/captures/unsound-reach-4.scala:17:6 --------------------------------- 17 | def use(@consume x: F): File^ = x // error @consume override diff --git a/tests/neg-custom-args/captures/unsound-reach-6.check b/tests/neg-custom-args/captures/unsound-reach-6.check index 8308e2336d7c..e53c05868e43 100644 --- a/tests/neg-custom-args/captures/unsound-reach-6.check +++ b/tests/neg-custom-args/captures/unsound-reach-6.check @@ -3,6 +3,7 @@ | ^ | Found: (x : () ->{ys*} Unit) | Required: () -> Unit + | Note that capability ys* is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/unsound-reach-6.scala:21:22 ------------------------------ @@ -10,6 +11,7 @@ | ^ | Found: (x : () ->{io} Unit) | Required: () -> Unit + | Note that capability (io : IO^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/unsound-reach-6.scala:7:13 ---------------------------------------------------- diff --git a/tests/neg-custom-args/captures/unsound-reach.check b/tests/neg-custom-args/captures/unsound-reach.check index 23af7d907362..b9cb97a9819a 100644 --- a/tests/neg-custom-args/captures/unsound-reach.check +++ b/tests/neg-custom-args/captures/unsound-reach.check @@ -20,4 +20,7 @@ | | where: ^ refers to a fresh root capability in the type of value backdoor | + | Note that capability cap is not included in capture set {cap} + | because cap is not visible from cap in value backdoor. + | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/use-capset.check b/tests/neg-custom-args/captures/use-capset.check index fc65636b1302..da88f021c56b 100644 --- a/tests/neg-custom-args/captures/use-capset.check +++ b/tests/neg-custom-args/captures/use-capset.check @@ -3,13 +3,15 @@ | ^ | Found: (h : () ->{io} Unit) | Required: () -> Unit + | Note that capability (io : Object^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:13:50 ----------------------------------- 13 | val _: () -> List[Object^{io}] -> Object^{io} = h2 // error, should be ->{io} | ^^ - | Found: (h2 : () ->{} List[Object^{io}]^{} ->{io} Object^{io}) - | Required: () -> List[Object^{io}] -> Object^{io} + | Found: (h2 : () ->{} List[Object^{io}]^{} ->{io} Object^{io}) + | Required: () -> List[Object^{io}] -> Object^{io} + | Note that capability (io : Object^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/use-capset.scala:5:49 --------------------------------------------------------- diff --git a/tests/neg-custom-args/captures/uses.check b/tests/neg-custom-args/captures/uses.check index d201d79133cf..c5044c647ce0 100644 --- a/tests/neg-custom-args/captures/uses.check +++ b/tests/neg-custom-args/captures/uses.check @@ -3,6 +3,7 @@ | ^ | Found: (d : D^{x, y}) | Required: D^{y} + | Note that capability (x : C^) is not included in capture set {y}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/uses.scala:9:13 ------------------------------------------ @@ -10,6 +11,7 @@ | ^ | Found: (d : D^{x, y}) | Required: D + | Note that capability (x : C^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/uses.scala:18:34 ----------------------------------------- @@ -17,6 +19,7 @@ | ^ | Found: () ->{x, y} () ->{y} Unit | Required: () ->{x} () ->{y} Unit + | Note that capability (y : C^) is not included in capture set {x}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/uses.scala:19:28 ----------------------------------------- @@ -24,5 +27,6 @@ | ^ | Found: () ->{x, y} () ->{y} Unit | Required: () -> () -> Unit + | Note that capability (x : C^) is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/usingLogFile.check b/tests/neg-custom-args/captures/usingLogFile.check index 81f57e8ba655..3add71106063 100644 --- a/tests/neg-custom-args/captures/usingLogFile.check +++ b/tests/neg-custom-args/captures/usingLogFile.check @@ -7,8 +7,8 @@ |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 ? + |Note that capability f.type + |cannot be included in outer capture set ?. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:27:36 --------------------------------- @@ -20,8 +20,8 @@ |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 ? + |Note that capability f.type + |cannot be included in outer capture set ?. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:43:33 --------------------------------- @@ -33,8 +33,8 @@ |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 ? + |Note that capability f.type + |cannot be included in outer capture set ?. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/usingLogFile.scala:52:6 ---------------------------------- @@ -46,7 +46,7 @@ |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 ? + |Note that capability _$1.type + |cannot be included in outer capture set ?. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/vars-simple.check b/tests/neg-custom-args/captures/vars-simple.check index 7454ba0ecfbd..931fb0c19cca 100644 --- a/tests/neg-custom-args/captures/vars-simple.check +++ b/tests/neg-custom-args/captures/vars-simple.check @@ -6,12 +6,15 @@ | | where: => refers to a fresh root capability created in method scope | + | Note that capability cap is not included in capture set {cap1, cap2}. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars-simple.scala:16:8 ----------------------------------- 16 | a = g // error | ^ | Found: (x: String) ->{cap3} String | Required: String ->{cap1, cap2} String + | Note that capability (cap3 : CC^) is not included in capture set {cap1, cap2}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars-simple.scala:17:12 ---------------------------------- @@ -19,5 +22,6 @@ | ^^^^^^^ | Found: List[String ->{cap3} String] | Required: List[String ->{cap1, cap2} String] + | Note that capability (cap3 : CC^) is not included in capture set {cap1, cap2}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/vars.check b/tests/neg-custom-args/captures/vars.check index 484f9270e71f..568bd90b746d 100644 --- a/tests/neg-custom-args/captures/vars.check +++ b/tests/neg-custom-args/captures/vars.check @@ -3,6 +3,8 @@ | ^^^^^^^^^ | Found: (x: String) ->{cap3} String | Required: String ->{cap1} String + | Note that capability (cap3 : CC^), defined in method scope + | cannot be included in outer capture set {cap1} of variable a. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars.scala:25:8 ------------------------------------------ @@ -10,6 +12,8 @@ | ^ | Found: (x: String) ->{cap3} String | Required: String ->{cap1} String + | Note that capability (cap3 : CC^), defined in method scope + | cannot be included in outer capture set {cap1} of variable a. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars.scala:27:12 ----------------------------------------- @@ -17,18 +21,20 @@ | ^^^^^^^ | Found: List[String ->{cap3} String] | Required: List[String ->{cap1, cap2} String] + | Note that capability (cap3 : CC^) is not included in capture set {cap1, cap2}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars.scala:36:8 ------------------------------------------ 36 | local { cap3 => // error | ^ | Found: (cap3: CC^) ->? String ->{cap3} String - | Required: CC^ -> String ->? String + | Required: CC^ -> String => String | - | where: ^ refers to the universal root capability + | where: => refers to a fresh root capability created in method test + | ^ refers to the universal root capability | - | Note that reference cap3.type - | cannot be included in outer capture set ? + | Note that capability cap3.type + | cannot be included in outer capture set {cap}. 37 | def g(x: String): String = if cap3 == cap3 then "" else "a" 38 | g 39 | } diff --git a/tests/neg-custom-args/captures/widen-reach.check b/tests/neg-custom-args/captures/widen-reach.check index 9d0ecceb1808..07a8c301a0c0 100644 --- a/tests/neg-custom-args/captures/widen-reach.check +++ b/tests/neg-custom-args/captures/widen-reach.check @@ -14,6 +14,9 @@ | where: ^ refers to the universal root capability | ^² refers to a fresh root capability in the type of value foo | + | Note that capability x.type is not included in capture set {cap} + | because x.type is not visible from cap in value foo. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/widen-reach.scala:13:26 ---------------------------------- 13 | val y2: IO^ -> IO^ = y1.foo // error @@ -24,6 +27,8 @@ | where: ^ refers to the universal root capability | ^² refers to a fresh root capability in the type of value y2 | + | Note that capability x* is not included in capture set {}. + | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/widen-reach.scala:14:30 ---------------------------------- 14 | val y3: IO^ -> IO^{x*} = y1.foo // error @@ -33,4 +38,6 @@ | | where: ^ refers to the universal root capability | + | Note that capability x* is not included in capture set {}. + | | longer explanation available when compiling with `-explain` diff --git a/tests/pos-custom-args/captures/boxed1.scala b/tests/pos-custom-args/captures/boxed1.scala index e2ff69c305d2..447b18eaed21 100644 --- a/tests/pos-custom-args/captures/boxed1.scala +++ b/tests/pos-custom-args/captures/boxed1.scala @@ -1,6 +1,6 @@ class Box[T](val x: T) -class Cap extends caps.Capability +class Cap extends caps.SharedCapability def foo(x: => Int): Unit = () diff --git a/tests/pos-custom-args/captures/cap-problem.scala b/tests/pos-custom-args/captures/cap-problem.scala index 483b4e938b1b..145e548058e3 100644 --- a/tests/pos-custom-args/captures/cap-problem.scala +++ b/tests/pos-custom-args/captures/cap-problem.scala @@ -5,9 +5,9 @@ trait Suspend: def resume(s: Suspension): Unit -import caps.Capability +import caps.SharedCapability -trait Async(val support: Suspend) extends Capability +trait Async(val support: Suspend) extends SharedCapability class CancelSuspension(ac: Async, suspension: ac.support.Suspension): ac.support.resume(suspension) diff --git a/tests/pos-custom-args/captures/cap-refine.scala b/tests/pos-custom-args/captures/cap-refine.scala index ed0b4d018b88..dd0194f50bb8 100644 --- a/tests/pos-custom-args/captures/cap-refine.scala +++ b/tests/pos-custom-args/captures/cap-refine.scala @@ -1,7 +1,7 @@ //> using options -Werror -import caps.Capability +import caps.SharedCapability -trait Buffer[T] extends Capability: +trait Buffer[T] extends SharedCapability: def append(x: T): this.type def f(buf: Buffer[Int]) = diff --git a/tests/pos-custom-args/captures/capt-capability.scala b/tests/pos-custom-args/captures/capt-capability.scala index 21c63d3fa608..df253bf59dfe 100644 --- a/tests/pos-custom-args/captures/capt-capability.scala +++ b/tests/pos-custom-args/captures/capt-capability.scala @@ -1,4 +1,4 @@ -import caps.{Capability, Sharable} +import caps.{SharedCapability, Capability} def f1(c: Capability): () ->{c} c.type = () => c // ok @@ -14,7 +14,7 @@ def f3: Int = x def foo() = - val x: Sharable = ??? + val x: SharedCapability = ??? val y: Capability = x val x2: () ->{x} Capability = ??? val y2: () ->{x} Capability = x2 @@ -23,7 +23,7 @@ def foo() = def h[X](a: X)(b: X) = a val z2: (y: Unit) ->{x} Capability^ = - if x == null then (y: Unit) => x else (y: Unit) => new Capability() {} + if x == null then (y: Unit) => x else (y: Unit) => new SharedCapability() {} // z2's type cannot be inferred, see neg test //val z3 = // if x == null then (y: Unit) => x else (y: Unit) => new Capability() {} diff --git a/tests/pos-custom-args/captures/caseclass.scala b/tests/pos-custom-args/captures/caseclass.scala index bae55a82c3bc..22b7f1b1eb9a 100644 --- a/tests/pos-custom-args/captures/caseclass.scala +++ b/tests/pos-custom-args/captures/caseclass.scala @@ -1,4 +1,4 @@ -class C extends caps.Capability +class C extends caps.SharedCapability class STR(s: String) object test1: case class Ref(x: STR^) diff --git a/tests/pos-custom-args/captures/cc-poly-1.scala b/tests/pos-custom-args/captures/cc-poly-1.scala index 96bd58d65334..986564204bfd 100644 --- a/tests/pos-custom-args/captures/cc-poly-1.scala +++ b/tests/pos-custom-args/captures/cc-poly-1.scala @@ -1,10 +1,10 @@ import language.experimental.captureChecking import annotation.experimental -import caps.{CapSet, Capability} +import caps.{CapSet, SharedCapability} @experimental object Test: - class C extends Capability + class C extends SharedCapability class D def f[X^](x: D^{X}): D^{X} = x diff --git a/tests/pos-custom-args/captures/cc-poly-source-capability.scala b/tests/pos-custom-args/captures/cc-poly-source-capability.scala index 7d06edd36415..c76e6067fbef 100644 --- a/tests/pos-custom-args/captures/cc-poly-source-capability.scala +++ b/tests/pos-custom-args/captures/cc-poly-source-capability.scala @@ -1,11 +1,11 @@ import language.experimental.captureChecking import annotation.experimental -import caps.{CapSet, Sharable} +import caps.{CapSet, SharedCapability} import caps.use @experimental object Test: - class Async extends Sharable + class Async extends SharedCapability def listener(async: Async): Listener^{async} = ??? diff --git a/tests/pos-custom-args/captures/cc-this.scala b/tests/pos-custom-args/captures/cc-this.scala index 72c848630def..6aa21a7a6c70 100644 --- a/tests/pos-custom-args/captures/cc-this.scala +++ b/tests/pos-custom-args/captures/cc-this.scala @@ -2,7 +2,7 @@ import caps.consume import caps.unsafe.unsafeAssumeSeparate -class Cap extends caps.Capability +class Cap extends caps.SharedCapability def eff(using Cap): Unit = () diff --git a/tests/pos-custom-args/captures/check-override-typebounds.scala b/tests/pos-custom-args/captures/check-override-typebounds.scala index 7a662c78b208..279d3d9a9252 100644 --- a/tests/pos-custom-args/captures/check-override-typebounds.scala +++ b/tests/pos-custom-args/captures/check-override-typebounds.scala @@ -6,7 +6,7 @@ trait A: class B extends A: type T = C -class C extends caps.Capability +class C extends caps.SharedCapability trait A2: diff --git a/tests/pos-custom-args/captures/erased-methods2-shared.scala b/tests/pos-custom-args/captures/erased-methods2-shared.scala new file mode 100644 index 000000000000..24e42dae4322 --- /dev/null +++ b/tests/pos-custom-args/captures/erased-methods2-shared.scala @@ -0,0 +1,34 @@ +import language.experimental.saferExceptions +import language.experimental.erasedDefinitions +import language.experimental.captureChecking + +class Ex1 extends Exception("Ex1") +class Ex2 extends Exception("Ex2") +class Ex3 extends Exception("Ex3") + +class CT[-E <: Exception] extends caps.SharedCapability, compiletime.Erased + +def Throw[Ex <: Exception](ex: Ex)(using CT[Ex]^): Nothing = ??? + +def foo8a(i: Int) = + (erased xx1: CT[Ex2]^) ?=> Throw(new Ex2) + +def foo9a(i: Int) + : (x$1: CT[Ex3]^) + ?=> (x$2: CT[Ex2]^) + ?=> Unit + = (x$1: CT[Ex3]^) // error + ?=> (x$2: CT[Ex2]^) + ?=> + //given (CT[Ex3]^) = x$1 + Throw(new Ex3) + +def foo10a(i: Int) + : (erased x$0: CT[Ex3]^) + ?=> (erased x$1: CT[Ex2]^) + ?=> (erased x$2: CT[Ex1]^) + ?=> Unit + = (erased x$1: CT[Ex3]^) // error + ?=> (erased x$2: CT[Ex2]^) + ?=> (erased x$3: CT[Ex1]^) + ?=> Throw(new Ex3) diff --git a/tests/pos-custom-args/captures/eta-expansions.scala b/tests/pos-custom-args/captures/eta-expansions.scala index cbe72137bd65..09c369d47ba6 100644 --- a/tests/pos-custom-args/captures/eta-expansions.scala +++ b/tests/pos-custom-args/captures/eta-expansions.scala @@ -1,4 +1,4 @@ -class Cap extends caps.Capability +class Cap extends caps.SharedCapability def test(d: Cap) = def map2(xs: List[Int])(f: Int => Int): List[Int] = xs.map(f) diff --git a/tests/pos-custom-args/captures/ex-fun-aliases.scala.disabled b/tests/pos-custom-args/captures/ex-fun-aliases.scala.disabled index ff86927b874c..6f2acd2b2a33 100644 --- a/tests/pos-custom-args/captures/ex-fun-aliases.scala.disabled +++ b/tests/pos-custom-args/captures/ex-fun-aliases.scala.disabled @@ -1,5 +1,5 @@ import language.experimental.captureChecking -import caps.{Exists, Capability} +import caps.{Exists, SharedCapability} class C diff --git a/tests/pos-custom-args/captures/filevar-tracked.scala b/tests/pos-custom-args/captures/filevar-tracked.scala index dc8d0b18908b..8c48017502b8 100644 --- a/tests/pos-custom-args/captures/filevar-tracked.scala +++ b/tests/pos-custom-args/captures/filevar-tracked.scala @@ -18,7 +18,7 @@ object test1: o.log object test2: - class IO extends caps.Capability + class IO extends caps.SharedCapability class File: def write(x: String): Unit = ??? diff --git a/tests/pos-custom-args/captures/filevar.scala b/tests/pos-custom-args/captures/filevar.scala index dc8d0b18908b..8c48017502b8 100644 --- a/tests/pos-custom-args/captures/filevar.scala +++ b/tests/pos-custom-args/captures/filevar.scala @@ -18,7 +18,7 @@ object test1: o.log object test2: - class IO extends caps.Capability + class IO extends caps.SharedCapability class File: def write(x: String): Unit = ??? diff --git a/tests/pos-custom-args/captures/i16116.scala b/tests/pos-custom-args/captures/i16116.scala index a103b9a740e2..e66b2cea6711 100644 --- a/tests/pos-custom-args/captures/i16116.scala +++ b/tests/pos-custom-args/captures/i16116.scala @@ -15,7 +15,7 @@ object CpsMonad { @experimental object Test { - class CpsTransform[F[_]] extends caps.Capability { + class CpsTransform[F[_]] extends caps.SharedCapability { def await[T](ft: F[T]): T^{ this } = ??? } diff --git a/tests/pos-custom-args/captures/i16226.scala b/tests/pos-custom-args/captures/i16226.scala index 79893d7266ba..af0a44e6bdfc 100644 --- a/tests/pos-custom-args/captures/i16226.scala +++ b/tests/pos-custom-args/captures/i16226.scala @@ -1,4 +1,4 @@ -class Cap extends caps.Sharable +class Cap extends caps.SharedCapability class LazyRef[T](val elem: () => T): val get: () ->{elem} T = elem diff --git a/tests/pos-custom-args/captures/i19751.scala b/tests/pos-custom-args/captures/i19751.scala index b41017f4f3e7..3450535308a5 100644 --- a/tests/pos-custom-args/captures/i19751.scala +++ b/tests/pos-custom-args/captures/i19751.scala @@ -1,13 +1,12 @@ import language.experimental.captureChecking -import caps.cap +import caps.{cap, Shared, SharedCapability} trait Ptr[A] -trait Scope extends caps.Capability: +trait Scope extends caps.SharedCapability: def allocate(size: Int): Ptr[Unit]^{this} - object Scope: - def confined[A](fn: Scope ?->{cap} A): A = + def confined[A](fn: Scope ?->{cap.only[Shared]} A): A = val scope = new Scope: def allocate(size: Int) = new Ptr[Unit] {} fn(using scope) diff --git a/tests/pos-custom-args/captures/i20237-explicit.scala b/tests/pos-custom-args/captures/i20237-explicit.scala index 0999d4acd50e..16b52266bc1b 100644 --- a/tests/pos-custom-args/captures/i20237-explicit.scala +++ b/tests/pos-custom-args/captures/i20237-explicit.scala @@ -1,6 +1,6 @@ import language.experimental.captureChecking -class Cap extends caps.Capability: +class Cap extends caps.SharedCapability: def use[T](body: Cap => T) = body(this) class Box[T](body: Cap => T): diff --git a/tests/pos-custom-args/captures/i20237.scala b/tests/pos-custom-args/captures/i20237.scala index 53efbb2e7583..80618141998c 100644 --- a/tests/pos-custom-args/captures/i20237.scala +++ b/tests/pos-custom-args/captures/i20237.scala @@ -1,10 +1,10 @@ import language.experimental.captureChecking import caps.* -class Cap extends caps.Capability: +class Cap extends caps.SharedCapability: def use[T](body: Cap ?=> T) = body(using this) -class Cap2 extends caps.Capability: +class Cap2 extends caps.SharedCapability: def use[T](body: Cap2 => T) = body(this) class Box[T](body: Cap ?=> T): diff --git a/tests/pos-custom-args/captures/i21646.scala b/tests/pos-custom-args/captures/i21646.scala index 92aba9fda5d1..23698cfb14bc 100644 --- a/tests/pos-custom-args/captures/i21646.scala +++ b/tests/pos-custom-args/captures/i21646.scala @@ -1,7 +1,7 @@ import language.experimental.captureChecking -import caps.Capability +import caps.{Capability, SharedCapability} -trait File extends Capability +trait File extends SharedCapability class Resource[T <: Capability](gen: T): def use[U](f: T => U): U = diff --git a/tests/pos-custom-args/captures/i23422.scala b/tests/pos-custom-args/captures/i23422.scala index 8e03d6701763..f014473f3f2d 100644 --- a/tests/pos-custom-args/captures/i23422.scala +++ b/tests/pos-custom-args/captures/i23422.scala @@ -1,7 +1,7 @@ import language.experimental.captureChecking import caps.* trait Cap -class Inv[T] extends Capability +class Inv[T] extends SharedCapability class Inv2[T] class Inv3[T] extends Mutable def test(c: Cap^): Unit = diff --git a/tests/pos-custom-args/captures/infer-exists.scala b/tests/pos-custom-args/captures/infer-exists.scala index 6d5225f75128..3f959e273bbc 100644 --- a/tests/pos-custom-args/captures/infer-exists.scala +++ b/tests/pos-custom-args/captures/infer-exists.scala @@ -1,6 +1,6 @@ import language.experimental.captureChecking -class C extends caps.Capability +class C extends caps.SharedCapability class D def test1 = diff --git a/tests/pos-custom-args/captures/lazyref.scala b/tests/pos-custom-args/captures/lazyref.scala index f4c85de9a51a..6b5d62c743b6 100644 --- a/tests/pos-custom-args/captures/lazyref.scala +++ b/tests/pos-custom-args/captures/lazyref.scala @@ -1,7 +1,7 @@ import caps.consume -class Cap extends caps.Capability +class Cap extends caps.SharedCapability class LazyRef[T](val elem: () => T): val get: () ->{elem} T = elem @@ -25,3 +25,4 @@ def test(@consume cap1: Cap, @consume cap2: Cap) = val ref3c: LazyRef[Int]^{cap2, ref1} = ref3 val ref4 = (if cap1 == cap2 then ref1 else ref2).map(g) val ref4c: LazyRef[Int]^{cap1, cap2} = ref4 + diff --git a/tests/pos-custom-args/captures/lists.scala b/tests/pos-custom-args/captures/lists.scala index 7ca26e74f484..fa8a5b813758 100644 --- a/tests/pos-custom-args/captures/lists.scala +++ b/tests/pos-custom-args/captures/lists.scala @@ -18,7 +18,7 @@ object NIL extends LIST[Nothing]: def map[A, B](f: A => B)(xs: LIST[A]): LIST[B] = xs.map(f) -class Cap extends caps.Capability +class Cap extends caps.SharedCapability def test(c: Cap, d: Cap, e: Cap) = diff --git a/tests/pos-custom-args/captures/logger-tracked.scala b/tests/pos-custom-args/captures/logger-tracked.scala index 053731de444d..adb989702e3f 100644 --- a/tests/pos-custom-args/captures/logger-tracked.scala +++ b/tests/pos-custom-args/captures/logger-tracked.scala @@ -1,7 +1,7 @@ import language.experimental.saferExceptions import language.experimental.modularity -class FileSystem extends caps.Capability +class FileSystem extends caps.SharedCapability class Logger(using tracked val fs: FileSystem): def log(s: String): Unit = ??? diff --git a/tests/pos-custom-args/captures/logger.scala b/tests/pos-custom-args/captures/logger.scala index c2cfed0462b6..3eec73ce25f0 100644 --- a/tests/pos-custom-args/captures/logger.scala +++ b/tests/pos-custom-args/captures/logger.scala @@ -1,6 +1,6 @@ import language.experimental.saferExceptions -class FileSystem extends caps.Capability +class FileSystem extends caps.SharedCapability class Logger(using fs: FileSystem): def log(s: String): Unit = ??? diff --git a/tests/pos-custom-args/captures/nested-classes-tracked.scala b/tests/pos-custom-args/captures/nested-classes-tracked.scala index 1c81441f321b..7bf0e8701fee 100644 --- a/tests/pos-custom-args/captures/nested-classes-tracked.scala +++ b/tests/pos-custom-args/captures/nested-classes-tracked.scala @@ -2,7 +2,7 @@ import language.experimental.captureChecking import language.experimental.modularity import annotation.{capability, constructorOnly} -class IO extends caps.Capability +class IO extends caps.SharedCapability class Blah class Pkg(using tracked val io: IO): class Foo: diff --git a/tests/pos-custom-args/captures/nested-classes.scala b/tests/pos-custom-args/captures/nested-classes.scala index 1c624d37cee1..e9227889f10e 100644 --- a/tests/pos-custom-args/captures/nested-classes.scala +++ b/tests/pos-custom-args/captures/nested-classes.scala @@ -1,7 +1,7 @@ import language.experimental.captureChecking import annotation.{capability, constructorOnly} -class IO extends caps.Capability +class IO extends caps.SharedCapability class Blah class Pkg(using io: IO): class Foo: diff --git a/tests/pos-custom-args/captures/null-logger.scala b/tests/pos-custom-args/captures/null-logger.scala index d532b5f74b38..3c1e98923f3e 100644 --- a/tests/pos-custom-args/captures/null-logger.scala +++ b/tests/pos-custom-args/captures/null-logger.scala @@ -1,6 +1,6 @@ import annotation.constructorOnly -class FileSystem extends caps.Capability +class FileSystem extends caps.SharedCapability class NullLogger(using @constructorOnly fs: FileSystem) diff --git a/tests/pos-custom-args/captures/opaque-cap.scala b/tests/pos-custom-args/captures/opaque-cap.scala index dc3d48a2d311..93e850c9c9d7 100644 --- a/tests/pos-custom-args/captures/opaque-cap.scala +++ b/tests/pos-custom-args/captures/opaque-cap.scala @@ -1,6 +1,6 @@ import language.experimental.captureChecking -trait A extends caps.Capability +trait A extends caps.SharedCapability object O: opaque type B = A \ No newline at end of file diff --git a/tests/pos-custom-args/captures/opaque-inline-problem.scala b/tests/pos-custom-args/captures/opaque-inline-problem.scala index ed482e3fc164..2911d6fca51f 100644 --- a/tests/pos-custom-args/captures/opaque-inline-problem.scala +++ b/tests/pos-custom-args/captures/opaque-inline-problem.scala @@ -1,4 +1,4 @@ -trait Async extends caps.Capability: +trait Async extends caps.SharedCapability: def group: Int object Async: diff --git a/tests/pos-custom-args/captures/open-existential.scala b/tests/pos-custom-args/captures/open-existential.scala index 8b43f27a051c..1be107f04228 100644 --- a/tests/pos-custom-args/captures/open-existential.scala +++ b/tests/pos-custom-args/captures/open-existential.scala @@ -1,4 +1,4 @@ -trait Async extends caps.Capability +trait Async extends caps.SharedCapability class Future[+T](x: () => T)(using val a: Async) diff --git a/tests/pos-custom-args/captures/pairs.scala b/tests/pos-custom-args/captures/pairs.scala index da7f30185ad3..b5abaf273703 100644 --- a/tests/pos-custom-args/captures/pairs.scala +++ b/tests/pos-custom-args/captures/pairs.scala @@ -1,6 +1,6 @@ //class CC //type Cap = CC^ -class Cap extends caps.Capability +class Cap extends caps.SharedCapability object Generic: diff --git a/tests/pos-custom-args/captures/reach-capability.scala b/tests/pos-custom-args/captures/reach-capability.scala index 77bd91957fa0..7160b280ce4f 100644 --- a/tests/pos-custom-args/captures/reach-capability.scala +++ b/tests/pos-custom-args/captures/reach-capability.scala @@ -1,6 +1,6 @@ import language.experimental.captureChecking import annotation.experimental -import caps.Sharable +import caps.SharedCapability import caps.use @experimental object Test2: @@ -8,7 +8,7 @@ import caps.use class List[+A]: def map[B](f: A => B): List[B] = ??? - class Label extends Sharable + class Label extends SharedCapability class Listener diff --git a/tests/pos-custom-args/captures/reach-in-results-shared.scala b/tests/pos-custom-args/captures/reach-in-results-shared.scala new file mode 100644 index 000000000000..cd625810af37 --- /dev/null +++ b/tests/pos-custom-args/captures/reach-in-results-shared.scala @@ -0,0 +1,28 @@ +import language.experimental.captureChecking +import caps.{cap, Shared, SharedCapability} + +class IO extends SharedCapability +class C + +def test(io: IO^): Unit = + val f = (x: () ->{cap.only[Shared]} IO^) => x() + val g = (x: () ->{cap.only[Shared]} IO^{cap.only[Shared]}) => x() + val h = (x: () ->{cap.only[Shared]} C^{cap.only[Shared]}) => x() +/* + val _: (x: () ->{cap.only[Shared]} IO^) => IO^{x} = (x: () ->{cap.only[Shared]} IO^) => f(x) + val _: (x: () ->{cap.only[Shared]} IO^) => IO^{x} = f//(x: () => IO^) => f(x) + def g(x: IO^ => IO^) = x(io) + def h(x: (y: IO^) => IO^) = x(io) + + val a: () -> IO^ = ??? + val _: () -> IO^{a*} = a + val b: (x: IO^) -> IO^ = ??? + val _: (x: IO^) -> IO^ = b + val c: IO^ -> IO^ = ??? + val cc: IO^ -> IO^{c*} = c + +def testByName(io: IO^): Unit = + def f(x: => () => IO^) = x() + def g(x: => IO^ => IO^) = x(io) + def h(x: => (y: IO^) => IO^) = x(io) +*/ \ No newline at end of file diff --git a/tests/pos-custom-args/captures/reach-in-results.scala b/tests/pos-custom-args/captures/reach-in-results.scala index a00f7a4499da..7a2e77c214f9 100644 --- a/tests/pos-custom-args/captures/reach-in-results.scala +++ b/tests/pos-custom-args/captures/reach-in-results.scala @@ -1,9 +1,16 @@ import language.experimental.captureChecking +import caps.{cap, Shared} -class IO extends caps.Capability +class IO def test(io: IO^): Unit = + val f = (x: () ->{cap.only[Shared]} IO^{cap.only[Shared]}) => x() + + val _: (x: () ->{cap.only[Shared]} IO^{cap.only[Shared]}) => IO^{x} = (x: () ->{cap.only[Shared]} IO^{cap.only[Shared]}) => f(x) + val _: (x: () ->{cap.only[Shared]} IO^{cap.only[Shared]}) => IO^{x} = f//(x: () => IO^) => f(x) +/* val f = (x: () => IO^) => x() + val _: (x: () => IO^) => IO^{x} = (x: () => IO^) => f(x) val _: (x: () => IO^) => IO^{x} = f//(x: () => IO^) => f(x) def g(x: IO^ => IO^) = x(io) def h(x: (y: IO^) => IO^) = x(io) @@ -19,3 +26,4 @@ def testByName(io: IO^): Unit = def f(x: => () => IO^) = x() def g(x: => IO^ => IO^) = x(io) def h(x: => (y: IO^) => IO^) = x(io) +*/ \ No newline at end of file diff --git a/tests/pos-custom-args/captures/reaches.scala b/tests/pos-custom-args/captures/reaches.scala index 131dce862b02..97d110d438bc 100644 --- a/tests/pos-custom-args/captures/reaches.scala +++ b/tests/pos-custom-args/captures/reaches.scala @@ -51,7 +51,7 @@ def compose2[A, B, C](@consume f: A => B, @consume g: B => C): A => C = //def mapCompose[A](ps: List[(A => A, A => A)]): List[A ->{ps*} A] = // ps.map((x, y) => compose1(x, y)) // Does not work, see neg-customargs/../reaches2.scala -class IO extends caps.Capability +class IO extends caps.SharedCapability def test(io: IO) = val a: () ->{io} Unit = () => () diff --git a/tests/pos-custom-args/captures/restrict-subsumes.scala b/tests/pos-custom-args/captures/restrict-subsumes.scala index b22c11371fe2..8061f907e69a 100644 --- a/tests/pos-custom-args/captures/restrict-subsumes.scala +++ b/tests/pos-custom-args/captures/restrict-subsumes.scala @@ -1,6 +1,6 @@ -import caps.{cap, Classifier, Capability} +import caps.{cap, Classifier, SharedCapability} -trait Read extends Capability, Classifier +trait Read extends SharedCapability, Classifier trait A extends Read diff --git a/tests/pos-custom-args/captures/restrict-try.scala b/tests/pos-custom-args/captures/restrict-try.scala index ac23abc71eb9..fc2a09ecb535 100644 --- a/tests/pos-custom-args/captures/restrict-try.scala +++ b/tests/pos-custom-args/captures/restrict-try.scala @@ -1,4 +1,4 @@ -import caps.{Capability, Control, Mutable} +import caps.{SharedCapability, Control, Mutable} class Try[+T] case class Ok[T](x: T) extends Try[T] diff --git a/tests/pos-custom-args/captures/rinaudo.scala b/tests/pos-custom-args/captures/rinaudo.scala index 7091f8e94d6d..4b0e1f555309 100644 --- a/tests/pos-custom-args/captures/rinaudo.scala +++ b/tests/pos-custom-args/captures/rinaudo.scala @@ -1,7 +1,7 @@ import language.experimental.captureChecking import caps.* -trait FileSystem extends Capability: +trait FileSystem extends SharedCapability: def print(msg: String): Unit class Logger(using fs: FileSystem): diff --git a/tests/pos-custom-args/captures/sep-exclusive.scala b/tests/pos-custom-args/captures/sep-exclusive.scala new file mode 100644 index 000000000000..c4d922955572 --- /dev/null +++ b/tests/pos-custom-args/captures/sep-exclusive.scala @@ -0,0 +1,7 @@ +class E extends caps.ExclusiveCapability +class S extends caps.SharedCapability + +def par(x: S^, y: S^): S = ??? + +def test(x: S^) = par(x, x) + diff --git a/tests/pos-custom-args/captures/shared-capability.scala b/tests/pos-custom-args/captures/shared-capability.scala new file mode 100644 index 000000000000..78214dc15348 --- /dev/null +++ b/tests/pos-custom-args/captures/shared-capability.scala @@ -0,0 +1,11 @@ + + +import caps.SharedCapability + +class Async extends SharedCapability + +def test1(a: Async): Object^ = a // OK + +def test2(a: Async^): Object^ = a // also OK since Async^ means Async^{cap.only[SharedCaoability]} + + diff --git a/tests/pos-custom-args/captures/try3.scala b/tests/pos-custom-args/captures/try3.scala index a1a1bab8724a..4924dc61e875 100644 --- a/tests/pos-custom-args/captures/try3.scala +++ b/tests/pos-custom-args/captures/try3.scala @@ -1,7 +1,7 @@ import language.experimental.erasedDefinitions import java.io.IOException -class CanThrow[-E] extends caps.Capability +class CanThrow[-E] extends caps.SharedCapability def handle[E <: Exception, T](op: CanThrow[E] ?=> T)(handler: E => T): T = val x: CanThrow[E] = ??? diff --git a/tests/pos-custom-args/captures/vars.scala b/tests/pos-custom-args/captures/vars.scala index 5c9598fab508..37044f7e7529 100644 --- a/tests/pos-custom-args/captures/vars.scala +++ b/tests/pos-custom-args/captures/vars.scala @@ -1,4 +1,4 @@ -class Cap extends caps.Capability +class Cap extends caps.SharedCapability def test(cap1: Cap, cap2: Cap) = def f(x: String): String = if cap1 == cap1 then "" else "a" diff --git a/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala b/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala index f95c25635d9f..1f27c0224a68 100644 --- a/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala +++ b/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala @@ -38,8 +38,10 @@ val experimentalDefinitionInLibrary = Set( "scala.caps.Contains$", "scala.caps.Contains$.containsImpl", "scala.caps.Exists", + "scala.caps.SharedCapability", + "scala.caps.ExclusiveCapability", "scala.caps.Mutable", - "scala.caps.Sharable", + "scala.caps.Read", "scala.caps.Control", "scala.caps.consume", "scala.caps.internal", @@ -49,6 +51,8 @@ val experimentalDefinitionInLibrary = Set( "scala.caps.unsafe", "scala.caps.unsafe$", "scala.caps.use", + "scala.caps.package$package$.Exclusive", + "scala.caps.package$package$.Shared", //// New feature: into "scala.Conversion$.into",