|
1 | 1 | -- Error: tests/neg-custom-args/captures/sep-counter.scala:12:19 ------------------------------------------------------- |
2 | 2 | 12 | def mkCounter(): Pair[Ref^, Ref^] = // error |
3 | 3 | | ^^^^^^^^^^^^^^^^ |
4 | | - |Separation failure in method mkCounter's result type Pair[Ref^, Ref^²]. |
5 | | - |One part, Ref^, hides capabilities {c, cap, cap²}. |
6 | | - |Another part, Ref^², captures capabilities {c}. |
7 | | - |The two sets overlap at {c}. |
| 4 | + | Separation failure in method mkCounter's result type Pair[Ref^, Ref^²]. |
| 5 | + | One part, Ref^, hides capabilities {c, cap, cap²}. |
| 6 | + | Another part, Ref^², captures capabilities {c}. |
| 7 | + | The two sets overlap at {c}. |
8 | 8 | | |
9 | | - |where: ^ refers to a fresh root capability in the result type of method mkCounter |
10 | | - | ^² refers to a fresh root capability in the result type of method mkCounter |
11 | | - | cap is a fresh root capability classified as Mutable in the type of value c |
12 | | - | cap² is a fresh root capability classified as Mutable created in value c when constructing instance Ref |
| 9 | + | where: ^ refers to a fresh root capability in the result type of method mkCounter |
| 10 | + | ^² refers to a fresh root capability in the result type of method mkCounter |
| 11 | + | cap is a fresh root capability in the type of value c |
| 12 | + | cap² is a fresh root capability created in value c when constructing instance Ref |
0 commit comments