Skip to content

Commit 04b3e29

Browse files
oderskyodersky
committed
Use different scheme for preventing mapping to Result
1 parent a92e444 commit 04b3e29

File tree

7 files changed

+93
-88
lines changed

7 files changed

+93
-88
lines changed

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

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1252,14 +1252,11 @@ object Capabilities:
12521252
def toResultInResults(sym: Symbol, fail: Message => Unit, keepAliases: Boolean = false)(tp: Type)(using Context): Type =
12531253
val m = new TypeMap with FollowAliasesMap:
12541254
def apply(t: Type): Type = t match
1255-
case AnnotatedType(parent @ defn.RefinedFunctionOf(mt), ann) if ann.symbol == defn.InferredDepFunAnnot =>
1256-
val mt1 = mapOver(mt).asInstanceOf[MethodType]
1257-
if mt1 ne mt then mt1.toFunctionType(alwaysDependent = true)
1258-
else parent
1259-
case defn.RefinedFunctionOf(mt) =>
1260-
val mt1 = apply(mt)
1261-
if mt1 ne mt then mt1.toFunctionType(alwaysDependent = true)
1262-
else t
1255+
case rt @ defn.RefinedFunctionOf(mt) =>
1256+
rt.derivedRefinedType(refinedInfo =
1257+
if rt.isInstanceOf[InferredRefinedType]
1258+
then mapOver(mt)
1259+
else apply(mt))
12631260
case t: MethodType if variance > 0 && t.marksExistentialScope =>
12641261
val t1 = mapOver(t).asInstanceOf[MethodType]
12651262
t1.derivedLambdaType(resType = toResult(t1.resType, t1, fail))

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

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -193,11 +193,12 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
193193
case AppliedType(`tycon`, args0) => args0.last ne args.last
194194
case _ => false
195195
if expand then
196-
val fn = depFun(
196+
val (fn: RefinedType) = depFun(
197197
args.init, args.last,
198198
isContextual = defn.isContextFunctionClass(tycon.classSymbol))
199199
.showing(i"add function refinement $tp ($tycon, ${args.init}, ${args.last}) --> $result", capt)
200-
AnnotatedType(fn, Annotation(defn.InferredDepFunAnnot, util.Spans.NoSpan))
200+
.runtimeChecked
201+
RefinedType.inferred(fn.parent, fn.refinedName, fn.refinedInfo)
201202
else tp
202203
case _ => tp
203204

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

Lines changed: 19 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3268,12 +3268,14 @@ object Types extends TypeUtils {
32683268

32693269
def checkInst(using Context): this.type = this // debug hook
32703270

3271+
def newLikeThis(parent: Type, refinedName: Name, refinedInfo: Type)(using Context): Type =
3272+
RefinedType(parent, refinedName, refinedInfo)
3273+
32713274
final def derivedRefinedType
32723275
(parent: Type = this.parent, refinedName: Name = this.refinedName, refinedInfo: Type = this.refinedInfo)
32733276
(using Context): Type =
32743277
if ((parent eq this.parent) && (refinedName eq this.refinedName) && (refinedInfo eq this.refinedInfo)) this
3275-
else if isPrecise then RefinedType.precise(parent, refinedName, refinedInfo)
3276-
else RefinedType(parent, refinedName, refinedInfo)
3278+
else newLikeThis(parent, refinedName, refinedInfo)
32773279

32783280
/** Add this refinement to `parent`, provided `refinedName` is a member of `parent`. */
32793281
def wrapIfMember(parent: Type)(using Context): Type =
@@ -3308,6 +3310,17 @@ object Types extends TypeUtils {
33083310
class PreciseRefinedType(parent: Type, refinedName: Name, refinedInfo: Type)
33093311
extends RefinedType(parent, refinedName, refinedInfo):
33103312
override def isPrecise = true
3313+
override def newLikeThis(parent: Type, refinedName: Name, refinedInfo: Type)(using Context): Type =
3314+
PreciseRefinedType(parent, refinedName, refinedInfo)
3315+
3316+
/** Used for refined function types created at cc/Setup that come from original
3317+
* generic function types. Function types of this class don't get their result
3318+
* captures mapped from FreshCaps to ResultCaps with toResult.
3319+
*/
3320+
class InferredRefinedType(parent: Type, refinedName: Name, refinedInfo: Type)
3321+
extends RefinedType(parent, refinedName, refinedInfo):
3322+
override def newLikeThis(parent: Type, refinedName: Name, refinedInfo: Type)(using Context): Type =
3323+
InferredRefinedType(parent, refinedName, refinedInfo)
33113324

33123325
object RefinedType {
33133326
@tailrec def make(parent: Type, names: List[Name], infos: List[Type])(using Context): Type =
@@ -3322,6 +3335,10 @@ object Types extends TypeUtils {
33223335
def precise(parent: Type, name: Name, info: Type)(using Context): RefinedType =
33233336
assert(!ctx.erasedTypes)
33243337
unique(new PreciseRefinedType(parent, name, info)).checkInst
3338+
3339+
def inferred(parent: Type, name: Name, info: Type)(using Context): RefinedType =
3340+
assert(!ctx.erasedTypes)
3341+
unique(new InferredRefinedType(parent, name, info)).checkInst
33253342
}
33263343

33273344
/** A recursive type. Instances should be constructed via the companion object.

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

Lines changed: 28 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -1,60 +1,56 @@
11
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:8:24 --------------------
22
8 | val y: A -> Fun[B^] = x // error
33
| ^
4-
| Found: (x : A -> (x²: A) -> B^)
5-
| Required: A -> A -> B^²
4+
| Found: (x : A -> (x²: A) -> B^)
5+
| Required: A -> A -> B^²
66
|
7-
| Note that capability cap is not included in capture set {cap²}
8-
| because cap is not visible from cap² in value y.
7+
| Note that capability cap is not included in capture set {cap²}
8+
| because cap is not visible from cap² in value y.
99
|
10-
| where: ^ and cap refer to a root capability associated with the result type of (x²: A): B^
11-
| ^² and cap² refer to a fresh root capability in the type of value y
12-
| x is a value in method test
13-
| x² is a reference to a value parameter
10+
| where: ^ refers to a root capability associated with the result type of (x²: A): B^
11+
| ^² and cap² refer to a fresh root capability in the type of value y
12+
| cap is the universal root capability
13+
| x is a value in method test
14+
| x² is a reference to a value parameter
1415
|
1516
| longer explanation available when compiling with `-explain`
1617
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:9:29 --------------------
1718
9 | val z: A -> (x: A) -> B^ = y // error
1819
| ^
19-
| Found: A -> A -> B^{y*}
20-
| Required: A -> (x: A) -> B^
20+
| Found: A -> A -> B^{y*}
21+
| Required: A -> (x: A) -> B^
2122
|
22-
| Note that capability y* is not included in capture set {cap}.
23+
| Note that capability y* is not included in capture set {cap}.
2324
|
24-
| Note that the existential capture root in B^²
25-
| cannot subsume the capability y* since that capability is not a `Sharable` capability..
26-
|
27-
| where: ^ and cap refer to a root capability associated with the result type of (x: A): B^
28-
| ^² refers to the universal root capability
25+
| where: ^ refers to a root capability associated with the result type of (x: A): B^
26+
| cap is the universal root capability
2927
|
3028
| longer explanation available when compiling with `-explain`
3129
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:13:19 -------------------
3230
13 | val y: Fun[B^] = x // error
3331
| ^
34-
| Found: (x : (x²: A) -> B^)
35-
| Required: A -> B^²
32+
| Found: (x : (x²: A) -> B^)
33+
| Required: A -> B^²
3634
|
37-
| Note that capability cap is not included in capture set {cap²}
38-
| because cap is not visible from cap² in value y.
35+
| Note that capability cap is not included in capture set {cap²}
36+
| because cap is not visible from cap² in value y.
3937
|
40-
| where: ^ and cap refer to a root capability associated with the result type of (x²: A): B^
41-
| ^² and cap² refer to a fresh root capability in the type of value y
42-
| x is a value in method test2
43-
| x² is a reference to a value parameter
38+
| where: ^ refers to a root capability associated with the result type of (x²: A): B^
39+
| ^² and cap² refer to a fresh root capability in the type of value y
40+
| cap is the universal root capability
41+
| x is a value in method test2
42+
| x² is a reference to a value parameter
4443
|
4544
| longer explanation available when compiling with `-explain`
4645
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-existential-conformance.scala:14:24 -------------------
4746
14 | val z: (x: A) -> B^ = y // error
4847
| ^
49-
| Found: A -> B^{y*}
50-
| Required: (x: A) -> B^
51-
|
52-
| Note that capability y* is not included in capture set {cap}.
48+
| Found: A -> B^{y*}
49+
| Required: (x: A) -> B^
5350
|
54-
| Note that the existential capture root in B^²
55-
| cannot subsume the capability y* since that capability is not a `Sharable` capability..
51+
| Note that capability y* is not included in capture set {cap}.
5652
|
57-
| where: ^ and cap refer to a root capability associated with the result type of (x: A): B^
58-
| ^² refers to the universal root capability
53+
| where: ^ refers to a root capability associated with the result type of (x: A): B^
54+
| cap is the universal root capability
5955
|
6056
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/scoped-caps.check‎

Lines changed: 25 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
11
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:7:20 -----------------------------------
22
7 | val g: A^ -> B^ = f // error
33
| ^
4-
| Found: (f : (x: A^) -> B^²)
5-
| Required: A^ -> B^³
4+
| Found: (f : (x: A^) -> B^²)
5+
| Required: A^ -> B^³
66
|
7-
| Note that capability cap is not included in capture set {cap²}
8-
| because cap is not visible from cap² in value g.
7+
| Note that capability cap is not included in capture set {cap²}
8+
| because cap is not visible from cap² in value g.
99
|
10-
| where: ^ refers to the universal root capability
11-
| ^² and cap refer to a root capability associated with the result type of (x: A^): B^²
12-
| ^³ and cap² refer to a fresh root capability in the type of value g
10+
| where: ^ and cap refer to the universal root capability
11+
| ^² refers to a root capability associated with the result type of (x: A^): B^²
12+
| ^³ and cap² refer to a fresh root capability in the type of value g
1313
|
1414
| longer explanation available when compiling with `-explain`
1515
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:9:25 -----------------------------------
@@ -20,25 +20,22 @@
2020
|
2121
| Note that capability g* is not included in capture set {cap}.
2222
|
23-
| Note that the existential capture root in B^
24-
| cannot subsume the capability g* since that capability is not a `Sharable` capability..
25-
|
26-
| where: ^ refers to the universal root capability
27-
| ^² and cap refer to a root capability associated with the result type of (x: A^): B^²
23+
| where: ^ and cap refer to the universal root capability
24+
| ^² refers to a root capability associated with the result type of (x: A^): B^²
2825
|
2926
| longer explanation available when compiling with `-explain`
3027
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:10:20 ----------------------------------
3128
10 | val _: A^ -> B^ = f // error
3229
| ^
33-
| Found: (f : (x: A^) -> B^²)
34-
| Required: A^ -> B^³
30+
| Found: (f : (x: A^) -> B^²)
31+
| Required: A^ -> B^³
3532
|
36-
| Note that capability cap is not included in capture set {cap²}
37-
| because cap is not visible from cap² in value _$3.
33+
| Note that capability cap is not included in capture set {cap²}
34+
| because cap is not visible from cap² in value _$3.
3835
|
39-
| where: ^ refers to the universal root capability
40-
| ^² and cap refer to a root capability associated with the result type of (x: A^): B^²
41-
| ^³ and cap² refer to a fresh root capability in the type of value _$3
36+
| where: ^ and cap refer to the universal root capability
37+
| ^² refers to a root capability associated with the result type of (x: A^): B^²
38+
| ^³ and cap² refer to a fresh root capability in the type of value _$3
4239
|
4340
| longer explanation available when compiling with `-explain`
4441
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:12:20 ----------------------------------
@@ -63,25 +60,22 @@
6360
|
6461
| Note that capability h* is not included in capture set {cap}.
6562
|
66-
| Note that the existential capture root in B^
67-
| cannot subsume the capability h* since that capability is not a `Sharable` capability..
68-
|
69-
| where: ^ refers to the universal root capability
70-
| ^² and cap refer to a root capability associated with the result type of (x: S^): B^²
63+
| where: ^ and cap refer to the universal root capability
64+
| ^² refers to a root capability associated with the result type of (x: S^): B^²
7165
|
7266
| longer explanation available when compiling with `-explain`
7367
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:26:19 ----------------------------------
7468
26 | val _: S -> B^ = j // error
7569
| ^
76-
| Found: (j : (x: S) -> B^)
77-
| Required: S^² -> B^³
70+
| Found: (j : (x: S) -> B^)
71+
| Required: S^² -> B^³
7872
|
79-
| Note that capability cap is not included in capture set {cap²}
80-
| because cap is not visible from cap² in value _$13.
73+
| Note that capability cap is not included in capture set {cap²}
74+
| because cap is not visible from cap² in value _$13.
8175
|
82-
| where: ^ and cap refer to a root capability associated with the result type of (x: S^²): B^
83-
| ^² refers to the universal root capability
84-
| ^³ and cap² refer to a fresh root capability in the type of value _$13
76+
| where: ^ refers to a root capability associated with the result type of (x: S^²): B^
77+
| ^² and cap refer to the universal root capability
78+
| ^³ and cap² refer to a fresh root capability in the type of value _$13
8579
|
8680
| longer explanation available when compiling with `-explain`
8781
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps.scala:27:25 ----------------------------------

‎tests/neg-custom-args/captures/scoped-caps2.check‎

Lines changed: 8 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,15 @@
11
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps2.scala:5:23 ----------------------------------
22
5 | val _: (x: C) => C = b // error
33
| ^
4-
| Found: (b : C => C)
5-
| Required: (x: C^) =>² C^²
4+
| Found: (b : C => C)
5+
| Required: (x: C^) =>² C^²
66
|
7-
| Note that the existential capture root in C^
8-
| cannot subsume the capability cap..
7+
| Note that capability cap is not included in capture set {cap²}.
98
|
10-
| Note that capability cap² is not included in capture set {cap³}.
11-
|
12-
| where: => and cap² refer to a fresh root capability in the type of value b
13-
| =>² and cap³ refer to a fresh root capability in the type of value _$1
14-
| ^ refers to the universal root capability
15-
| ^² refers to a root capability associated with the result type of (x: C^): C^²
16-
| cap is a fresh root capability classified as SharedCapability in the type of value b
9+
| where: => and cap refer to a fresh root capability in the type of value b
10+
| =>² and cap² refer to a fresh root capability in the type of value _$1
11+
| ^ refers to the universal root capability
12+
| ^² refers to a root capability associated with the result type of (x: C^): C^²
1713
|
1814
| longer explanation available when compiling with `-explain`
1915
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps2.scala:6:18 ----------------------------------
@@ -54,9 +50,8 @@
5450
| Note that capability cap is not included in capture set {cap²}
5551
| because cap is not visible from cap² in value _$6.
5652
|
57-
| where: ^ refers to the universal root capability
53+
| where: ^ and cap refer to the universal root capability
5854
| ^² and cap² refer to a fresh root capability classified as SharedCapability in the type of value _$6
59-
| cap is a root capability associated with the result type of (x: C^): C^³
6055
|
6156
| longer explanation available when compiling with `-explain`
6257
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps2.scala:16:29 ---------------------------------

‎tests/pos-custom-args/captures/ascribe-apply.scala‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
def test(): Unit =
2+
val fun = ??? : (() -> Object^)
3+
val l = fun() // Since `fun` is pure we get `l: Object` with the APPLY rule
4+
val _: Object = l
5+

0 commit comments

Comments
 (0)