Skip to content

Commit 56de8df

Browse files
committed
Fix isPartOf
This fixes one error in the lists pos test and several spurious errors in neg tests. There remains an error in lists.scala that has to do with bindings getting lost for polymorphic closures. This needs to be followd up separately.
1 parent 6d9dbf6 commit 56de8df

File tree

6 files changed

+25
-28
lines changed

6 files changed

+25
-28
lines changed

compiler/src/dotty/tools/dotc/cc/CaptureSet.scala

Lines changed: 11 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -596,7 +596,7 @@ object CaptureSet:
596596
val find = new TypeAccumulator[Boolean]:
597597
def apply(b: Boolean, t: Type) =
598598
b || t.match
599-
case CapturingType(p, refs) => (refs eq this) || this(b, p)
599+
case CapturingType(p, refs) => (refs eq Var.this) || this(b, p)
600600
case _ => foldOver(b, t)
601601
find(false, binder)
602602

@@ -618,7 +618,9 @@ object CaptureSet:
618618
case elem: ParamRef if !this.isInstanceOf[BiMapped] =>
619619
isPartOf(elem.binder.resType)
620620
|| {
621-
capt.println(i"LEVEL ERROR $elem for $this")
621+
capt.println(
622+
i"""LEVEL ERROR $elem for $this
623+
|elem binder = ${elem.binder}""")
622624
false
623625
}
624626
case ReachCapability(elem1) =>
@@ -796,9 +798,13 @@ object CaptureSet:
796798
else if accountsFor(elem) then
797799
CompareResult.OK
798800
else
799-
source.tryInclude(bimap.backward(elem), this)
800-
.showing(i"propagating new elem $elem backward from $this to $source = $result", captDebug)
801-
.andAlso(addNewElem(elem))
801+
try
802+
source.tryInclude(bimap.backward(elem), this)
803+
.showing(i"propagating new elem $elem backward from $this to $source = $result", captDebug)
804+
.andAlso(addNewElem(elem))
805+
catch case ex: AssertionError =>
806+
println(i"fail while tryInclude $elem of ${elem.getClass} in $this / ${this.summarize}")
807+
throw ex
802808

803809
/** For a BiTypeMap, supertypes of the mapped type also constrain
804810
* the source via the inverse type mapping and vice versa. That is, if

compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1259,7 +1259,7 @@ class CheckCaptures extends Recheck, SymTransformer:
12591259
if other.isRootCapability then ""
12601260
else " since that capability is not a SharedCapability"
12611261
i"""the existential capture root in ${ex.rootAnnot.originalBinder.resType}
1262-
|cannot subsume the capability $other$since"""
1262+
|cannot subsume the capability $other$since"""
12631263
i"""
12641264
|
12651265
|Note that ${msg.toString}"""

tests/neg-custom-args/captures/curried-closures.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ import language.experimental.captureChecking
88

99
def map3(f: Int => Int)(xs: List[Int]): List[Int] = xs.map(f)
1010
private val f2 = map3
11-
val fc2: (f: Int => Int) -> List[Int] ->{f} List[Int] = f2 // error (?)
11+
val fc2: (f: Int => Int) -> List[Int] ->{f} List[Int] = f2
1212

1313
val f3 = (f: Int => Int) =>
1414
println(f(3))
@@ -27,7 +27,7 @@ import java.io.*
2727
def Test4(g: OutputStream^) =
2828
val xs: List[Int] = ???
2929
val later = (f: OutputStream^) => (y: Int) => xs.foreach(x => f.write(x + y))
30-
val _: (f: OutputStream^) ->{} Int ->{f} Unit = later // error (?)
30+
val _: (f: OutputStream^) ->{} Int ->{f} Unit = later
3131

3232
val later2 = () => (y: Int) => xs.foreach(x => g.write(x + y))
3333
val _: () ->{} Int ->{g} Unit = later2 // error, inferred type is () ->{later2} Int ->{g} Unit

tests/neg-custom-args/captures/heal-tparam-cs.check

Lines changed: 5 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -13,32 +13,20 @@
1313
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:15:13 -------------------------------
1414
15 | localCap { c => // error
1515
| ^
16-
| Found: (x$0: Capp^?) ->? () ->{x$0} Unit
16+
| Found: (x$0: Capp^) ->? () ->{x$0} Unit
1717
| Required: (c: Capp^) -> () ->{localcap} Unit
18+
|
19+
| Note that the existential capture root in () => Unit
20+
| cannot subsume the capability x$0.type since that capability is not a SharedCapability
1821
16 | (c1: Capp^) => () => { c1.use() }
1922
17 | }
2023
|
2124
| longer explanation available when compiling with `-explain`
22-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:20:13 -------------------------------
23-
20 | localCap { c => // error (???) since change to cs mapping
24-
| ^
25-
| Found: (x$0: Capp^?) ->? () ->{x$0} Unit
26-
| Required: (c: Capp^{io}) -> () ->{io} Unit
27-
|
28-
| Note that the existential capture root in () ->? Unit
29-
| cannot subsume the capability <cap of (x$0: Capp^?): () ->{x$0} Unit>
30-
21 | (c1: Capp^{io}) => () => { c1.use() }
31-
22 | }
32-
|
33-
| longer explanation available when compiling with `-explain`
3425
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/heal-tparam-cs.scala:25:13 -------------------------------
3526
25 | localCap { c => // error
3627
| ^
37-
| Found: (x$0: Capp^?) ->? () ->{x$0} Unit
28+
| Found: (x$0: Capp^{io}) ->? () ->{x$0} Unit
3829
| Required: (c: Capp^{io}) -> () ->{net} Unit
39-
|
40-
| Note that the existential capture root in () ->? Unit
41-
| cannot subsume the capability <cap of (x$0: Capp^?): () ->{x$0} Unit>
4230
26 | (c1: Capp^{io}) => () => { c1.use() }
4331
27 | }
4432
|

tests/neg-custom-args/captures/heal-tparam-cs.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ def main(io: Capp^, net: Capp^): Unit = {
1717
}
1818

1919
val test3: (c: Capp^{io}) -> () ->{io} Unit =
20-
localCap { c => // error (???) since change to cs mapping
20+
localCap { c =>
2121
(c1: Capp^{io}) => () => { c1.use() }
2222
}
2323

tests/pending/pos-custom-args/lists.scala renamed to tests/pos-custom-args/captures/lists.scala

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,9 @@ def map[A, B](f: A => B)(xs: LIST[A]): LIST[B] =
2121
class Cap extends caps.Capability
2222

2323
def test(c: Cap, d: Cap, e: Cap) =
24+
2425
def f(x: Cap): Unit = if c == x then ()
26+
2527
def g(x: Cap): Unit = if d == x then ()
2628
val y = f
2729
val ys = CONS(y, NIL)
@@ -43,7 +45,9 @@ def test(c: Cap, d: Cap, e: Cap) =
4345
def m2 = [A, B] =>
4446
(f: A => B) => (xs: LIST[A]) => xs.map(f)
4547

46-
def m2c: [A, B] -> (f: A => B) -> LIST[A] ->{f} LIST[B] = m2
48+
// def m2c: [A, B] -> (f: A => B) -> LIST[A] ->{f} LIST[B] = m2
49+
// !!! m2 has a bad type due to spurious level error. Need to follow up and
50+
// fix this.
4751

4852
def eff[A](x: A) = if x == e then x else x
4953

@@ -87,4 +91,3 @@ def test(c: Cap, d: Cap, e: Cap) =
8791
val c2c: LIST[Cap ->{d, y} Unit]^{e} = c2
8892
val c3 = zs.map(eff2[Cap ->{d, y} Unit])
8993
val c3c: LIST[Cap ->{d, y} Unit]^{e} = c3
90-

0 commit comments

Comments
 (0)