Skip to content

Commit 3c8aa5e

Browse files
committed
Improve printing of Fresh in parts of types
We need to keep track of the enclosing type structure with all Fresh binders and restore it at the point where we are printing a part of a type.
1 parent 76ce72f commit 3c8aa5e

File tree

8 files changed

+53
-30
lines changed

8 files changed

+53
-30
lines changed

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

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -101,6 +101,8 @@ class CCState:
101101
private var curLevel: Level = outermostLevel
102102
private val symLevel: mutable.Map[Symbol, Int] = mutable.Map()
103103

104+
private var openedFreshBinders: List[MethodType] = Nil
105+
104106
object CCState:
105107

106108
opaque type Level = Int
@@ -126,6 +128,14 @@ object CCState:
126128
if !p then ccs.curLevel = ccs.curLevel.nextInner
127129
try op finally ccs.curLevel = saved
128130

131+
inline def inOpenedFreshBinder[T](mt: MethodType)(op: => T)(using Context): T =
132+
val ccs = ccState
133+
val saved = ccs.openedFreshBinders
134+
if mt.isFreshBinder then ccs.openedFreshBinders = mt :: ccs.openedFreshBinders
135+
try op finally ccs.openedFreshBinders = saved
136+
137+
def openedFreshBinders(using Context): List[MethodType] = ccState.openedFreshBinders
138+
129139
extension (x: Level)
130140
def isDefined: Boolean = x >= 0
131141
def <= (y: Level) = (x: Int) <= y
@@ -578,6 +588,10 @@ extension (tp: Type)
578588
case tp: MethodOrPoly => tp.resType.hasSuffix(other)
579589
case _ => false
580590

591+
def isFreshBinder(using Context): Boolean = tp match
592+
case tp: MethodType => !tp.resType.isInstanceOf[MethodOrPoly]
593+
case _ => false
594+
581595
extension (cls: ClassSymbol)
582596

583597
def pureBaseClass(using Context): Option[Symbol] =

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

Lines changed: 21 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -166,6 +166,7 @@ object CheckCaptures:
166166
val check = new TypeTraverser:
167167

168168
private val seen = new EqHashSet[TypeRef]
169+
var openFreshBinders: List[MethodType] = Nil
169170

170171
def traverse(t: Type) =
171172
t.dealiasKeepAnnots match
@@ -184,13 +185,32 @@ object CheckCaptures:
184185
()
185186
case CapturingType(parent, refs) =>
186187
if variance >= 0 then
188+
val openBinders = openFreshBinders
187189
refs.disallowRootCapability: () =>
188-
def part = if t eq tp then "" else i"the part $t of "
190+
def part =
191+
if t eq tp then ""
192+
else
193+
// Show in context of all enclosing traversed fresh binders.
194+
def showInOpenedFreshBinders(mts: List[MethodType]): String = mts match
195+
case Nil => i"the part $t of "
196+
case mt :: mts1 =>
197+
CCState.inOpenedFreshBinder(mt):
198+
showInOpenedFreshBinders(mts1)
199+
showInOpenedFreshBinders(openBinders.reverse)
189200
report.error(
190201
em"""$what cannot $have $tp since
191202
|${part}that type captures the root capability `cap`.$addendum""",
192203
pos)
193204
traverse(parent)
205+
case defn.RefinedFunctionOf(mt) =>
206+
traverse(mt)
207+
case t: MethodType if t.isFreshBinder =>
208+
atVariance(-variance):
209+
t.paramInfos.foreach(traverse)
210+
val saved = openFreshBinders
211+
openFreshBinders = t :: openFreshBinders
212+
try traverse(t.resType)
213+
finally openFreshBinders = saved
194214
case t =>
195215
traverseChildren(t)
196216
if ccConfig.useSealed then check.traverse(tp)

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -311,7 +311,7 @@ object Existential:
311311
case t: MethodType =>
312312
// skip parameters
313313
val saved = localBinders
314-
if !t.resType.isInstanceOf[MethodOrPoly] && !deep then localBinders = localBinders + t
314+
if t.isFreshBinder && !deep then localBinders = localBinders + t
315315
try t.derivedLambdaType(resType = this(t.resType))
316316
finally localBinders = saved
317317
case t: PolyType =>
@@ -484,7 +484,7 @@ object Existential:
484484
val mt1 = apply(mt)
485485
if mt1 ne mt then mt1.toFunctionType(alwaysDependent = true)
486486
else t
487-
case t: MethodType if variance > 0 && !t.resType.isInstanceOf[MethodOrPoly] =>
487+
case t: MethodType if variance > 0 && t.isFreshBinder =>
488488
val t1 = mapOver(t).asInstanceOf[MethodType]
489489
t1.derivedLambdaType(resType =
490490
if ccConfig.newScheme then mapCap(t1.resType, t1, fail)

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

Lines changed: 2 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -823,7 +823,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
823823
(tp1.signature consistentParams tp2.signature) &&
824824
matchingMethodParams(tp1, tp2) &&
825825
(!tp2.isImplicitMethod || tp1.isImplicitMethod) &&
826-
inOpenedMethod(tp2):
826+
CCState.inOpenedFreshBinder(tp2):
827827
isSubType(tp1.resultType, tp2.resultType.subst(tp2, tp1))
828828
case _ => false
829829
}
@@ -2829,11 +2829,6 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
28292829
finally
28302830
assocExistentialsOLD = saved
28312831

2832-
private def inOpenedMethod[T](mt: MethodType)(op: => T)(using Context): T =
2833-
val saved = openedMethods
2834-
if !mt.resType.isInstanceOf[MethodOrPoly] then openedMethods = mt :: openedMethods
2835-
try op finally openedMethods = saved
2836-
28372832
/** Is `tp1` an existential var that subsumes `tp2`? This is the case if `tp1` is
28382833
* instantiatable (i.e. it's a key in `assocExistentials`) and one of the
28392834
* following is true:
@@ -2865,7 +2860,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
28652860

28662861
def isOpenedExistential(ref: CaptureRef)(using Context): Boolean =
28672862
ref match
2868-
case Existential.Vble(mt) => openedMethods.contains(mt)
2863+
case Existential.Vble(mt) => CCState.openedFreshBinders.contains(mt)
28692864
case _ => openedExistentialsOLD.contains(ref)
28702865

28712866
/** bi-map taking existentials to the left of a comparison to matching

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

Lines changed: 5 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -48,14 +48,6 @@ class PlainPrinter(_ctx: Context) extends Printer {
4848
limiter.register(str)
4949
Texts.Str(str, lineRange)
5050

51-
private var openMethods: List[MethodOrPoly] = Nil
52-
53-
protected def inOpenMethod[T](mt: MethodOrPoly | Null)(op: => T)(using Context): T =
54-
val saved = openMethods
55-
if mt != null && !mt.resType.isInstanceOf[MethodOrPoly] then
56-
openMethods = mt :: openMethods
57-
try op finally openMethods = saved
58-
5951
given stringToText: Conversion[String, Text] = Str(_)
6052

6153
/** If true, tweak output so it is the same before and after pickling */
@@ -270,7 +262,9 @@ class PlainPrinter(_ctx: Context) extends Printer {
270262
&& (refs.isUniversal
271263
|| refs.elems.nth(0).match
272264
case Existential.Vble(binder) =>
273-
openMethods.nonEmpty && openMethods.head == binder
265+
CCState.openedFreshBinders match
266+
case b :: _ => binder eq b
267+
case _ => false
274268
case _ =>
275269
false
276270
)
@@ -307,7 +301,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
307301
~ paramsText(tp)
308302
~ ")"
309303
~ (Str(": ") provided !tp.resultType.isInstanceOf[MethodOrPoly])
310-
~ inOpenMethod(tp)(toText(tp.resultType))
304+
~ CCState.inOpenedFreshBinder(tp)(toText(tp.resultType))
311305
}
312306
case ExprType(restp) =>
313307
def arrowText: Text = restp match
@@ -463,7 +457,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
463457
case Existential.VarOLD(bv) => toTextRef(bv)
464458
case Existential.Vble(binder) =>
465459
// TODO: Better printing? USe a mode where we print more detailed
466-
val vbleText: Text = openMethods.indexOf(binder) match
460+
val vbleText: Text = CCState.openedFreshBinders.indexOf(binder) match
467461
case -1 =>
468462
"<cap of " ~ toText(binder) ~ ">"
469463
case n => "outer_" * n ++ "cap"

compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -181,7 +181,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
181181
argStr ~ " " ~ arrow(isContextual, isPure) ~ refs ~ " " ~ argText(res)
182182

183183
protected def toTextMethodAsFunction(info: Type, isPure: Boolean, refs: Text = Str("")): Text =
184-
def recur(tp: Type, enclInfo: MethodOrPoly | Null): Text = tp match
184+
def recur(tp: Type, enclInfo: MethodType | Null): Text = tp match
185185
case tp: MethodType =>
186186
val isContextual = tp.isImplicitMethod
187187
val capturesRoot = refs == rootSetText
@@ -190,7 +190,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
190190
&& !showUniqueIds && !printDebug
191191
then
192192
// cc.Setup converts all functions to dependent functions. Undo that when printing.
193-
inOpenMethod(tp):
193+
CCState.inOpenedFreshBinder(tp):
194194
toTextFunction(tp.paramInfos, tp.resType, refs.provided(!capturesRoot), isContextual, isPure && !capturesRoot)
195195
else
196196
changePrec(GlobalPrec):
@@ -206,11 +206,11 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
206206
"["
207207
~ paramsText(tp)
208208
~ "] => "
209-
~ recur(tp.resultType, tp)
209+
~ recur(tp.resultType, enclInfo)
210210
}
211211
case _ =>
212-
inOpenMethod(enclInfo):
213-
toText(tp)
212+
if enclInfo != null then CCState.inOpenedFreshBinder(enclInfo)(toText(tp))
213+
else toText(tp)
214214
recur(info, null)
215215

216216
override def toText(tp: Type): Text = controlled {

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@
3737
36 | val z2 = h[() -> Cap](() => x) // error // error
3838
| ^^^^^^^^^
3939
| 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`.
40+
| the part 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
| ^
@@ -47,7 +47,7 @@
4747
38 | val z3 = h[(() -> Cap) @retains(x)](() => x)(() => C()) // error
4848
| ^^^^^^^^^^^^^^^^^^^^^^^
4949
| 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`.
50+
| the part 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
| ^

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^] since
25-
|the part box IO^{<cap of (x$0: Boxed[box IO^]): Boxed[box IO^]>} 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^ of that type captures the root capability `cap`.

0 commit comments

Comments
 (0)