Skip to content

Commit f6407e3

Browse files
oderskyodersky
committed
WIP: Turn on box-aware subtyping
1 parent f12f221 commit f6407e3

File tree

14 files changed

+132
-31
lines changed

14 files changed

+132
-31
lines changed

‎compiler/src/dotty/tools/dotc/config/Config.scala

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -245,4 +245,6 @@ object Config {
245245
* cases, though.
246246
*/
247247
inline val ccAllowUnsoundMaps = false
248+
249+
@annotation.internal.sharable var checkBoxes = true
248250
}

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1650,8 +1650,8 @@ class Definitions {
16501650
def isFunctionType(tp: Type)(using Context): Boolean =
16511651
isNonRefinedFunction(tp.dropDependentRefinement)
16521652

1653-
def isFunctionOrPolyType(tp: RefinedType)(using Context): Boolean =
1654-
isFunctionType(tp) || (tp.parent.typeSymbol eq defn.PolyFunctionClass)
1653+
def isFunctionOrPolyType(tp: Type)(using Context): Boolean =
1654+
isFunctionType(tp) || (tp.typeSymbol eq defn.PolyFunctionClass)
16551655

16561656
private def withSpecMethods(cls: ClassSymbol, bases: List[Name], paramTypes: Set[TypeRef]) =
16571657
for base <- bases; tp <- paramTypes do

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

Lines changed: 10 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ import typer.ProtoTypes.constrained
2323
import typer.Applications.productSelectorTypes
2424
import reporting.trace
2525
import annotation.constructorOnly
26-
import cc.{CapturingType, derivedCapturingType, CaptureSet, stripCapturing}
26+
import cc.{CapturingType, derivedCapturingType, CaptureSet, stripCapturing, isBoxedCapturing}
2727

2828
/** Provides methods to compare types.
2929
*/
@@ -514,10 +514,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
514514
// loop for a very long time without the recursion brake.
515515

516516
case CapturingType(parent1, refs1) =>
517-
if subCaptures(refs1, tp2.captureSet, frozenConstraint).isOK then
518-
recur(parent1, tp2)
519-
else
520-
thirdTry
517+
if subCaptures(refs1, tp2.captureSet, frozenConstraint).isOK && sameBoxed(tp1, tp2, refs1)
518+
then recur(parent1, tp2)
519+
else thirdTry
521520
case tp1: AnnotatedType if !tp1.isRefining =>
522521
recur(tp1.parent, tp2)
523522
case tp1: MatchType =>
@@ -803,6 +802,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
803802
try
804803
if refs1.isAlwaysEmpty then recur(tp1, parent2)
805804
else subCaptures(refs1, refs2, frozenConstraint).isOK
805+
&& sameBoxed(tp1, tp2, refs1)
806806
&& recur(tp1.widen.stripCapturing, parent2)
807807
catch case ex: AssertionError =>
808808
println(i"assertion failed while compare captured $tp1 <:< $tp2")
@@ -2554,6 +2554,11 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
25542554
protected def subCaptures(refs1: CaptureSet, refs2: CaptureSet, frozen: Boolean)(using Context): CaptureSet.CompareResult.Type =
25552555
refs1.subCaptures(refs2, frozen)
25562556

2557+
protected def sameBoxed(tp1: Type, tp2: Type, refs: CaptureSet)(using Context): Boolean =
2558+
!Config.checkBoxes
2559+
|| (tp1.isBoxedCapturing == tp2.isBoxedCapturing)
2560+
|| refs.subCaptures(CaptureSet.empty, frozenConstraint).isOK
2561+
25572562
// ----------- Diagnostics --------------------------------------------------
25582563

25592564
/** A hook for showing subtype traces. Overridden in ExplainingTypeComparer */

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

Lines changed: 60 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ import Phases.*, DenotTransformers.*, SymDenotations.*
77
import Contexts.*, Names.*, Flags.*, Symbols.*, Decorators.*
88
import Types.*, StdNames.*
99
import config.Printers.{capt, recheckr}
10+
import config.Config
1011
import ast.{tpd, untpd, Trees}
1112
import Trees.*
1213
import typer.RefChecks.{checkAllOverrides, checkParents}
@@ -120,7 +121,9 @@ class CheckCaptures extends Recheck, SymTransformer:
120121
// ^^^ TODO: Can we avoid doing overrides checks twice?
121122
// We need to do them here since only at this phase CaptureTypes are relevant
122123
// But maybe we can then elide the check during the RefChecks phase if -Ycc is set?
124+
Config.checkBoxes = false // !!!
123125
checkAllOverrides(ctx.owner.asClass)
126+
Config.checkBoxes = true // !!!
124127
case _ =>
125128
traverseChildren(t)
126129

@@ -529,12 +532,63 @@ class CheckCaptures extends Recheck, SymTransformer:
529532
expected.derivedCapturingType(ecore, erefs1)
530533
case _ =>
531534
expected
532-
val actual1 = adaptBoxed(actual, expected1, covariant = true)
533-
//println(i"check conforms $actual <<< $expected1")
534-
super.checkConformsExpr(actual1, expected1, tree)
535-
536-
def adaptBoxed(actual: Type, expected: Type, covariant: Boolean)(using Context): Type =
537-
actual
535+
val normActual = adaptBoxed(actual, expected1, tree.srcPos)
536+
//println(i"check conforms $actual1 <<< $expected1")
537+
super.checkConformsExpr(normActual, expected1, tree)
538+
539+
/** Adapt `actual` type to `expected` type by inserting boxing and unboxing conversions */
540+
def adaptBoxed(actual: Type, expected: Type, pos: SrcPos)(using Context): Type =
541+
542+
def adaptFun(actual: Type, aargs: List[Type], ares: Type, expected: Type,
543+
covariant: Boolean,
544+
reconstruct: (List[Type], Type) => Type): Type =
545+
val (eargs, eres) = expected.dealias match
546+
case defn.FunctionOf(eargs, eres, _, _) => (eargs, eres)
547+
case _ => (aargs.map(_ => WildcardType), WildcardType)
548+
val aargs1 = aargs.zipWithConserve(eargs)(adapt(_, _, !covariant))
549+
val ares1 = adapt(ares, eres, covariant)
550+
if (ares1 eq ares) && (aargs1 eq aargs) then actual
551+
else reconstruct(aargs1, ares1)
552+
553+
def adapt(actual: Type, expected: Type, covariant: Boolean): Type = actual.dealias match
554+
case actual @ CapturingType(parent, refs) =>
555+
val parent1 = adapt(parent, expected, covariant)
556+
if actual.isBoxed != expected.isBoxedCapturing then
557+
val uni = if covariant then refs.isUniversal else expected.captureSet.isUniversal
558+
if uni then // TODO: better to constrain the set to be not universal
559+
capt.println(i"ABORTING $actual vs $expected")
560+
actual
561+
else
562+
if covariant == actual.isBoxed then includeBoxedCaptures(refs, pos)
563+
CapturingType(parent1, refs, boxed = !actual.isBoxed)
564+
else if parent1 eq parent then actual
565+
else CapturingType(parent1, refs, boxed = actual.isBoxed)
566+
case actual @ AppliedType(tycon, args) if defn.isNonRefinedFunction(actual) =>
567+
adaptFun(actual, args.init, args.last, expected, covariant,
568+
(aargs1, ares1) => actual.derivedAppliedType(tycon, aargs1 :+ ares1))
569+
case actual @ RefinedType(_, _, rinfo: MethodType) if defn.isFunctionType(actual) =>
570+
adaptFun(actual, rinfo.paramInfos, rinfo.resType, expected, covariant,
571+
(aargs1, ares1) =>
572+
rinfo.derivedLambdaType(paramInfos = aargs1, resType = ares1)
573+
.toFunctionType(isJava = false, alwaysDependent = true))
574+
case _ => actual
575+
576+
if Config.checkBoxes then
577+
var actualw = actual.widenDealias
578+
actual match
579+
case ref: CaptureRef if ref.isTracked =>
580+
actualw match
581+
case CapturingType(p, refs) =>
582+
actualw = actualw.derivedCapturingType(p, ref.singletonCaptureSet)
583+
case _ =>
584+
case _ =>
585+
val adapted = adapt(actualw, expected, covariant = true)
586+
if adapted ne actualw then
587+
capt.println(i"adapt boxed $actual vs $expected ===> $adapted")
588+
adapted
589+
else actual
590+
else actual
591+
end adaptBoxed
538592

539593
override def checkUnit(unit: CompilationUnit)(using Context): Unit =
540594
Setup(preRecheckPhase, thisPhase, recheckDef)

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

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -38,9 +38,16 @@
3838
|
3939
| longer explanation available when compiling with `-explain`
4040
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:31:24 ----------------------------------------
41-
31 | val z2 = h[() -> Cap](() => x)(() => C()) // error
41+
31 | val z2 = h[() -> Cap](() => x) // error
4242
| ^^^^^^^
43-
| Found: {x} () -> Cap
43+
| Found: {x} () -> {*} C
4444
| Required: () -> box {*} C
4545
|
4646
| longer explanation available when compiling with `-explain`
47+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:32:5 -----------------------------------------
48+
32 | (() => C()) // error
49+
| ^^^^^^^^^
50+
| Found: ? () -> {*} C
51+
| Required: () -> box {*} C
52+
|
53+
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/capt1.scala

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,8 @@ def h4(x: Cap, y: Int): A =
2828
def foo() =
2929
val x: C @retains(*) = ???
3030
def h[X](a: X)(b: X) = a
31-
val z2 = h[() -> Cap](() => x)(() => C()) // error
31+
val z2 = h[() -> Cap](() => x) // error
32+
(() => C()) // error
3233
val z3 = h[(() -> Cap) @retains(x)](() => x)(() => C()) // ok
3334
val z4 = h[(() -> Cap) @retains(x)](() => x)(() => C()) // what was inferred for z3
3435

‎tests/neg-custom-args/captures/curried-simplified.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/curried-simplified.scala:9:28 ----------------------------
99
9 | def y2: () -> () => Int = x2 // error
1010
| ^^
11-
| Found: {x} () -> () => Int
11+
| Found: {x} () -> {*} () -> Int
1212
| Required: () -> () => Int
1313
|
1414
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/i15749a.scala

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
class Unit
2+
object unit extends Unit
3+
4+
type Top = {*} Any
5+
6+
type Wrapper[T] = [X] -> (op: {*} T -> X) -> X
7+
8+
def test =
9+
10+
def wrapper[T](x: T): Wrapper[T] =
11+
[X] => (op: {*} T -> X) => op(x)
12+
13+
def strictMap[A <: Top, B <: Top](mx: Wrapper[A])(f: {*} A -> B): Wrapper[B] =
14+
mx((x: A) => wrapper(f(x)))
15+
16+
def force[A](thunk: {*} Unit -> A): A = thunk(unit)
17+
18+
def forceWrapper[A](mx: Wrapper[{*} Unit -> A]): Wrapper[A] =
19+
// Γ ⊢ mx: Wrapper[□ {*} Unit => A]
20+
// `force` should be typed as ∀(□ {*} Unit -> A) A, but it can not
21+
strictMap[{*} Unit -> A, A](mx)(t => force[A](t)) // error

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

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,16 @@
1-
-- Error: tests/neg-custom-args/captures/try.scala:24:3 ----------------------------------------------------------------
2-
22 | val a = handle[Exception, CanThrow[Exception]] {
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:22:49 ------------------------------------------
2+
22 | val a = handle[Exception, CanThrow[Exception]] { // error !!! was for 2nd arg
3+
| ^
4+
| Found: ? ({*} CT[Exception]) -> {*} CT[? >: box ? Exception <: box ? Exception]
5+
| Required: CanThrow[Exception] => box {*} CT[Exception]
36
23 | (x: CanThrow[Exception]) => x
4-
24 | }{ // error
5-
| ^
6-
| The expression's type box {*} CT[Exception] is not allowed to capture the root capability `*`.
7-
| This usually means that a capability persists longer than its allowed lifetime.
8-
25 | (ex: Exception) => ???
9-
26 | }
7+
24 | }{
8+
|
9+
| longer explanation available when compiling with `-explain`
1010
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/try.scala:28:43 ------------------------------------------
1111
28 | val b = handle[Exception, () -> Nothing] { // error
1212
| ^
13-
| Found: ? (x: CanThrow[Exception]) -> {x} () -> ? Nothing
13+
| Found: ? (x: {*} CT[Exception]) -> {x} () -> ? Nothing
1414
| Required: CanThrow[Exception] => () -> Nothing
1515
29 | (x: CanThrow[Exception]) => () => raise(new Exception)(using x)
1616
30 | } {

‎tests/neg-custom-args/captures/try.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,9 +19,9 @@ def handle[E <: Exception, R <: Top](op: CanThrow[E] => R)(handler: E => R): R =
1919
catch case ex: E => handler(ex)
2020

2121
def test =
22-
val a = handle[Exception, CanThrow[Exception]] {
22+
val a = handle[Exception, CanThrow[Exception]] { // error !!! was for 2nd arg
2323
(x: CanThrow[Exception]) => x
24-
}{ // error
24+
}{
2525
(ex: Exception) => ???
2626
}
2727

0 commit comments

Comments
 (0)