Skip to content

Commit 825f0e9

Browse files
committed
Widen type parameters before box adaptation
1 parent ee2f641 commit 825f0e9

File tree

4 files changed

+84
-4
lines changed

4 files changed

+84
-4
lines changed

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

Lines changed: 49 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ import typer.Inferencing.isFullyDefined
1515
import typer.RefChecks.{checkAllOverrides, checkSelfAgainstParents, OverridingPairsChecker}
1616
import typer.Checking.{checkBounds, checkAppliedTypesIn}
1717
import typer.ErrorReporting.{Addenda, NothingToAdd, err}
18-
import typer.ProtoTypes.{LhsProto, WildcardSelectionProto}
18+
import typer.ProtoTypes.{LhsProto, WildcardSelectionProto, SelectionProto}
1919
import util.{SimpleIdentitySet, EqHashMap, EqHashSet, SrcPos, Property}
2020
import transform.{Recheck, PreRecheck, CapturedVars}
2121
import Recheck.*
@@ -1309,17 +1309,61 @@ class CheckCaptures extends Recheck, SymTransformer:
13091309
override def checkConformsExpr(actual: Type, expected: Type, tree: Tree, addenda: Addenda)(using Context): Type =
13101310
testAdapted(actual, expected, tree, addenda)(err.typeMismatch)
13111311

1312+
@annotation.tailrec
1313+
private def widenNamed(tp: Type)(using Context): Type = tp match
1314+
case stp: SingletonType => widenNamed(stp.widen)
1315+
case ntp: NamedType => ntp.info match
1316+
case info: TypeBounds => widenNamed(info.hi)
1317+
case _ => tp
1318+
case _ => tp
1319+
13121320
inline def testAdapted(actual: Type, expected: Type, tree: Tree, addenda: Addenda)
13131321
(fail: (Tree, Type, Addenda) => Unit)(using Context): Type =
1322+
13141323
var expected1 = alignDependentFunction(expected, actual.stripCapturing)
13151324
val falseDeps = expected1 ne expected
1316-
val actualBoxed = adapt(actual, expected1, tree)
1325+
val actual1 =
1326+
if expected.stripCapturing.isInstanceOf[SelectionProto] then
1327+
// If the expected type is a `SelectionProto`, we should be careful about cases when
1328+
// the actual type is a type parameter (for instance, `X <: box IO^`).
1329+
// If `X` were not widen to reveal the boxed type, both sides are unboxed and thus
1330+
// no box adaptation happens. But it is unsound: selecting a member from `X` implicitly
1331+
// unboxes the value.
1332+
//
1333+
// Therefore, when the expected type is a selection proto, we conservatively widen
1334+
// the actual type to strip type parameters.
1335+
widenNamed(actual)
1336+
else actual
1337+
val actualBoxed = adapt(actual1, expected1, tree)
13171338
//println(i"check conforms $actualBoxed <<< $expected1")
13181339

13191340
if actualBoxed eq actual then
13201341
// Only `addOuterRefs` when there is no box adaptation
13211342
expected1 = addOuterRefs(expected1, actual, tree.srcPos)
1322-
TypeComparer.compareResult(isCompatible(actualBoxed, expected1)) match
1343+
1344+
def tryCurrentType: Boolean =
1345+
isCompatible(actualBoxed, expected1)
1346+
1347+
/** When the actual type is a named type, and the previous attempt failed, try to widen the named type
1348+
* and try another time.
1349+
*
1350+
* This is useful for cases like:
1351+
*
1352+
* def id[X <: box IO^{a}](x: X): IO^{a} = x
1353+
*
1354+
* When typechecking the body, we need to show that `(x: X)` can be typed at `IO^{a}`.
1355+
* In the first attempt, since `X` is simply a parameter reference, we treat it as non-boxed and perform
1356+
* no box adptation. But its upper bound is in fact boxed, and adaptation is needed for typechecking the body.
1357+
* In those cases, we widen such types and try box adaptation another time.
1358+
*/
1359+
def tryWidenNamed: Boolean =
1360+
val actual1 = widenNamed(actual)
1361+
(actual1 ne actual) && {
1362+
val actualBoxed1 = adapt(actual1, expected1, tree)
1363+
isCompatible(actualBoxed1, expected1)
1364+
}
1365+
1366+
TypeComparer.compareResult(tryCurrentType || tryWidenNamed) match
13231367
case TypeComparer.CompareResult.Fail(notes) =>
13241368
capt.println(i"conforms failed for ${tree}: $actual vs $expected")
13251369
if falseDeps then expected1 = unalignFunction(expected1)
@@ -1477,7 +1521,8 @@ class CheckCaptures extends Recheck, SymTransformer:
14771521
(actualShape, CaptureSet())
14781522
end adaptShape
14791523

1480-
def adaptStr = i"adapting $actual ${if covariant then "~~>" else "<~~"} $expected"
1524+
//val adaptStr = i"adapting $actual ${if covariant then "~~>" else "<~~"} $expected"
1525+
//println(adaptStr)
14811526

14821527
// Get wildcards out of the way
14831528
expected match
Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23746.scala:5:2 -----------------------------------------
2+
5 | () => op.run() // error
3+
| ^^^^^^^^^^^^^^
4+
| Found: () => Unit
5+
| Required: () -> Unit
6+
|
7+
| Note that capability cap is not included in capture set {}.
8+
|
9+
| where: => refers to a fresh root capability in the type of type X
10+
| cap is a fresh root capability in the type of type X
11+
|
12+
| longer explanation available when compiling with `-explain`
13+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23746.scala:10:4 ----------------------------------------
14+
10 | () => op.run() // error
15+
| ^^^^^^^^^^^^^^
16+
| Found: () ->{a} Unit
17+
| Required: () -> Unit
18+
|
19+
| Note that capability a is not included in capture set {}.
20+
|
21+
| longer explanation available when compiling with `-explain`
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
import language.experimental.captureChecking
2+
trait Op:
3+
def run(): Unit
4+
def helper[X <: Op^](op: X): () -> Unit =
5+
() => op.run() // error
6+
def test1(a: Op^): Unit =
7+
def foo[X <: Op^{a}](op: X): () ->{a} Unit =
8+
() => op.run() // ok
9+
def bar[X <: Op^{a}](op: X): () ->{} Unit =
10+
() => op.run() // error
Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
import language.experimental.captureChecking
2+
trait IO
3+
def main(a: IO^): Unit =
4+
def foo[X <: IO^{a}](x: X): IO^{a} = x // now ok

0 commit comments

Comments
 (0)