Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix #21868, #21869, and #21870: handle CapsOf in more places #21875

Merged
merged 5 commits into from
Nov 21, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
Original file line number Diff line number Diff line change
Expand Up @@ -198,7 +198,7 @@ extension (tp: Type)
|| tp.isRootCapability
) && !tp.symbol.isOneOf(UnstableValueFlags)
case tp: TypeRef =>
tp.symbol.isAbstractOrParamType && tp.derivesFrom(defn.Caps_CapSet)
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@odersky Do you remember why we require the arguments of CapsOf to be abstract before? I think any type derived from CapSet should work.

tp.symbol.isType && tp.derivesFrom(defn.Caps_CapSet)
case tp: TypeParamRef =>
tp.derivesFrom(defn.Caps_CapSet)
case AnnotatedType(parent, annot) =>
Expand Down
2 changes: 2 additions & 0 deletions compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
Original file line number Diff line number Diff line change
Expand Up @@ -140,6 +140,8 @@ trait CaptureRef extends TypeProxy, ValueType:
case ReachCapability(x1) => x1.subsumes(y.stripReach)
case x: TermRef => viaInfo(x.info)(subsumingRefs(_, y))
case x: TermParamRef => subsumesExistentially(x, y)
case x: TypeRef if x.symbol.info.derivesFrom(defn.Caps_CapSet) =>
x.captureSetOfInfo.elems.exists(_.subsumes(y))
case x: TypeRef => assumedContainsOf(x).contains(y)
case _ => false
end subsumes
Expand Down
2 changes: 1 addition & 1 deletion compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
Original file line number Diff line number Diff line change
Expand Up @@ -135,7 +135,7 @@ object CheckCaptures:
elem match
case CapsOfApply(arg) =>
def isLegalCapsOfArg =
arg.symbol.isAbstractOrParamType && arg.symbol.info.derivesFrom(defn.Caps_CapSet)
arg.symbol.isType && arg.symbol.info.derivesFrom(defn.Caps_CapSet)
if !isLegalCapsOfArg then
report.error(
em"""$arg is not a legal prefix for `^` here,
Expand Down
7 changes: 6 additions & 1 deletion compiler/src/dotty/tools/dotc/cc/Setup.scala
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ import reporting.Message
import printing.{Printer, Texts}, Texts.{Text, Str}
import collection.mutable
import CCState.*
import dotty.tools.dotc.util.NoSourcePosition

/** Operations accessed from CheckCaptures */
trait SetupAPI:
Expand Down Expand Up @@ -323,7 +324,11 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
val parent2 = stripImpliedCaptureSet(parent1)
for tpt <- tptToCheck do
checkWellformedLater(parent2, ann.tree, tpt)
CapturingType(parent2, ann.tree.toCaptureSet)
try
CapturingType(parent2, ann.tree.toCaptureSet)
catch case ex: IllegalCaptureRef =>
report.error(em"Illegal capture reference: ${ex.getMessage.nn}", tptToCheck.fold(NoSourcePosition)(_.srcPos))
parent2
else
t.derivedAnnotatedType(parent1, ann)
case throwsAlias(res, exc) =>
Expand Down
4 changes: 3 additions & 1 deletion compiler/src/dotty/tools/dotc/core/Types.scala
Original file line number Diff line number Diff line change
Expand Up @@ -4007,7 +4007,7 @@ object Types extends TypeUtils {
(compute(status, parent, theAcc) /: refs.elems) {
(s, ref) => ref.stripReach match
case tp: TermParamRef if tp.binder eq thisLambdaType => combine(s, CaptureDeps)
case _ => s
case tp => combine(s, compute(status, tp, theAcc))
}
case _ =>
if tp.annot.refersToParamOf(thisLambdaType) then TrueDeps
Expand Down Expand Up @@ -6078,6 +6078,8 @@ object Types extends TypeUtils {
case tp: CaptureRef =>
if tp.isTrackableRef then tp
else ensureTrackable(tp.underlying)
case tp: TypeAlias =>
ensureTrackable(tp.alias)
case _ =>
assert(false, i"not a trackable captureRef ref: $result, ${result.underlyingIterator.toList}")
ensureTrackable(result)
Expand Down
18 changes: 18 additions & 0 deletions tests/neg-custom-args/captures/capset-bound.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
import caps.*

class IO

case class File(io: IO^)

def test(io1: IO^, io2: IO^) =
def f[C >: CapSet^{io1} <: CapSet^](file: File^{C^}) = ???
val f1: File^{io1} = ???
val f2: File^{io2} = ???
val f3: File^{io1, io2} = ???
f[CapSet^{io1}](f1)
f[CapSet^{io1}](f2) // error
f[CapSet^{io1}](f3) // error
f[CapSet^{io2}](f2) // error
f[CapSet^{io1, io2}](f1)
f[CapSet^{io1, io2}](f2)
f[CapSet^{io1, io2}](f3)
25 changes: 25 additions & 0 deletions tests/neg-custom-args/captures/capture-poly.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
import caps.*

trait Foo extends Capability

trait CaptureSet:
type C <: CapSet^

def capturePoly[C^](a: Foo^{C^}): Foo^{C^} = a
def capturePoly2(c: CaptureSet)(a: Foo^{c.C^}): Foo^{c.C^} = a

def test =
val x: Foo^ = ???
val y: Foo^ = ???

object X extends CaptureSet:
type C = CapSet^{x}

val z1: Foo^{X.C^} = x
val z2: Foo^{X.C^} = y // error

val z3: Foo^{x} = capturePoly(x)
val z4: Foo^{x} = capturePoly(y) // error

val z5: Foo^{x} = capturePoly2(X)(x)
val z6: Foo^{x} = capturePoly2(X)(y) // error
14 changes: 14 additions & 0 deletions tests/neg-custom-args/captures/i21868.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
import caps.*

trait AbstractWrong:
type C <: CapSet
def boom(): Unit^{C^} // error

trait Abstract:
type C <: CapSet^
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Idealy, we'd like to retrict the capture parameter and member bounded by >: CapSet^{} <: CapSet^, which can forbid instantiating to meaningless types, like Nothing.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's certainly cleaner. The question is how far we want to take it for now. A fully general solution would also have to deal with the presence of explicit lower bounds, which could be themselves type variables, etc.

trait Abstract[L >: CapSet^{}]:
    type T >: L <: CapSet^

Maybe let's track this in a separate issue? The point of the current fix is to prevent the uncaught exception and compiler crash.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think this is an issue, as long as L is also bounded by CapSet.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As the below examples show, there's a still a few quirks. I'm also somewhat uneasy with automatically presuming that the lower bound of a CapSet^-bounded type variable is CapSet^{}. E.g., should this always be the case, or only with cc enabled?

Since the specific issues are resolved, let's merge this and have a separate issue to make capture set intervals and subtyping airtight.

def boom(): Unit^{C^}

class Concrete extends Abstract:
type C = Nothing
def boom() = () // error

Loading