Skip to content

Commit

Permalink
Sharpen range approximation for applied types with capture set ranges (
Browse files Browse the repository at this point in the history
…#16261)

This is a stopgap to avoid approximating the core type to Nothing. It
can probably be dropped once we have capture set ranges that we can keep
as inference results. The problem is, what should be the approximation
of the range

    C[{cs1} A .. {cs2} A]

where the type constructor `C` is non-variant? If the variance of the
enclosing map is positive, this is `C[? >: {cs1} A <: {cs2} A]`, which
is a supertype of both range end points `C[{cs1} A]` and `C[{cs2} A]`.
But if the variance is negative, we would normally fall back to
`Nothing`, since that is the only known subtype of both range end
points. This reasoning seems too strict for capture checking. In a
sense, we have already inferred `C[A]` before; now we just need to find
out what the set should be. What we are after is a notion of a _capture
set range_. I.e. something like

    C[{cs1}..{cs2} A]

with the meaning that the capture set of `C` is an unknown set between
`cs1` and `cs2`. We don't have that abstraction yet, so for now we
approximate by the bounds, which avoids the failures, even though its
soundness status is currently a bit unclear.
  • Loading branch information
Linyxus authored Oct 31, 2022
2 parents 9c68fd7 + ae1fa0b commit 8de6d88
Show file tree
Hide file tree
Showing 5 changed files with 45 additions and 3 deletions.
12 changes: 12 additions & 0 deletions compiler/src/dotty/tools/dotc/core/TypeOps.scala
Original file line number Diff line number Diff line change
Expand Up @@ -533,6 +533,18 @@ object TypeOps:
val sym = tp.symbol
forbidden.contains(sym)

/** We need to split the set into upper and lower approximations
* only if it contains a local element. The idea here is that at the
* time we perform an `avoid` all local elements are already accounted for
* and no further elements will be added afterwards. So we can just keep
* the set as it is. See comment by @linyxus on #16261.
*/
override def needsRangeIfInvariant(refs: CaptureSet): Boolean =
refs.elems.exists {
case ref: TermRef => toAvoid(ref)
case _ => false
}

override def apply(tp: Type): Type = tp match
case tp: TypeVar if mapCtx.typerState.constraint.contains(tp) =>
val lo = TypeComparer.instanceType(
Expand Down
5 changes: 4 additions & 1 deletion compiler/src/dotty/tools/dotc/core/Types.scala
Original file line number Diff line number Diff line change
Expand Up @@ -6027,8 +6027,11 @@ object Types {
tp.derivedLambdaType(tp.paramNames, formals, restpe)
}

/** Overridden in TypeOps.avoid */
protected def needsRangeIfInvariant(refs: CaptureSet): Boolean = true

override def mapCapturingType(tp: Type, parent: Type, refs: CaptureSet, v: Int): Type =
if v == 0 then
if v == 0 && needsRangeIfInvariant(refs) then
range(mapCapturingType(tp, parent, refs, -1), mapCapturingType(tp, parent, refs, 1))
else
super.mapCapturingType(tp, parent, refs, v)
Expand Down
4 changes: 2 additions & 2 deletions tests/neg-custom-args/captures/try.check
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:23:49 ------------------------------------------
23 | val a = handle[Exception, CanThrow[Exception]] { // error
| ^
| Found: ? ({*} CT[Exception]) -> {*} CT[? >: ? Exception <: ? Exception]
| Required: CanThrow[Exception] => box {*} CT[Exception]
| Found: ? ({*} CT[Exception]) -> CanThrow[? Exception]
| Required: CanThrow[Exception] => box {*} CT[Exception]
24 | (x: CanThrow[Exception]) => x
25 | }{
|
Expand Down
14 changes: 14 additions & 0 deletions tests/pos-custom-args/captures/i16226.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
@annotation.capability class Cap

class LazyRef[T](val elem: () => T):
val get: {elem} () -> T = elem
def map[U](f: T => U): {f, this} LazyRef[U] =
new LazyRef(() => f(elem()))

def map[A, B](ref: {*} LazyRef[A], f: A => B): {f, ref} LazyRef[B] =
new LazyRef(() => f(ref.elem()))

def main(io: Cap) = {
def mapd[A, B]: ({io} LazyRef[A], A => B) => {*} LazyRef[B] =
(ref1, f1) => map[A, B](ref1, f1)
}
13 changes: 13 additions & 0 deletions tests/pos-custom-args/captures/i16226a.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
class Name
class TermName extends Name
class TypeName extends Name

trait ParamInfo:
type ThisName <: Name
def variance: Long
object ParamInfo:
type Of[N <: Name] = ParamInfo { type ThisName = N }

def test(tparams1: List[ParamInfo{ type ThisName = TypeName }], tparams2: List[ParamInfo.Of[TypeName]]) =
tparams1.lazyZip(tparams2).map((p1, p2) => p1.variance + p2.variance)

0 comments on commit 8de6d88

Please sign in to comment.