Skip to content

Commit aa06e07

Browse files
oderskyodersky
committed
Expand cap arguments of function aliases before de-aliasing
This is needed to that we can express functions where the result existential scopes over a method type before the directly enclosing one. Example, from `cc-existential-conformance.scala`: type Fun[X] = A -> X A -> A -> B^ prints as A -> A -> B^ A -> Fun[B^] prints as A -> A -> B^{outer_cap} That is, the B^ is tied to the outer function.
1 parent 8e67d6c commit aa06e07

File tree

11 files changed

+111
-60
lines changed

11 files changed

+111
-60
lines changed

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

Lines changed: 19 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -101,7 +101,7 @@ 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
104+
private var openExistentialScopes: List[MethodType] = Nil
105105

106106
object CCState:
107107

@@ -134,20 +134,21 @@ object CCState:
134134
if !p then ccs.curLevel = ccs.curLevel.nextInner
135135
try op finally ccs.curLevel = saved
136136

137-
/** If we are currently in capture checking or setup, perform `op` assuming
138-
* a fresh enclosing binder `mt`, otherwise perform `op` directly.
137+
/** If we are currently in capture checking or setup, and `mt` is a method
138+
* type that is not a prefix of a curried method, perform `op` assuming
139+
* a fresh enclosing existential scope `mt`, otherwise perform `op` directly.
139140
*/
140-
inline def inOpenedFreshBinder[T](mt: MethodType)(op: => T)(using Context): T =
141+
inline def inNewExistentialScope[T](mt: MethodType)(op: => T)(using Context): T =
141142
if isCaptureCheckingOrSetup then
142143
val ccs = ccState
143-
val saved = ccs.openedFreshBinders
144-
if mt.isFreshBinder then ccs.openedFreshBinders = mt :: ccs.openedFreshBinders
145-
try op finally ccs.openedFreshBinders = saved
144+
val saved = ccs.openExistentialScopes
145+
if mt.marksExistentialScope then ccs.openExistentialScopes = mt :: ccs.openExistentialScopes
146+
try op finally ccs.openExistentialScopes = saved
146147
else
147148
op
148149

149-
/** The currently opened fresh binders */
150-
def openedFreshBinders(using Context): List[MethodType] = ccState.openedFreshBinders
150+
/** The currently opened existential scopes */
151+
def openExistentialScopes(using Context): List[MethodType] = ccState.openExistentialScopes
151152

152153
extension (x: Level)
153154
def isDefined: Boolean = x >= 0
@@ -590,14 +591,19 @@ extension (tp: Type)
590591
case tp: ThisType => tp.cls.ccLevel.nextInner
591592
case _ => undefinedLevel
592593

594+
/** Is this a method or function that has `other` as its direct or indirect result
595+
* type?
596+
*/
593597
def hasSuffix(other: MethodType)(using Context): Boolean =
594598
(tp eq other) || tp.match
595-
case tp: MethodOrPoly => tp.resType.hasSuffix(other)
599+
case defn.RefinedFunctionOf(mt) => mt.hasSuffix(other)
600+
case mt: MethodType => mt.resType.hasSuffix(other)
596601
case _ => false
597602

598-
def isFreshBinder(using Context): Boolean = tp match
599-
case tp: MethodType => !tp.resType.isInstanceOf[MethodOrPoly]
600-
case _ => false
603+
extension (tp: MethodType)
604+
/** A method marks an existential scope unless it is the prefix of a curried method */
605+
def marksExistentialScope(using Context): Boolean =
606+
!tp.resType.isInstanceOf[MethodOrPoly]
601607

602608
extension (cls: ClassSymbol)
603609

‎compiler/src/dotty/tools/dotc/cc/CaptureRef.scala

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ import compiletime.uninitialized
1414
import StdNames.nme
1515
import CaptureSet.VarState
1616
import Annotations.Annotation
17+
import config.Printers.capt
1718

1819
/** A trait for references in CaptureSets. These can be NamedTypes, ThisTypes or ParamRefs,
1920
* as well as three kinds of AnnotatedTypes representing readOnly, reach, and maybe capabilities.
@@ -259,6 +260,7 @@ trait CaptureRef extends TypeProxy, ValueType:
259260
case Existential.Vble(binder) =>
260261
y.stripReadOnly match
261262
case Existential.Vble(binder1) => binder1.hasSuffix(binder)
263+
.showing(i"cmp existential $binder maxSubsumes $binder1 = $result", capt)
262264
case _ => true
263265
case _ =>
264266
this.isCap && canAddHidden && vs != VarState.HardSeparate

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -572,7 +572,7 @@ object CaptureSet:
572572
else elem match
573573
case elem @ Existential.Vble(mt) =>
574574
!noUniversal
575-
&& !CCState.openedFreshBinders.contains(elem)
575+
&& !CCState.openExistentialScopes.contains(elem)
576576
// Opened existentials on the left cannot be added to nested capture sets on the right
577577
// of a comparison. Test case is open-existential.scala.
578578
case elem: TermRef if level.isDefined =>

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

Lines changed: 12 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -165,7 +165,10 @@ object CheckCaptures:
165165
val check = new TypeTraverser:
166166

167167
private val seen = new EqHashSet[TypeRef]
168-
var openFreshBinders: List[MethodType] = Nil
168+
169+
// We keep track of open existential scopes here so that we can set these scopes
170+
// in ccState when printing a part of the offending type.
171+
var openExistentialScopes: List[MethodType] = Nil
169172

170173
def traverse(t: Type) =
171174
t.dealiasKeepAnnots match
@@ -184,32 +187,32 @@ object CheckCaptures:
184187
()
185188
case CapturingType(parent, refs) =>
186189
if variance >= 0 then
187-
val openBinders = openFreshBinders
190+
val openScopes = openExistentialScopes
188191
refs.disallowRootCapability: () =>
189192
def part =
190193
if t eq tp then ""
191194
else
192-
// Show in context of all enclosing traversed fresh binders.
195+
// Show in context of all enclosing traversed existential scopes.
193196
def showInOpenedFreshBinders(mts: List[MethodType]): String = mts match
194197
case Nil => i"the part $t of "
195198
case mt :: mts1 =>
196-
CCState.inOpenedFreshBinder(mt):
199+
CCState.inNewExistentialScope(mt):
197200
showInOpenedFreshBinders(mts1)
198-
showInOpenedFreshBinders(openBinders.reverse)
201+
showInOpenedFreshBinders(openScopes.reverse)
199202
report.error(
200203
em"""$what cannot $have $tp since
201204
|${part}that type captures the root capability `cap`.$addendum""",
202205
pos)
203206
traverse(parent)
204207
case defn.RefinedFunctionOf(mt) =>
205208
traverse(mt)
206-
case t: MethodType if t.isFreshBinder =>
209+
case t: MethodType if t.marksExistentialScope =>
207210
atVariance(-variance):
208211
t.paramInfos.foreach(traverse)
209-
val saved = openFreshBinders
210-
openFreshBinders = t :: openFreshBinders
212+
val saved = openExistentialScopes
213+
openExistentialScopes = t :: openExistentialScopes
211214
try traverse(t.resType)
212-
finally openFreshBinders = saved
215+
finally openExistentialScopes = saved
213216
case t =>
214217
traverseChildren(t)
215218
if ccConfig.useSealed then check.traverse(tp)

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -238,7 +238,7 @@ object Existential:
238238
case t: MethodType =>
239239
// skip parameters
240240
val saved = localBinders
241-
if t.isFreshBinder then localBinders = localBinders + t
241+
if t.marksExistentialScope then localBinders = localBinders + t
242242
try t.derivedLambdaType(resType = this(t.resType))
243243
finally localBinders = saved
244244
case t: PolyType =>
@@ -318,21 +318,21 @@ object Existential:
318318
end mapCap
319319

320320
/** Map `cap` in function results to fresh existentials */
321-
def mapCapInResults(fail: Message => Unit)(using Context): TypeMap = new TypeMap with FollowAliasesMap:
321+
def mapCapInResults(fail: Message => Unit, keepAliases: Boolean = false)(using Context): TypeMap = new TypeMap with FollowAliasesMap:
322322
def apply(t: Type): Type = t match
323323
case defn.RefinedFunctionOf(mt) =>
324324
val mt1 = apply(mt)
325325
if mt1 ne mt then mt1.toFunctionType(alwaysDependent = true)
326326
else t
327-
case t: MethodType if variance > 0 && t.isFreshBinder =>
327+
case t: MethodType if variance > 0 && t.marksExistentialScope =>
328328
val t1 = mapOver(t).asInstanceOf[MethodType]
329329
t1.derivedLambdaType(resType = mapCap(t1.resType, t1, fail))
330330
case CapturingType(parent, refs) =>
331331
t.derivedCapturingType(this(parent), refs)
332332
case t: (LazyRef | TypeVar) =>
333333
mapConserveSuper(t)
334334
case _ =>
335-
mapFollowingAliases(t)
335+
if keepAliases then mapOver(t) else mapFollowingAliases(t)
336336
end mapCapInResults
337337

338338
end Existential

‎compiler/src/dotty/tools/dotc/cc/Setup.scala

Lines changed: 39 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -201,17 +201,19 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
201201
/** Map parametric functions with results that have a capture set somewhere
202202
* to dependent functions.
203203
*/
204-
protected def normalizeFunctions(tp: Type, original: Type)(using Context): Type = tp match
204+
protected def normalizeFunctions(tp: Type, original: Type, expandAlways: Boolean = false)(using Context): Type =
205+
tp match
205206
case AppliedType(tycon, args)
206207
if defn.isNonRefinedFunction(tp) && isTopLevel =>
207-
original match
208-
case AppliedType(`tycon`, args0) if args0.last ne args.last =>
209-
// We have an applied type that underwent some addition of capture sets.
210-
// Map to a dependent type so that things are more uniform.
211-
depFun(args.init, args.last,
212-
isContextual = defn.isContextFunctionClass(tycon.classSymbol))
213-
.showing(i"add function refinement $tp ($tycon, ${args.init}, ${args.last}) --> $result", capt)
214-
case _ => tp
208+
// Expand if we have an applied type that underwent some addition of capture sets
209+
val expand = expandAlways || original.match
210+
case AppliedType(`tycon`, args0) => args0.last ne args.last
211+
case _ => false
212+
if expand then
213+
depFun(args.init, args.last,
214+
isContextual = defn.isContextFunctionClass(tycon.classSymbol))
215+
.showing(i"add function refinement $tp ($tycon, ${args.init}, ${args.last}) --> $result", capt)
216+
else tp
215217
case _ => tp
216218

217219
/** Pull out an embedded capture set from a part of `tp` */
@@ -334,8 +336,11 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
334336
def fail(msg: Message) =
335337
if !tptToCheck.isEmpty then report.error(msg, tptToCheck.srcPos)
336338

337-
val toCapturing = new DeepTypeMap with SetupTypeMap:
338-
override def toString = "expand aliases"
339+
object toCapturing extends DeepTypeMap, SetupTypeMap:
340+
override def toString = "transformExplicitType"
341+
342+
var keepFunAliases = true
343+
var keptFunAliases = false
339344

340345
/** Expand $throws aliases. This is hard-coded here since $throws aliases in stdlib
341346
* are defined with `?=>` rather than `?->`.
@@ -425,21 +430,33 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
425430
case throwsAlias(res, exc) =>
426431
this(expandThrowsAlias(res, exc, Nil))
427432
case t @ AppliedType(tycon, args)
428-
if defn.isNonRefinedFunction(tp)
429-
&& !defn.isFunctionSymbol(tp.typeSymbol) && (tp.dealias ne tp) =>
430-
// Expand arguments of aliases of function types before proceeding with dealias.
431-
// This is necessary to bind existentialFresh instances to the right method binder.
432-
val args1 = atVariance(-variance):
433-
args.map(this)
434-
defaultApply(t.derivedAppliedType(tycon, args1))
433+
if defn.isNonRefinedFunction(t)
434+
&& !defn.isFunctionSymbol(t.typeSymbol) && (t.dealias ne tp) =>
435+
if keepFunAliases then
436+
// Hold off with dealising and expand in a second pass.
437+
// This is necessary to bind existentialFresh instances to the right method binder.
438+
keptFunAliases = true
439+
mapOver(t)
440+
else
441+
// In the second pass, map the alias and make sure it has the form
442+
// of a dependent function.
443+
normalizeFunctions(apply(t.dealias), t, expandAlways = true)
435444
case t =>
436445
defaultApply(t)
437446
end toCapturing
438447

439-
val tp1 = toCapturing(tp)
440-
val tp2 = Existential.mapCapInResults(fail)(tp1)
441-
if tp2 ne tp then capt.println(i"expanded explicit in ${ctx.owner}: $tp --> $tp1 --> $tp2")
442-
tp2
448+
def transform(tp: Type): Type =
449+
val tp1 = toCapturing(tp)
450+
val tp2 = Existential.mapCapInResults(fail, toCapturing.keepFunAliases)(tp1)
451+
val snd = if toCapturing.keepFunAliases then "" else " 2nd time"
452+
if tp2 ne tp then capt.println(i"expanded explicit$snd in ${ctx.owner}: $tp --> $tp1 --> $tp2")
453+
tp2
454+
455+
val tp1 = transform(tp)
456+
if toCapturing.keptFunAliases then
457+
toCapturing.keepFunAliases = false
458+
transform(tp1)
459+
else tp1
443460
end transformExplicitType
444461

445462
/** Substitute parameter symbols in `from` to paramRefs in corresponding

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -804,7 +804,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
804804
(tp1.signature consistentParams tp2.signature) &&
805805
matchingMethodParams(tp1, tp2) &&
806806
(!tp2.isImplicitMethod || tp1.isImplicitMethod) &&
807-
CCState.inOpenedFreshBinder(tp2):
807+
CCState.inNewExistentialScope(tp2):
808808
isSubType(tp1.resultType, tp2.resultType.subst(tp2, tp1))
809809
case _ => false
810810
}

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -260,9 +260,9 @@ class PlainPrinter(_ctx: Context) extends Printer {
260260
def isUniversal =
261261
refs.elems.size == 1
262262
&& (refs.isUniversal
263-
|| refs.elems.nth(0).match
263+
|| !printDebug && !showUniqueIds && refs.elems.nth(0).match
264264
case Existential.Vble(binder) =>
265-
CCState.openedFreshBinders match
265+
CCState.openExistentialScopes match
266266
case b :: _ => binder eq b
267267
case _ => false
268268
case _ =>
@@ -301,7 +301,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
301301
~ paramsText(tp)
302302
~ ")"
303303
~ (Str(": ") provided !tp.resultType.isInstanceOf[MethodOrPoly])
304-
~ CCState.inOpenedFreshBinder(tp)(toText(tp.resultType))
304+
~ CCState.inNewExistentialScope(tp)(toText(tp.resultType))
305305
}
306306
case ExprType(restp) =>
307307
def arrowText: Text = restp match
@@ -456,7 +456,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
456456
case MaybeCapability(tp1) => toTextCaptureRef(tp1) ~ "?"
457457
case Existential.Vble(binder) =>
458458
// TODO: Better printing? USe a mode where we print more detailed
459-
val vbleText: Text = CCState.openedFreshBinders.indexOf(binder) match
459+
val vbleText: Text = CCState.openExistentialScopes.indexOf(binder) match
460460
case -1 =>
461461
"<cap of " ~ toText(binder) ~ ">"
462462
case n => "outer_" * n ++ "cap"

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

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -165,9 +165,9 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
165165
val capturesRoot = refs == rootSetText
166166
val isPure =
167167
Feature.pureFunsEnabled && !tsym.name.isImpureFunction && !capturesRoot
168-
toTextFunction(args.init, args.last, refs.provided(!capturesRoot), isContextual, isPure)
168+
toTextFunction(args.init, args.last, tp, refs.provided(!capturesRoot), isContextual, isPure)
169169

170-
private def toTextFunction(args: List[Type], res: Type, refs: Text,
170+
private def toTextFunction(args: List[Type], res: Type, fn: MethodType | AppliedType, refs: Text,
171171
isContextual: Boolean, isPure: Boolean): Text =
172172
changePrec(GlobalPrec):
173173
val argStr: Text = args match
@@ -178,7 +178,10 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
178178
"("
179179
~ argsText(args)
180180
~ ")"
181-
argStr ~ " " ~ arrow(isContextual, isPure) ~ refs ~ " " ~ argText(res)
181+
argStr ~ " " ~ arrow(isContextual, isPure) ~ refs ~ " "
182+
~ fn.match
183+
case fn: MethodType => CCState.inNewExistentialScope(fn)(argText(res))
184+
case _ => argText(res)
182185

183186
protected def toTextMethodAsFunction(info: Type, isPure: Boolean, refs: Text = Str("")): Text =
184187
def recur(tp: Type, enclInfo: MethodType | Null): Text = tp match
@@ -190,8 +193,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
190193
&& !showUniqueIds && !printDebug
191194
then
192195
// cc.Setup converts all functions to dependent functions. Undo that when printing.
193-
CCState.inOpenedFreshBinder(tp):
194-
toTextFunction(tp.paramInfos, tp.resType, refs.provided(!capturesRoot), isContextual, isPure && !capturesRoot)
196+
toTextFunction(tp.paramInfos, tp.resType, tp, refs.provided(!capturesRoot), isContextual, isPure && !capturesRoot)
195197
else
196198
changePrec(GlobalPrec):
197199
"("
@@ -209,7 +211,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
209211
~ recur(tp.resultType, enclInfo)
210212
}
211213
case _ =>
212-
if enclInfo != null then CCState.inOpenedFreshBinder(enclInfo)(toText(tp))
214+
if enclInfo != null then CCState.inNewExistentialScope(enclInfo)(toText(tp))
213215
else toText(tp)
214216
recur(info, null)
215217

‎tests/neg-custom-args/captures/cc-existential-conformance.check

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:8:24 --------------------
2+
8 | val y: A -> Fun[B^] = x // error
3+
| ^
4+
| Found: (x : A -> A -> B^)
5+
| Required: A -> A -> B^{outer_cap}
6+
|
7+
| longer explanation available when compiling with `-explain`

0 commit comments

Comments
 (0)