Skip to content

Commit 3ad3660

Browse files
committed
Simplify Existential.mapCapInResults
1 parent d77b3c1 commit 3ad3660

File tree

7 files changed

+38
-43
lines changed

7 files changed

+38
-43
lines changed

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

Lines changed: 9 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -372,28 +372,23 @@ object Existential:
372372
end mapCap
373373

374374
/** Map `cap` in function results to fresh existentials */
375-
def mapCapInResults(fail: Message => Unit)(using Context): TypeMap = new:
376-
377-
def mapFunOrMethod(tp: Type, args: List[Type], res: Type): Type =
378-
val args1 = atVariance(-variance)(args.map(this))
379-
val res1 = res match
380-
case res: MethodType => mapFunOrMethod(res, res.paramInfos, res.resType)
381-
case res: PolyType => mapFunOrMethod(res, Nil, res.resType) // TODO: Also map bounds of PolyTypes
382-
case _ => mapCap(apply(res), fail)
383-
//.showing(i"map cap res $res / ${apply(res)} of $tp = $result")
384-
tp.derivedFunctionOrMethod(args1, res1)
385-
375+
def mapCapInResults(fail: Message => Unit)(using Context): TypeMap = new TypeMap with FollowAliasesMap:
386376
def apply(t: Type): Type = t match
387-
case FunctionOrMethod(args, res) if variance > 0 && !isAliasFun(t) =>
388-
mapFunOrMethod(t, args, res)
377+
case defn.RefinedFunctionOf(mt) =>
378+
val mt1 = apply(mt)
379+
if mt1 ne mt then mt1.toFunctionType(alwaysDependent = true)
380+
else t
381+
case t: MethodType if variance > 0 && !t.resType.isInstanceOf[MethodOrPoly] =>
382+
val t1 = mapOver(t).asInstanceOf[MethodType]
383+
t1.derivedLambdaType(resType = mapCap(t1.resType, fail))
389384
case CapturingType(parent, refs) =>
390385
t.derivedCapturingType(this(parent), refs)
391386
case Existential(_, _) =>
392387
t
393388
case t: (LazyRef | TypeVar) =>
394389
mapConserveSuper(t)
395390
case _ =>
396-
mapOver(t)
391+
mapFollowingAliases(t)
397392
end mapCapInResults
398393

399394
/** Is `mt` a method represnting an existential type when used in a refinement? */

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 () -> (ex$18: caps.Exists) -> C^{ex$18} since
40-
| the part C^{ex$18} of that type captures the root capability `cap`.
39+
| Type variable X of method h cannot be instantiated to () -> (ex$14: caps.Exists) -> C^{ex$14} since
40+
| the part C^{ex$14} 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 () -> (ex$18: caps.Exists) -> C^{ex$18}
45+
| of an enclosing function literal with expected type () -> (ex$14: caps.Exists) -> C^{ex$14}
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} (ex$23: caps.Exists) -> C^{ex$23} since
50-
| the part C^{ex$23} of that type captures the root capability `cap`.
49+
| Type variable X of method h cannot be instantiated to box () ->{x} (ex$19: caps.Exists) -> C^{ex$19} since
50+
| the part C^{ex$19} 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 () => (ex$27: caps.Exists) -> C^{ex$27}.
55+
| of value z1 with type () => (ex$23: caps.Exists) -> C^{ex$23}.
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 () => (ex$27: caps.Exists) -> C^{ex$27}.
61+
| of value z1 with type () => (ex$23: caps.Exists) -> C^{ex$23}.
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 () => (ex$27: caps.Exists) -> C^{ex$27}.
67+
| of value z1 with type () => (ex$23: caps.Exists) -> C^{ex$23}.
6868
| This type hides capabilities {x}

tests/neg-custom-args/captures/depfun-reach.check

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,14 +2,14 @@
22
13 | op // error
33
| ^^
44
| Found: (xs: List[(X, box () ->{io} Unit)]) ->{op} List[box () ->{xs*} Unit]
5-
| Required: (xs: List[(X, box () ->{io} Unit)]) ->{fresh} List[() -> Unit]
5+
| Required: (xs: List[(X, box () ->{io} Unit)]) => List[() -> Unit]
66
|
77
| longer explanation available when compiling with `-explain`
88
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/depfun-reach.scala:20:60 ---------------------------------
99
20 | val b: (xs: List[() ->{io} Unit]) => List[() ->{} Unit] = a // error
1010
| ^
1111
| Found: (xs: List[box () ->{io} Unit]) ->{a} List[box () ->{xs*} Unit]
12-
| Required: (xs: List[box () ->{io} Unit]) ->{fresh} List[() -> Unit]
12+
| Required: (xs: List[box () ->{io} Unit]) => List[() -> Unit]
1313
|
1414
| longer explanation available when compiling with `-explain`
1515
-- Error: tests/neg-custom-args/captures/depfun-reach.scala:12:17 ------------------------------------------------------

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

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -19,70 +19,70 @@
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^) -> (ex$11: caps.Exists) -> C^{ex$11})
22+
| Found: (x3 : A^ -> (x: C^) -> (ex$9: caps.Exists) -> C^{ex$9})
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^ -> (ex$19: caps.Exists) -> C^{ex$19})
29+
| Found: (x4 : A^ -> C^ -> (ex$17: caps.Exists) -> C^{ex$17})
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^) -> (ex$27: caps.Exists) -> C^{ex$27})
36+
| Found: (x5 : A^ -> (x: C^) -> (ex$23: caps.Exists) -> C^{ex$23})
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^ -> (ex$36: caps.Exists) -> (x: C^) ->{ex$36} (ex$35: caps.Exists) -> C^{ex$35})
44-
| Required: A^ -> (ex$39: caps.Exists) -> (x: C^) ->{ex$39} C
43+
| Found: (x6 : A^ -> (ex$32: caps.Exists) -> (x: C^) ->{ex$32} (ex$31: caps.Exists) -> C^{ex$31})
44+
| Required: A^ -> (ex$35: caps.Exists) -> (x: C^) ->{ex$35} 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} (ex$41: caps.Exists) -> C^{ex$41})
50+
| Found: (y1 : (x: C^) ->{fresh} (ex$37: caps.Exists) -> C^{ex$37})
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} (ex$45: caps.Exists) -> C^{ex$45})
57+
| Found: (y2 : C^ ->{fresh} (ex$41: caps.Exists) -> C^{ex$41})
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} (ex$50: caps.Exists) -> (x: C^) ->{ex$50} (ex$49: caps.Exists) -> C^{ex$49})
65-
| Required: A^ ->{fresh} (ex$53: caps.Exists) -> (x: C^) ->{ex$53} C
64+
| Found: (y3 : A^ ->{fresh} (ex$44: caps.Exists) -> (x: C^) ->{ex$44} (ex$43: caps.Exists) -> C^{ex$43})
65+
| Required: A^ ->{fresh} (ex$47: caps.Exists) -> (x: C^) ->{ex$47} 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} (ex$56: caps.Exists) -> C^ ->{ex$56} (ex$55: caps.Exists) -> C^{ex$55})
72-
| Required: A^ ->{fresh} (ex$59: caps.Exists) -> C^ ->{ex$59} C
71+
| Found: (y4 : A^ ->{fresh} (ex$50: caps.Exists) -> C^ ->{ex$50} (ex$49: caps.Exists) -> C^{ex$49})
72+
| Required: A^ ->{fresh} (ex$52: caps.Exists) -> C^ ->{ex$52} 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^) -> (ex$61: caps.Exists) -> C^{ex$61})
78+
| Found: (y5 : A^ ->{fresh} (x: C^) -> (ex$54: caps.Exists) -> C^{ex$54})
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} (ex$70: caps.Exists) -> (x: C^) ->{ex$70} (ex$69: caps.Exists) -> C^{ex$69})
86-
| Required: A^ ->{fresh} (ex$73: caps.Exists) -> (x: C^) ->{ex$73} C
85+
| Found: (y6 : A^ ->{fresh} (ex$63: caps.Exists) -> (x: C^) ->{ex$63} (ex$62: caps.Exists) -> C^{ex$62})
86+
| Required: A^ ->{fresh} (ex$66: caps.Exists) -> (x: C^) ->{ex$66} C
8787
|
8888
| longer explanation available when compiling with `-explain`

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,11 +7,11 @@
77
22 | val bad: bar.T = foo(bar) // error
88
| ^^^^^^^^
99
| Found: () => Logger^
10-
| Required: () ->{fresh} (ex$9: caps.Exists) -> Logger^{ex$9}
10+
| Required: () ->{fresh} (ex$7: caps.Exists) -> Logger^{ex$7}
1111
|
1212
| longer explanation available when compiling with `-explain`
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 () => (ex$5: caps.Exists) -> Logger^{ex$5} hides parameter l.
16+
| Separation failure: value t's type () => (ex$3: caps.Exists) -> Logger^{ex$3} 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^] -> (ex$20: caps.Exists) -> Boxed[box IO^{ex$20}] since
25-
|the part box IO^{ex$20} of that type captures the root capability `cap`.
24+
|Type variable X of value leaked cannot be instantiated to Boxed[box IO^] -> (ex$14: caps.Exists) -> Boxed[box IO^{ex$14}] since
25+
|the part box IO^{ex$14} of that type captures the root capability `cap`.

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
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*} (ex$16: caps.Exists) -> box Logger{val f: File^{_$1}}^{ex$16.rd, _$1}
11+
|Found: (_$1: box File^{files*}) ->{files*} (ex$14: caps.Exists) -> box Logger{val f: File^{_$1}}^{ex$14.rd, _$1}
1212
|Required: (_$1: box File^{files*}) => box Logger{val f: File^?}^?
1313
|
1414
|Note that the universal capability `cap.rd`

0 commit comments

Comments
 (0)