Skip to content

Commit 21bd994

Browse files
oderskyodersky
committed
Fix mapping of cap to existentials
Still missing: Mapping parameters
1 parent 5c527b6 commit 21bd994

File tree

9 files changed

+233
-71
lines changed

9 files changed

+233
-71
lines changed

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ object ccConfig:
2828
inline val allowUnsoundMaps = false
2929

3030
/** If true, expand capability classes in Setup instead of treating them
31-
* in adapt.
31+
* in adapt.
3232
*/
3333
inline val expandCapabilityInSetup = true
3434

@@ -568,6 +568,7 @@ trait ConservativeFollowAliasMap(using Context) extends TypeMap:
568568
end ConservativeFollowAliasMap
569569

570570
/** An extractor for all kinds of function types as well as method and poly types.
571+
* It includes aliases of function types such as `=>`. TODO: Can we do without?
571572
* @return 1st half: The argument types or empty if this is a type function
572573
* 2nd half: The result type
573574
*/

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

Lines changed: 62 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ import ast.tpd.*
1010
import Decorators.*
1111
import typer.ErrorReporting.errorType
1212
import NameKinds.ExistentialBinderName
13+
import NameOps.isImpureFunction
1314
import reporting.Message
1415

1516
/**
@@ -258,6 +259,13 @@ object Existential:
258259
tp1.derivedAnnotatedType(toCapDeeply(parent), ann)
259260
case _ => tp
260261

262+
/** Knowing that `tp` is a function type, is an alias to a function other
263+
* than `=>`?
264+
*/
265+
private def isAliasFun(tp: Type)(using Context) = tp match
266+
case AppliedType(tycon, _) => !defn.isFunctionSymbol(tycon.typeSymbol)
267+
case _ => false
268+
261269
/** Replace all occurrences of `cap` in parts of this type by an existentially bound
262270
* variable. If there are such occurrences, or there might be in the future due to embedded
263271
* capture set variables, create an existential with the variable wrapping the type.
@@ -266,56 +274,69 @@ object Existential:
266274
def mapCap(tp: Type, fail: Message => Unit)(using Context): Type =
267275
var needsWrap = false
268276

269-
class Wrap(boundVar: TermParamRef) extends BiTypeMap, ConservativeFollowAliasMap:
270-
def apply(t: Type) = // go deep first, so that we map parts of alias types before dealiasing
271-
mapOver(t) match
272-
case t1: TermRef if t1.isRootCapability =>
273-
if variance > 0 then
274-
needsWrap = true
275-
boundVar
276-
else
277-
if variance == 0 then
278-
fail(em"cap appears in invariant position in $tp")
279-
// we accept variance < 0, and leave the cap as it is
280-
t1
281-
case t1 @ FunctionOrMethod(_, _) =>
282-
// These have been mapped before
283-
t1
284-
case t1 @ CapturingType(_, _: CaptureSet.Var) =>
285-
if variance > 0 then needsWrap = true // the set might get a cap later.
286-
t1
287-
case t1 =>
288-
applyToAlias(t, t1)
289-
290-
lazy val inverse = new BiTypeMap with ConservativeFollowAliasMap:
291-
def apply(t: Type) = mapOver(t) match
292-
case t1: TermParamRef if t1 eq boundVar => defn.captureRoot.termRef
293-
case t1 @ FunctionOrMethod(_, _) => t1
294-
case t1 => applyToAlias(t, t1)
277+
abstract class CapMap extends BiTypeMap:
278+
override def mapOver(t: Type): Type = t match
279+
case t @ FunctionOrMethod(args, res) if variance > 0 && !isAliasFun(t) =>
280+
t // `t` should be mapped in this case by a different call to `mapCap`.
281+
case Existential(_, _) =>
282+
t
283+
case t: (LazyRef | TypeVar) =>
284+
mapConserveSuper(t)
285+
case _ =>
286+
super.mapOver(t)
287+
288+
class Wrap(boundVar: TermParamRef) extends CapMap:
289+
def apply(t: Type) = t match
290+
case t: TermRef if t.isRootCapability =>
291+
if variance > 0 then
292+
needsWrap = true
293+
boundVar
294+
else
295+
if variance == 0 then
296+
fail(em"""$tp captures the root capability `cap` in invariant position""")
297+
// we accept variance < 0, and leave the cap as it is
298+
super.mapOver(t)
299+
case t @ CapturingType(parent, refs: CaptureSet.Var) =>
300+
if variance > 0 then needsWrap = true
301+
super.mapOver(t)
302+
case _ =>
303+
mapOver(t)
304+
//.showing(i"mapcap $t = $result")
305+
306+
lazy val inverse = new BiTypeMap:
307+
def apply(t: Type) = t match
308+
case t: TermParamRef if t eq boundVar => defn.captureRoot.termRef
309+
case _ => mapOver(t)
295310
def inverse = Wrap.this
296311
override def toString = "Wrap.inverse"
297312
end Wrap
298313

299314
if ccConfig.useExistentials then
300-
tp match
301-
case Existential(_, _) => tp
302-
case _ =>
303-
val wrapped = apply(Wrap(_)(tp))
304-
if needsWrap then wrapped else tp
315+
val wrapped = apply(Wrap(_)(tp))
316+
if needsWrap then wrapped else tp
305317
else tp
306318
end mapCap
307319

308-
/** Map `cap` to existential in the results of functions or methods.
309-
*/
310-
def mapCapInResult(tp: Type, fail: Message => Unit)(using Context): Type =
311-
def mapCapInFinalResult(tp: Type): Type = tp match
312-
case tp: MethodOrPoly =>
313-
tp.derivedLambdaType(resType = mapCapInFinalResult(tp.resultType))
320+
def mapCapInResults(fail: Message => Unit)(using Context): TypeMap = new:
321+
322+
def mapFunOrMethod(tp: Type, args: List[Type], res: Type): Type =
323+
val args1 = atVariance(-variance)(args.map(this))
324+
val res1 = res match
325+
case res: MethodType => mapFunOrMethod(res, res.paramInfos, res.resType)
326+
case res: PolyType => mapFunOrMethod(res, Nil, res.resType) // TODO: Also map bounds of PolyTypes
327+
case _ => mapCap(apply(res), fail)
328+
tp.derivedFunctionOrMethod(args1, res1)
329+
330+
def apply(t: Type): Type = t match
331+
case FunctionOrMethod(args, res) if variance > 0 && !isAliasFun(t) =>
332+
mapFunOrMethod(t, args, res)
333+
case CapturingType(parent, refs) =>
334+
t.derivedCapturingType(this(parent), refs)
335+
case t: (LazyRef | TypeVar) =>
336+
mapConserveSuper(t)
314337
case _ =>
315-
mapCap(tp, fail)
316-
tp match
317-
case tp: MethodOrPoly => mapCapInFinalResult(tp)
318-
case _ => tp
338+
mapOver(t)
339+
end mapCapInResults
319340

320341
/** Is `mt` a method represnting an existential type when used in a refinement? */
321342
def isExistentialMethod(mt: TermLambda)(using Context): Boolean = mt.paramInfos match

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

Lines changed: 16 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -269,12 +269,9 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
269269
end transformInferredType
270270

271271
private def transformExplicitType(tp: Type, tptToCheck: Option[Tree] = None)(using Context): Type =
272-
val expandAliases = new DeepTypeMap:
272+
val toCapturing = new DeepTypeMap:
273273
override def toString = "expand aliases"
274274

275-
def fail(msg: Message) =
276-
for tree <- tptToCheck do report.error(msg, tree.srcPos)
277-
278275
/** Expand $throws aliases. This is hard-coded here since $throws aliases in stdlib
279276
* are defined with `?=>` rather than `?->`.
280277
* We also have to add a capture set to the last expanded throws alias. I.e.
@@ -314,23 +311,20 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
314311
t.derivedAnnotatedType(parent1, ann)
315312
case throwsAlias(res, exc) =>
316313
this(expandThrowsAlias(res, exc, Nil))
317-
case t: LazyRef =>
318-
val t1 = this(t.ref)
319-
if t1 ne t.ref then t1 else t
320-
case t: TypeVar =>
321-
this(t.underlying)
322314
case t =>
323-
Existential.mapCapInResult(
324-
// Map references to capability classes C to C^
325-
if ccConfig.expandCapabilityInSetup && t.derivesFromCapability && t.typeSymbol != defn.Caps_Exists
326-
then CapturingType(t, CaptureSet.universal, boxed = false)
327-
else normalizeCaptures(mapOver(t)),
328-
fail)
329-
end expandAliases
330-
331-
val tp1 = expandAliases(tp) // TODO: Do we still need to follow aliases?
332-
if tp1 ne tp then capt.println(i"expanded in ${ctx.owner}: $tp --> $tp1")
333-
tp1
315+
// Map references to capability classes C to C^
316+
if ccConfig.expandCapabilityInSetup && t.derivesFromCapability && t.typeSymbol != defn.Caps_Exists
317+
then CapturingType(t, CaptureSet.universal, boxed = false)
318+
else normalizeCaptures(mapOver(t))
319+
end toCapturing
320+
321+
def fail(msg: Message) =
322+
for tree <- tptToCheck do report.error(msg, tree.srcPos)
323+
324+
val tp1 = toCapturing(tp)
325+
val tp2 = Existential.mapCapInResults(fail)(tp1)
326+
if tp2 ne tp then capt.println(i"expanded in ${ctx.owner}: $tp --> $tp1 --> $tp2")
327+
tp2
334328
end transformExplicitType
335329

336330
/** Transform type of type tree, and remember the transformed type as the type the tree */
@@ -538,9 +532,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
538532

539533
if sym.exists && signatureChanges then
540534
val newInfo =
541-
Existential.mapCapInResult(
542-
integrateRT(sym.info, sym.paramSymss, localReturnType, Nil, Nil),
543-
report.error(_, tree.srcPos))
535+
Existential.mapCapInResults(report.error(_, tree.srcPos)):
536+
integrateRT(sym.info, sym.paramSymss, localReturnType, Nil, Nil)
544537
.showing(i"update info $sym: ${sym.info} = $result", capt)
545538
if newInfo ne sym.info then
546539
val updatedInfo =

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1161,6 +1161,8 @@ class Definitions {
11611161
if mt.hasErasedParams then RefinedType(PolyFunctionClass.typeRef, nme.apply, mt)
11621162
else FunctionNOf(args, resultType, isContextual)
11631163

1164+
// Unlike PolyFunctionOf and RefinedFunctionOf this extractor follows aliases.
1165+
// Can we do without? Same for FunctionNOf and isFunctionNType.
11641166
def unapply(ft: Type)(using Context): Option[(List[Type], Type, Boolean)] = {
11651167
ft match
11661168
case PolyFunctionOf(mt: MethodType) =>

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

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6273,6 +6273,15 @@ object Types extends TypeUtils {
62736273
try derivedCapturingType(tp, this(parent), refs.map(this))
62746274
finally variance = saved
62756275

6276+
/** Utility method. Maps the supertype of a type proxy. Returns the
6277+
* type proxy itself if the mapping leaves the supertype unchanged.
6278+
* This avoids needless changes in mapped types.
6279+
*/
6280+
protected def mapConserveSuper(t: TypeProxy): Type =
6281+
val t1 = t.superType
6282+
val t2 = apply(t1)
6283+
if t2 ne t1 then t2 else t
6284+
62766285
/** Map this function over given type */
62776286
def mapOver(tp: Type): Type = {
62786287
record(s"TypeMap mapOver ${getClass}")

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,8 @@
88
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylist.scala:35:29 -------------------------------------
99
35 | val ref1c: LazyList[Int] = ref1 // error
1010
| ^^^^
11-
| Found: (ref1 : lazylists.LazyCons[Int]{val xs: () ->{cap1} lazylists.LazyList[Int]^?}^{cap1})
12-
| Required: lazylists.LazyList[Int]
11+
| Found: lazylists.LazyCons[Int]{val xs: () ->{cap1} lazylists.LazyList[Int]^?}^{ref1}
12+
| Required: lazylists.LazyList[Int]
1313
|
1414
| longer explanation available when compiling with `-explain`
1515
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylist.scala:37:36 -------------------------------------
@@ -29,8 +29,8 @@
2929
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylist.scala:41:48 -------------------------------------
3030
41 | val ref4c: LazyList[Int]^{cap1, ref3, cap3} = ref4 // error
3131
| ^^^^
32-
| Found: (ref4 : lazylists.LazyList[Int]^{cap3, cap2, ref1, cap1})
33-
| Required: lazylists.LazyList[Int]^{cap1, ref3, cap3}
32+
| Found: (ref4 : lazylists.LazyList[Int]^{cap3, cap2, ref1})
33+
| Required: lazylists.LazyList[Int]^{cap1, ref3, cap3}
3434
|
3535
| longer explanation available when compiling with `-explain`
3636
-- [E164] Declaration Error: tests/neg-custom-args/captures/lazylist.scala:22:6 ----------------------------------------

‎tests/neg/existential-mapping.check

Lines changed: 88 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,88 @@
1+
-- Error: tests/neg/existential-mapping.scala:44:13 --------------------------------------------------------------------
2+
44 | val z1: A^ => Array[C^] = ??? // error
3+
| ^^^^^^^^^^^^^^^
4+
| Array[box C^] captures the root capability `cap` in invariant position
5+
-- [E007] Type Mismatch Error: tests/neg/existential-mapping.scala:9:25 ------------------------------------------------
6+
9 | val _: (x: C^) -> C = x1 // error
7+
| ^^
8+
| Found: (x1 : (x: C^) -> (ex$3: caps.Exists) -> C^{ex$3})
9+
| Required: (x: C^) -> C
10+
|
11+
| longer explanation available when compiling with `-explain`
12+
-- [E007] Type Mismatch Error: tests/neg/existential-mapping.scala:12:20 -----------------------------------------------
13+
12 | val _: C^ -> C = x2 // error
14+
| ^^
15+
| Found: (x2 : C^ -> (ex$9: caps.Exists) -> C^{ex$9})
16+
| Required: C^ -> C
17+
|
18+
| longer explanation available when compiling with `-explain`
19+
-- [E007] Type Mismatch Error: tests/neg/existential-mapping.scala:15:30 -----------------------------------------------
20+
15 | val _: A^ -> (x: C^) -> C = x3 // error
21+
| ^^
22+
| Found: (x3 : A^ -> (x: C^) -> (ex$15: caps.Exists) -> C^{ex$15})
23+
| Required: A^ -> (x: C^) -> C
24+
|
25+
| longer explanation available when compiling with `-explain`
26+
-- [E007] Type Mismatch Error: tests/neg/existential-mapping.scala:18:25 -----------------------------------------------
27+
18 | val _: A^ -> C^ -> C = x4 // error
28+
| ^^
29+
| Found: (x4 : A^ -> C^ -> (ex$25: caps.Exists) -> C^{ex$25})
30+
| Required: A^ -> C^ -> C
31+
|
32+
| longer explanation available when compiling with `-explain`
33+
-- [E007] Type Mismatch Error: tests/neg/existential-mapping.scala:21:30 -----------------------------------------------
34+
21 | val _: A^ -> (x: C^) -> C = x5 // error
35+
| ^^
36+
| Found: (x5 : A^ -> (ex$35: caps.Exists) -> Fun[C^{ex$35}])
37+
| Required: A^ -> (x: C^) -> C
38+
|
39+
| longer explanation available when compiling with `-explain`
40+
-- [E007] Type Mismatch Error: tests/neg/existential-mapping.scala:24:30 -----------------------------------------------
41+
24 | val _: A^ -> (x: C^) => C = x6 // error
42+
| ^^
43+
| Found: (x6 : A^ -> (ex$43: caps.Exists) -> IFun[C^{ex$43}])
44+
| Required: A^ -> (ex$48: caps.Exists) -> (x: C^) ->{ex$48} C
45+
|
46+
| longer explanation available when compiling with `-explain`
47+
-- [E007] Type Mismatch Error: tests/neg/existential-mapping.scala:27:25 -----------------------------------------------
48+
27 | val _: (x: C^) => C = y1 // error
49+
| ^^
50+
| Found: (y1 : (x: C^) => (ex$54: caps.Exists) -> C^{ex$54})
51+
| Required: (x: C^) => C
52+
|
53+
| longer explanation available when compiling with `-explain`
54+
-- [E007] Type Mismatch Error: tests/neg/existential-mapping.scala:30:20 -----------------------------------------------
55+
30 | val _: C^ => C = y2 // error
56+
| ^^
57+
| Found: (y2 : C^ => (ex$60: caps.Exists) -> C^{ex$60})
58+
| Required: C^ => C
59+
|
60+
| longer explanation available when compiling with `-explain`
61+
-- [E007] Type Mismatch Error: tests/neg/existential-mapping.scala:33:30 -----------------------------------------------
62+
33 | val _: A^ => (x: C^) => C = y3 // error
63+
| ^^
64+
| Found: (y3 : A^ => (ex$67: caps.Exists) -> (x: C^) ->{ex$67} (ex$66: caps.Exists) -> C^{ex$66})
65+
| Required: A^ => (ex$78: caps.Exists) -> (x: C^) ->{ex$78} C
66+
|
67+
| longer explanation available when compiling with `-explain`
68+
-- [E007] Type Mismatch Error: tests/neg/existential-mapping.scala:36:25 -----------------------------------------------
69+
36 | val _: A^ => C^ => C = y4 // error
70+
| ^^
71+
| Found: (y4 : A^ => C^ => (ex$84: caps.Exists) -> C^{ex$84})
72+
| Required: A^ => C^ => C
73+
|
74+
| longer explanation available when compiling with `-explain`
75+
-- [E007] Type Mismatch Error: tests/neg/existential-mapping.scala:39:30 -----------------------------------------------
76+
39 | val _: A^ => (x: C^) -> C = y5 // error
77+
| ^^
78+
| Found: (y5 : A^ => (ex$94: caps.Exists) -> Fun[C^{ex$94}])
79+
| Required: A^ => (x: C^) -> C
80+
|
81+
| longer explanation available when compiling with `-explain`
82+
-- [E007] Type Mismatch Error: tests/neg/existential-mapping.scala:42:30 -----------------------------------------------
83+
42 | val _: A^ => (x: C^) => C = y6 // error
84+
| ^^
85+
| Found: (y6 : A^ => (ex$102: caps.Exists) -> IFun[C^{ex$102}])
86+
| Required: A^ => (ex$107: caps.Exists) -> (x: C^) ->{ex$107} C
87+
|
88+
| longer explanation available when compiling with `-explain`

‎tests/neg/existential-mapping.scala

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
import language.experimental.captureChecking
2+
3+
class A
4+
class C
5+
type Fun[X] = (x: C^) -> X
6+
type IFun[X] = (x: C^) => X
7+
def Test =
8+
val x1: (x: C^) -> C^ = ???
9+
val _: (x: C^) -> C = x1 // error
10+
11+
val x2: C^ -> C^ = ???
12+
val _: C^ -> C = x2 // error
13+
14+
val x3: A^ -> (x: C^) -> C^ = ???
15+
val _: A^ -> (x: C^) -> C = x3 // error
16+
17+
val x4: A^ -> C^ -> C^ = ???
18+
val _: A^ -> C^ -> C = x4 // error
19+
20+
val x5: A^ -> Fun[C^] = ???
21+
val _: A^ -> (x: C^) -> C = x5 // error
22+
23+
val x6: A^ -> IFun[C^] = ???
24+
val _: A^ -> (x: C^) => C = x6 // error
25+
26+
val y1: (x: C^) => C^ = ???
27+
val _: (x: C^) => C = y1 // error
28+
29+
val y2: C^ => C^ = ???
30+
val _: C^ => C = y2 // error
31+
32+
val y3: A^ => (x: C^) => C^ = ???
33+
val _: A^ => (x: C^) => C = y3 // error
34+
35+
val y4: A^ => C^ => C^ = ???
36+
val _: A^ => C^ => C = y4 // error
37+
38+
val y5: A^ => Fun[C^] = ???
39+
val _: A^ => (x: C^) -> C = y5 // error
40+
41+
val y6: A^ => IFun[C^] = ???
42+
val _: A^ => (x: C^) => C = y6 // error
43+
44+
val z1: A^ => Array[C^] = ??? // error
45+
46+
47+

0 commit comments

Comments
 (0)