Skip to content

Commit

Permalink
Canonicalize capture variable subtype comparisons
Browse files Browse the repository at this point in the history
Fixes #22103

Subtype problems where at least one side is a type variable
representing a capture variable are canonicalized to
capturing type comparisons on the special `CapSet` for the
universe capture sets. For example, `C <: CapSet^{C^}`
becomes `CapSet^{C^} <: CapSet^{C^}`, and `A <: B` becomes
`CapSet^{A^} <: CapSet^{B^}` if both `A` and `B` are capture
variables.
  • Loading branch information
bracevac committed Jan 1, 2025
1 parent 1f0c576 commit 079d4f5
Show file tree
Hide file tree
Showing 3 changed files with 88 additions and 6 deletions.
41 changes: 40 additions & 1 deletion compiler/src/dotty/tools/dotc/core/TypeComparer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -298,6 +298,43 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
}
}

//TODO move the following functions somewhere more appropriate
/**
* Is the type `tp` a `CapSet` type, i.e., a capture variable?
*
* @param tp The type to check
* @param includeCapSet Whether to include the bare `CapSet` type itself in the check, false at the top level
*/
def isCapSet(tp: Type, includeCapSet: Boolean = false): Boolean = tp match {
case tp: TypeRef => (includeCapSet && (tp.symbol eq defn.Caps_CapSet)) || {
tp.underlying match
case TypeBounds(lo, hi) => isCapSet(lo, true) && isCapSet(hi, true)
case TypeAlias(alias) => isCapSet(alias) // TODO: test cases involving type aliases
case _ => false
}
case tp: SingletonType => isCapSet(tp.underlying)
case CapturingType(parent, _) => isCapSet(parent, true)
case _ => false
}

/**
* Assumes that isCapSet(tp) is true.
*/
def canonicalizeToCapSet(tp: Type): Type = tp match
case ct @ CapturingType(_,_) => ct
case tp: TypeRef if tp.symbol eq defn.Caps_CapSet => CapturingType(tp, CaptureSet.empty)
case tp: SingletonType => canonicalizeToCapSet(tp.underlying)
case tp: CaptureRef => CapturingType(defn.Caps_CapSet.typeRef, CaptureSet(tp))


/** In capture checking, implements the logic to compare type variables which represent
* capture variables.
*
* Note: should only be called in a context where tp1 or tp2 is a type variable representing a capture variable.
*/
def tryHandleCaptureVars: Boolean =
isCaptureCheckingOrSetup && isCapSet(tp1) && isCapSet(tp2) && recur(canonicalizeToCapSet(tp1), canonicalizeToCapSet(tp2)) // TODO: we could probably just call subcapturing right away here and terminate early

def firstTry: Boolean = tp2 match {
case tp2: NamedType =>
def compareNamed(tp1: Type, tp2: NamedType): Boolean =
Expand Down Expand Up @@ -346,6 +383,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
&& isSubPrefix(tp1.prefix, tp2.prefix)
&& tp1.signature == tp2.signature
&& !(sym1.isClass && sym2.isClass) // class types don't subtype each other
|| tryHandleCaptureVars
|| thirdTryNamed(tp2)
case _ =>
secondTry
Expand Down Expand Up @@ -858,9 +896,10 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
}
compareTypeBounds
case CapturingType(parent2, refs2) =>
def compareCapturing =
def compareCapturing: Boolean =
val refs1 = tp1.captureSet
try
if tp1.isInstanceOf[TypeRef] && tryHandleCaptureVars then return true
if refs1.isAlwaysEmpty then recur(tp1, parent2)
else
// The singletonOK branch is because we sometimes have a larger capture set in a singleton
Expand Down
47 changes: 47 additions & 0 deletions tests/neg-custom-args/captures/capture-vars-subtyping.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,47 @@
import language.experimental.captureChecking
import caps.*

def test[C^] =
val a: C = ???
val b: CapSet^{C^} = a
val c: C = b
val d: CapSet^{C^, c} = a

// TODO: make "CapSet-ness" of type variables somehow contagious?
// Then we don't have to spell out the bounds explicitly...
def testTrans[C^, D >: CapSet <: C, E >: CapSet <: D, F >: C <: CapSet^] =
val d1: D = ???
val d2: CapSet^{D^} = d1
val d3: D = d2
val e1: E = ???
val e2: CapSet^{E^} = e1
val e3: E = e2
val d4: D = e1
val c1: C = d1
val c2: C = e1
val f1: F = c1
val d_e_f1: CapSet^{D^,E^,F^} = d1
val d_e_f2: CapSet^{D^,E^,F^} = e1
val d_e_f3: CapSet^{D^,E^,F^} = f1
val f2: F = d_e_f1
val c3: C = d_e_f1 // error
val c4: C = f1 // error
val e4: E = f1 // error
val e5: E = d1 // error


trait A[+T]

trait B[-C]

def testCong[C^, D^] =
val a: A[C] = ???
val b: A[CapSet^{C^}] = a
val c: A[CapSet^{D^}] = a // error
val d: A[CapSet^{C^,D^}] = a
val e: A[C] = d // error
val f: B[C] = ???
val g: B[CapSet^{C^}] = f
val h: B[C] = g
val i: B[CapSet^{C^,D^}] = h // error
val j: B[C] = i
6 changes: 1 addition & 5 deletions tests/pos-custom-args/captures/cc-poly-varargs.scala
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,4 @@ def either[T1, T2, Cap^](
src2: Source[T2, Cap]^{Cap^}): Source[Either[T1, T2], Cap]^{Cap^} =
val left = src1.transformValuesWith(Left(_))
val right = src2.transformValuesWith(Right(_))
race[Either[T1, T2], Cap](left, right)
// Explicit type arguments are required here because the second argument
// is inferred as `CapSet^{Cap^}` instead of `Cap`.
// Although `CapSet^{Cap^}` subsumes `Cap` in terms of capture sets,
// `Cap` is not a subtype of `CapSet^{Cap^}` in terms of subtyping.
race(left, right)

0 comments on commit 079d4f5

Please sign in to comment.