Skip to content

Commit 76ce72f

Browse files
oderskyodersky
committed
Improve printing of existential Fresh instances
Print them as - cap if bound to the immediately enclosing method - (outer_)*cap if bound to some outer enclosing method - <cap of MT> if bound to some other method type MT Sets that only consist of a reference that prints as `cap` are elided by printing just `^` or `=>`.
1 parent 41e7556 commit 76ce72f

File tree

9 files changed

+54
-41
lines changed

9 files changed

+54
-41
lines changed

‎compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala

Lines changed: 21 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,8 @@ class PlainPrinter(_ctx: Context) extends Printer {
5252

5353
protected def inOpenMethod[T](mt: MethodOrPoly | Null)(op: => T)(using Context): T =
5454
val saved = openMethods
55-
if mt != null then openMethods = mt :: openMethods
55+
if mt != null && !mt.resType.isInstanceOf[MethodOrPoly] then
56+
openMethods = mt :: openMethods
5657
try op finally openMethods = saved
5758

5859
given stringToText: Conversion[String, Text] = Str(_)
@@ -262,9 +263,20 @@ class PlainPrinter(_ctx: Context) extends Printer {
262263
then
263264
toText(parent)
264265
else
266+
// The set if universal if it consists only of caps.cap or
267+
// only of an existential Fresh that is bound to the immediately enclosing method.
268+
def isUniversal =
269+
refs.elems.size == 1
270+
&& (refs.isUniversal
271+
|| refs.elems.nth(0).match
272+
case Existential.Vble(binder) =>
273+
openMethods.nonEmpty && openMethods.head == binder
274+
case _ =>
275+
false
276+
)
265277
val refsText =
266-
if refs.isUniversal then
267-
if refs.elems.size == 1 then rootSetText else toTextCaptureSet(refs)
278+
if isUniversal then
279+
rootSetText
268280
else if !refs.elems.isEmpty && refs.elems.forall(_.isCapOrFresh) && !printFresh then
269281
rootSetText
270282
else
@@ -295,7 +307,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
295307
~ paramsText(tp)
296308
~ ")"
297309
~ (Str(": ") provided !tp.resultType.isInstanceOf[MethodOrPoly])
298-
~ toText(tp.resultType)
310+
~ inOpenMethod(tp)(toText(tp.resultType))
299311
}
300312
case ExprType(restp) =>
301313
def arrowText: Text = restp match
@@ -451,10 +463,11 @@ class PlainPrinter(_ctx: Context) extends Printer {
451463
case Existential.VarOLD(bv) => toTextRef(bv)
452464
case Existential.Vble(binder) =>
453465
// TODO: Better printing? USe a mode where we print more detailed
454-
val vbleStr = openMethods.indexOf(binder) match
455-
case -1 => "unknown.localcap"
456-
case n => "outer_" * n ++ "localcap"
457-
vbleStr ~ hashStr(binder)
466+
val vbleText: Text = openMethods.indexOf(binder) match
467+
case -1 =>
468+
"<cap of " ~ toText(binder) ~ ">"
469+
case n => "outer_" * n ++ "cap"
470+
vbleText ~ hashStr(binder)
458471
case Fresh(hidden) =>
459472
val idStr = if showUniqueIds then s"#${hidden.id}" else ""
460473
if printFreshDetailed then s"<cap$idStr hiding " ~ toTextCaptureSet(hidden) ~ ">"

‎tests/neg-custom-args/captures/capt1.check

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -36,33 +36,33 @@
3636
-- Error: tests/neg-custom-args/captures/capt1.scala:36:16 -------------------------------------------------------------
3737
36 | val z2 = h[() -> Cap](() => x) // error // error
3838
| ^^^^^^^^^
39-
| Type variable X of method h cannot be instantiated to () -> box C^{localcap} since
40-
| the part box C^{unknown.localcap} of that type captures the root capability `cap`.
39+
| Type variable X of method h cannot be instantiated to () -> box C^ since
40+
| the part box C^{<cap of (): box C^>} of that type captures the root capability `cap`.
4141
-- Error: tests/neg-custom-args/captures/capt1.scala:36:30 -------------------------------------------------------------
4242
36 | val z2 = h[() -> Cap](() => x) // error // error
4343
| ^
4444
| reference (x : C^) is not included in the allowed capture set {}
45-
| of an enclosing function literal with expected type () -> box C^{localcap}
45+
| of an enclosing function literal with expected type () -> box C^
4646
-- Error: tests/neg-custom-args/captures/capt1.scala:38:13 -------------------------------------------------------------
4747
38 | val z3 = h[(() -> Cap) @retains(x)](() => x)(() => C()) // error
4848
| ^^^^^^^^^^^^^^^^^^^^^^^
49-
| Type variable X of method h cannot be instantiated to box () ->{x} C^{localcap} since
50-
| the part C^{unknown.localcap} of that type captures the root capability `cap`.
49+
| Type variable X of method h cannot be instantiated to box () ->{x} C^ since
50+
| the part C^{<cap of (): C^>} of that type captures the root capability `cap`.
5151
-- Error: tests/neg-custom-args/captures/capt1.scala:43:7 --------------------------------------------------------------
5252
43 | if x == null then // error: separation
5353
| ^
5454
| Separation failure: Illegal access to {x} which is hidden by the previous definition
55-
| of value z1 with type () => C^{localcap}.
55+
| of value z1 with type () => C^.
5656
| This type hides capabilities {x}
5757
-- Error: tests/neg-custom-args/captures/capt1.scala:44:12 -------------------------------------------------------------
5858
44 | () => x // error: separation
5959
| ^
6060
| Separation failure: Illegal access to {x} which is hidden by the previous definition
61-
| of value z1 with type () => C^{localcap}.
61+
| of value z1 with type () => C^.
6262
| This type hides capabilities {x}
6363
-- Error: tests/neg-custom-args/captures/capt1.scala:47:2 --------------------------------------------------------------
6464
47 | x // error: separation
6565
| ^
6666
| Separation failure: Illegal access to {x} which is hidden by the previous definition
67-
| of value z1 with type () => C^{localcap}.
67+
| of value z1 with type () => C^.
6868
| This type hides capabilities {x}

‎tests/neg-custom-args/captures/existential-mapping.check

Lines changed: 16 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -5,84 +5,84 @@
55
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:9:25 ---------------------------
66
9 | val _: (x: C^) -> C = x1 // error
77
| ^^
8-
| Found: (x1 : (x: C^) -> C^{localcap})
8+
| Found: (x1 : (x: C^) -> C^)
99
| Required: (x: C^) -> C
1010
|
1111
| longer explanation available when compiling with `-explain`
1212
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:12:20 --------------------------
1313
12 | val _: C^ -> C = x2 // error
1414
| ^^
15-
| Found: (x2 : C^ -> C^{localcap})
15+
| Found: (x2 : C^ -> C^)
1616
| Required: C^ -> C
1717
|
1818
| longer explanation available when compiling with `-explain`
1919
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:15:30 --------------------------
2020
15 | val _: A^ -> (x: C^) -> C = x3 // error
2121
| ^^
22-
| Found: (x3 : A^ -> (x: C^) -> C^{localcap})
22+
| Found: (x3 : A^ -> (x: C^) -> C^)
2323
| Required: A^ -> (x: C^) -> C
2424
|
2525
| longer explanation available when compiling with `-explain`
2626
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:18:25 --------------------------
2727
18 | val _: A^ -> C^ -> C = x4 // error
2828
| ^^
29-
| Found: (x4 : A^ -> C^ -> C^{localcap})
29+
| Found: (x4 : A^ -> C^ -> C^)
3030
| Required: A^ -> C^ -> C
3131
|
3232
| longer explanation available when compiling with `-explain`
3333
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:21:30 --------------------------
3434
21 | val _: A^ -> (x: C^) -> C = x5 // error
3535
| ^^
36-
| Found: (x5 : A^ -> (x: C^) -> C^{localcap})
36+
| Found: (x5 : A^ -> (x: C^) -> C^)
3737
| Required: A^ -> (x: C^) -> C
3838
|
3939
| longer explanation available when compiling with `-explain`
4040
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:24:30 --------------------------
4141
24 | val _: A^ -> (x: C^) => C = x6 // error
4242
| ^^
43-
| Found: (x6 : A^ -> (x: C^) ->{localcap} C^{localcap})
44-
| Required: A^ -> (x: C^) ->{localcap} C
43+
| Found: (x6 : A^ -> (x: C^) => C^)
44+
| Required: A^ -> (x: C^) => C
4545
|
4646
| longer explanation available when compiling with `-explain`
4747
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:27:25 --------------------------
4848
27 | val _: (x: C^) => C = y1 // error
4949
| ^^
50-
| Found: (y1 : (x: C^) ->{fresh} C^{localcap})
50+
| Found: (y1 : (x: C^) ->{fresh} C^)
5151
| Required: (x: C^) ->{fresh} C
5252
|
5353
| longer explanation available when compiling with `-explain`
5454
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:30:20 --------------------------
5555
30 | val _: C^ => C = y2 // error
5656
| ^^
57-
| Found: (y2 : C^ ->{fresh} C^{localcap})
57+
| Found: (y2 : C^ ->{fresh} C^)
5858
| Required: C^ ->{fresh} C
5959
|
6060
| longer explanation available when compiling with `-explain`
6161
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:33:30 --------------------------
6262
33 | val _: A^ => (x: C^) => C = y3 // error
6363
| ^^
64-
| Found: (y3 : A^ ->{fresh} (x: C^) ->{localcap} C^{localcap})
65-
| Required: A^ ->{fresh} (x: C^) ->{localcap} C
64+
| Found: (y3 : A^ ->{fresh} (x: C^) => C^)
65+
| Required: A^ ->{fresh} (x: C^) => C
6666
|
6767
| longer explanation available when compiling with `-explain`
6868
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:36:25 --------------------------
6969
36 | val _: A^ => C^ => C = y4 // error
7070
| ^^
71-
| Found: (y4 : A^ ->{fresh} C^ ->{localcap} C^{localcap})
72-
| Required: A^ ->{fresh} C^ ->{localcap} C
71+
| Found: (y4 : A^ ->{fresh} C^ => C^)
72+
| Required: A^ ->{fresh} C^ => C
7373
|
7474
| longer explanation available when compiling with `-explain`
7575
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:39:30 --------------------------
7676
39 | val _: A^ => (x: C^) -> C = y5 // error
7777
| ^^
78-
| Found: (y5 : A^ ->{fresh} (x: C^) -> C^{localcap})
78+
| Found: (y5 : A^ ->{fresh} (x: C^) -> C^)
7979
| Required: A^ ->{fresh} (x: C^) -> C
8080
|
8181
| longer explanation available when compiling with `-explain`
8282
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:42:30 --------------------------
8383
42 | val _: A^ => (x: C^) => C = y6 // error
8484
| ^^
85-
| Found: (y6 : A^ ->{fresh} (x: C^) ->{localcap} C^{localcap})
86-
| Required: A^ ->{fresh} (x: C^) ->{localcap} C
85+
| Found: (y6 : A^ ->{fresh} (x: C^) => C^)
86+
| Required: A^ ->{fresh} (x: C^) => C
8787
|
8888
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/i19330.check

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,5 +13,5 @@
1313
-- Error: tests/neg-custom-args/captures/i19330.scala:16:14 ------------------------------------------------------------
1414
16 | val t: () => Logger^ = () => l // error
1515
| ^^^^^^^^^^^^^
16-
| Separation failure: value t's type () => Logger^{localcap} hides parameter l.
16+
| Separation failure: value t's type () => Logger^ hides parameter l.
1717
| The parameter needs to be annotated with @consume to allow this.

‎tests/neg-custom-args/captures/i21401.check

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,5 +21,5 @@
2121
-- Error: tests/neg-custom-args/captures/i21401.scala:17:52 ------------------------------------------------------------
2222
17 | val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error
2323
| ^^^^^^^^^^^^^^^^^^^^^^^^
24-
| Type variable X of value leaked cannot be instantiated to Boxed[box IO^] -> Boxed[box IO^{localcap}] since
25-
| the part box IO^{unknown.localcap} of that type captures the root capability `cap`.
24+
|Type variable X of value leaked cannot be instantiated to Boxed[box IO^] -> Boxed[box IO^] since
25+
|the part box IO^{<cap of (x$0: Boxed[box IO^]): Boxed[box IO^]>} of that type captures the root capability `cap`.

‎tests/neg-custom-args/captures/i21614.check

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,10 @@
88
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:15:12 ---------------------------------------
99
15 | files.map(new Logger(_)) // error, Q: can we improve the error message?
1010
| ^^^^^^^^^^^^^
11-
| Found: (_$1: box File^{files*}) ->{files*} box Logger{val f: File^{_$1}}^{localcap.rd, _$1}
11+
| Found: (_$1: box File^{files*}) ->{files*} box Logger{val f: File^{_$1}}^{cap.rd, _$1}
1212
| Required: (_$1: box File^{files*}) ->{fresh} box Logger{val f: File^?}^?
1313
|
14-
| Note that reference unknown.localcap.rd
14+
| Note that reference <cap of (f: box F^{files*.rd}): box Logger{val f: File^?}^?>.rd
1515
| cannot be included in outer capture set ?
1616
|
1717
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/leaked-curried.check

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,9 @@
22
14 | () => () => io // error
33
| ^^
44
| reference (io : Cap^) is not included in the allowed capture set {}
5-
| of an enclosing function literal with expected type () -> () ->{io} Cap^{localcap}
5+
| of an enclosing function literal with expected type () -> () ->{io} Cap^
66
-- Error: tests/neg-custom-args/captures/leaked-curried.scala:17:20 ----------------------------------------------------
77
17 | () => () => io // error
88
| ^^
99
| reference (io : Cap^) is not included in the allowed capture set {}
10-
| of an enclosing function literal with expected type () -> () ->{io} Cap^{localcap}
10+
| of an enclosing function literal with expected type () -> () ->{io} Cap^

‎tests/neg-custom-args/captures/sep-use2.check

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@
2727
18 | { f(cc) } // error // error
2828
| ^^
2929
| Separation failure: argument of type (cc : -> Object^)
30-
| to a function of type Object^ ->{c} Object^{localcap}
30+
| to a function of type Object^ ->{c} Object^
3131
| corresponds to capture-polymorphic formal parameter x$0 of type Object^
3232
| and hides capabilities {cap, c}.
3333
| Some of these overlap with the captures of the function prefix.

‎tests/neg-custom-args/captures/unsound-reach-4.check

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,6 @@
1414
17 | def use(@consume x: F): File^ = x // error @consume override
1515
| ^
1616
|error overriding method use in trait Foo of type (x: File^): box File^;
17-
| method use of type (x: File^): File^{unknown.localcap} has a parameter x with different @consume status than the corresponding parameter in the overridden definition
17+
| method use of type (x: File^): File^ has a parameter x with different @consume status than the corresponding parameter in the overridden definition
1818
|
1919
| longer explanation available when compiling with `-explain`

0 commit comments

Comments
 (0)