diff --git a/compiler/src/dotty/tools/dotc/ast/tpd.scala b/compiler/src/dotty/tools/dotc/ast/tpd.scala index eddc0c675e9a..909387bbb809 100644 --- a/compiler/src/dotty/tools/dotc/ast/tpd.scala +++ b/compiler/src/dotty/tools/dotc/ast/tpd.scala @@ -517,7 +517,7 @@ object tpd extends Trees.Instance[Type] with TypedTreeInfo { def singleton(tp: Type, needLoad: Boolean = true)(using Context): Tree = tp.dealias match { case tp: TermRef => ref(tp, needLoad) case tp: ThisType => This(tp.cls) - case tp: SkolemType => singleton(tp.narrow, needLoad) + case tp: SkolemType => singleton(tp.narrow(), needLoad) case SuperType(qual, _) => singleton(qual, needLoad) case ConstantType(value) => Literal(value) } diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index d665e8d4bd3c..19f2da7bff1c 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -23,6 +23,7 @@ import printing.Texts.Text import reporting.{Message, trace} import NameOps.isImpureFunction import annotation.internal.sharable +import collection.immutable /** Capabilities are members of capture sets. They partially overlap with types * as shown in the trait hierarchy below. @@ -147,10 +148,30 @@ object Capabilities: * @param origin an indication where and why the FreshCap was created, used * for diagnostics */ - case class FreshCap (owner: Symbol, origin: Origin)(using @constructorOnly ctx: Context) extends RootCapability: - val hiddenSet = CaptureSet.HiddenSet(owner, this: @unchecked) + case class FreshCap(val prefix: Type) + (val owner: Symbol, val origin: Origin, origHidden: CaptureSet.HiddenSet | Null) + (using @constructorOnly ctx: Context) + extends RootCapability: + val hiddenSet = + if origHidden == null then CaptureSet.HiddenSet(owner, this: @unchecked) + else origHidden // fails initialization check without the @unchecked + def derivedFreshCap(newPrefix: Type)(using Context): FreshCap = + if newPrefix eq prefix then this + else if newPrefix eq hiddenSet.owningCap.prefix then + hiddenSet.owningCap + else + hiddenSet.derivedCaps + .getOrElseUpdate(newPrefix, FreshCap(newPrefix)(owner, origin, hiddenSet)) + + /** A map from context owners to skolem TermRefs that were created by ensurePath + * TypeMap's mapCapability. + */ + var skolems: immutable.Map[Symbol, TermRef] = immutable.HashMap.empty + + //assert(rootId != 10, i"fresh $prefix, ${ctx.owner}") + /** 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 @@ -167,12 +188,6 @@ object Capabilities: case _ => false /** Is this fresh cap at the right level to be able to subsume `ref`? - * Only outer freshes can be subsumed. - * TODO Can we merge this with levelOK? Right now we use two different schemes: - * - For level checking capsets with levelOK: Check that the visibility of the element - * os not properly contained in the captset owner. - * - For level checking elements subsumed by FreshCaps: Check that the widened scope - * (using levelOwner) of the elements contains the owner of the FreshCap. */ def acceptsLevelOf(ref: Capability)(using Context): Boolean = if ccConfig.useFreshLevels && !CCState.collapseFresh then @@ -190,6 +205,11 @@ object Capabilities: hiddenSet.adoptClassifier(cls) if freeze then isClassified = true + def ccOwnerStr(using Context): String = + val owner = ccOwner + if owner.name == nme.SKOLEM then i"a new instance of ${hiddenSet.owner}" + else owner.show + def descr(using Context) = val originStr = origin match case Origin.InDecl(sym) if sym.exists => @@ -203,8 +223,12 @@ object Capabilities: i"a fresh root capability$classifierStr$originStr" object FreshCap: + def apply(owner: Symbol, prefix: Type, origin: Origin)(using Context): FreshCap = + new FreshCap(prefix)(owner, origin, null) + def apply(owner: Symbol, origin: Origin)(using Context): FreshCap = + apply(owner, owner.skipWeakOwner.thisType, origin) def apply(origin: Origin)(using Context): FreshCap = - FreshCap(ctx.owner, origin) + apply(ctx.owner, origin) /** A root capability associated with a function type. These are conceptually * existentially quantified over the function's result type. @@ -441,6 +465,7 @@ object Capabilities: * the form this.C but their pathroot is still this.C, not this. */ final def pathRoot(using Context): Capability = this match + case FreshCap(pre: Capability) => pre.pathRoot case _: RootCapability => this case self: DerivedCapability => self.underlying.pathRoot case self: CoreCapability => self.dealias match @@ -485,7 +510,13 @@ object Capabilities: case TermRef(prefix: Capability, _) => prefix.ccOwner case self: NamedType => self.symbol case self: DerivedCapability => self.underlying.ccOwner - case self: FreshCap => self.hiddenSet.owner + case self: FreshCap => + val setOwner = self.hiddenSet.owner + self.prefix match + case prefix: ThisType if setOwner.isTerm && setOwner.owner == prefix.cls => + setOwner + case prefix: Capability => prefix.ccOwner + case _ => setOwner case _ /* : GlobalCap | ResultCap | ParamRef */ => NoSymbol final def visibility(using Context): Symbol = this match @@ -665,6 +696,8 @@ object Capabilities: try (this eq y) || maxSubsumes(y, canAddHidden = !vs.isOpen) + // if vs is open, we should add new elements to the set containing `this` + // instead of adding them to the hidden set of of `this`. || y.match case y: TermRef => y.prefix.match @@ -732,12 +765,26 @@ object Capabilities: (this eq y) || this.match case x: FreshCap => + def classifierOK = + if y.tryClassifyAs(x.hiddenSet.classifier) then true + else + capt.println(i"$y cannot be classified as $x") + false + + def prefixAllowsAddHidden: Boolean = + CCState.collapseFresh || x.prefix.match + case NoPrefix => true + case pre: ThisType => x.ccOwner.isContainedIn(pre.cls) + case pre => + capt.println(i"fresh not open $x, ${x.rootId}, $pre, ${x.ccOwner.skipWeakOwner.thisType}") + false + vs.ifNotSeen(this)(x.hiddenSet.elems.exists(_.subsumes(y))) + || x.coversFresh(y) || x.acceptsLevelOf(y) - && ( y.tryClassifyAs(x.hiddenSet.classifier) - || { capt.println(i"$y cannot be classified as $x"); false } - ) + && classifierOK && canAddHidden + && prefixAllowsAddHidden && vs.addHidden(x.hiddenSet, y) case x: ResultCap => val result = y match @@ -800,15 +847,39 @@ object Capabilities: case _ => false || x.match - case x: FreshCap if !seen.contains(x) => - seen.add(x) - x.hiddenSet.exists(recur(_, y)) + case x: FreshCap => + if x.coversFresh(y) then true + else if !seen.contains(x) then + seen.add(x) + x.hiddenSet.exists(recur(_, y)) + else false case Restricted(x1, _) => recur(x1, y) case _ => false recur(this, y) end covers + /** `x eq y` or `x` is a fresh cap, `y` is a fresh cap with prefix + * `p`, and there is a prefix of `p` that contains `x` in its + * capture set. + */ + final def coversFresh(y: Capability)(using Context): Boolean = + (this eq y) || this.match + case x: FreshCap => y match + case y: FreshCap => + x.origin match + case Origin.InDecl(sym) => + def occursInPrefix(pre: Type): Boolean = pre match + case pre @ TermRef(pre1, _) => + pre.symbol == sym + && pre.info.captureSet.elems.contains(x) + || occursInPrefix(pre1) + case _ => false + occursInPrefix(y.prefix) + case _ => false + case _ => false + case _ => false + def assumedContainsOf(x: TypeRef)(using Context): SimpleIdentitySet[Capability] = CaptureSet.assumedContains.getOrElse(x, SimpleIdentitySet.empty) @@ -857,18 +928,26 @@ object Capabilities: else if cls2.isSubClass(cls1) then cls2 else defn.NothingClass - def joinClassifiers(cs1: Classifiers, cs2: Classifiers)(using Context): Classifiers = + /** The smallest list D of class symbols in cs1 and cs2 such that + * every class symbol in cs1 and cs2 is a subclass of a class symbol in D + */ + def dominators(cs1: List[ClassSymbol], cs2: List[ClassSymbol])(using Context): List[ClassSymbol] = // Drop classes that subclass classes of the other set // @param proper If true, only drop proper subclasses of a class of the other set def filterSub(cs1: List[ClassSymbol], cs2: List[ClassSymbol], proper: Boolean) = cs1.filter: cls1 => !cs2.exists: cls2 => cls1.isSubClass(cls2) && (!proper || cls1 != cls2) + filterSub(cs1, cs2, proper = true) ++ filterSub(cs2, cs1, proper = false) + + def joinClassifiers(cs1: Classifiers, cs2: Classifiers)(using Context): Classifiers = (cs1, cs2) match - case (Unclassified, _) | (_, Unclassified) => Unclassified - case (UnknownClassifier, _) | (_, UnknownClassifier) => UnknownClassifier + case (Unclassified, _) | (_, Unclassified) => + Unclassified + case (UnknownClassifier, _) | (_, UnknownClassifier) => + UnknownClassifier case (ClassifiedAs(cs1), ClassifiedAs(cs2)) => - ClassifiedAs(filterSub(cs1, cs2, proper = true) ++ filterSub(cs2, cs1, proper = false)) + ClassifiedAs(dominators(cs1, cs2)) /** The place of - and cause for - creating a fresh capability. Used for * error diagnostics @@ -881,7 +960,7 @@ object Capabilities: case ResultInstance(methType: Type, meth: Symbol) case UnapplyInstance(info: MethodType) case LocalInstance(restpe: Type) - case NewMutable(tp: Type) + case NewInstance(tp: Type) case NewCapability(tp: Type) case LambdaExpected(respt: Type) case LambdaActual(restp: Type) @@ -911,10 +990,11 @@ object Capabilities: i" when instantiating argument of unapply with type $info" case LocalInstance(restpe) => i" when instantiating expected result type $restpe of function literal" - case NewMutable(tp) => - i" when constructing mutable $tp" + case NewInstance(tp) => + i" when constructing instance $tp" case NewCapability(tp) => - i" when constructing Capability instance $tp" + val kind = if tp.derivesFromMutable then "mutable" else "Capability instance" + i" when constructing $kind $tp" case LambdaExpected(respt) => i" when instantiating expected result type $respt of lambda" case LambdaActual(restp: Type) => @@ -1172,14 +1252,11 @@ object Capabilities: def toResultInResults(sym: Symbol, fail: Message => Unit, keepAliases: Boolean = false)(tp: Type)(using Context): Type = val m = new TypeMap with FollowAliasesMap: def apply(t: Type): Type = t match - case AnnotatedType(parent @ defn.RefinedFunctionOf(mt), ann) if ann.symbol == defn.InferredDepFunAnnot => - val mt1 = mapOver(mt).asInstanceOf[MethodType] - if mt1 ne mt then mt1.toFunctionType(alwaysDependent = true) - else parent - case defn.RefinedFunctionOf(mt) => - val mt1 = apply(mt) - if mt1 ne mt then mt1.toFunctionType(alwaysDependent = true) - else t + case rt @ defn.RefinedFunctionOf(mt) => + rt.derivedRefinedType(refinedInfo = + if rt.isInstanceOf[InferredRefinedType] + then mapOver(mt) + else apply(mt)) case t: MethodType if variance > 0 && t.marksExistentialScope => val t1 = mapOver(t).asInstanceOf[MethodType] t1.derivedLambdaType(resType = toResult(t1.resType, t1, fail)) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index bb667c3af14a..2ae80192f3e1 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -467,8 +467,7 @@ extension (tp: Type) acc(false, tp) def refinedOverride(name: Name, rinfo: Type)(using Context): Type = - RefinedType(tp, name, - AnnotatedType(rinfo, Annotation(defn.RefineOverrideAnnot, util.Spans.NoSpan))) + RefinedType.precise(tp, name, rinfo) def dropUseAndConsumeAnnots(using Context): Type = tp.dropAnnot(defn.UseAnnot).dropAnnot(defn.ConsumeAnnot) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index 86c502b489f8..313db27c3e28 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -12,7 +12,7 @@ import annotation.internal.sharable import reporting.trace import printing.{Showable, Printer} import printing.Texts.* -import util.{SimpleIdentitySet, Property} +import util.{SimpleIdentitySet, Property, EqHashMap} import typer.ErrorReporting.Addenda import scala.collection.{mutable, immutable} import TypeComparer.ErrorNote @@ -560,8 +560,10 @@ object CaptureSet: def universal(using Context): Const = Const(SimpleIdentitySet(GlobalCap)) + def fresh(owner: Symbol, prefix: Type, origin: Origin)(using Context): Const = + FreshCap(owner, prefix, origin).singletonCaptureSet def fresh(origin: Origin)(using Context): Const = - FreshCap(origin).singletonCaptureSet + fresh(ctx.owner, ctx.owner.thisType, origin) /** The shared capture set `{cap.rd}` */ def shared(using Context): Const = @@ -964,8 +966,7 @@ object CaptureSet: case elem: FreshCap if !nestedOK && !elems.contains(elem) - && !owner.isAnonymousFunction - && ccConfig.newScheme => + && !owner.isAnonymousFunction => def fail = i"attempting to add $elem to $this" def hideIn(fc: FreshCap): Unit = assert(elem.tryClassifyAs(fc.hiddenSet.classifier), fail) @@ -990,7 +991,7 @@ object CaptureSet: case _ => isSubsumed if !isSubsumed then if elem.origin != Origin.InDecl(owner) || elem.hiddenSet.isConst then - val fc = new FreshCap(owner, Origin.InDecl(owner)) + val fc = FreshCap(owner, Origin.InDecl(owner)) assert(fc.tryClassifyAs(elem.hiddenSet.classifier), fail) hideIn(fc) super.includeElem(fc) @@ -1225,12 +1226,16 @@ object CaptureSet: override def owner = givenOwner + /** The FreshCaps generated by derivedFreshCap, indexed by prefix */ + val derivedCaps = new EqHashMap[Type, FreshCap]() + //assert(id != 3) description = i"of elements subsumed by a fresh cap in $initialOwner" /** Add element to hidden set. */ def add(elem: Capability)(using ctx: Context, vs: VarState): Unit = + assert(elem ne owningCap) includeElem(elem) /** Apply function `f` to `elems` while setting `elems` to empty for the @@ -1387,7 +1392,7 @@ object CaptureSet: def addHidden(hidden: HiddenSet, elem: Capability)(using Context): Boolean = if hidden.isConst then false else - hidden.add(elem)(using ctx, this) + if !CCState.collapseFresh then hidden.add(elem)(using ctx, this) true /** If root1 and root2 belong to the same binder but have different originalBinders diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index d5cc2811f264..194d0444d890 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -17,6 +17,7 @@ import typer.Checking.{checkBounds, checkAppliedTypesIn} import typer.ErrorReporting.{Addenda, NothingToAdd, err} import typer.ProtoTypes.{LhsProto, WildcardSelectionProto, SelectionProto} import util.{SimpleIdentitySet, EqHashMap, EqHashSet, SrcPos, Property} +import util.chaining.tap import transform.{Recheck, PreRecheck, CapturedVars} import Recheck.* import scala.collection.mutable @@ -101,7 +102,7 @@ object CheckCaptures: end SubstParamsMap /** A prototype that indicates selection with an immutable value */ - class PathSelectionProto(val sym: Symbol, val pt: Type)(using Context) extends WildcardSelectionProto + class PathSelectionProto(val select: Select, val pt: Type)(using Context) extends WildcardSelectionProto /** Check that a @retains annotation only mentions references that can be tracked. * This check is performed at Typer. @@ -193,6 +194,11 @@ object CheckCaptures: check.traverse(tp) end disallowBadRootsIn + private def contributesFreshToClass(sym: Symbol)(using Context): Boolean = + sym.isField + && !sym.isOneOf(DeferredOrTermParamOrAccessor) + && !sym.hasAnnotation(defn.UntrackedCapturesAnnot) + private def ownerStr(owner: Symbol)(using Context): String = if owner.isAnonymousFunction then "enclosing function" else owner.show @@ -247,6 +253,11 @@ class CheckCaptures extends Recheck, SymTransformer: val ccState1 = new CCState // Dotty problem: Rename to ccState ==> Crash in ExplicitOuter + /** A cache that stores for each class the classifiers of all fresh instances + * in the types of its fields. + */ + val knownFresh = new util.EqHashMap[Symbol, List[ClassSymbol]] + class CaptureChecker(ictx: Context) extends Rechecker(ictx), CheckerAPI: // println(i"checking ${ictx.source}"(using ictx)) @@ -620,9 +631,7 @@ class CheckCaptures extends Recheck, SymTransformer: fn.tpe.widenDealias match case tl: TypeLambda => tl.paramNames case ref: AppliedType if ref.typeSymbol.isClass => ref.typeSymbol.typeParams.map(_.name) - case t => - println(i"parent type: $t") - args.map(_ => EmptyTypeName) + case t => args.map(_ => EmptyTypeName) for case (arg: TypeTree, pname) <- args.lazyZip(paramNames) do def where = if sym.exists then i" in an argument of $sym" else "" @@ -648,33 +657,35 @@ class CheckCaptures extends Recheck, SymTransformer: if sym.is(Method) then // If ident refers to a parameterless method, charge its cv to the environment includeCallCaptures(sym, sym.info, tree) - else if !sym.isStatic then - markFree(sym, pathRef(sym.termRef, pt), tree) + else if sym.exists && !sym.isStatic then + markPathFree(sym.termRef, pt, tree) mapResultRoots(super.recheckIdent(tree, pt), tree.symbol) override def recheckThis(tree: This, pt: Type)(using Context): Type = - markFree(pathRef(tree.tpe.asInstanceOf[ThisType], pt), tree) + markPathFree(tree.tpe.asInstanceOf[ThisType], pt, tree) super.recheckThis(tree, pt) /** Add all selections and also any `.rd modifier implied by the expected - * type `pt` to `base`. Example: + * type `pt` to `ref`. Expand the marked tree accordingly to take account of + * the added path. Example: * If we have `x` and the expected type says we select that with `.a.b` - * where `b` is a read-only method, we charge `x.a.b.rd` instead of `x`. + * where `b` is a read-only method, we charge `x.a.b.rd` for tree `x.a.b` + * instead of just charging `x`. */ - private def pathRef(base: TermRef | ThisType, pt: Type)(using Context): Capability = - def addSelects(ref: TermRef | ThisType, pt: Type): Capability = pt match + private def markPathFree(ref: TermRef | ThisType, pt: Type, tree: Tree)(using Context): Unit = + pt match case pt: PathSelectionProto if ref.isTracked => - if pt.sym.isReadOnlyMethod then - ref.readOnly + // if `ref` is not tracked then the selection could not give anything new + // class SerializationProxy in stdlib-cc/../LazyListIterable.scala has an example where this matters. + if pt.select.symbol.isReadOnlyMethod then + markFree(ref.readOnly, tree) else - // if `ref` is not tracked then the selection could not give anything new - // class SerializationProxy in stdlib-cc/../LazyListIterable.scala has an example where this matters. - addSelects(ref.select(pt.sym).asInstanceOf[TermRef], pt.pt) - case _ => ref - val ref: Capability = addSelects(base, pt) - if ref.derivesFromMutable && pt.isValueType && !pt.isMutableType - then ref.readOnly - else ref + markPathFree(ref.select(pt.select.symbol).asInstanceOf[TermRef], pt.pt, pt.select) + case _ => + if ref.derivesFromMutable && pt.isValueType && !pt.isMutableType then + markFree(ref.readOnly, tree) + else + markFree(ref, tree) /** The expected type for the qualifier of a selection. If the selection * could be part of a capability path or is a a read-only method, we return @@ -684,7 +695,7 @@ class CheckCaptures extends Recheck, SymTransformer: val sym = tree.symbol if !sym.isOneOf(UnstableValueFlags) && !sym.isStatic || sym.isReadOnlyMethod - then PathSelectionProto(sym, pt) + then PathSelectionProto(tree, pt) else super.selectionProto(tree, pt) /** A specialized implementation of the selection rule. @@ -721,19 +732,26 @@ class CheckCaptures extends Recheck, SymTransformer: |since its capture set ${qualType.captureSet} is read-only""", tree.srcPos) - val selType = mapResultRoots(recheckSelection(tree, qualType, name, disambiguate), tree.symbol) + val origSelType = recheckSelection(tree, qualType, name, disambiguate) + val selType = mapResultRoots(origSelType, tree.symbol) val selWiden = selType.widen + def capturesResult = origSelType.widenSingleton match + case ExprType(resType) => resType.captureSet.containsResultCapability + case _ => false + // Don't apply the rule // - on the LHS of assignments, or // - if the qualifier or selection type is boxed, or - // - the selection is either a trackable capture reference or a pure type + // - the selection is either a trackable capture reference or a pure type, or + // - if the selection is of a parameterless method capturing a result cap if noWiden(selType, pt) || qualType.isBoxedCapturing || selType.isBoxedCapturing || selWiden.isBoxedCapturing || selType.isTrackableRef || selWiden.captureSet.isAlwaysEmpty + || capturesResult then selType else @@ -808,9 +826,8 @@ class CheckCaptures extends Recheck, SymTransformer: */ protected override def recheckApplication(tree: Apply, qualType: Type, funType: MethodType, argTypes: List[Type])(using Context): Type = - val appType = resultToFresh( - super.recheckApplication(tree, qualType, funType, argTypes), - Origin.ResultInstance(funType, tree.symbol)) + val resultType = super.recheckApplication(tree, qualType, funType, argTypes) + val appType = resultToFresh(resultType, Origin.ResultInstance(funType, tree.symbol)) val qualCaptures = qualType.captureSet val argCaptures = for (argType, formal) <- argTypes.lazyZip(funType.paramInfos) yield @@ -819,6 +836,7 @@ class CheckCaptures extends Recheck, SymTransformer: case appType @ CapturingType(appType1, refs) if qualType.exists && !tree.fun.symbol.isConstructor + && !resultType.captureSet.containsResultCapability && qualCaptures.mightSubcapture(refs) && argCaptures.forall(_.mightSubcapture(refs)) => val callCaptures = argCaptures.foldLeft(qualCaptures)(_ ++ _) @@ -863,17 +881,14 @@ class CheckCaptures extends Recheck, SymTransformer: * * Second half: union of initial capture set and all capture sets of arguments * to tracked parameters. The initial capture set `initCs` is augmented with - * - FreshCap(...) if `core` extends Mutable - * - FreshCap(...).rd if `core` extends Capability + * a fresh cap if `core` extends Capability. */ def addParamArgRefinements(core: Type, initCs: CaptureSet): (Type, CaptureSet) = var refined: Type = core var allCaptures: CaptureSet = - if core.derivesFromMutable then - initCs ++ FreshCap(Origin.NewMutable(core)).singletonCaptureSet - else if core.derivesFromCapability then - initCs ++ FreshCap(Origin.NewCapability(core)).readOnly.singletonCaptureSet - else initCs + if core.derivesFromCapability + then initCs ++ FreshCap(Origin.NewCapability(core)).singletonCaptureSet + else initCs ++ impliedByFields(core) for (getterName, argType) <- mt.paramNames.lazyZip(argTypes) do val getter = cls.info.member(getterName).suchThat(_.isRefiningParamAccessor).symbol if !getter.is(Private) && getter.hasTrackedParts then @@ -897,6 +912,53 @@ class CheckCaptures extends Recheck, SymTransformer: val (refined, cs) = addParamArgRefinements(core, initCs) refined.capturing(cs) + /** The additional capture set implied by the capture sets of its fields. This + * is either empty or, if some fields have a terminal capability in their span + * capture sets, it consists of a single fresh cap that subsumes all these terminal + * capabiltities. Class parameters are not counted. + */ + def impliedByFields(core: Type): CaptureSet = + var infos: List[String] = Nil + def pushInfo(msg: => String) = + if ctx.settings.YccVerbose.value then infos = msg :: infos + + /** The classifiers of the fresh caps in the span capture sets of all fields + * in the given class `cls`. + */ + def impliedClassifiers(cls: Symbol): List[ClassSymbol] = cls match + case cls: ClassSymbol => + val fieldClassifiers = + for + sym <- cls.info.decls.toList + if contributesFreshToClass(sym) + case fresh: FreshCap <- sym.info.spanCaptureSet.elems + .filter(_.isTerminalCapability) + .map(_.stripReadOnly) + .toList + _ = pushInfo(i"Note: ${sym.showLocated} captures a $fresh") + yield fresh.hiddenSet.classifier + val parentClassifiers = + cls.parentSyms.map(impliedClassifiers).filter(_.nonEmpty) + if fieldClassifiers.isEmpty && parentClassifiers.isEmpty + then Nil + else parentClassifiers.foldLeft(fieldClassifiers.distinct)(dominators) + case _ => Nil + + def fresh = + FreshCap(Origin.NewInstance(core)).tap: fresh => + if ctx.settings.YccVerbose.value then + pushInfo(i"Note: instance of $cls captures a $fresh that comes from a field") + report.echo(infos.mkString("\n"), ctx.owner.srcPos) + + knownFresh.getOrElseUpdate(cls, impliedClassifiers(cls)) match + case Nil => CaptureSet.empty + case cl :: Nil => + val result = fresh + result.hiddenSet.adoptClassifier(cl) + result.singletonCaptureSet + case _ => fresh.singletonCaptureSet + end impliedByFields + augmentConstructorType(resType, capturedVars(cls)) .showing(i"constr type $mt with $argTypes%, % in $constr = $result", capt) end refineConstructorInstance @@ -1109,15 +1171,15 @@ class CheckCaptures extends Recheck, SymTransformer: def checkInferredResult(tp: Type, tree: ValOrDefDef)(using Context): Type = val sym = tree.symbol - def canUseInferred = // If canUseInferred is false, all capturing types in the type of `sym` need to be given explicitly - sym.isLocalToCompilationUnit // Symbols that can't be seen outside the compilation unit can always have inferred types - || ctx.owner.enclosingPackageClass.isEmptyPackage - // We make an exception for symbols in the empty package. - // these could theoretically be accessed from other files in the empty package, but - // usually it would be too annoying to require explicit types. - || sym.name.is(DefaultGetterName) // Default getters are exempted since otherwise it would be - // too annoying. This is a hole since a defualt getter's result type - // might leak into a type variable. + def isExemptFromChecks = + ctx.owner.enclosingPackageClass.isEmptyPackage + // We make an exception for symbols in the empty package. + // these could theoretically be accessed from other files in the empty package, but + // usually it would be too annoying to require explicit types. + || sym.name.is(DefaultGetterName) + // Default getters are exempted since otherwise it would be + // too annoying. This is a hole since a defualt getter's result type + // might leak into a type variable. def fail(tree: Tree, expected: Type, addenda: Addenda): Unit = def maybeResult = if sym.is(Method) then " result" else "" @@ -1140,14 +1202,30 @@ class CheckCaptures extends Recheck, SymTransformer: |must conform to this type.""" tree.tpt match - case tpt: InferredTypeTree if !canUseInferred => - val expected = tpt.tpe.dropAllRetains - todoAtPostCheck += { () => - withCapAsRoot: - testAdapted(tp, expected, tree.rhs, addenda(expected))(fail) - // The check that inferred <: expected is done after recheck so that it - // does not interfere with normal rechecking by constraining capture set variables. - } + case tpt: InferredTypeTree if !isExemptFromChecks => + if !sym.isLocalToCompilationUnit + // Symbols that can't be seen outside the compilation unit can have inferred types + // except for the else clause below. + then + val expected = tpt.tpe.dropAllRetains + todoAtPostCheck += { () => + withCapAsRoot: + testAdapted(tp, expected, tree.rhs, addenda(expected))(fail) + // The check that inferred <: expected is done after recheck so that it + // does not interfere with normal rechecking by constraining capture set variables. + } + else if sym.is(Private) + && !sym.isLocalToCompilationUnitIgnoringPrivate + && tree.tpt.nuType.spanCaptureSet.containsTerminalCapability + && contributesFreshToClass(sym) + // Private symbols capturing a root capability need explicit types + // so that we can compute field constributions to class instance + // capture sets across compilation units. + then + report.error( + em"""$sym needs an explicit type because it captures a root capability in its type ${tree.tpt.nuType}. + |Fields of publicily accessible classes that capture a root capability need to be given an explicit type.""", + tpt.srcPos) case _ => tp end checkInferredResult @@ -1771,7 +1849,7 @@ class CheckCaptures extends Recheck, SymTransformer: private def noWiden(actual: Type, expected: Type)(using Context): Boolean = actual.isSingleton && expected.match - case expected: PathSelectionProto => !expected.sym.isOneOf(UnstableValueFlags) + case expected: PathSelectionProto => !expected.select.symbol.isOneOf(UnstableValueFlags) case _ => expected.stripCapturing.isSingleton || expected == LhsProto /** Adapt `actual` type to `expected` type. This involves: @@ -1939,6 +2017,7 @@ class CheckCaptures extends Recheck, SymTransformer: private val setup: SetupAPI = thisPhase.prev.asInstanceOf[Setup] override def checkUnit(unit: CompilationUnit)(using Context): Unit = + capt.println(i"cc check ${unit.source}") ccState.start() setup.setupUnit(unit.tpdTree, this) collectCapturedMutVars.traverse(unit.tpdTree) diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index 65aa2fdce124..42d31dccd887 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -221,7 +221,7 @@ object SepCheck: refs1.foreach: ref => if !ref.isReadOnly then val coreRef = ref.stripRestricted - if refs2.exists(_.stripRestricted.stripReadOnly eq coreRef) then + if refs2.exists(_.stripRestricted.stripReadOnly.coversFresh(coreRef)) then acc += coreRef acc assert(refs.forall(_.isTerminalCapability)) @@ -272,7 +272,6 @@ object SepCheck: * 3. the set itself if it consists only of hidden terminal capabilities. */ def reduced(using Context): Refs = - assert(!refs.isEmpty) val concrete = refs.nonPeaks if !concrete.isEmpty then concrete else @@ -356,9 +355,11 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: val hiddenFootprint = hiddenSet.directFootprint val clashFootprint = clashSet.directFootprint val shared = hiddenFootprint.overlapWith(clashFootprint).reduced - shared.nth(0) match + if shared.isEmpty then i"${CaptureSet(shared)}" + else shared.nth(0) match case fresh: FreshCap => - if fresh.hiddenSet.owner.exists then i"$fresh of ${fresh.hiddenSet.owner}" else i"$fresh" + val where = if ctx.settings.YccVerbose.value then "" else i" of ${fresh.ccOwnerStr}" + i"{$fresh$where}" case _ => i"${CaptureSet(shared)}" @@ -402,8 +403,9 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: else i" with type ${clashing.nuType}" val hiddenSet = formalCaptures(polyArg).transHiddenSet val clashSet = if clashIdx == -1 then deepCaptures(clashing) else spanCaptures(clashing) - val hiddenFootprint = hiddenSet.directFootprint - val clashFootprint = clashSet.directFootprint + val hiddenFootprint = hiddenSet.completeFootprint + val clashFootprint = clashSet.completeFootprint + report.error( em"""Separation failure: argument of type ${polyArg.nuType} |to $funStr @@ -430,6 +432,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: def sepUseError(tree: Tree, clashingDef: ValOrDefDef | Null, used: Refs, hidden: Refs)(using Context): Unit = if clashingDef != null then def resultStr = if clashingDef.isInstanceOf[DefDef] then " result" else "" + //println(i"sep use error: previous ${clashingDef.tpt.nuType}, ref = $used") report.error( em"""Separation failure: Illegal access to ${overlapStr(hidden, used)} which is hidden by the previous definition |of ${clashingDef.symbol} with$resultStr type ${clashingDef.tpt.nuType}. @@ -567,11 +570,17 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: val usedPeaks = used.allPeaks val overlap = defsShadow.allPeaks.sharedPeaks(usedPeaks) if !defsShadow.allPeaks.sharedPeaks(usedPeaks).isEmpty then - val sym = tree.symbol + // Drop all Selects unless they select from a `this` + def pathRoot(tree: Tree): Tree = tree match + case Select(This(_), _) => tree + case Select(prefix, _) => pathRoot(prefix) + case _ => tree + + val rootSym = pathRoot(tree).symbol def findClashing(prevDefs: List[DefInfo]): Option[DefInfo] = prevDefs match case prevDef :: prevDefs1 => - if prevDef.symbol == sym then Some(prevDef) + if prevDef.symbol == rootSym then Some(prevDef) else if !prevDef.hiddenPeaks.sharedPeaks(usedPeaks).isEmpty then Some(prevDef) else findClashing(prevDefs1) case Nil => @@ -579,10 +588,12 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: findClashing(previousDefs) match case Some(clashing) => - if clashing.symbol != sym then + //println(i"check use $tree, $used, $rootSym, ${clashing.symbol}") + if clashing.symbol != rootSym then sepUseError(tree, clashing.tree, used, clashing.hidden) case None => sepUseError(tree, null, used, defsShadow) + end if for ref <- used do val pos = consumed.clashing(ref) diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala index d1b0f0c5cc72..efcfea69e49c 100644 --- a/compiler/src/dotty/tools/dotc/cc/Setup.scala +++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala @@ -193,11 +193,12 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: case AppliedType(`tycon`, args0) => args0.last ne args.last case _ => false if expand then - val fn = depFun( + val (fn: RefinedType) = depFun( args.init, args.last, isContextual = defn.isContextFunctionClass(tycon.classSymbol)) .showing(i"add function refinement $tp ($tycon, ${args.init}, ${args.last}) --> $result", capt) - AnnotatedType(fn, Annotation(defn.InferredDepFunAnnot, util.Spans.NoSpan)) + .runtimeChecked + RefinedType.inferred(fn.parent, fn.refinedName, fn.refinedInfo) else tp case _ => tp @@ -273,7 +274,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: then val getterType = mapInferred(inCaptureRefinement = true)(tp.memberInfo(getter)).strippedDealias - RefinedType(core, getter.name, + RefinedType.precise(core, getter.name, CapturingType(getterType, CaptureSet.ProperVar(ctx.owner, isRefining = true))) .showing(i"add capture refinement $tp --> $result", capt) @@ -690,7 +691,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: if cls.derivesFrom(defn.Caps_Capability) then // If cls is a capability class, we need to add a fresh readonly capability to // ensure we cannot treat the class as pure. - CaptureSet.fresh(Origin.InDecl(cls)).readOnly.subCaptures(cs) + CaptureSet.fresh(cls, cls.thisType, Origin.InDecl(cls)).readOnly.subCaptures(cs) CapturingType(cinfo.selfType, cs) // Compute new parent types diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala index dbe1602e2d82..d8d00cc298ce 100644 --- a/compiler/src/dotty/tools/dotc/core/Definitions.scala +++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala @@ -1086,7 +1086,6 @@ class Definitions { @tu lazy val UseAnnot: ClassSymbol = requiredClass("scala.caps.use") @tu lazy val ReserveAnnot: ClassSymbol = requiredClass("scala.caps.reserve") @tu lazy val ConsumeAnnot: ClassSymbol = requiredClass("scala.caps.internal.consume") - @tu lazy val RefineOverrideAnnot: ClassSymbol = requiredClass("scala.caps.internal.refineOverride") @tu lazy val VolatileAnnot: ClassSymbol = requiredClass("scala.volatile") @tu lazy val LanguageFeatureMetaAnnot: ClassSymbol = requiredClass("scala.annotation.meta.languageFeature") @tu lazy val BeanGetterMetaAnnot: ClassSymbol = requiredClass("scala.annotation.meta.beanGetter") @@ -1130,7 +1129,7 @@ class Definitions { // Set of annotations that are not printed in types except under -Yprint-debug @tu lazy val SilentAnnots: Set[Symbol] = - Set(InlineParamAnnot, ErasedParamAnnot, RefineOverrideAnnot, SilentIntoAnnot, UseAnnot, ConsumeAnnot) + Set(InlineParamAnnot, ErasedParamAnnot, SilentIntoAnnot, UseAnnot, ConsumeAnnot) // A list of annotations that are commonly used to indicate that a field/method argument or return // type is not null. These annotations are used by the nullification logic in JavaNullInterop to diff --git a/compiler/src/dotty/tools/dotc/core/NamerOps.scala b/compiler/src/dotty/tools/dotc/core/NamerOps.scala index 53e2112ead95..0417ae554bef 100644 --- a/compiler/src/dotty/tools/dotc/core/NamerOps.scala +++ b/compiler/src/dotty/tools/dotc/core/NamerOps.scala @@ -52,7 +52,7 @@ object NamerOps: */ def addParamRefinements(resType: Type, paramss: List[List[Symbol]])(using Context): Type = paramss.flatten.foldLeft(resType): (rt, param) => - if param.is(Tracked) then RefinedType(rt, param.name, param.termRef) + if param.is(Tracked) then RefinedType.precise(rt, param.name, param.termRef) else rt /** Split dependent class refinements off parent type. Add them to `refinements`, diff --git a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala index 6dcf2a83ba5c..53a96931c83e 100644 --- a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala +++ b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala @@ -1248,11 +1248,13 @@ object SymDenotations { || isClass && (!isOneOf(EffectivelyOpenFlags) || isLocalToCompilationUnit) - final def isLocalToCompilationUnit(using Context): Boolean = - is(Private) - || owner.ownersIterator.takeWhile(!_.isStaticOwner).exists(_.isTerm) + final def isLocalToCompilationUnitIgnoringPrivate(using Context): Boolean = + owner.ownersIterator.takeWhile(!_.isStaticOwner).exists(_.isTerm) || accessBoundary(defn.RootClass).isProperlyContainedIn(symbol.topLevelClass) + final def isLocalToCompilationUnit(using Context): Boolean = + is(Private) || isLocalToCompilationUnitIgnoringPrivate + final def isTransparentClass(using Context): Boolean = is(TransparentType) || defn.isAssumedTransparent(symbol) diff --git a/compiler/src/dotty/tools/dotc/core/SymUtils.scala b/compiler/src/dotty/tools/dotc/core/SymUtils.scala index c7733acbfdec..435320fec568 100644 --- a/compiler/src/dotty/tools/dotc/core/SymUtils.scala +++ b/compiler/src/dotty/tools/dotc/core/SymUtils.scala @@ -313,7 +313,7 @@ class SymUtils: } def isField(using Context): Boolean = - self.isTerm && !self.is(Method) + self.isTerm && !self.isOneOf(Method | PhantomSymbol | NonMember) def isEnumCase(using Context): Boolean = self.isAllOf(EnumCase, butNot = JavaDefined) diff --git a/compiler/src/dotty/tools/dotc/core/Symbols.scala b/compiler/src/dotty/tools/dotc/core/Symbols.scala index d86c50cbe2e3..f3496a8636dd 100644 --- a/compiler/src/dotty/tools/dotc/core/Symbols.scala +++ b/compiler/src/dotty/tools/dotc/core/Symbols.scala @@ -900,8 +900,8 @@ object Symbols extends SymUtils { /** Create a new skolem symbol. This is not the same as SkolemType, even though the * motivation (create a singleton referencing to a type) is similar. */ - def newSkolem(tp: Type)(using Context): TermSymbol = - newSymbol(defn.RootClass, nme.SKOLEM, SyntheticArtifact | NonMember | Permanent, tp) + def newSkolem(owner: Symbol, tp: Type)(using Context): TermSymbol = + newSymbol(owner, nme.SKOLEM, SyntheticArtifact | NonMember | Permanent, tp) def newErrorSymbol(owner: Symbol, name: Name, msg: Message)(using Context): Symbol = { val errType = ErrorType(msg) diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala index 97a172966701..0b02900f8178 100644 --- a/compiler/src/dotty/tools/dotc/core/Types.scala +++ b/compiler/src/dotty/tools/dotc/core/Types.scala @@ -914,15 +914,14 @@ object Types extends TypeUtils { pdenot.asSingleDenotation.derivedSingleDenotation(pdenot.symbol, jointInfo) } else - val overridingRefinement = rinfo match - case AnnotatedType(rinfo1, ann) if ann.symbol == defn.RefineOverrideAnnot => rinfo1 - case _ if pdenot.symbol.is(Tracked) => rinfo - case _ => NoType - if overridingRefinement.exists then - pdenot.asSingleDenotation.derivedSingleDenotation(pdenot.symbol, overridingRefinement) + if tp.isPrecise then + pdenot.asSingleDenotation.derivedSingleDenotation(pdenot.symbol, rinfo) else val isRefinedMethod = rinfo.isInstanceOf[MethodOrPoly] val joint = CCState.withCollapsedFresh: + // We have to do a collapseFresh here since `pdenot` will see the class + // view and a fresh in the class will not be able to subsume a + // refinement from outside since level checking would fail. pdenot.meet( new JointRefDenotation(NoSymbol, rinfo, Period.allInRun(ctx.runId), pre, isRefinedMethod), pre, @@ -1706,11 +1705,10 @@ object Types extends TypeUtils { if hasNext then current = f(current.asInstanceOf[TypeProxy]) res - /** A prefix-less refined this or a termRef to a new skolem symbol - * that has the given type as info. + /** A prefix-less TermRef to a new skolem symbol that has this type as info. */ - def narrow(using Context): TermRef = - TermRef(NoPrefix, newSkolem(this)) + def narrow(using Context)(owner: Symbol = defn.RootClass): TermRef = + TermRef(NoPrefix, newSkolem(owner, this)) /** Useful for diagnostics: The underlying type if this type is a type proxy, * otherwise NoType @@ -2319,14 +2317,14 @@ object Types extends TypeUtils { override def dropIfProto = WildcardType } - /** Implementations of this trait cache the results of `narrow`. */ - trait NarrowCached extends Type { + /** Implementations of this trait cache the results of `narrow` if the owner is RootClass. */ + trait NarrowCached extends Type: private var myNarrow: TermRef | Null = null - override def narrow(using Context): TermRef = { - if (myNarrow == null) myNarrow = super.narrow - myNarrow.nn - } - } + override def narrow(using Context)(owner: Symbol): TermRef = + if owner == defn.RootClass then + if myNarrow == null then myNarrow = super.narrow(owner) + myNarrow.nn + else super.narrow(owner) // --- NamedTypes ------------------------------------------------------------------ @@ -3257,6 +3255,12 @@ object Types extends TypeUtils { else assert(refinedInfo.isInstanceOf[TypeType], this) assert(!refinedName.is(NameKinds.ExpandedName), this) + /** If true we know that refinedInfo is always more precise than the info for + * field `refinedName` in parent, so no type intersection needs to be computed + * for the type of this field. + */ + def isPrecise: Boolean = false + override def underlying(using Context): Type = parent private def badInst = @@ -3264,11 +3268,14 @@ object Types extends TypeUtils { def checkInst(using Context): this.type = this // debug hook + def newLikeThis(parent: Type, refinedName: Name, refinedInfo: Type)(using Context): Type = + RefinedType(parent, refinedName, refinedInfo) + final def derivedRefinedType (parent: Type = this.parent, refinedName: Name = this.refinedName, refinedInfo: Type = this.refinedInfo) (using Context): Type = if ((parent eq this.parent) && (refinedName eq this.refinedName) && (refinedInfo eq this.refinedInfo)) this - else RefinedType(parent, refinedName, refinedInfo) + else newLikeThis(parent, refinedName, refinedInfo) /** Add this refinement to `parent`, provided `refinedName` is a member of `parent`. */ def wrapIfMember(parent: Type)(using Context): Type = @@ -3300,6 +3307,21 @@ object Types extends TypeUtils { class CachedRefinedType(parent: Type, refinedName: Name, refinedInfo: Type) extends RefinedType(parent, refinedName, refinedInfo) + class PreciseRefinedType(parent: Type, refinedName: Name, refinedInfo: Type) + extends RefinedType(parent, refinedName, refinedInfo): + override def isPrecise = true + override def newLikeThis(parent: Type, refinedName: Name, refinedInfo: Type)(using Context): Type = + PreciseRefinedType(parent, refinedName, refinedInfo) + + /** Used for refined function types created at cc/Setup that come from original + * generic function types. Function types of this class don't get their result + * captures mapped from FreshCaps to ResultCaps with toResult. + */ + class InferredRefinedType(parent: Type, refinedName: Name, refinedInfo: Type) + extends RefinedType(parent, refinedName, refinedInfo): + override def newLikeThis(parent: Type, refinedName: Name, refinedInfo: Type)(using Context): Type = + InferredRefinedType(parent, refinedName, refinedInfo) + object RefinedType { @tailrec def make(parent: Type, names: List[Name], infos: List[Type])(using Context): Type = if (names.isEmpty) parent @@ -3309,6 +3331,14 @@ object Types extends TypeUtils { assert(!ctx.erasedTypes) unique(new CachedRefinedType(parent, name, info)).checkInst } + + def precise(parent: Type, name: Name, info: Type)(using Context): RefinedType = + assert(!ctx.erasedTypes) + unique(new PreciseRefinedType(parent, name, info)).checkInst + + def inferred(parent: Type, name: Name, info: Type)(using Context): RefinedType = + assert(!ctx.erasedTypes) + unique(new InferredRefinedType(parent, name, info)).checkInst } /** A recursive type. Instances should be constructed via the companion object. @@ -6330,6 +6360,23 @@ object Types extends TypeUtils { null def mapCapability(c: Capability, deep: Boolean = false): Capability | (CaptureSet, Boolean) = c match + case c @ FreshCap(prefix) => + // If `pre` is not a path, transform it to a path starting with a skolem TermRef. + // We create at most one such skolem per FreshCap/context owner pair. + // This approximates towards creating fewer skolems than otherwise needed, + // which means we might get more separation conflicts than otherwise. But + // it's not clear we will get such conflicts anyway. + def ensurePath(pre: Type)(using Context): Type = pre match + case pre @ TermRef(pre1, _) => pre.withPrefix(ensurePath(pre1)) + case NoPrefix | _: SingletonType => pre + case pre => + c.skolems.get(ctx.owner) match + case Some(skolem) => skolem + case None => + val skolem = pre.narrow(ctx.owner) + c.skolems = c.skolems.updated(ctx.owner, skolem) + skolem + c.derivedFreshCap(ensurePath(apply(prefix))) case c: RootCapability => c case Reach(c1) => mapCapability(c1, deep = true) diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala index 3a0611e74ec1..f6584a22f5bc 100644 --- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala +++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala @@ -491,8 +491,16 @@ class PlainPrinter(_ctx: Context) extends Printer { def classified = if c.hiddenSet.classifier == defn.AnyClass then "" else s" classified as ${c.hiddenSet.classifier.name.show}" - if ccVerbose then s"" - else "cap" + def prefixTxt: Text = c.prefix match + case NoPrefix => "" + case _: ThisType if !ccVerbose => "" + case pre: TermRef if !ccVerbose && pre.name == nme.SKOLEM => "" + case pre: SingletonType => toTextRef(pre) ~ "." + case pre => toText(pre) ~ "." + def core: Text = + if ccVerbose then s"" + else "cap" + prefixTxt ~ core case tp: TypeProxy => homogenize(tp) match case tp: SingletonType => toTextRef(tp) diff --git a/compiler/src/dotty/tools/dotc/reporting/Message.scala b/compiler/src/dotty/tools/dotc/reporting/Message.scala index 9fd89ca91066..32c9bf91f919 100644 --- a/compiler/src/dotty/tools/dotc/reporting/Message.scala +++ b/compiler/src/dotty/tools/dotc/reporting/Message.scala @@ -142,7 +142,7 @@ object Message: end record /** Create explanation for single `Recorded` type or symbol */ - private def explanation(entry: AnyRef, key: String)(using Context): String = + private def explanation(entry: AnyRef, keys: List[String])(using Context): String = def boundStr(bound: Type, default: ClassSymbol, cmp: String) = if (bound.isRef(default)) "" else i"$cmp $bound" @@ -178,7 +178,8 @@ object Message: s"is an unknown value of type ${tp.widen.show}" case ref: RootCapability => val relation = - if List("^", "=>", "?=>").exists(key.startsWith) then "refers to" + if keys.length > 1 then "refer to" + else if List("^", "=>", "?=>").exists(keys(0).startsWith) then "refers to" else "is" s"$relation ${ref.descr}" end explanation @@ -207,16 +208,20 @@ object Message: res // help the inferencer out }.sortBy(_._1) - def columnar(parts: List[(String, String)]): List[String] = { + def columnar(parts: List[(String, String)]): List[String] = lazy val maxLen = parts.map(_._1.length).max - parts.map { - case (leader, trailer) => - val variable = hl(leader) - s"""$variable${" " * (maxLen - leader.length)} $trailer""" - } - } - - val explainParts = toExplain.map { case (str, entry) => (str, explanation(entry, str)) } + parts.map: (leader, trailer) => + val variable = hl(leader) + s"""$variable${" " * (maxLen - leader.length)} $trailer""" + + // Group keys with the same Recorded entry together. We can't use groupBy here + // since we want to maintain the order in which entries first appear in the + // original list. + val toExplainGrouped: List[(Recorded, List[String])] = + for entry <- toExplain.map(_._2).distinct + yield (entry, for (key, e) <- toExplain if e == entry yield key) + val explainParts = toExplainGrouped.map: + (entry, keys) => (keys.mkString(" and "), explanation(entry, keys)) val explainLines = columnar(explainParts) if (explainLines.isEmpty) "" else i"where: $explainLines%\n %\n" end explanations diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala index 7857f8c86189..5ff098e0dc35 100644 --- a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala +++ b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala @@ -395,7 +395,7 @@ object SpaceEngine { case _ => // Pattern is an arbitrary expression; assume a skolem (i.e. an unknown value) of the pattern type - Typ(pat.tpe.narrow, decomposed = false) + Typ(pat.tpe.narrow(), decomposed = false) }) private def project(tp: Type)(using Context): Space = tp match { diff --git a/compiler/src/dotty/tools/dotc/typer/Applications.scala b/compiler/src/dotty/tools/dotc/typer/Applications.scala index 5ecf1601db8a..b2b36e438597 100644 --- a/compiler/src/dotty/tools/dotc/typer/Applications.scala +++ b/compiler/src/dotty/tools/dotc/typer/Applications.scala @@ -337,7 +337,7 @@ object Applications { case pre: SingletonType => singleton(pre, needLoad = !testOnly) case pre if testOnly => // In this case it is safe to skolemize now; we will produce a stable prefix for the actual call. - ref(pre.narrow) + ref(pre.narrow()) case _ => EmptyTree if fn.symbol.hasDefaultParams then @@ -1845,7 +1845,7 @@ trait Applications extends Compatibility { case methRef: TermRef if methRef.widenSingleton.isInstanceOf[MethodicType] => p(methRef) case mt: MethodicType => - p(mt.narrow) + p(mt.narrow()) case _ => followApply && tp.member(nme.apply).hasAltWith(d => p(TermRef(tp, nme.apply, d))) } diff --git a/library/src/scala/caps/package.scala b/library/src/scala/caps/package.scala index 2cd75efdf197..b668a8d0e53d 100644 --- a/library/src/scala/caps/package.scala +++ b/library/src/scala/caps/package.scala @@ -145,6 +145,7 @@ object internal: * info from the parent type, so no intersection needs to be formed. * This could be useful for tracked parameters as well. */ + @deprecated final class refineOverride extends annotation.StaticAnnotation /** An annotation used internally for root capability wrappers of `cap` that @@ -173,10 +174,23 @@ end internal @experimental object unsafe: - /** - * Marks the constructor parameter as untracked. - * The capture set of this parameter will not be included in - * the capture set of the constructed object. + /** Two usages: + * + * 1. Marks the constructor parameter as untracked. + * The capture set of this parameter will not be included in + * the capture set of the constructed object. + * + * 2. Marks a class field that has a cap in its capture set, so that + * the cap is not contributed to the class instance. + * Exampple: + * + * class A { val b B^ = ... }; new A() + * + * has type A^ since b contributes a cap. But + * + * class A { @untrackedCaptures val b: B^ = ... }; new A() + * + * has type A. The `b` field does not contribute its cap. * * @note This should go into annotations. For now it is here, so that we * can experiment with it quickly between minor releases diff --git a/library/src/scala/collection/Iterator.scala b/library/src/scala/collection/Iterator.scala index 4ddef7dcb18f..bb90b859944f 100644 --- a/library/src/scala/collection/Iterator.scala +++ b/library/src/scala/collection/Iterator.scala @@ -18,6 +18,7 @@ import scala.collection.mutable.{ArrayBuffer, ArrayBuilder, Builder, ImmutableBu import scala.annotation.tailrec import scala.annotation.unchecked.uncheckedVariance import scala.runtime.Statics +import caps.unsafe.untrackedCaptures /** Iterators are data structures that allow to iterate over a sequence * of elements. They have a `hasNext` method for checking @@ -917,7 +918,12 @@ trait Iterator[+A] extends IterableOnce[A] with IterableOnceOps[A, Iterator, Ite */ def patch[B >: A](from: Int, patchElems: Iterator[B]^, replaced: Int): Iterator[B]^{this, patchElems} = new AbstractIterator[B] { - private[this] var origElems: Iterator[B]^ = self + // TODO We should be able to prove that origElems is safe even though it is + // declared as Iterator[B]^. We could show that origElems is never assigned a + // freh cap. Maybe we can invent another annotation that is checked and that + // shows that the `^` is just used as an upper bound for concete non-fresh + // capabilities. + @untrackedCaptures private[this] var origElems: Iterator[B]^ = self // > 0 => that many more elems from `origElems` before switching to `patchElems` // 0 => need to drop elems from `origElems` and start using `patchElems` // -1 => have dropped elems from `origElems`, will be using `patchElems` until it's empty diff --git a/library/src/scala/collection/generic/IsIterable.scala b/library/src/scala/collection/generic/IsIterable.scala index 0b80203037fc..4ba72ff3fe08 100644 --- a/library/src/scala/collection/generic/IsIterable.scala +++ b/library/src/scala/collection/generic/IsIterable.scala @@ -15,6 +15,7 @@ package generic import scala.language.`2.13` import language.experimental.captureChecking +import caps.unsafe.untrackedCaptures /** A trait which can be used to avoid code duplication when defining extension * methods that should be applicable both to existing Scala collections (i.e., @@ -123,6 +124,7 @@ transparent trait IsIterable[Repr] extends IsIterableOnce[Repr] { type C @deprecated("'conversion' is now a method named 'apply'", "2.13.0") + @untrackedCaptures override val conversion: Repr => IterableOps[A, Iterable, C] = apply(_) /** A conversion from the type `Repr` to `IterableOps[A, Iterable, C]` */ diff --git a/library/src/scala/collection/generic/IsIterableOnce.scala b/library/src/scala/collection/generic/IsIterableOnce.scala index bced6e190206..6bdad3287ede 100644 --- a/library/src/scala/collection/generic/IsIterableOnce.scala +++ b/library/src/scala/collection/generic/IsIterableOnce.scala @@ -16,6 +16,7 @@ package generic import scala.language.`2.13` import language.experimental.captureChecking +import caps.unsafe.untrackedCaptures /** Type class witnessing that a collection representation type `Repr` has * elements of type `A` and has a conversion to `IterableOnce[A]`. @@ -46,6 +47,7 @@ transparent trait IsIterableOnce[Repr] { type A @deprecated("'conversion' is now a method named 'apply'", "2.13.0") + @untrackedCaptures val conversion: Repr => IterableOnce[A] = apply(_) /** A conversion from the representation type `Repr` to a `IterableOnce[A]`. */ diff --git a/library/src/scala/collection/generic/IsSeq.scala b/library/src/scala/collection/generic/IsSeq.scala index 04a94c5e5da0..3e5b644a7ea1 100644 --- a/library/src/scala/collection/generic/IsSeq.scala +++ b/library/src/scala/collection/generic/IsSeq.scala @@ -15,6 +15,7 @@ package generic import scala.language.`2.13` import language.experimental.captureChecking +import caps.unsafe.untrackedCaptures import scala.reflect.ClassTag @@ -31,6 +32,7 @@ import scala.reflect.ClassTag transparent trait IsSeq[Repr] extends IsIterable[Repr] { @deprecated("'conversion' is now a method named 'apply'", "2.13.0") + @untrackedCaptures override val conversion: Repr => SeqOps[A, Iterable, C] = apply(_) /** A conversion from the type `Repr` to `SeqOps[A, Iterable, C]` diff --git a/library/src/scala/collection/immutable/LazyListIterable.scala b/library/src/scala/collection/immutable/LazyListIterable.scala index f1d14bbb1fad..4f6f30e9cc14 100644 --- a/library/src/scala/collection/immutable/LazyListIterable.scala +++ b/library/src/scala/collection/immutable/LazyListIterable.scala @@ -25,6 +25,7 @@ import scala.collection.generic.SerializeEnd import scala.collection.mutable.{Builder, ReusableBuilder, StringBuilder} import scala.language.implicitConversions import scala.runtime.Statics +import caps.unsafe.untrackedCaptures /** This class implements an immutable linked list. We call it "lazy" * because it computes its elements only when they are needed. @@ -310,7 +311,7 @@ final class LazyListIterable[+A] private (lazyState: LazyListIterable.EmptyMarke throw new RuntimeException( "LazyListIterable evaluation depends on its own result (self-reference); see docs for more info") - val fun = _tail.asInstanceOf[() ->{this} LazyListIterable[A]^] + val fun = _tail.asInstanceOf[() ->{this} LazyListIterable[A]^{this}] _tail = MidEvaluation val l = // `fun` returns a LazyListIterable that represents the state (head/tail) of `this`. We call `l.evaluated` to ensure @@ -1374,7 +1375,7 @@ object LazyListIterable extends IterableFactory[LazyListIterable] { private final class WithFilter[A] private[LazyListIterable](lazyList: LazyListIterable[A]^, p: A => Boolean) extends collection.WithFilter[A, LazyListIterable] { - private[this] val filtered = lazyList.filter(p) + @untrackedCaptures private[this] val filtered = lazyList.filter(p) def map[B](f: A => B): LazyListIterable[B]^{this, f} = filtered.map(f) def flatMap[B](f: A => IterableOnce[B]^): LazyListIterable[B]^{this, f} = filtered.flatMap(f) def foreach[U](f: A => U): Unit = filtered.foreach(f) diff --git a/tests/neg-custom-args/captures/apply-fresh.check b/tests/neg-custom-args/captures/apply-fresh.check new file mode 100644 index 000000000000..82924140bd9f --- /dev/null +++ b/tests/neg-custom-args/captures/apply-fresh.check @@ -0,0 +1,31 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/apply-fresh.scala:17:15 ---------------------------------- +17 | val _: Ref = x // error + | ^ + | Found: (x : Ref^) + | Required: Ref + | + | Note that capability cap is not included in capture set {}. + | + | where: ^ and cap refer to a fresh root capability in the type of value x + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/apply-fresh.scala:21:15 ---------------------------------- +21 | val _: Ref = y // error + | ^ + | Found: (y : Ref^) + | Required: Ref + | + | Note that capability cap is not included in capture set {}. + | + | where: ^ and cap refer to a fresh root capability in the type of value y + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/apply-fresh.scala:25:15 ---------------------------------- +25 | val _: Ref = z // error + | ^ + | Found: (z : Ref^{bar.newRef}) + | Required: Ref + | + | Note that capability bar.newRef is not included in capture set {}. + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/apply-fresh.scala b/tests/neg-custom-args/captures/apply-fresh.scala new file mode 100644 index 000000000000..7056af3cda38 --- /dev/null +++ b/tests/neg-custom-args/captures/apply-fresh.scala @@ -0,0 +1,25 @@ +object Test + +class Ref + +class Foo: + def newRef: Ref^ = Ref() + +class Bar: + val newRef: Ref^ = Ref() + +def newRef: Ref^ = Ref() + +def test = + + val f = () => newRef + val x = f() + val _: Ref = x // error + + val foo = Foo() + val y = foo.newRef + val _: Ref = y // error + + val bar = Bar() + val z = bar.newRef + val _: Ref = z // error diff --git a/tests/neg-custom-args/captures/boundary.check b/tests/neg-custom-args/captures/boundary.check index 0cac2ec2f60d..1d624c9d18bf 100644 --- a/tests/neg-custom-args/captures/boundary.check +++ b/tests/neg-custom-args/captures/boundary.check @@ -2,15 +2,14 @@ 4 | boundary[AnyRef^]: 5 | l1 ?=> // error // error | ^ - |Found: scala.util.boundary.Label[Object^'s1]^{cap.rd} - |Required: scala.util.boundary.Label[Object^]^² + |Found: scala.util.boundary.Label[Object^'s1]^ + |Required: scala.util.boundary.Label[Object^²]^³ | - |Note that capability cap² cannot be included in outer capture set 's1. + |Note that capability cap cannot be included in outer capture set 's1. | - |where: ^ refers to the universal root capability - | ^² refers to a fresh root capability classified as Control in the type of value local - | cap is a fresh root capability classified as Control created in value local when constructing Capability instance scala.util.boundary.Label[Object^'s1] - | cap² is the universal root capability + |where: ^ refers to a fresh root capability classified as Control created in value local when constructing Capability instance scala.util.boundary.Label[Object^'s1] + | ^² and cap refer to the universal root capability + | ^³ refers to a fresh root capability classified as Control in the type of value local 6 | boundary[Unit]: l2 ?=> 7 | boundary.break(l2)(using l1) // error 8 | ??? @@ -31,11 +30,10 @@ | |Note that capability cap is not included in capture set {cap²}. | - |where: ^ refers to the universal root capability - | ^² refers to a fresh root capability classified as Control in the type of value local² - | ^³ refers to a fresh root capability classified as Control created in package when checking argument to parameter label of method break - | cap is a fresh root capability classified as Control in the type of value local - | cap² is a fresh root capability classified as Control created in package when checking argument to parameter label of method break + |where: ^ refers to the universal root capability + | ^² refers to a fresh root capability classified as Control in the type of value local² + | ^³ and cap² refer to a fresh root capability classified as Control created in package when checking argument to parameter label of method break + | cap is a fresh root capability classified as Control in the type of value local | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/boundary.scala:5:4 --------------------------------------- @@ -47,10 +45,8 @@ | | Note that capability cap is not included in capture set {cap²}. | - | where: ^ refers to the universal root capability - | ^² refers to a fresh root capability created in package - | cap is a fresh root capability created in package - | cap² is the universal root capability + | where: ^ and cap² refer to the universal root capability + | ^² and cap refer to a fresh root capability created in package 6 | boundary[Unit]: l2 ?=> 7 | boundary.break(l2)(using l1) // error 8 | ??? diff --git a/tests/neg-custom-args/captures/box-adapt-contra.check b/tests/neg-custom-args/captures/box-adapt-contra.check index a598656743fc..eeb710c27ae3 100644 --- a/tests/neg-custom-args/captures/box-adapt-contra.check +++ b/tests/neg-custom-args/captures/box-adapt-contra.check @@ -9,8 +9,7 @@ | Cap^{c} => Unit cannot be box-converted to Cap^{c} ->{cap, c} Unit | since the additional capture set {c} resulting from box conversion is not allowed in Cap^{c} => Unit | - | where: => refers to the universal root capability - | cap is the universal root capability + | where: => and cap refer to the universal root capability -- Error: tests/neg-custom-args/captures/box-adapt-contra.scala:19:54 -------------------------------------------------- 19 | val f3: (Cap^{c} -> Unit) => Unit = useCap3[Cap^{c}](c) // error | ^^^^^^^^^^^^^^^^^^^ diff --git a/tests/neg-custom-args/captures/capt-depfun.check b/tests/neg-custom-args/captures/capt-depfun.check index f2e8911a5f36..41cafe951ede 100644 --- a/tests/neg-custom-args/captures/capt-depfun.check +++ b/tests/neg-custom-args/captures/capt-depfun.check @@ -1,11 +1,12 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt-depfun.scala:11:43 ---------------------------------- 11 | val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error | ^^^^^^^ - | Found: Str^{} ->{ac, y, z} Str^{y, z} - | Required: Str^{y, z} => Str^{y, z} + |Found: Str^{} => Str^{y, z} + |Required: Str^{y, z} =>² Str^{y, z} | - | Note that capability y is not included in capture set {}. + |Note that capability y is not included in capture set {}. | - | where: => refers to a fresh root capability in the type of value dc + |where: => refers to a fresh root capability created in value dc when instantiating method apply's type (x: C^): Str^{x} =>³ Str^{x} + | =>² refers to a fresh root capability in the type of value dc | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/capt1.check b/tests/neg-custom-args/captures/capt1.check index 6af772cd2a0b..93b90d2d1279 100644 --- a/tests/neg-custom-args/captures/capt1.check +++ b/tests/neg-custom-args/captures/capt1.check @@ -59,10 +59,8 @@ |Note that capability cap is not included in capture set {cap²} |because cap is not visible from cap² in value z2. | - |where: ^ refers to a root capability associated with the result type of (): C^ - | ^² refers to a fresh root capability created in value z2 when checking argument to parameter a of method h - | cap is a root capability associated with the result type of (): C^ - | cap² is a fresh root capability created in value z2 when checking argument to parameter a of method h + |where: ^ and cap refer to a root capability associated with the result type of (): C^ + | ^² and cap² refer to a fresh root capability created in value z2 when checking argument to parameter a of method h | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:37:5 ----------------------------------------- @@ -74,10 +72,8 @@ |Note that capability cap is not included in capture set {cap²} |because cap is not visible from cap² in value z2. | - |where: ^ refers to a root capability associated with the result type of (): C^ - | ^² refers to a fresh root capability created in value z2 when checking argument to parameter b of method h - | cap is a root capability associated with the result type of (): C^ - | cap² is a fresh root capability created in value z2 when checking argument to parameter b of method h + |where: ^ and cap refer to a root capability associated with the result type of (): C^ + | ^² and cap² refer to a fresh root capability created in value z2 when checking argument to parameter b of method h | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/capt1.scala:38:13 ------------------------------------------------------------- diff --git a/tests/neg-custom-args/captures/caseclass/Test_2.scala b/tests/neg-custom-args/captures/caseclass/Test_2.scala index 5d3f9aaa6524..2d20f4c81852 100644 --- a/tests/neg-custom-args/captures/caseclass/Test_2.scala +++ b/tests/neg-custom-args/captures/caseclass/Test_2.scala @@ -22,4 +22,4 @@ def test(c: C) = val y4 = y3 match case Ref(xx) => xx - val y4c: () ->{y3} Unit = y4 + val y4c: () ->{y3} Unit = y4 // error diff --git a/tests/neg-custom-args/captures/cc-existential-conformance.check b/tests/neg-custom-args/captures/cc-existential-conformance.check index bed763707de5..d3117709d6c6 100644 --- a/tests/neg-custom-args/captures/cc-existential-conformance.check +++ b/tests/neg-custom-args/captures/cc-existential-conformance.check @@ -1,18 +1,17 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:8:24 -------------------- 8 | val y: A -> Fun[B^] = x // error | ^ - | Found: (x : A -> (x²: A) -> B^) - | Required: A -> A -> B^² + | Found: (x : A -> (x²: A) -> B^) + | Required: A -> A -> B^² | - | Note that capability cap is not included in capture set {cap²} - | because cap is not visible from cap² in value y. + | Note that capability cap is not included in capture set {cap²} + | because cap is not visible from cap² in value y. | - | where: ^ 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 y - | cap is a root capability associated with the result type of (x²: A): B^ - | cap² is a fresh root capability in the type of value y - | x is a value in method test - | x² is a reference to a value parameter + | where: ^ refers to a root capability associated with the result type of (x²: A): B^ + | ^² and cap² refer to a fresh root capability in the type of value y + | cap is the universal root capability + | x is a value in method test + | x² is a reference to a value parameter | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:9:29 -------------------- @@ -23,29 +22,24 @@ | | Note that capability y* is not included in capture set {cap}. | - | Note that the existential capture root in B^² - | cannot subsume the capability y* since that capability is not a `Sharable` capability.. - | | where: ^ refers to a root capability associated with the result type of (x: A): B^ - | ^² refers to the universal root capability - | cap is a root capability associated with the result type of (x: A): B^ + | cap is the universal root capability | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:13:19 ------------------- 13 | val y: Fun[B^] = x // error | ^ - | Found: (x : (x²: A) -> B^) - | Required: A -> B^² + | Found: (x : (x²: A) -> B^) + | Required: A -> B^² | - | Note that capability cap is not included in capture set {cap²} - | because cap is not visible from cap² in value y. + | Note that capability cap is not included in capture set {cap²} + | because cap is not visible from cap² in value y. | - | where: ^ 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 y - | cap is a root capability associated with the result type of (x²: A): B^ - | cap² is a fresh root capability in the type of value y - | x is a value in method test2 - | x² is a reference to a value parameter + | where: ^ refers to a root capability associated with the result type of (x²: A): B^ + | ^² and cap² refer to a fresh root capability in the type of value y + | cap is the universal root capability + | x is a value in method test2 + | x² is a reference to a value parameter | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:14:24 ------------------- @@ -56,11 +50,7 @@ | | Note that capability y* is not included in capture set {cap}. | - | Note that the existential capture root in B^² - | cannot subsume the capability y* since that capability is not a `Sharable` capability.. - | | where: ^ refers to a root capability associated with the result type of (x: A): B^ - | ^² refers to the universal root capability - | cap is a root capability associated with the result type of (x: A): B^ + | cap is the universal root capability | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/cc-poly-2.check b/tests/neg-custom-args/captures/cc-poly-2.check index 1082f2bf7a0b..77cb6e369c2e 100644 --- a/tests/neg-custom-args/captures/cc-poly-2.check +++ b/tests/neg-custom-args/captures/cc-poly-2.check @@ -6,8 +6,7 @@ | | Note that capability cap is not included in capture set {c1}. | - | where: ^ refers to a fresh root capability in the type of value d - | cap is a fresh root capability in the type of value d + | where: ^ and cap refer to a fresh root capability in the type of value d | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-poly-2.scala:16:20 ------------------------------------ diff --git a/tests/neg-custom-args/captures/cc-poly-varargs.check b/tests/neg-custom-args/captures/cc-poly-varargs.check deleted file mode 100644 index 764274813faf..000000000000 --- a/tests/neg-custom-args/captures/cc-poly-varargs.check +++ /dev/null @@ -1,34 +0,0 @@ --- Error: tests/neg-custom-args/captures/cc-poly-varargs.scala:11:13 --------------------------------------------------- -11 | val left = src1.transformValuesWith(Left(_)) // error - | ^^^^ - |Separation failure: argument of type (src1 : Source[T1, scala.caps.CapSet^{Cap}]^{Cap}) - |to method transformValuesWith: [T, Cap >: scala.caps.CapSet <: scala.caps.CapSet^] - | (src: Source[T, scala.caps.CapSet^{Cap}]^)[U](f: T ->{Cap} U): Source[U, scala.caps.CapSet^{Cap}]^{src, f} - |corresponds to capture-polymorphic formal parameter src of type Source[T1^'s3, scala.caps.CapSet^{Cap}]^ - |and hides capabilities {src1}. - |Some of these overlap with the captures of the function result with type Source[Left[T1^'s1, Nothing]^'s2, scala.caps.CapSet^{Cap}]^{src1}. - | - | Hidden set of current argument : {src1} - | Hidden footprint of current argument : {src1, Cap} - | Capture set of function result : {src1, Cap} - | Footprint set of function result : {src1, Cap} - | The two sets overlap at : {src1, Cap} - | - |where: ^ refers to a fresh root capability created in value left when checking argument to parameter src of method transformValuesWith --- Error: tests/neg-custom-args/captures/cc-poly-varargs.scala:12:14 --------------------------------------------------- -12 | val right = src2.transformValuesWith(Right(_)) // error - | ^^^^ - |Separation failure: argument of type (src2 : Source[T2, scala.caps.CapSet^{Cap}]^{Cap}) - |to method transformValuesWith: [T, Cap >: scala.caps.CapSet <: scala.caps.CapSet^] - | (src: Source[T, scala.caps.CapSet^{Cap}]^)[U](f: T ->{Cap} U): Source[U, scala.caps.CapSet^{Cap}]^{src, f} - |corresponds to capture-polymorphic formal parameter src of type Source[T2^'s6, scala.caps.CapSet^{Cap}]^ - |and hides capabilities {src2}. - |Some of these overlap with the captures of the function result with type Source[Right[Nothing, T2^'s4]^'s5, scala.caps.CapSet^{Cap}]^{src2}. - | - | Hidden set of current argument : {src2} - | Hidden footprint of current argument : {src2, Cap} - | Capture set of function result : {src2, Cap} - | Footprint set of function result : {src2, Cap} - | The two sets overlap at : {src2, Cap} - | - |where: ^ refers to a fresh root capability created in value right when checking argument to parameter src of method transformValuesWith diff --git a/tests/neg-custom-args/captures/cc-this.check b/tests/neg-custom-args/captures/cc-this.check index a66e210461ee..d7bd06246218 100644 --- a/tests/neg-custom-args/captures/cc-this.check +++ b/tests/neg-custom-args/captures/cc-this.check @@ -15,7 +15,3 @@ 19 | class C4(val f: () => Int) extends C3 // error | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ |reference (C4.this.f : () => Int) captured by this self type is not included in the allowed capture set {} of pure base class class C3 --- Error: tests/neg-custom-args/captures/cc-this.scala:33:8 ------------------------------------------------------------ -33 | def c3 = c2.y // error - | ^ - | Separation failure: method c3's inferred result type C{val x: () => Int}^{cc} hides non-local parameter cc diff --git a/tests/neg-custom-args/captures/cc-this.scala b/tests/neg-custom-args/captures/cc-this.scala index 3d9f8ca5cf53..6182e840edef 100644 --- a/tests/neg-custom-args/captures/cc-this.scala +++ b/tests/neg-custom-args/captures/cc-this.scala @@ -30,6 +30,6 @@ def test2(using consume cc: Cap) = def c1 = new C(f) def c2 = c1 - def c3 = c2.y // error + def c3 = c2.y // was error, now OK val c4: C^ = c3 val _ = c3: C^ diff --git a/tests/neg-custom-args/captures/cc-this4.check b/tests/neg-custom-args/captures/cc-this4.check index 1a704c84c77a..ecceb9479fc1 100644 --- a/tests/neg-custom-args/captures/cc-this4.check +++ b/tests/neg-custom-args/captures/cc-this4.check @@ -6,7 +6,6 @@ | | Note that capability cap is not included in capture set {}. | - | where: ^ refers to the universal root capability - | cap is the universal root capability + | where: ^ and cap refer to the universal root capability | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/check-inferred.check b/tests/neg-custom-args/captures/check-inferred.check new file mode 100644 index 000000000000..7e3f9022f5a5 --- /dev/null +++ b/tests/neg-custom-args/captures/check-inferred.check @@ -0,0 +1,35 @@ +-- Error: tests/neg-custom-args/captures/check-inferred.scala:12:19 ---------------------------------------------------- +12 | private val count = Ref() // error + | ^ + | value count needs an explicit type because it captures a root capability in its type test.Ref^. + | Fields of publicily accessible classes that capture a root capability need to be given an explicit type. + | + | where: ^ refers to a fresh root capability classified as Mutable in the type of value count +-- Error: tests/neg-custom-args/captures/check-inferred.scala:18:13 ---------------------------------------------------- +18 | val incr = () => // error + | ^ + | value incr needs an explicit type because the inferred type does not conform to + | the type that is externally visible in other compilation units. + | + | Inferred type : () ->{Counter.this.count} Unit + | Externally visible type: () -> Unit +19 | count.put(count.get + 1) +-- Error: tests/neg-custom-args/captures/check-inferred.scala:20:13 ---------------------------------------------------- +20 | val decr = () => // error + | ^ + | value decr needs an explicit type because the inferred type does not conform to + | the type that is externally visible in other compilation units. + | + | Inferred type : () ->{Counter.this.count} Unit + | Externally visible type: () -> Unit +21 | count.put(count.get - 1) +-- Error: tests/neg-custom-args/captures/check-inferred.scala:24:14 ---------------------------------------------------- +24 | val count = Ref(): Object^ // error + | ^^^^^^^^^^^^^^ + | value count needs an explicit type because the inferred type does not conform to + | the type that is externally visible in other compilation units. + | + | Inferred type : Object^ + | Externally visible type: Object + | + | where: ^ refers to a fresh root capability created in value count diff --git a/tests/neg-custom-args/captures/check-inferred.scala b/tests/neg-custom-args/captures/check-inferred.scala new file mode 100644 index 000000000000..2462e4cb2e82 --- /dev/null +++ b/tests/neg-custom-args/captures/check-inferred.scala @@ -0,0 +1,34 @@ +package test +import caps.Mutable +import caps.cap +import caps.unsafe.untrackedCaptures + +class Ref extends Mutable: + var x = 0 + def get: Int = x + update def put(y: Int): Unit = x = y + +class Counter: + private val count = Ref() // error + private val altCount: Ref^ = Ref() // ok + + @untrackedCaptures + private val altAltCount = Ref() // ok + + val incr = () => // error + count.put(count.get + 1) + val decr = () => // error + count.put(count.get - 1) + +trait CounterAPI: + val count = Ref(): Object^ // error + private def count2 = Ref() // ok + +def test() = + class Counter: + private val count = Ref() // ok + val incr = () => + count.put(count.get + 1) + val decr = () => + count.put(count.get - 1) + diff --git a/tests/neg-custom-args/captures/class-level-attack.check b/tests/neg-custom-args/captures/class-level-attack.check index 7b08a8d52538..d6fa9e5821a4 100644 --- a/tests/neg-custom-args/captures/class-level-attack.check +++ b/tests/neg-custom-args/captures/class-level-attack.check @@ -14,8 +14,7 @@ | Note that capability x is not included in capture set {cap} | because (x : IO^²) in method set is not visible from cap in value r. | - | where: ^ refers to a fresh root capability in the type of value r - | ^² refers to a fresh root capability in the type of parameter x - | cap is a fresh root capability in the type of value r + | where: ^ and cap refer to a fresh root capability in the type of value r + | ^² refers to a fresh root capability in the type of parameter x | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/closure-result-typing.check b/tests/neg-custom-args/captures/closure-result-typing.check index 7ab0066e9095..c1a963355017 100644 --- a/tests/neg-custom-args/captures/closure-result-typing.check +++ b/tests/neg-custom-args/captures/closure-result-typing.check @@ -6,7 +6,6 @@ | | Note that capability cap is not included in capture set {}. | - | where: ^ refers to a fresh root capability in the type of parameter c - | cap is a fresh root capability in the type of parameter c + | where: ^ and cap refer to a fresh root capability in the type of parameter c | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/contracap.check b/tests/neg-custom-args/captures/contracap.check index ee7078350936..7b2b04ae5eb1 100644 --- a/tests/neg-custom-args/captures/contracap.check +++ b/tests/neg-custom-args/captures/contracap.check @@ -6,7 +6,6 @@ | | Note that capability a is not included in capture set {cap}. | - | where: ^ refers to the universal root capability - | cap is the universal root capability + | where: ^ and cap refer to the universal root capability | | 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 8ea4e43adcb3..9460f3e7b45e 100644 --- a/tests/neg-custom-args/captures/dcs-tvar.check +++ b/tests/neg-custom-args/captures/dcs-tvar.check @@ -6,8 +6,7 @@ | | Note that capability cap is not included in capture set {}. | - | where: => refers to a fresh root capability in the type of type T - | cap is a fresh root capability in the type of type T + | where: => and cap refer to a fresh root capability in the type of type T | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/dcs-tvar.scala:9:2 --------------------------------------- @@ -18,7 +17,6 @@ | | Note that capability cap is not included in capture set {}. | - | where: => refers to a fresh root capability in the type of type U - | cap is a fresh root capability in the type of type U + | where: => and cap refer to a fresh root capability in the type of type U | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/depfun-reach.check b/tests/neg-custom-args/captures/depfun-reach.check index c66910d198ce..096fbf36e975 100644 --- a/tests/neg-custom-args/captures/depfun-reach.check +++ b/tests/neg-custom-args/captures/depfun-reach.check @@ -17,23 +17,19 @@ | | Note that capability cap is not included in capture set {cap²}. | - | 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 - | cap is a fresh root capability in the type of parameter op - | cap² is a fresh root capability in the result type of method foo + | where: => and cap refer to a fresh root capability in the type of parameter op + | =>² and cap² refer to a fresh root capability in the result type of method foo | | 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 | ^ - | Found: (a : (xs: List[() ->{io} Unit]) => List[() ->{xs*} Unit]) - | Required: (xs: List[() ->{io} Unit]) =>² List[() -> Unit] + | Found: (a : (xs: List[() ->{io} Unit]) => List[() ->{xs*} Unit]) + | Required: (xs: List[() ->{io} Unit]) =>² List[() -> Unit] | - | Note that capability cap is not included in capture set {cap²}. + | Note that capability cap is not included in capture set {cap²}. | - | 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 - | cap is a fresh root capability in the type of value a - | cap² is a fresh root capability in the type of value b + | where: => and cap refer to a fresh root capability in the type of value a + | =>² and cap² refer to a fresh root capability in the type of value b | | 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 53999323a742..67f4afc25373 100644 --- a/tests/neg-custom-args/captures/existential-mapping.check +++ b/tests/neg-custom-args/captures/existential-mapping.check @@ -8,14 +8,13 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:9:25 --------------------------- 9 | val _: (x: C^) -> C = x1 // error | ^^ - | Found: (x1 : (x: C^) -> C^²) - | Required: (x: C^) -> C + | Found: (x1 : (x: C^) -> C^²) + | Required: (x: C^) -> C | - | Note that capability cap is not included in capture set {}. + | Note that capability cap is not included in capture set {}. | - | where: ^ refers to the universal root capability - | ^² refers to a root capability associated with the result type of (x: C^): C^² - | cap is a root capability associated with the result type of (x: C^): C^² + | where: ^ refers to the universal root capability + | ^² and cap refer to a root capability associated with the result type of (x: C^): C^² | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:12:20 -------------------------- @@ -32,14 +31,13 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:15:30 -------------------------- 15 | val _: A^ -> (x: C^) -> C = x3 // error | ^^ - | Found: (x3 : A^ -> (x: C^) -> C^²) - | Required: A^ -> (x: C^) -> C + | Found: (x3 : A^ -> (x: C^) -> C^²) + | Required: A^ -> (x: C^) -> C | - | Note that capability cap is not included in capture set {}. + | Note that capability cap is not included in capture set {}. | - | where: ^ refers to the universal root capability - | ^² refers to a root capability associated with the result type of (x: C^): C^² - | cap is a root capability associated with the result type of (x: C^): C^² + | where: ^ refers to the universal root capability + | ^² and cap refer to a root capability associated with the result type of (x: C^): C^² | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:18:25 -------------------------- @@ -56,44 +54,40 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:21:30 -------------------------- 21 | val _: A^ -> (x: C^) -> C = x5 // error | ^^ - | Found: (x5 : A^ -> (x: C^) -> C^²) - | Required: A^ -> (x: C^) -> C + | Found: (x5 : A^ -> (x: C^) -> C^²) + | Required: A^ -> (x: C^) -> C | - | Note that capability cap is not included in capture set {}. + | Note that capability cap is not included in capture set {}. | - | where: ^ refers to the universal root capability - | ^² refers to a root capability associated with the result type of (x: C^): C^² - | cap is a root capability associated with the result type of (x: C^): C^² + | where: ^ refers to the universal root capability + | ^² and cap refer to a root capability associated with the result type of (x: C^): C^² | | 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 | ^^ - | Found: A^ -> (x: C^) ->{x6*} C^² - | Required: A^ -> (x: C^) => C + | Found: A^ -> (x: C^) ->{x6*} C^² + | Required: A^ -> (x: C^) => C | - | Note that capability cap is not included in capture set {}. + | Note that capability cap is not included in capture set {}. | - | where: => refers to a fresh root capability in the type of value _$6 - | ^ refers to the universal root capability - | ^² refers to a root capability associated with the result type of (x: C^): C^² - | cap is a root capability associated with the result type of (x: C^): C^² + | where: => refers to a fresh root capability in the type of value _$6 + | ^ refers to the universal root capability + | ^² and cap refer to a root capability associated with the result type of (x: C^): C^² | | 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 | ^^ - | Found: (y1 : (x: C^) => C^²) - | Required: (x: C^) =>² C + | Found: (y1 : (x: C^) => C^²) + | Required: (x: C^) =>² C | - | Note that capability cap is not included in capture set {cap²}. + | Note that capability cap is not included in capture set {cap²}. | - | where: => refers to a fresh root capability in the type of value y1 - | =>² refers to a fresh root capability in the type of value _$7 - | ^ refers to the universal root capability - | ^² refers to a root capability associated with the result type of (x: C^): C^² - | cap is a fresh root capability in the type of value y1 - | cap² is a fresh root capability in the type of value _$7 + | where: => and cap refer to a fresh root capability in the type of value y1 + | =>² and cap² refer to a fresh root capability in the type of value _$7 + | ^ refers to the universal root capability + | ^² refers to a root capability associated with the result type of (x: C^): C^² | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:30:20 -------------------------- @@ -111,16 +105,15 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:33:30 -------------------------- 33 | val _: A^ => (x: C^) => C = y3 // error | ^^ - | Found: A^ ->{y3} (x: C^) ->{y3*} C^² - | Required: A^ => (x: C^) =>² C + | Found: A^ ->{y3} (x: C^) ->{y3*} C^² + | Required: A^ => (x: C^) =>² C | - | Note that capability cap is not included in capture set {}. + | Note that capability cap is not included in capture set {}. | - | where: => refers to a fresh root capability in the type of value _$9 - | =>² refers to a fresh root capability in the type of value _$9 - | ^ refers to the universal root capability - | ^² refers to a root capability associated with the result type of (x: C^): C^² - | cap is a root capability associated with the result type of (x: C^): C^² + | where: => refers to a fresh root capability in the type of value _$9 + | =>² refers to a fresh root capability in the type of value _$9 + | ^ refers to the universal root capability + | ^² and cap refer to a root capability associated with the result type of (x: C^): C^² | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:36:25 -------------------------- @@ -139,31 +132,28 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:39:30 -------------------------- 39 | val _: A^ => (x: C^) -> C = y5 // error | ^^ - | Found: (y5 : A^ => (x: C^) -> C^²) - | Required: A^ =>² (x: C^) -> C + | Found: (y5 : A^ => (x: C^) -> C^²) + | Required: A^ =>² (x: C^) -> C | - | Note that capability cap is not included in capture set {cap²}. + | Note that capability cap is not included in capture set {cap²}. | - | where: => refers to a fresh root capability in the type of value y5 - | =>² refers to a fresh root capability in the type of value _$11 - | ^ refers to the universal root capability - | ^² refers to a root capability associated with the result type of (x: C^): C^² - | cap is a fresh root capability in the type of value y5 - | cap² is a fresh root capability in the type of value _$11 + | where: => and cap refer to a fresh root capability in the type of value y5 + | =>² and cap² refer to a fresh root capability in the type of value _$11 + | ^ refers to the universal root capability + | ^² refers to a root capability associated with the result type of (x: C^): C^² | | 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 | ^^ - | Found: A^ ->{y6} (x: C^) ->{y6*} C^² - | Required: A^ => (x: C^) =>² C + | Found: A^ ->{y6} (x: C^) ->{y6*} C^² + | Required: A^ => (x: C^) =>² C | - | Note that capability cap is not included in capture set {}. + | Note that capability cap is not included in capture set {}. | - | where: => refers to a fresh root capability in the type of value _$12 - | =>² refers to a fresh root capability in the type of value _$12 - | ^ refers to the universal root capability - | ^² refers to a root capability associated with the result type of (x: C^): C^² - | cap is a root capability associated with the result type of (x: C^): C^² + | where: => refers to a fresh root capability in the type of value _$12 + | =>² refers to a fresh root capability in the type of value _$12 + | ^ refers to the universal root capability + | ^² and cap refer to a root capability associated with the result type of (x: C^): C^² | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/extending-cap-classes.check b/tests/neg-custom-args/captures/extending-cap-classes.check index be0e94316f71..44234bf2384c 100644 --- a/tests/neg-custom-args/captures/extending-cap-classes.check +++ b/tests/neg-custom-args/captures/extending-cap-classes.check @@ -1,23 +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} + |Found: C2^ |Required: C1 | - |Note that capability cap.rd is not included in capture set {}. + |Note that capability cap is not included in capture set {}. | - |where: cap is a fresh root capability classified as SharedCapability created in value x2 when constructing Capability instance C2 + |where: ^ and cap refer to a fresh root capability classified as SharedCapability created in value x2 when constructing Capability instance C2 | | 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} + |Found: C3^ |Required: C1 | - |Note that capability cap.rd is not included in capture set {}. + |Note that capability cap is not included in capture set {}. | - |where: cap is a fresh root capability classified as SharedCapability created in value x3 when constructing Capability instance C3 + |where: ^ and cap refer to a fresh root capability classified as SharedCapability created in value x3 when constructing Capability instance C3 | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/extending-cap-classes.scala:13:15 ------------------------ diff --git a/tests/neg-custom-args/captures/fresh-counter.check b/tests/neg-custom-args/captures/fresh-counter.check new file mode 100644 index 000000000000..84d3137b63bb --- /dev/null +++ b/tests/neg-custom-args/captures/fresh-counter.check @@ -0,0 +1,32 @@ +-- Error: tests/neg-custom-args/captures/fresh-counter.scala:23:6 ------------------------------------------------------ +23 | par(i, d) // error: separation failure + | ^ + |Separation failure: argument of type (i : () ->{c.incr} Unit) + |to method par: (p1: () => Unit, p2: () => Unit): Unit + |corresponds to capture-polymorphic formal parameter p1 of type () => Unit + |and hides capabilities {i}. + |Some of these overlap with the captures of the second argument with type (d : () ->{c.decr} Unit). + | + | Hidden set of current argument : {i} + | Hidden footprint of current argument : {i, c.incr, c.count} + | Capture set of second argument : {d} + | Footprint set of second argument : {d, c.decr, c} + | The two sets overlap at : {c.incr, c.count} + | + |where: => refers to a fresh root capability created in method test when checking argument to parameter p1 of method par +-- Error: tests/neg-custom-args/captures/fresh-counter.scala:33:4 ------------------------------------------------------ +33 | () => count.put(count.get + 1), // error: separation failure + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + |Separation failure: argument of type () ->{count} Unit + |to constructor Pair: (a: () => Unit, b: () => Unit): Pair + |corresponds to capture-polymorphic formal parameter a of type () => Unit + |and hides capabilities {count}. + |Some of these overlap with the captures of the second argument with type () ->{count} Unit. + | + | Hidden set of current argument : {count} + | Hidden footprint of current argument : {count} + | Capture set of second argument : {count} + | Footprint set of second argument : {count} + | The two sets overlap at : {count} + | + |where: => refers to a fresh root capability created in method mkCounter when checking argument to parameter a of constructor Pair diff --git a/tests/neg-custom-args/captures/fresh-counter.scala b/tests/neg-custom-args/captures/fresh-counter.scala new file mode 100644 index 000000000000..233b0e3c91e2 --- /dev/null +++ b/tests/neg-custom-args/captures/fresh-counter.scala @@ -0,0 +1,35 @@ +import caps.Mutable +import caps.cap + +class Ref extends Mutable: + var x = 0 + def get: Int = x + update def put(y: Int): Unit = x = y + +class Counter: + private val count: Ref^ = Ref() + val incr = () => + count.put(count.get + 1) + val decr: () ->{this} Unit = () => + count.put(count.get - 1) + +def par(p1: () => Unit, p2: () => Unit) = () +def seq(p1: () => Unit, p2: () ->{cap, p1} Unit) = () + +def test() = + val c = Counter() + val i = c.incr + val d = c.decr + par(i, d) // error: separation failure + seq(i, d) + +type Proc = () => Unit + +class Pair(val a: Proc, val b: Proc) + +def mkCounter(): Pair^ = + val count = Ref() + Pair( + () => count.put(count.get + 1), // error: separation failure + () => count.put(count.get - 1)) + diff --git a/tests/neg-custom-args/captures/fresh-fields.check b/tests/neg-custom-args/captures/fresh-fields.check new file mode 100644 index 000000000000..4fca44da38b0 --- /dev/null +++ b/tests/neg-custom-args/captures/fresh-fields.check @@ -0,0 +1,55 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/fresh-fields.scala:25:13 --------------------------------- +25 | val _: B = b // error + | ^ + | Found: (b : B^) + | Required: B + | + | Note that capability cap is not included in capture set {}. + | + | where: ^ and cap refer to a fresh root capability in the type of value b + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/fresh-fields.scala:27:13 --------------------------------- +27 | val _: C = c // error + | ^ + | Found: (c : C^) + | Required: C + | + | Note that capability cap is not included in capture set {}. + | + | where: ^ and cap refer to a fresh root capability in the type of value c + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/fresh-fields.scala:29:13 --------------------------------- +29 | val _: D = d // error + | ^ + | Found: (d : D^) + | Required: D + | + | Note that capability cap is not included in capture set {}. + | + | where: ^ and cap refer to a fresh root capability in the type of value d + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/fresh-fields.scala:31:13 --------------------------------- +31 | val _: E = e // error + | ^ + | Found: (e : E^) + | Required: E + | + | Note that capability cap is not included in capture set {}. + | + | where: ^ and cap refer to a fresh root capability classified as SharedCapability in the type of value e + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/fresh-fields.scala:33:13 --------------------------------- +33 | val _: F = f // error + | ^ + | Found: (f : F^) + | Required: F + | + | Note that capability cap is not included in capture set {}. + | + | where: ^ and cap refer to a fresh root capability in the type of value f + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/fresh-fields.scala b/tests/neg-custom-args/captures/fresh-fields.scala new file mode 100644 index 000000000000..cbfa32cb201a --- /dev/null +++ b/tests/neg-custom-args/captures/fresh-fields.scala @@ -0,0 +1,33 @@ +open class A: + def a: A^ = A() // no fresh contribution since `a` is a method + val as: List[A^] = List(A()) // no fresh contribution since A^ is boxed + +class B: + private val b: A^ = A() // contributes fresh + +class C extends B // contributes fresh via B + +class D: + private val f: () -> A = () => new A() + private val b: () -> A^ = f // contributes fresh + +class Shared extends caps.SharedCapability + +trait E: + private val e: Shared = Shared() + +class F extends B, E + +def test() = + val a = A() + val _: A = a // ok + val b = B() + val _: B = b // error + val c = C() + val _: C = c // error + val d = D() + val _: D = d // error + val e = new E() {} + val _: E = e // error + val f = F() + val _: F = f // error diff --git a/tests/neg-custom-args/captures/heal-tparam-cs.check b/tests/neg-custom-args/captures/heal-tparam-cs.check index d23ebe064866..eb910f007614 100644 --- a/tests/neg-custom-args/captures/heal-tparam-cs.check +++ b/tests/neg-custom-args/captures/heal-tparam-cs.check @@ -22,10 +22,9 @@ | Note that the existential capture root in () =>² Unit | cannot subsume the capability (x$0 : Capp^'s4) since that capability is not a `Sharable` capability.. | - | where: => refers to a root capability associated with the result type of (c: Capp^): () => Unit - | =>² refers to the universal root capability - | ^ refers to the universal root capability - | cap is a root capability associated with the result type of (x$0: Capp^'s4): () ->{x$0} Unit + | where: => refers to a root capability associated with the result type of (c: Capp^): () => Unit + | =>² and ^ refer to the universal root capability + | cap is a root capability associated with the result type of (x$0: Capp^'s4): () ->{x$0} Unit 16 | (c1: Capp^) => () => { c1.use() } 17 | } | diff --git a/tests/neg-custom-args/captures/i15772.check b/tests/neg-custom-args/captures/i15772.check index b167580f548c..08536e05a189 100644 --- a/tests/neg-custom-args/captures/i15772.check +++ b/tests/neg-custom-args/captures/i15772.check @@ -8,20 +8,16 @@ |C^ => Unit cannot be box-converted to C{val arg: C^²}^{c} ->{cap, c} Unit |since the additional capture set {c} resulting from box conversion is not allowed in C{val arg: C^²}^{c} => Unit | - |where: => refers to the universal root capability - | ^ refers to the universal root capability - | ^² refers to a fresh root capability in the type of value arg - | cap is the universal root capability + |where: => and ^ and cap refer to the universal root capability + | ^² refers to a fresh root capability in the type of value arg -- Error: tests/neg-custom-args/captures/i15772.scala:29:35 ------------------------------------------------------------ 29 | val boxed2 : Observe[C^] = box2(c) // error | ^^^^^^^ |C^ => Unit cannot be box-converted to C{val arg: C^²}^{c} ->{cap, c} Unit |since the additional capture set {c} resulting from box conversion is not allowed in C{val arg: C^²}^{c} => Unit | - |where: => refers to the universal root capability - | ^ refers to the universal root capability - | ^² refers to a fresh root capability in the type of value arg - | cap is the universal root capability + |where: => and ^ and cap refer to the universal root capability + | ^² refers to a fresh root capability in the type of value arg -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15772.scala:35:33 --------------------------------------- 35 | val boxed2 : Observe[C]^ = box2(c) // error | ^^^^^^^ @@ -30,11 +26,10 @@ | |Note that capability cap is not included in capture set {}. | - |where: => refers to the universal root capability - | =>² refers to a fresh root capability in the type of value boxed2 - | ^ 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²} - | cap is a fresh root capability created in value boxed2 when instantiating method c's type -> C^{cap²} + |where: => refers to the universal root capability + | =>² refers to a fresh root capability in the type of value boxed2 + | ^ refers to a fresh root capability in the type of value arg + | ^² and cap refer to a fresh root capability created in value boxed2 when instantiating method c's type -> C^{cap²} | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15772.scala:46:2 ---------------------------------------- diff --git a/tests/neg-custom-args/captures/i16226.check b/tests/neg-custom-args/captures/i16226.check index 76111efa2a32..d48897126600 100644 --- a/tests/neg-custom-args/captures/i16226.check +++ b/tests/neg-custom-args/captures/i16226.check @@ -8,12 +8,11 @@ |Note that capability f1 is not included in capture set {cap} |because (f1 : A^'s5 ->'s6 B^'s7) is not visible from cap in method mapc. | - |where: => refers to a root capability associated with the result type of (ref1: LazyRef[A^'s1]{val elem: () ->'s2 A^'s3}^'s4, f1: A^'s5 ->'s6 B^'s7): + |where: => refers to a root capability associated with the result type of (ref1: LazyRef[A^'s1]{val elem: () ->'s2 A^'s3}^'s4, f1: A^'s5 ->'s6 B^'s7): | LazyRef[B^'s9]{val elem: () => B^'s10}^{f1, ref1} - | =>² refers to the universal root capability - | =>³ 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 - | cap is a fresh root capability in the result type of method mapc + | =>² refers to the universal root capability + | =>³ refers to a fresh root capability in the result type of method mapc + | ^ and cap refer to a fresh root capability in the result type of method mapc | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i16226.scala:15:4 ---------------------------------------- @@ -28,13 +27,10 @@ |Note that the existential capture root in LazyRef[B]^² |cannot subsume the capability (f1 : A^'s15 ->'s16 B^'s17) since that capability is not a `Sharable` capability.. | - |where: => refers to a root capability associated with the result type of (ref1: LazyRef[A^'s11]{val elem: () ->'s12 A^'s13}^'s14, f1: A^'s15 ->'s16 B^'s17): - | LazyRef[B^'s19]{val elem: () => B^'s20}^{f1, ref1} - | =>² refers to the universal root capability - | =>³ 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]^ - | ^² refers to the universal root capability - | cap is a root capability associated with the result type of (ref1: LazyRef[A^'s11]{val elem: () ->'s12 A^'s13}^'s14, f1: A^'s15 ->'s16 B^'s17): + |where: => and cap refer to a root capability associated with the result type of (ref1: LazyRef[A^'s11]{val elem: () ->'s12 A^'s13}^'s14, f1: A^'s15 ->'s16 B^'s17): | LazyRef[B^'s19]{val elem: () => B^'s20}^{f1, ref1} + | =>² and ^² refer to the universal root capability + | =>³ 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]^ | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i19330.check b/tests/neg-custom-args/captures/i19330.check index 72947fb1bcf6..abdeeb1eded3 100644 --- a/tests/neg-custom-args/captures/i19330.check +++ b/tests/neg-custom-args/captures/i19330.check @@ -12,21 +12,6 @@ | Note that capability t 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 --------------------------------------- -22 | val bad: bar.T = foo(bar) // error - | ^^^^^^^^ - | Found: bar.T - | Required: () => Logger^ - | - | Note that capability cap is not included in capture set {cap²} - | because cap in class Bar is not visible from cap² in value bad. - | - | 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 - | cap is a fresh root capability in the type of type T - | cap² is a fresh root capability in the type of 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/i19330.scala b/tests/neg-custom-args/captures/i19330.scala index cdc0367bc7d3..57a54ef81a20 100644 --- a/tests/neg-custom-args/captures/i19330.scala +++ b/tests/neg-custom-args/captures/i19330.scala @@ -19,5 +19,5 @@ def foo(x: Foo): x.T = def test(): Unit = val bar = new Bar - val bad: bar.T = foo(bar) // error + val bad: bar.T = foo(bar) val leaked: Logger^ = bad() // leaked scoped capability! diff --git a/tests/neg-custom-args/captures/i21401.check b/tests/neg-custom-args/captures/i21401.check index ae82cd8f08fd..ac8cecf98514 100644 --- a/tests/neg-custom-args/captures/i21401.check +++ b/tests/neg-custom-args/captures/i21401.check @@ -21,10 +21,9 @@ |Note that capability x is not included in capture set {cap} |because (x : IO^'s1) is not visible from cap in value a. | - |where: => refers to a fresh root capability created in value a when checking argument to parameter op of method usingIO - | ^ 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 - | cap is a fresh root capability created in value a when checking argument to parameter op of method usingIO + |where: => refers to a fresh root capability created in value a when checking argument to parameter op of method usingIO + | ^ refers to the universal root capability + | ^² and cap refer to a fresh root capability created in value a when checking argument to parameter op of method usingIO | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/i21401.scala:16:66 ------------------------------------------------------------ @@ -51,18 +50,16 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21401.scala:17:67 --------------------------------------- 17 | val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error // error | ^^^^^^ - | Found: (x: Boxed[IO^]^'s3) ->'s4 Boxed[IO^²] - | Required: Boxed[IO^] -> Boxed[IO^³] + |Found: (x: Boxed[IO^]^'s3) ->'s4 Boxed[IO^²] + |Required: Boxed[IO^] -> Boxed[IO^³] | - | Note that capability cap is not included in capture set {cap²} - | because cap is not visible from cap² in value x². + |Note that capability cap is not included in capture set {cap²} + |because cap is not visible from cap² in value x². | - | where: ^ refers to the universal root capability - | ^² refers to a root capability associated with the result type of (x: Boxed[IO^]^'s3): Boxed[IO^²] - | ^³ refers to a fresh root capability created in value x² - | cap is a root capability associated with the result type of (x: Boxed[IO^]^'s3): Boxed[IO^²] - | cap² is a fresh root capability created in value x² - | x is a reference to a value parameter - | x² is a value in method test2 + |where: ^ refers to the universal root capability + | ^² and cap refer to a root capability associated with the result type of (x: Boxed[IO^]^'s3): Boxed[IO^²] + | ^³ and cap² refer to a fresh root capability created in value x² + | x is a reference to a value parameter + | x² is a value in method test2 | | 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 89b9a4b216c1..fc6f23ec2dc8 100644 --- a/tests/neg-custom-args/captures/i21614.check +++ b/tests/neg-custom-args/captures/i21614.check @@ -1,35 +1,25 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:12:33 --------------------------------------- -12 | files.map((f: F) => new Logger(f)) // error // error, Q: can we make this pass (see #19076)? +12 | files.map((f: F) => new Logger(f)) // error, Q: can we make this pass (see #19076)? | ^ |Found: (f : F) |Required: File^ | |Note that capability cap is not included in capture set {cap²}. | - |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 - | cap is a fresh root capability classified as SharedCapability in the type of parameter f - | cap² is 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 + |where: ^ and cap² refer 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 + | cap is a fresh root capability classified as SharedCapability in the type of parameter f | | longer explanation available when compiling with `-explain` --- Error: tests/neg-custom-args/captures/i21614.scala:12:8 ------------------------------------------------------------- -12 | files.map((f: F) => new Logger(f)) // error // error, Q: can we make this pass (see #19076)? - | ^^^^^^^^^ - |Type variable U of method map cannot be instantiated to Logger{val f: File^'s1}^{cap.rd} since - |that type captures the root capability `cap`. - |This is often caused by a local capability in an argument of method map - |leaking as part of its result. - | - |where: cap is a root capability associated with the result type of (f²: F^{files*}): Logger{val f: File^'s1}^'s2 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:15:12 --------------------------------------- 15 | files.map(new Logger(_)) // error, Q: can we improve the error message? | ^^^^^^^^^^^^^ - |Found: (_$1: File^'s3) ->{C} Logger{val f: File^{_$1}}^{cap.rd, _$1} - |Required: File^{C} => Logger{val f: File^'s4}^'s5 + |Found: (_$1: File^'s1) ->{C} Logger{val f: File^{_$1}}^{cap, _$1} + |Required: File^{C} => Logger{val f: File^'s2}^'s3 | |Note that capability C is not classified as trait SharedCapability, therefore it - |cannot be included in capture set 's3 of parameter _$1 of SharedCapability elements. + |cannot be included in capture set 's1 of parameter _$1 of SharedCapability elements. | |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^'s3): Logger{val f: File^{_$1}}^{cap.rd, _$1} + | cap is a root capability associated with the result type of (_$1: File^'s1): Logger{val f: File^{_$1}}^{cap, _$1} | | 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 54e3ea863677..11929f2414db 100644 --- a/tests/neg-custom-args/captures/i21614.scala +++ b/tests/neg-custom-args/captures/i21614.scala @@ -9,7 +9,7 @@ trait File extends SharedCapability class Logger(f: File^) extends SharedCapability // <- will work if we remove the extends clause def mkLoggers1[F <: File^](files: List[F]): List[Logger^] = - files.map((f: F) => new Logger(f)) // error // error, Q: can we make this pass (see #19076)? + files.map((f: F) => new Logger(f)) // error, Q: can we make this pass (see #19076)? def mkLoggers2[C^](files: List[File^{C}]): List[Logger^] = files.map(new Logger(_)) // error, Q: can we improve the error message? diff --git a/tests/neg-custom-args/captures/i23431.check b/tests/neg-custom-args/captures/i23431.check index 722fd6d6e313..5bbcb2b720f0 100644 --- a/tests/neg-custom-args/captures/i23431.check +++ b/tests/neg-custom-args/captures/i23431.check @@ -7,10 +7,8 @@ | Note that capability cap is not included in capture set {cap²} | because cap in method setIO is not visible from cap² in variable myIO. | - | 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 - | cap is a fresh root capability in the type of parameter io - | cap² is a fresh root capability in the type of variable myIO + | where: ^ and cap refer to a fresh root capability in the type of parameter io + | ^² and cap² refer to a fresh root capability in the type of variable myIO | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23431.scala:11:13 --------------------------------------- @@ -22,10 +20,8 @@ | Note that capability cap is not included in capture set {cap²} | because cap in enclosing function is not visible from cap² in variable myIO. | - | 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 - | cap is a fresh root capability in the type of parameter io2 - | cap² is a fresh root capability in the type of variable myIO + | where: ^ and cap refer to a fresh root capability in the type of parameter io2 + | ^² and cap² refer to a fresh root capability in the type of variable myIO | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23431.scala:12:12 --------------------------------------- diff --git a/tests/neg-custom-args/captures/i23746.check b/tests/neg-custom-args/captures/i23746.check index 0f1dc797e10f..1db206879f02 100644 --- a/tests/neg-custom-args/captures/i23746.check +++ b/tests/neg-custom-args/captures/i23746.check @@ -6,8 +6,7 @@ | | Note that capability cap is not included in capture set {}. | - | where: => refers to a fresh root capability in the type of type X - | cap is a fresh root capability in the type of type X + | where: => and cap refer to a fresh root capability in the type of type X | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23746.scala:10:4 ---------------------------------------- diff --git a/tests/neg-custom-args/captures/i24137.check b/tests/neg-custom-args/captures/i24137.check new file mode 100644 index 000000000000..3f7d14144c32 --- /dev/null +++ b/tests/neg-custom-args/captures/i24137.check @@ -0,0 +1,22 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i24137.scala:16:21 --------------------------------------- +16 | val _: B^{async} = b // error, but could be OK if we have a way to mark + | ^ + | Found: (b : B{val elem1: A^{a}; val elem2: A^{a}}^{cap, a}) + | Required: B^{async} + | + | Note that capability cap is not included in capture set {async}. + | + | where: cap is a fresh root capability in the type of value b + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i24137.scala:18:23 --------------------------------------- +18 | val b1: B^{async} = B(a, a) // error but could also be OK + | ^^^^^^^ + | Found: B{val elem1: (a : A^{async}); val elem2: (a : A^{async})}^{cap, a} + | Required: B^{async} + | + | Note that capability cap is not included in capture set {async}. + | + | where: cap is a fresh root capability created in value b1 when constructing instance B + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/i24137.scala b/tests/neg-custom-args/captures/i24137.scala new file mode 100644 index 000000000000..033fa1b7d2f2 --- /dev/null +++ b/tests/neg-custom-args/captures/i24137.scala @@ -0,0 +1,18 @@ +//< using options -Ycc-verbose +import caps.{cap, Shared, SharedCapability} + +open class A + +class B(elem1: A^{cap.only[Shared]}, elem2: A^{cap.only[Shared]}): + private var curElem: A^ = elem1 // problem is curElem contibutes cap to B(). + def next() = + curElem = elem2 + +class Async extends caps.SharedCapability + +def test(async: Async) = + val a: A^{async} = A() + val b = B(a, a) + val _: B^{async} = b // error, but could be OK if we have a way to mark + // curElem above as not contributing anything + val b1: B^{async} = B(a, a) // error but could also be OK diff --git a/tests/neg-custom-args/captures/lazyref.check b/tests/neg-custom-args/captures/lazyref.check index 52e787f66553..56d0c8a2d329 100644 --- a/tests/neg-custom-args/captures/lazyref.check +++ b/tests/neg-custom-args/captures/lazyref.check @@ -34,14 +34,19 @@ | Note that capability ref4 is not included in capture set {cap1}. | | longer explanation available when compiling with `-explain` +-- Error: tests/neg-custom-args/captures/lazyref.scala:6:14 ------------------------------------------------------------ +6 | def get: () => T = elem // error: separation failure + | ^^^^^^^ + | Separation failure: method get's result type () => T hides non-local this of class class LazyRef. + | The access must be in a consume method to allow this. -- Error: tests/neg-custom-args/captures/lazyref.scala:8:24 ------------------------------------------------------------ 8 | new LazyRef(() => f(elem())) // error: separation failure | ^^^^ | Separation failure: Illegal access to {LazyRef.this.elem} which is hidden by the previous definition - | of value get with type () => T. + | of method get with result type () => T. | This type hides capabilities {LazyRef.this.elem} | - | where: => refers to a fresh root capability in the type of value get + | where: => refers to a fresh root capability in the result type of method get -- Error: tests/neg-custom-args/captures/lazyref.scala:29:9 ------------------------------------------------------------ 29 | .map(g) // error: separation failure | ^ diff --git a/tests/neg-custom-args/captures/lazyref.scala b/tests/neg-custom-args/captures/lazyref.scala index ea3897484857..28149c6d10a3 100644 --- a/tests/neg-custom-args/captures/lazyref.scala +++ b/tests/neg-custom-args/captures/lazyref.scala @@ -3,7 +3,7 @@ class CC type Cap = CC^ class LazyRef[T](val elem: () => T): - val get: () => T = elem + def get: () => T = elem // error: separation failure def map[U](f: T => U): LazyRef[U]^{f, this} = new LazyRef(() => f(elem())) // error: separation failure diff --git a/tests/neg-custom-args/captures/linear-buffer-2.check b/tests/neg-custom-args/captures/linear-buffer-2.check index 6d9493bddb02..700c37ee2302 100644 --- a/tests/neg-custom-args/captures/linear-buffer-2.check +++ b/tests/neg-custom-args/captures/linear-buffer-2.check @@ -1,11 +1,11 @@ -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:13:13 --------------------------------------------------- 13 | val buf3 = buf.append(3) // error | ^^^ - | Separation failure: Illegal access to {buf} which is hidden by the previous definition - | of value buf1 with type Buffer[Int]^. - | This type hides capabilities {buf} + | Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed to a + | consume parameter or was used as a prefix to a consume method on line 11 + | and therefore is no longer available. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of value buf1 + | where: ^ refers to a fresh root capability classified as Mutable in the type of parameter buf -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:20:13 --------------------------------------------------- 20 | val buf3 = buf1.append(4) // error | ^^^^ diff --git a/tests/neg-custom-args/captures/nested-classes-2.check b/tests/neg-custom-args/captures/nested-classes-2.check new file mode 100644 index 000000000000..7337c8f6c8ab --- /dev/null +++ b/tests/neg-custom-args/captures/nested-classes-2.check @@ -0,0 +1,11 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/nested-classes-2.scala:9:36 ------------------------------ +9 | val cc3: cc1.C2^{cc1, x1, x2} = cc2 // error + | ^^^ + | Found: cc1.C2{val y1: () ->{cc2*} Unit; val y2: (() => Unit) ->{cc2*} Unit}^{cc2} + | Required: cc1.C2^{cc1, x1, x2} + | + | Note that capability cc2 is not included in capture set {cc1, x1, x2}. + | + | where: => refers to the universal root capability + | + | longer explanation available when compiling with `-explain` diff --git a/tests/pos-custom-args/captures/nested-classes-2.scala b/tests/neg-custom-args/captures/nested-classes-2.scala similarity index 80% rename from tests/pos-custom-args/captures/nested-classes-2.scala rename to tests/neg-custom-args/captures/nested-classes-2.scala index 7290ed4a12ea..988f25a05eaa 100644 --- a/tests/pos-custom-args/captures/nested-classes-2.scala +++ b/tests/neg-custom-args/captures/nested-classes-2.scala @@ -6,5 +6,7 @@ def test2(x1: (() => Unit), x2: (() => Unit) => Unit) = def test3(y1: (() => Unit), y2: (() => Unit) => Unit) = val cc1: C1^{y1, y2} = C1(y1, y2) val cc2 = cc1.c2(x1, x2) - val cc3: cc1.C2^{cc1, x1, x2} = cc2 + val cc3: cc1.C2^{cc1, x1, x2} = cc2 // error + val cc4: cc1.C2^{cc2} = cc2 // ok + diff --git a/tests/neg-custom-args/captures/outer-var.check b/tests/neg-custom-args/captures/outer-var.check index 36ce2f308d8c..45489ab0ff5b 100644 --- a/tests/neg-custom-args/captures/outer-var.check +++ b/tests/neg-custom-args/captures/outer-var.check @@ -6,10 +6,9 @@ | | Note that capability cap is not included in capture set {p, q²}. | - | where: => refers to a fresh root capability in the type of parameter q - | cap is a fresh root capability in the type of parameter q - | q is a parameter in method inner - | q² is a parameter in method test + | where: => and cap refer to a fresh root capability in the type of parameter q + | q is a parameter in method inner + | q² is a parameter in method test | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/outer-var.scala:13:9 ------------------------------------- @@ -20,8 +19,7 @@ | | Note that capability cap is not included in capture set {p, q}. | - | where: => refers to a fresh root capability created in method inner - | cap is a fresh root capability created in method inner + | where: => and cap refer to a fresh root capability created in method inner | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/outer-var.scala:14:9 ------------------------------------- @@ -32,8 +30,7 @@ | | Note that capability cap cannot be included in capture set {p} of variable y. | - | where: => refers to a fresh root capability created in method inner - | cap is a fresh root capability created in method inner + | where: => and cap refer to a fresh root capability created in method inner | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/outer-var.scala:15:8 ------------------------------------- @@ -44,8 +41,7 @@ | | Note that capability cap cannot be included in capture set {p} of variable y. | - | where: => refers to a fresh root capability in the type of parameter q - | cap is a fresh root capability in the type of parameter q + | where: => and cap refer to a fresh root capability in the type of parameter q | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/outer-var.scala:17:57 --------------------------------------------------------- diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check index 70896596593e..e20a318064bb 100644 --- a/tests/neg-custom-args/captures/reaches.check +++ b/tests/neg-custom-args/captures/reaches.check @@ -43,10 +43,8 @@ | Note that capability cap is not included in capture set {cap²} | because cap is not visible from cap² in value next. | - | where: => refers to the universal root capability - | =>² refers to a fresh root capability in the type of value next - | cap is the universal root capability - | cap² is a fresh root capability in the type of value next + | where: => and cap refer to the universal root capability + | =>² and cap² refer to a fresh root capability in the type of value next | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:46:20 -------------------------------------- @@ -58,10 +56,8 @@ | Note that capability cap is not included in capture set {cap²} | because cap is not visible from cap² in method runAll3. | - | where: => refers to the universal root capability - | =>² refers to a fresh root capability created in method runAll3 - | cap is the universal root capability - | cap² is a fresh root capability created in method runAll3 + | where: => and cap refer to the universal root capability + | =>² and cap² refer to a fresh root capability created in method runAll3 | | longer explanation available when compiling with `-explain` -- Error: tests/neg-custom-args/captures/reaches.scala:52:51 ----------------------------------------------------------- @@ -74,39 +70,33 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:57:27 -------------------------------------- 57 | val id: File^ -> File^ = x => x // error | ^^^^^^ - | Found: (x: File^) ->'s5 File^² - | Required: File^ -> File^³ + | Found: (x: File^) ->'s5 File^² + | Required: File^ -> File^³ | - | Note that capability cap is not included in capture set {cap²} - | because cap is not visible from cap² in value id. + | Note that capability cap is not included in capture set {cap²} + | because cap is not visible from cap² in value id. | - | where: ^ refers to the universal root capability - | ^² refers to a root capability associated with the result type of (x: File^): File^² - | ^³ refers to a fresh root capability in the type of value id - | cap is a root capability associated with the result type of (x: File^): File^² - | cap² is a fresh root capability in the type of value id + | where: ^ refers to the universal root capability + | ^² and cap refer to a root capability associated with the result type of (x: File^): File^² + | ^³ and cap² refer to a fresh root capability in the type of value id | | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:67:38 -------------------------------------- -67 | val leaked = usingFile[File^{id*}]: f => // error - | ^ - |Found: (f: File^'s6) ->'s7 File^{id*} - |Required: File^ => File^{id*} +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:68:27 -------------------------------------- +68 | val f1: File^{id*} = id(f) // error + | ^^^^^ + |Found: File^ + |Required: File^{id*} | |Note that capability cap is not included in capture set {id*}. | - |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 - | cap is a fresh root capability created in anonymous function of type (f: File^'s6): File^{id*} of parameter parameter f² of method $anonfun -68 | val f1: File^{id*} = id(f) -69 | f1 + |where: ^ and cap refer to a fresh root capability created in value f1 when instantiating method apply's type (x: File^²): File^³ | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:85:10 -------------------------------------- 85 | ps.map((x, y) => compose1(x, y)) // error | ^^^^^^^^^^^^^^^^^^^^^^^ - |Found: (x$1: (A^ ->'s8 A^'s9, A^ ->'s10 A^'s11)^'s12) ->'s13 A^'s14 ->'s15 A^'s16 - |Required: ((A ->{ps*} A, A ->{ps*} A)) => A^'s17 ->'s18 A^'s19 + |Found: (x$1: (A^ ->'s6 A^'s7, A^ ->'s8 A^'s9)^'s10) ->'s11 A^'s12 ->'s13 A^'s14 + |Required: ((A ->{ps*} A, A ->{ps*} A)) => A^'s15 ->'s16 A^'s17 | |Note that capability ps* cannot be included in capture set {} of value x. | @@ -117,8 +107,8 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:88:10 -------------------------------------- 88 | ps.map((x, y) => compose1(x, y)) // error | ^^^^^^^^^^^^^^^^^^^^^^^ - |Found: (x$1: (A^ ->'s20 A^'s21, A^ ->'s22 A^'s23)^'s24) ->'s25 A^'s26 ->'s27 A^'s28 - |Required: ((A ->{C} A, A ->{C} A)) => A^'s29 ->'s30 A^'s31 + |Found: (x$1: (A^ ->'s18 A^'s19, A^ ->'s20 A^'s21)^'s22) ->'s23 A^'s24 ->'s25 A^'s26 + |Required: ((A ->{C} A, A ->{C} A)) => A^'s27 ->'s28 A^'s29 | |Note that capability C cannot be included in capture set {} of value x. | diff --git a/tests/neg-custom-args/captures/reaches.scala b/tests/neg-custom-args/captures/reaches.scala index daf326f17f98..2c700baccef5 100644 --- a/tests/neg-custom-args/captures/reaches.scala +++ b/tests/neg-custom-args/captures/reaches.scala @@ -64,8 +64,8 @@ def attack2 = def attack3 = val id: (x: File^) -> File^ = x => x // was error, now OK - val leaked = usingFile[File^{id*}]: f => // error - val f1: File^{id*} = id(f) + val leaked = usingFile[File^{id*}]: f => + val f1: File^{id*} = id(f) // error f1 class List[+A]: diff --git a/tests/neg-custom-args/captures/reference-cc.check b/tests/neg-custom-args/captures/reference-cc.check index be30a566d0cc..476cb2a09ceb 100644 --- a/tests/neg-custom-args/captures/reference-cc.check +++ b/tests/neg-custom-args/captures/reference-cc.check @@ -32,7 +32,6 @@ |Note that capability canThrow$1 is not included in capture set {cap} |because (canThrow$1 : CanThrow[LimitExceeded]) in method try$1 is not visible from cap in enclosing function. | - |where: => refers to a fresh root capability created in anonymous function of type (using erased x$1: CanThrow[LimitExceeded]): () => Double when instantiating expected result type () ->{cap²} Double of function literal - | cap is a fresh root capability created in anonymous function of type (using erased x$1: CanThrow[LimitExceeded]): () => Double when instantiating expected result type () ->{cap²} Double of function literal + |where: => and cap refer to a fresh root capability created in anonymous function of type (using erased x$1: CanThrow[LimitExceeded]): () => Double when instantiating expected result type () ->{cap²} Double of function literal | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/ro-mut-conformance.check b/tests/neg-custom-args/captures/ro-mut-conformance.check index 9e8a2f3a5548..0fde84ba4a78 100644 --- a/tests/neg-custom-args/captures/ro-mut-conformance.check +++ b/tests/neg-custom-args/captures/ro-mut-conformance.check @@ -6,15 +6,14 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/ro-mut-conformance.scala:12:21 --------------------------- 12 | val t: Ref^{cap} = a // error | ^ - | Found: (a : Ref) - | Required: Ref^ + | Found: (a : Ref) + | Required: Ref^ | - | Note that capability a is not included in capture set {}. + | Note that capability a is not included in capture set {}. | - | 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 {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).. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of value t - | cap is a fresh root capability classified as Mutable in the type of value t + | where: ^ and cap refer to a fresh root capability classified as Mutable in the type of value t | | 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 0d79f4f66fbc..2e4190168681 100644 --- a/tests/neg-custom-args/captures/scope-extrude-mut.check +++ b/tests/neg-custom-args/captures/scope-extrude-mut.check @@ -7,9 +7,7 @@ | Note that capability cap is not included in capture set {cap²} | because cap in method b is not visible from cap² in variable a. | - | where: ^ refers to a fresh root capability classified as Mutable in the type of value a1 - | ^² refers to a fresh root capability classified as Mutable in the type of variable a - | cap is a fresh root capability classified as Mutable in the type of value a1 - | cap² is a fresh root capability classified as Mutable in the type of variable a + | where: ^ and cap refer to a fresh root capability classified as Mutable in the type of value a1 + | ^² and cap² refer to a fresh root capability classified as Mutable in the type of 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 141e8ac4a9c6..4c738997c213 100644 --- a/tests/neg-custom-args/captures/scoped-caps.check +++ b/tests/neg-custom-args/captures/scoped-caps.check @@ -1,112 +1,93 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:7:20 ----------------------------------- 7 | val g: A^ -> B^ = f // error | ^ - | Found: (f : (x: A^) -> B^²) - | Required: A^ -> B^³ + | Found: (f : (x: A^) -> B^²) + | Required: A^ -> B^³ | - | Note that capability cap is not included in capture set {cap²} - | because cap is not visible from cap² in value g. + | Note that capability cap is not included in capture set {cap²} + | because cap is not visible from cap² in value g. | - | where: ^ refers to the universal root capability - | ^² 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 - | cap is a root capability associated with the result type of (x: A^): B^² - | cap² is a fresh root capability in the type of value g + | where: ^ and cap refer to the universal root capability + | ^² refers to a root capability associated with the result type of (x: A^): B^² + | ^³ and cap² refer to a fresh root capability in the type of 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 | ^ - | Found: A^ -> B^{g*} - | Required: (x: A^) -> B^² + | Found: A^ -> B^{g*} + | Required: (x: A^) -> B^² | - | Note that capability g* is not included in capture set {cap}. + | Note that capability g* is not included in capture set {cap}. | - | Note that the existential capture root in B^ - | cannot subsume the capability g* since that capability is not a `Sharable` capability.. - | - | where: ^ refers to the universal root capability - | ^² refers to a root capability associated with the result type of (x: A^): B^² - | cap is a root capability associated with the result type of (x: A^): B^² + | where: ^ and cap refer to the universal root capability + | ^² refers to a root capability associated with the result type of (x: A^): B^² | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:10:20 ---------------------------------- 10 | val _: A^ -> B^ = f // error | ^ - | Found: (f : (x: A^) -> B^²) - | Required: A^ -> B^³ + | Found: (f : (x: A^) -> B^²) + | Required: A^ -> B^³ | - | Note that capability cap is not included in capture set {cap²} - | because cap is not visible from cap² in value _$3. + | Note that capability cap is not included in capture set {cap²} + | because cap is not visible from cap² in value _$3. | - | where: ^ refers to the universal root capability - | ^² 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 - | cap is a root capability associated with the result type of (x: A^): B^² - | cap² is a fresh root capability in the type of value _$3 + | where: ^ and cap refer to the universal root capability + | ^² refers to a root capability associated with the result type of (x: A^): B^² + | ^³ and cap² refer to a fresh root capability in the type of 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^) ->'s1 B^² - | Required: A^ -> B^³ + | Found: (x: A^) ->'s1 B^² + | Required: A^ -> B^³ | - | Note that capability cap is not included in capture set {cap²} - | because cap is not visible from cap² in value _$5. + | Note that capability cap is not included in capture set {cap²} + | because cap is not visible from cap² in value _$5. | - | where: ^ refers to the universal root capability - | ^² 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 _$5 - | cap is a root capability associated with the result type of (x: A^): B^² - | cap² is a fresh root capability in the type of value _$5 + | where: ^ refers to the universal root capability + | ^² and cap refer to a root capability associated with the result type of (x: A^): B^² + | ^³ and cap² refer to a fresh root capability in the type of value _$5 | | 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^ -> B^{h*} - | Required: (x: S^) -> B^² - | - | Note that capability h* is not included in capture set {cap}. + | Found: S^ -> B^{h*} + | Required: (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 {cap}. | - | where: ^ refers to the universal root capability - | ^² refers to a root capability associated with the result type of (x: S^): B^² - | cap is a root capability associated with the result type of (x: S^): B^² + | where: ^ and cap refer to the universal root capability + | ^² refers to a root capability associated with the result type of (x: S^): B^² | | 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^² -> B^³ + | Found: (j : (x: S) -> B^) + | Required: S^² -> B^³ | - | Note that capability cap is not included in capture set {cap²} - | because cap is not visible from cap² in value _$13. + | Note that capability cap is not included in capture set {cap²} + | because cap is not visible from cap² in value _$13. | - | 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 _$13 - | cap is a root capability associated with the result type of (x: S^²): B^ - | cap² is a fresh root capability in the type of value _$13 + | where: ^ refers to a root capability associated with the result type of (x: S^²): B^ + | ^² and cap refer to the universal root capability + | ^³ and cap² refer to a fresh root capability in the type of value _$13 | | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:27:19 ---------------------------------- +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:27:25 ---------------------------------- 27 | val _: S -> B^ = x => j(x) // error - | ^^^^^^^^^ - | Found: (x: S^) ->'s2 B^² - | Required: S^ -> B^³ + | ^^^^ + |Found: B^ + |Required: B^² | - | Note that capability cap is not included in capture set {cap²} - | because cap is not visible from cap² in value _$14. + |Note that capability cap is not included in capture set {cap²} + |because cap in enclosing function is not visible from cap² in value _$14. | - | where: ^ refers to the universal root capability - | ^² refers to a root capability associated with the result type of (x: S^): B^² - | ^³ refers to a fresh root capability in the type of value _$14 - | cap is a root capability associated with the result type of (x: S^): B^² - | cap² is a fresh root capability in the type of value _$14 + |where: ^ and cap refer to a fresh root capability created in anonymous function of type (x: S): B^³ when instantiating method apply's type (x: S^³): B^⁴ + | ^² and cap² refer to a fresh root capability in the type of value _$14 | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/scoped-caps2.check b/tests/neg-custom-args/captures/scoped-caps2.check index ad4acc726fc4..21867171cb6b 100644 --- a/tests/neg-custom-args/captures/scoped-caps2.check +++ b/tests/neg-custom-args/captures/scoped-caps2.check @@ -1,81 +1,69 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps2.scala:5:23 ---------------------------------- 5 | val _: (x: C) => C = b // error | ^ - | Found: (b : C => C) - | Required: (x: C^) =>² C^² + | Found: (b : C => C) + | Required: (x: C^) =>² C^² | - | Note that the existential capture root in C^ - | cannot subsume the capability cap.. + | Note that capability cap is not included in capture set {cap²}. | - | Note that capability cap² is not included in capture set {cap³}. - | - | where: => refers to a fresh root capability in the type of value b - | =>² refers to a fresh root capability in the type of value _$1 - | ^ refers to the universal root capability - | ^² refers to a root capability associated with the result type of (x: C^): C^² - | cap is a fresh root capability classified as SharedCapability in the type of value b - | cap² is a fresh root capability in the type of value b - | cap³ is a fresh root capability in the type of value _$1 + | where: => and cap refer to a fresh root capability in the type of value b + | =>² and cap² refer to a fresh root capability in the type of value _$1 + | ^ refers to the universal root capability + | ^² refers to a root capability associated with the result type of (x: C^): C^² | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps2.scala:6:18 ---------------------------------- 6 | val _: C => C = a // error | ^ - | Found: (a : (x: C) => C) - | Required: C^ =>² C^² + | Found: (a : (x: C) => C) + | Required: C^ =>² C^² | - | Note that capability cap is not included in capture set {cap²}. + | Note that capability cap is not included in capture set {cap²}. | - | where: => refers to a fresh root capability in the type of value a - | =>² refers to a fresh root capability in the type of value _$2 - | ^ refers to the universal root capability - | ^² refers to a fresh root capability classified as SharedCapability in the type of value _$2 - | cap is a fresh root capability in the type of value a - | cap² is a fresh root capability in the type of value _$2 + | where: => and cap refer to a fresh root capability in the type of value a + | =>² and cap² refer to a fresh root capability in the type of value _$2 + | ^ refers to the universal root capability + | ^² refers to a fresh root capability classified as SharedCapability in the type of value _$2 | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps2.scala:8:18 ---------------------------------- 8 | val _: C => C = (x: C) => a(x) // error | ^^^^^^^^^^^^^^ - | Found: (x: C^) ->{a} C^² - | Required: C^ => C^³ + | Found: (x: C^) ->{a} C^² + | Required: C^ => C^³ | - | Note that capability cap is not included in capture set {cap²} - | because cap is not visible from cap² in value _$4. + | Note that capability cap is not included in capture set {cap²} + | because cap is not visible from cap² in value _$4. | - | where: => refers to a fresh root capability in the type of value _$4 - | ^ refers to the universal root capability - | ^² refers to a root capability associated with the result type of (x: C^): C^² - | ^³ refers to a fresh root capability classified as SharedCapability in the type of value _$4 - | cap is a root capability associated with the result type of (x: C^): C^² - | cap² is a fresh root capability classified as SharedCapability in the type of value _$4 + | where: => refers to a fresh root capability in the type of value _$4 + | ^ refers to the universal root capability + | ^² and cap refer to a root capability associated with the result type of (x: C^): C^² + | ^³ and cap² refer to a fresh root capability classified as SharedCapability in the type of value _$4 | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps2.scala:14:18 --------------------------------- 14 | val _: C -> C = a // error | ^ - | Found: (a : (x: C) -> C) - | Required: C^ -> C^² + | Found: (a : (x: C) -> C) + | Required: C^ -> C^² | - | Note that capability cap is not included in capture set {cap²} - | because cap is not visible from cap² in value _$6. + | Note that capability cap is not included in capture set {cap²} + | because cap is not visible from cap² in value _$6. | - | where: ^ refers to the universal root capability - | ^² refers to a fresh root capability classified as SharedCapability in the type of value _$6 - | cap is a root capability associated with the result type of (x: C^): C^³ - | cap² is a fresh root capability classified as SharedCapability in the type of value _$6 + | where: ^ and cap refer to the universal root capability + | ^² and cap² refer to a fresh root capability classified as SharedCapability in the type of value _$6 | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps2.scala:16:29 --------------------------------- 16 | val _: C -> C = (x: C) => a(x) // error | ^^^^ - | Found: C^{x} - | Required: C^ + |Found: C^ + |Required: C^² | - | Note that capability x is not included in capture set {cap} - | because (x : C) in enclosing function is not visible from cap in value _$8. + |Note that capability cap is not included in capture set {cap²} + |because cap in enclosing function is not visible from cap² in value _$8. | - | where: ^ refers to a fresh root capability classified as SharedCapability in the type of value _$8 - | cap is a fresh root capability classified as SharedCapability in the type of value _$8 + |where: ^ and cap refer to a fresh root capability classified as SharedCapability created in anonymous function of type (x: C): C when instantiating method apply's type (x: C^³): C^⁴ + | ^² and cap² refer to a fresh root capability classified as SharedCapability in the type of value _$8 | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/sep-curried-par.check b/tests/neg-custom-args/captures/sep-curried-par.check new file mode 100644 index 000000000000..04c052f9c7cc --- /dev/null +++ b/tests/neg-custom-args/captures/sep-curried-par.check @@ -0,0 +1,59 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/sep-curried-par.scala:23:32 ------------------------------ +23 | val bar = (p1: () => Unit) => (p2: () ->{p1, cap} Unit) => par(p1, p2) // error, but error message could be better + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | Found: (p2: () ->{p1, cap} Unit) ->{p1} Unit + | Required: (() ->'s1 Unit) ->'s2 Unit + | + | Note that capability p1, defined in method $anonfun + | cannot be included in outer capture set 's2. + | + | where: cap is the universal root capability + | + | longer explanation available when compiling with `-explain` +-- Error: tests/neg-custom-args/captures/sep-curried-par.scala:6:48 ---------------------------------------------------- +6 |def parCurriedBad(p1: () => Unit): (() => Unit) => Unit = // error: consume failure + | ^^^^^^^^^^^^^^^^^^^^ + | Separation failure: method parCurriedBad's result type (() => Unit) => Unit hides parameter p1. + | The parameter needs to be annotated with consume to allow this. +-- Error: tests/neg-custom-args/captures/sep-curried-par.scala:15:6 ---------------------------------------------------- +15 | par(p, p) // error: separation + | ^ + |Separation failure: argument of type (p : () => Unit) + |to method par: (p1: () => Unit, p2: () => Unit): Unit + |corresponds to capture-polymorphic formal parameter p1 of type () =>² Unit + |and hides capabilities {p}. + |Some of these overlap with the captures of the second argument with type (p : () => Unit). + | + | Hidden set of current argument : {p} + | Hidden footprint of current argument : {p} + | Capture set of second argument : {p} + | Footprint set of second argument : {p} + | The two sets overlap at : {p} + | + |where: => refers to a fresh root capability in the type of value p + | =>² refers to a fresh root capability created in method test when checking argument to parameter p1 of method par +-- Error: tests/neg-custom-args/captures/sep-curried-par.scala:18:16 --------------------------------------------------- +18 | parCurried(p)(p) // error: consume failure + | ^ + | Separation failure: Illegal access to (p : () => Unit), which was passed to a + | consume parameter or was used as a prefix to a consume method on line 18 + | and therefore is no longer available. + | + | where: => refers to a fresh root capability in the type of value p +-- Error: tests/neg-custom-args/captures/sep-curried-par.scala:21:9 ---------------------------------------------------- +21 | foo(c)(c) // error: separation + | ^ + |Separation failure: argument of type (c : () => Unit) + |to a function of type (() => Unit) ->{c} Unit + |corresponds to capture-polymorphic formal parameter v1 of type () =>² Unit + |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 : {c} + | Footprint set of function prefix : {c} + | The two sets overlap at : {c} + | + |where: => refers to a fresh root capability in the type of parameter c + | =>² refers to a fresh root capability created in method test when checking argument to parameter v1 of method apply diff --git a/tests/neg-custom-args/captures/sep-curried-par.scala b/tests/neg-custom-args/captures/sep-curried-par.scala new file mode 100644 index 000000000000..a1f4e54ac1a0 --- /dev/null +++ b/tests/neg-custom-args/captures/sep-curried-par.scala @@ -0,0 +1,29 @@ +import caps.cap + +def par(p1: () => Unit, p2: () => Unit) = () +def seq(p1: () => Unit, p2: () ->{cap, p1} Unit) = () + +def parCurriedBad(p1: () => Unit): (() => Unit) => Unit = // error: consume failure + (p2: () => Unit) => par(p1, p2) +def parCurried(consume p1: () => Unit): (() => Unit) => Unit = + (p2: () => Unit) => par(p1, p2) + +type Proc = () => Unit + +def test(c: () => Unit) = + val p: Proc = ??? + par(p, p) // error: separation + seq(p, p) + parCurriedBad(p)(p) // ok, but parCurriedBad ill-typed + parCurried(p)(p) // error: consume failure + + val foo = (p1: () => Unit) => (p2: () ->{c, cap} Unit) => par(p1, p2) + foo(c)(c) // error: separation + + val bar = (p1: () => Unit) => (p2: () ->{p1, cap} Unit) => par(p1, p2) // error, but error message could be better + bar(c)(c) + + + + + diff --git a/tests/neg-custom-args/captures/sep-curried.check b/tests/neg-custom-args/captures/sep-curried.check index ea892881a3b6..a2b576de8c3a 100644 --- a/tests/neg-custom-args/captures/sep-curried.check +++ b/tests/neg-custom-args/captures/sep-curried.check @@ -6,8 +6,7 @@ | | Note that capability a is not included in capture set {cap}. | - | where: ^ refers to the universal root capability - | cap is the universal root capability + | where: ^ and cap refer to the universal root capability | | 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-pairs-unboxed.check b/tests/neg-custom-args/captures/sep-pairs-unboxed.check new file mode 100644 index 000000000000..5baf11b03ec4 --- /dev/null +++ b/tests/neg-custom-args/captures/sep-pairs-unboxed.check @@ -0,0 +1,84 @@ +-- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:11:27 ------------------------------------------------- +11 |def mkPair(x: Ref^) = Pair(x, x) // error: separation failure + | ^ + |Separation failure: argument of type (x : Ref^) + |to constructor Pair: (fst: Ref^, snd: Ref^): Pair + |corresponds to capture-polymorphic formal parameter fst of type Ref^² + |and hides capabilities {x}. + |Some of these overlap with the captures of the second argument with type (x : Ref^). + | + | Hidden set of current argument : {x} + | Hidden footprint of current argument : {x} + | Capture set of second argument : {x} + | Footprint set of second argument : {x} + | The two sets overlap at : {x} + | + |where: ^ refers to a fresh root capability classified as Mutable in the type of parameter x + | ^² refers to a fresh root capability classified as Mutable created in method mkPair when checking argument to parameter fst of constructor Pair +-- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:35:25 ------------------------------------------------- +35 | val twoCopy = Pair(two.fst, two.fst) // error + | ^^^^^^^ + |Separation failure: argument of type (two.fst : Ref^) + |to constructor Pair: (fst: Ref^, snd: Ref^): Pair + |corresponds to capture-polymorphic formal parameter fst of type Ref^² + |and hides capabilities {two.fst}. + |Some of these overlap with the captures of the second argument with type (two.fst : Ref^). + | + | Hidden set of current argument : {two.fst} + | Hidden footprint of current argument : {two.fst} + | Capture set of second argument : {two.fst} + | Footprint set of second argument : {two.fst} + | The two sets overlap at : {two.fst} + | + |where: ^ refers to a fresh root capability classified as Mutable in the type of value fst + | ^² refers to a fresh root capability classified as Mutable created in value twoCopy when checking argument to parameter fst of constructor Pair +-- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:41:29 ------------------------------------------------- +41 | val twisted = PairPair(two.fst, two) // error + | ^^^^^^^ + |Separation failure: argument of type (two.fst : Ref^) + |to constructor PairPair: (fst: Ref^, snd: Pair^): PairPair + |corresponds to capture-polymorphic formal parameter fst of type Ref^² + |and hides capabilities {two.fst}. + |Some of these overlap with the captures of the second argument with type (two : Pair{val fst: Ref^; val snd: Ref^}^). + | + | Hidden set of current argument : {two.fst} + | Hidden footprint of current argument : {two.fst} + | Capture set of second argument : {two*} + | Footprint set of second argument : {two*} + | The two sets overlap at : {cap of a new instance of class Pair} + | + |where: ^ refers to a fresh root capability classified as Mutable in the type of value fst + | ^² refers to a fresh root capability classified as Mutable created in value twisted when checking argument to parameter fst of constructor PairPair +-- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:47:33 ------------------------------------------------- +47 | val twisted = swapped(two, two.snd) // error + | ^^^^^^^ + |Separation failure: argument of type (two.snd : Ref^) + |to method swapped: (@consume x: Pair^, @consume y: Ref^): PairPair^ + |corresponds to capture-polymorphic formal parameter y of type Ref^² + |and hides capabilities {two.snd}. + |Some of these overlap with the captures of the first argument with type (two : Pair{val fst: Ref^; val snd: Ref^}^). + | + | Hidden set of current argument : {two.snd} + | Hidden footprint of current argument : {two.snd} + | Capture set of first argument : {two*} + | Footprint set of first argument : {two*} + | The two sets overlap at : {cap of a new instance of class Pair} + | + |where: ^ refers to a fresh root capability classified as Mutable in the type of value snd + | ^² refers to a fresh root capability classified as Mutable created in value twisted when checking argument to parameter y of method swapped +-- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:58:26 ------------------------------------------------- +58 | val twoOther = Pair(two.fst, two.snd) // error // error + | ^^^^^^^ + | Separation failure: Illegal access to {two.fst} which is hidden by the previous definition + | of value twoCopy with type Pair^. + | This type hides capabilities {two.fst, two.snd} + | + | where: ^ refers to a fresh root capability in the type of value twoCopy +-- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:58:35 ------------------------------------------------- +58 | val twoOther = Pair(two.fst, two.snd) // error // error + | ^^^^^^^ + | Separation failure: Illegal access to {two.snd} which is hidden by the previous definition + | of value twoCopy with type Pair^. + | This type hides capabilities {two.fst, two.snd} + | + | where: ^ refers to a fresh root capability in the type of value twoCopy diff --git a/tests/neg-custom-args/captures/sep-pairs-unboxed.scala b/tests/neg-custom-args/captures/sep-pairs-unboxed.scala new file mode 100644 index 000000000000..22b8bf9e1d19 --- /dev/null +++ b/tests/neg-custom-args/captures/sep-pairs-unboxed.scala @@ -0,0 +1,60 @@ +import caps.Mutable +import caps.cap + +class Ref extends Mutable: + var x = 0 + def get: Int = x + update def put(y: Int): Unit = x = y + +class Pair(val fst: Ref^, val snd: Ref^) + +def mkPair(x: Ref^) = Pair(x, x) // error: separation failure + +def bad: Pair^ = + val r0 = Ref() + val r1 = mkPair(r0) + r1 + +def twoRefs(): Pair^ = + val r1 = Ref() + val r2 = Ref() + Pair(r1, r2) + +def good1(): Unit = + val two = twoRefs() + val fst = two.fst + val snd = two.snd + val twoCopy = Pair(fst, snd) // ok + +def good2(): Unit = + val two = twoRefs() + val twoCopy = Pair(two.fst, two.snd) // ok + +def bad2(): Unit = + val two = twoRefs() + val twoCopy = Pair(two.fst, two.fst) // error + +class PairPair(val fst: Ref^, val snd: Pair^) + +def bad3(): Unit = + val two = twoRefs() + val twisted = PairPair(two.fst, two) // error + +def swapped(consume x: Pair^, consume y: Ref^): PairPair^ = PairPair(y, x) + +def bad4(): Unit = + val two = twoRefs() + val twisted = swapped(two, two.snd) // error + +def good3(): Unit = + val two = twoRefs() + val twoCopy = Pair(two.fst, two.snd) + val _: Pair^{two.fst, two.snd} = twoCopy + val twoOther = Pair(two.fst, two.snd) + +def bad5(): Unit = + val two = twoRefs() + val twoCopy: Pair^ = Pair(two.fst, two.snd) + val twoOther = Pair(two.fst, two.snd) // error // error + + diff --git a/tests/neg-custom-args/captures/sep-pairs.check b/tests/neg-custom-args/captures/sep-pairs.check index 69909cf4f648..d51870f3eedf 100644 --- a/tests/neg-custom-args/captures/sep-pairs.check +++ b/tests/neg-custom-args/captures/sep-pairs.check @@ -26,7 +26,7 @@ | Separation failure in value sameToPair's type Pair[Ref^, Ref^²]. | One part, Ref^, hides capabilities {fstSame}. | Another part, Ref^², captures capabilities {sndSame, same.snd*}. - | The two sets overlap at cap of value same. + | The two sets overlap at {cap of value same}. | | where: ^ refers to a fresh root capability classified as Mutable in the type of value sameToPair | ^² refers to a fresh root capability classified as Mutable in the type of value sameToPair diff --git a/tests/neg-custom-args/captures/sep-use2.check b/tests/neg-custom-args/captures/sep-use2.check index 2be46304db34..5aa02461c983 100644 --- a/tests/neg-custom-args/captures/sep-use2.check +++ b/tests/neg-custom-args/captures/sep-use2.check @@ -10,11 +10,6 @@ | This type hides capabilities {c} | | where: ^ refers to a fresh root capability in the result type of method cc --- Error: tests/neg-custom-args/captures/sep-use2.scala:12:10 ---------------------------------------------------------- -12 | val x4: Object^ = // error - | ^^^^^^^ - | Separation failure: value x4's type Object^ hides parameter f. - | The parameter needs to be annotated with consume to allow this. -- Error: tests/neg-custom-args/captures/sep-use2.scala:16:10 ---------------------------------------------------------- 16 | def cc: Object^ = c // error | ^^^^^^^ diff --git a/tests/neg-custom-args/captures/sep-use2.scala b/tests/neg-custom-args/captures/sep-use2.scala index 9ce8a1ade72f..6cc80b899d87 100644 --- a/tests/neg-custom-args/captures/sep-use2.scala +++ b/tests/neg-custom-args/captures/sep-use2.scala @@ -9,7 +9,7 @@ def test1(consume c: Object^, f: (x: Object^) => Object^) = f(cc) // ok val x3: Object^ = f(cc) // ok - val x4: Object^ = // error + val x4: Object^ = { f(c) } // error def test2(consume c: Object^, f: (x: Object^) ->{c} Object^) = diff --git a/tests/neg-custom-args/captures/try.check b/tests/neg-custom-args/captures/try.check index 60029abb8202..aa0137e1a08a 100644 --- a/tests/neg-custom-args/captures/try.check +++ b/tests/neg-custom-args/captures/try.check @@ -14,10 +14,9 @@ |Note that capability x is not included in capture set {cap} |because (x : CT[Exception]^) is not visible from cap in value a. | - |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 - | cap is a fresh root capability created in value a when checking argument to parameter op of method handle + |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 + | ^² and cap refer to a fresh root capability created in value a when checking argument to parameter op of method handle | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:30:4 ------------------------------------------- diff --git a/tests/neg-custom-args/captures/unsound-reach-4.check b/tests/neg-custom-args/captures/unsound-reach-4.check index cddcc58e38b4..441a6c25aec7 100644 --- a/tests/neg-custom-args/captures/unsound-reach-4.check +++ b/tests/neg-custom-args/captures/unsound-reach-4.check @@ -14,9 +14,8 @@ | Note that capability cap is not included in capture set {cap²} | because cap is not visible from cap² in value backdoor. | - | where: ^ refers to a fresh root capability in the type of value backdoor - | cap is the universal root capability - | cap² is a fresh root capability in the type of value backdoor + | where: ^ and cap² refer to a fresh root capability in the type of value backdoor + | cap is the universal root capability | | longer explanation available when compiling with `-explain` -- [E164] Declaration Error: tests/neg-custom-args/captures/unsound-reach-4.scala:17:6 --------------------------------- diff --git a/tests/neg-custom-args/captures/unsound-reach.check b/tests/neg-custom-args/captures/unsound-reach.check index 0313ebe37b88..b06515b42053 100644 --- a/tests/neg-custom-args/captures/unsound-reach.check +++ b/tests/neg-custom-args/captures/unsound-reach.check @@ -15,14 +15,13 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/unsound-reach.scala:18:31 -------------------------------- 18 | val backdoor: Foo[File^] = new Bar // error (follow-on, since the parent Foo[File^] of bar is illegal). | ^^^^^^^ - | Found: Bar - | Required: Foo[File^] + | Found: Bar + | Required: Foo[File^] | - | Note that capability cap is not included in capture set {cap²} - | because cap is not visible from cap² in value backdoor. + | Note that capability cap is not included in capture set {cap²} + | because cap is not visible from cap² in value backdoor. | - | where: ^ refers to a fresh root capability in the type of value backdoor - | cap is the universal root capability - | cap² is a fresh root capability in the type of value backdoor + | where: ^ and cap² refer to a fresh root capability in the type of value backdoor + | cap is the universal root capability | | 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 b4b4cac8fb99..e19f414d0b2e 100644 --- a/tests/neg-custom-args/captures/vars-simple.check +++ b/tests/neg-custom-args/captures/vars-simple.check @@ -6,8 +6,7 @@ | | Note that capability cap is not included in capture set {cap1, cap2}. | - | where: => refers to a fresh root capability created in method scope - | cap is a fresh root capability created in method scope + | where: => and cap refer to a fresh root capability created in method scope | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars-simple.scala:16:8 ----------------------------------- diff --git a/tests/neg-custom-args/captures/widen-reach.check b/tests/neg-custom-args/captures/widen-reach.check index 23f18c88c9f9..48c5989b285b 100644 --- a/tests/neg-custom-args/captures/widen-reach.check +++ b/tests/neg-custom-args/captures/widen-reach.check @@ -8,17 +8,15 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/widen-reach.scala:9:24 ----------------------------------- 9 | val foo: IO^ -> IO^ = x => x // error | ^^^^^^ - | Found: (x: IO^) ->'s1 IO^² - | Required: IO^ -> IO^³ + | Found: (x: IO^) ->'s1 IO^² + | Required: IO^ -> IO^³ | - | Note that capability cap is not included in capture set {cap²} - | because cap is not visible from cap² in value foo. + | Note that capability cap is not included in capture set {cap²} + | because cap is not visible from cap² in value foo. | - | where: ^ refers to the universal root capability - | ^² refers to a root capability associated with the result type of (x: IO^): IO^² - | ^³ refers to a fresh root capability in the type of value foo - | cap is a root capability associated with the result type of (x: IO^): IO^² - | cap² is a fresh root capability in the type of value foo + | where: ^ refers to the universal root capability + | ^² and cap refer to a root capability associated with the result type of (x: IO^): IO^² + | ^³ and cap² refer to a fresh root capability in the type of value foo | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/widen-reach.scala:13:26 ---------------------------------- diff --git a/tests/pos-custom-args/captures/ascribe-apply.scala b/tests/pos-custom-args/captures/ascribe-apply.scala new file mode 100644 index 000000000000..c43a08a06b9d --- /dev/null +++ b/tests/pos-custom-args/captures/ascribe-apply.scala @@ -0,0 +1,5 @@ +def test(): Unit = + val fun = ??? : (() -> Object^) + val l = fun() // Since `fun` is pure we get `l: Object` with the APPLY rule + val _: Object = l + diff --git a/tests/pos-custom-args/captures/caseclass.scala b/tests/pos-custom-args/captures/caseclass.scala index 22b7f1b1eb9a..d735de1a2c78 100644 --- a/tests/pos-custom-args/captures/caseclass.scala +++ b/tests/pos-custom-args/captures/caseclass.scala @@ -7,7 +7,7 @@ object test1: val x1 = Ref(STR("hello")) val y = x1 match case Ref(z) => z - val yc: STR = y + val yc: STR^ = y object test2: case class Ref(x: () => Unit) @@ -32,4 +32,4 @@ object test2: val y4 = y3 match case Ref(xx) => xx - val y4c: () ->{y3} Unit = y4 + val y4c: () => Unit = y4 diff --git a/tests/neg-custom-args/captures/cc-poly-varargs.scala b/tests/pos-custom-args/captures/cc-poly-varargs-original.scala similarity index 73% rename from tests/neg-custom-args/captures/cc-poly-varargs.scala rename to tests/pos-custom-args/captures/cc-poly-varargs-original.scala index 6907bc7f91fa..9b2bba06e2d1 100644 --- a/tests/neg-custom-args/captures/cc-poly-varargs.scala +++ b/tests/pos-custom-args/captures/cc-poly-varargs-original.scala @@ -8,6 +8,6 @@ def race[T, Cap^](sources: Source[T, {Cap}]^{Cap}*): Source[T, {Cap}]^{Cap} = ?? def either[T1, T2, Cap^]( src1: Source[T1, {Cap}]^{Cap}, src2: Source[T2, {Cap}]^{Cap}): Source[Either[T1, T2], {Cap}]^{Cap} = - val left = src1.transformValuesWith(Left(_)) // error - val right = src2.transformValuesWith(Right(_)) // error + val left = src1.transformValuesWith(Left(_)) // was error, now OK + val right = src2.transformValuesWith(Right(_)) // was error, now OK race(left, right) diff --git a/tests/pos-custom-args/captures/cc-poly-varargs.scala b/tests/pos-custom-args/captures/cc-poly-varargs.scala new file mode 100644 index 000000000000..b6c270d35cc7 --- /dev/null +++ b/tests/pos-custom-args/captures/cc-poly-varargs.scala @@ -0,0 +1,15 @@ +import language.experimental.captureChecking +import language.experimental.separationChecking +abstract class Source[+T] + +extension[T](src: Source[T]^) + def transformValuesWith[U](f: (T -> U)^{src, caps.cap}): Source[U]^{src, f} = ??? + +def race[T, D^](sources: Source[T]^{D}*): Source[T]^{D} = ??? + +def either[T1, T2]( + src1: Source[T1]^, + src2: Source[T2]^): Source[Either[T1, T2]]^{src1, src2} = + val left = src1.transformValuesWith(Left(_)) // ok + val right = src2.transformValuesWith(Right(_)) // ok + race(left, right) \ No newline at end of file diff --git a/tests/pos-custom-args/captures/i21507.scala b/tests/pos-custom-args/captures/i21507.scala index 455aa3940fb6..953c8a0b0dca 100644 --- a/tests/pos-custom-args/captures/i21507.scala +++ b/tests/pos-custom-args/captures/i21507.scala @@ -4,7 +4,8 @@ trait Box[Cap^]: def store(f: (() -> Unit)^{Cap}): Unit def run[Cap^](f: Box[{Cap}]^{Cap} => Unit): Box[{Cap}]^{Cap} = - new Box[{Cap}]: + new Box[{Cap}] { private var item: () ->{Cap} Unit = () => () def store(f: () ->{Cap} Unit): Unit = item = f // was error, now ok + } diff --git a/tests/pos-macros/i22584/Main.scala b/tests/pos-macros/i22584/Main.scala index 4b6442078f96..0de80bbf4e07 100644 --- a/tests/pos-macros/i22584/Main.scala +++ b/tests/pos-macros/i22584/Main.scala @@ -1,4 +1,4 @@ -import Types.* +import types.* @main def main() = Macros.myMacro[MyClass1] diff --git a/tests/pos-macros/i22584/Types.scala b/tests/pos-macros/i22584/Types.scala index 01560035ca60..a8c29430ad82 100644 --- a/tests/pos-macros/i22584/Types.scala +++ b/tests/pos-macros/i22584/Types.scala @@ -1,4 +1,4 @@ -object Types { +object types { final case class MyClass1( int: Int, string: String, diff --git a/tests/pos/inline-null-wrapper.scala b/tests/pos/inline-null-wrapper.scala new file mode 100644 index 000000000000..3b53974ea4b9 --- /dev/null +++ b/tests/pos/inline-null-wrapper.scala @@ -0,0 +1,17 @@ +//> using options -Yexplicit-nulls +import annotation.targetName + +class A +class B(x: A) + +object Test: + def convert(x: A): B = B(x) + @targetName("inlineConvert") + inline def convert(x: A | Null): B | Null = + if x == null then null else convert(x) + + val x = convert(A()) + val an: A | Null = A() + val y = convert(null) + val z = convert(an) + diff --git a/tests/run/curried-using-threading.scala b/tests/run/curried-using-threading.scala new file mode 100644 index 000000000000..329e4698fe39 --- /dev/null +++ b/tests/run/curried-using-threading.scala @@ -0,0 +1,10 @@ +case class Context(str: String) + +def root(using Context): String = summon[Context].str + +def narrow(using Context)(owner: String = root) = owner + +given Context("alpha") + +@main def Test = assert(narrow() == "alpha") +