-
Notifications
You must be signed in to change notification settings - Fork 1.1k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
CC: Fix maximal capability handling and expand aliases (#22341)
## 1. Fix various issues with maximal capabilities The subsumes check mistakenly allowed any capability to subsume `cap`, since `cap` is expanded as `caps.cap`, and by the path subcapturing rule `caps.cap <: caps`, where the capture set of `caps` is empty. This allowed quite a few hidden errors to go through. This commit fixes the subcapturing issue and all downstream issues caused by that fix. ## 2. Expand aliases when mapping explicit types in Setup This is necessary because the compiler is free in previous phases to dealias or not. Therefore, capture checking should not depend on aliasing. The main difference is that now arguments to type aliases are not necessarily boxed. They are boxed only if they need boxing in the dealiased type.
- Loading branch information
Showing
33 changed files
with
211 additions
and
128 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,4 @@ | ||
| -- Error: tests/neg-custom-args/captures/boundschecks3.scala:11:13 ----------------------------------------------------- | ||
| 11 | val bar: T -> T = ??? // error, since `T` is expanded here. But the msg is not very good. | ||
| | ^^^^^^ | ||
| | test.C[box test.Tree^] captures the root capability `cap` in invariant position |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| object test { | ||
|
|
||
| class Tree | ||
|
|
||
| def f[X <: Tree](x: X): Unit = () | ||
|
|
||
| class C[X <: Tree](x: X) | ||
|
|
||
| val foo: C[Tree^] = ??? // hidden error | ||
| type T = C[Tree^] // hidden error | ||
| val bar: T -> T = ??? // error, since `T` is expanded here. But the msg is not very good. | ||
| val baz: C[Tree^] -> Unit = ??? // hidden error | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,14 @@ | ||
| -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/box-adapt-cases.scala:14:10 ------------------------------ | ||
| 14 | x.value(cap => cap.use()) // error | ||
| | ^^^^^^^^^^^^^^^^ | ||
| | Found: (cap: box Cap^?) ->{io} Int | ||
| | Required: (cap: box Cap^{io}) -> Int | ||
| | | ||
| | longer explanation available when compiling with `-explain` | ||
| -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/box-adapt-cases.scala:28:10 ------------------------------ | ||
| 28 | x.value(cap => cap.use()) // error | ||
| | ^^^^^^^^^^^^^^^^ | ||
| | Found: (cap: box Cap^?) ->{io, fs} Int | ||
| | Required: (cap: box Cap^{io, fs}) ->{io} Int | ||
| | | ||
| | longer explanation available when compiling with `-explain` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,29 +1,29 @@ | ||
| trait Cap { def use(): Int } | ||
|
|
||
| def test1(): Unit = { | ||
| type Id[X] = [T] -> (op: X => T) -> T | ||
| class Id[X](val value: [T] -> (op: X => T) -> T) | ||
|
|
||
| val x: Id[Cap^] = ??? | ||
| x(cap => cap.use()) | ||
| x.value(cap => cap.use()) | ||
| } | ||
|
|
||
| def test2(io: Cap^): Unit = { | ||
| type Id[X] = [T] -> (op: X -> T) -> T | ||
| class Id[X](val value: [T] -> (op: X -> T) -> T) | ||
|
|
||
| val x: Id[Cap^{io}] = ??? | ||
| x(cap => cap.use()) // error | ||
| x.value(cap => cap.use()) // error | ||
| } | ||
|
|
||
| def test3(io: Cap^): Unit = { | ||
| type Id[X] = [T] -> (op: X ->{io} T) -> T | ||
| class Id[X](val value: [T] -> (op: X ->{io} T) -> T) | ||
|
|
||
| val x: Id[Cap^{io}] = ??? | ||
| x(cap => cap.use()) // ok | ||
| x.value(cap => cap.use()) // ok | ||
| } | ||
|
|
||
| def test4(io: Cap^, fs: Cap^): Unit = { | ||
| type Id[X] = [T] -> (op: X ->{io} T) -> T | ||
| class Id[X](val value: [T] -> (op: X ->{io} T) -> T) | ||
|
|
||
| val x: Id[Cap^{io, fs}] = ??? | ||
| x(cap => cap.use()) // error | ||
| x.value(cap => cap.use()) // error | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,14 +1,14 @@ | ||
| trait Cap | ||
|
|
||
| def test1(io: Cap^) = { | ||
| type Op[X] = [T] -> Unit -> X | ||
| class Op[+X](val value: [T] -> Unit -> X) | ||
| val f: Op[Cap^{io}] = ??? | ||
| val x: [T] -> Unit -> Cap^{io} = f // error | ||
| val x: [T] -> Unit -> Cap^{io} = f.value // error | ||
| } | ||
|
|
||
| def test2(io: Cap^) = { | ||
| type Op[X] = [T] -> Unit -> X^{io} | ||
| class Op[+X](val value: [T] -> Unit -> X^{io}) | ||
| val f: Op[Cap^{io}] = ??? | ||
| val x: Unit -> Cap^{io} = f[Unit] // error | ||
| val x1: Unit ->{io} Cap^{io} = f[Unit] // ok | ||
| val x: Unit -> Cap^{io} = f.value[Unit] // error | ||
| val x1: Unit ->{io} Cap^{io} = f.value[Unit] // ok | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,23 +1,23 @@ | ||
| trait Cap { def use(): Int } | ||
|
|
||
| def test1(io: Cap^): Unit = { | ||
| type Id[X] = [T] -> (op: X ->{io} T) -> T | ||
| class Id[X](val value: [T] -> (op: X ->{io} T) -> T) | ||
|
|
||
| val x: Id[Cap]^{io} = ??? | ||
| x(cap => cap.use()) // ok | ||
| x.value(cap => cap.use()) // ok | ||
| } | ||
|
|
||
| def test2(io: Cap^): Unit = { | ||
| type Id[X] = [T] -> (op: (x: X) ->{io} T) -> T | ||
| class Id[X](val value: [T] -> (op: (x: X) ->{io} T) -> T) | ||
|
|
||
| val x: Id[Cap^{io}] = ??? | ||
| x(cap => cap.use()) | ||
| x.value(cap => cap.use()) | ||
| // should work when the expected type is a dependent function | ||
| } | ||
|
|
||
| def test3(io: Cap^): Unit = { | ||
| type Id[X] = [T] -> (op: (x: X) ->{} T) -> T | ||
| class Id[X](val value: [T] -> (op: (x: X) ->{} T) -> T) | ||
|
|
||
| val x: Id[Cap^{io}] = ??? | ||
| x(cap => cap.use()) // error | ||
| x.value(cap => cap.use()) // error | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,13 +1,13 @@ | ||
| trait Cap { def use(): Int } | ||
|
|
||
| def test1(io: Cap^): Unit = { | ||
| type Op[X] = [T] -> X -> Unit | ||
| class Op[X](val value: [T] -> X -> Unit) | ||
| val f: [T] -> (Cap^{io}) -> Unit = ??? | ||
| val op: Op[Cap^{io}] = f // error | ||
| val op: Op[Cap^{io}] = Op(f) // was error, now ok | ||
| } | ||
|
|
||
| def test2(io: Cap^): Unit = { | ||
| type Lazy[X] = [T] -> Unit -> X | ||
| class Lazy[X](val value: [T] -> Unit -> X) | ||
| val f: Lazy[Cap^{io}] = ??? | ||
| val test: [T] -> Unit -> (Cap^{io}) = f // error | ||
| val test: [T] -> Unit -> (Cap^{io}) = f.value // error | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.