Skip to content

Commit b27874c

Browse files
committed
Prevent fallback to normal function when comparing dependent functions
A dependent function is represented as a refinement type with a normal applied function type as parent. When capture checking two dependent function types, the parents should be ignored. But there was a case where this did not happen: If the left hand side is a sinletontype with a capturing type over a dependent function type, and the original method type comparisons fail, then the parent type of the left hand type was tried as a fallback. This commit adds a test that prevents the fallback.
1 parent 390233e commit b27874c

File tree

3 files changed

+32
-4
lines changed

3 files changed

+32
-4
lines changed

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -856,10 +856,10 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
856856
else
857857
// The singletonOK branch is because we sometimes have a larger capture set in a singleton
858858
// than in its underlying type. An example is `f: () -> () ->{x} T`, which might be
859-
// the type of a closure. In that case the capture set of `f.type` is `{x}` but the
860-
// capture set of the underlying type is `{}`. So without the `singletonOK` test, a singleton
861-
// might not be a subtype of its underlying type. Examples where this arises is
862-
// capt-capibility.scala and function-combinators.scala
859+
// the type of a closure (in one of the variants we are considering). In that case the
860+
// capture set of `f.type` is `{x}` but the capture set of the underlying type is `{}`.
861+
// So without the `singletonOK` test, a singleton might not be a subtype of its underlying type.
862+
// Eamples where this arises is capt-capibility.scala and function-combinators.scala
863863
val singletonOK = tp1 match
864864
case tp1: SingletonType
865865
if subCaptures(tp1.underlying.captureSet, refs2, CaptureSet.VarState.Separate).isOK =>
@@ -1013,6 +1013,11 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
10131013

10141014
comparePaths || isSubType(tp1widened, tp2, approx.addLow)
10151015
case tp1: RefinedType =>
1016+
if isCaptureCheckingOrSetup then
1017+
tp2.stripCapturing match
1018+
case defn.RefinedFunctionOf(_) => // was already handled in thirdTry
1019+
return false
1020+
case _ =>
10161021
isNewSubType(tp1.parent)
10171022
case tp1: RecType =>
10181023
isNewSubType(tp1.parent)
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i15923b.scala:8:21 ---------------------------------------
2+
8 | val leak = withCap(f) // error
3+
| ^
4+
|Found: (x$0: Cap^) -> Id[box Cap^{x$0}]
5+
|Required: (lcap: Cap^) => box Id[box Cap^?]^?
6+
|
7+
|where: => refers to a fresh root capability created in value leak when checking argument to parameter op of method withCap
8+
| ^ refers to the universal root capability
9+
|
10+
|
11+
|Note that reference lcap.type
12+
|cannot be included in outer capture set ?
13+
|
14+
| longer explanation available when compiling with `-explain`
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
import language.experimental.captureChecking
2+
trait Cap
3+
case class Id[X](x: X)
4+
def mkId[X](x: X): Id[X] = Id(x)
5+
def withCap[X](op: (lcap: Cap^) => X): X = ???
6+
def bar() =
7+
val f = (lcap: Cap^) => mkId(lcap)
8+
val leak = withCap(f) // error
9+
val leaked = leak.x

0 commit comments

Comments
 (0)