Skip to content

Commit

Permalink
Fix #21868, #21869, and #21870: handle CapsOf in more places (#21875)
Browse files Browse the repository at this point in the history
Fix #21868, #21869, and #21870
  • Loading branch information
bracevac authored Nov 21, 2024
2 parents 2be2a60 + a163f0c commit 5d1d274
Show file tree
Hide file tree
Showing 8 changed files with 70 additions and 4 deletions.
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)
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^
def boom(): Unit^{C^}

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

0 comments on commit 5d1d274

Please sign in to comment.