Skip to content

Commit

Permalink
Expand aliases when mapping explicit types in Setup
Browse files Browse the repository at this point in the history
This is necessary because the compiler is free in previous phases to dealias or not.
Therefore, capture checking should not depend on aliasing. The main difference is that
now arguments to type aliases are not necessarily boxed. They are boxed only if they need
boxing in the dealiased type.
  • Loading branch information
odersky committed Dec 31, 2024
1 parent 8049a9d commit eae9c07
Show file tree
Hide file tree
Showing 16 changed files with 68 additions and 53 deletions.
2 changes: 1 addition & 1 deletion compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ object ccConfig:
Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.6`)

def followAliases(using Context): Boolean =
Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`)
Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.6`)
end ccConfig

/** Are we at checkCaptures phase? */
Expand Down
2 changes: 1 addition & 1 deletion tests/neg-custom-args/captures/boundschecks2.scala
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,6 @@ object test {

val foo: C[Tree^] = ??? // error
type T = C[Tree^] // error
val bar: T -> T = ???
//val bar: T -> T = ??? // --> boundschecks3.scala for what happens if we uncomment
val baz: C[Tree^] -> Unit = ??? // error
}
4 changes: 4 additions & 0 deletions tests/neg-custom-args/captures/boundschecks3.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
-- Error: tests/neg-custom-args/captures/boundschecks3.scala:11:13 -----------------------------------------------------
11 | val bar: T -> T = ??? // error, since `T` is expanded here. But the msg is not very good.
| ^^^^^^
| test.C[box test.Tree^] captures the root capability `cap` in invariant position
13 changes: 13 additions & 0 deletions tests/neg-custom-args/captures/boundschecks3.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
object test {

class Tree

def f[X <: Tree](x: X): Unit = ()

class C[X <: Tree](x: X)

val foo: C[Tree^] = ??? // hidden error
type T = C[Tree^] // hidden error
val bar: T -> T = ??? // error, since `T` is expanded here. But the msg is not very good.
val baz: C[Tree^] -> Unit = ??? // hidden error
}
10 changes: 5 additions & 5 deletions tests/neg-custom-args/captures/box-adapt-cov.scala
Original file line number Diff line number Diff line change
@@ -1,14 +1,14 @@
trait Cap

def test1(io: Cap^) = {
type Op[X] = [T] -> Unit -> X
class Op[+X](val value: [T] -> Unit -> X)
val f: Op[Cap^{io}] = ???
val x: [T] -> Unit -> Cap^{io} = f // error
val x: [T] -> Unit -> Cap^{io} = f.value // error
}

def test2(io: Cap^) = {
type Op[X] = [T] -> Unit -> X^{io}
class Op[+X](val value: [T] -> Unit -> X^{io})
val f: Op[Cap^{io}] = ???
val x: Unit -> Cap^{io} = f[Unit] // error
val x1: Unit ->{io} Cap^{io} = f[Unit] // ok
val x: Unit -> Cap^{io} = f.value[Unit] // error
val x1: Unit ->{io} Cap^{io} = f.value[Unit] // ok
}
12 changes: 6 additions & 6 deletions tests/neg-custom-args/captures/box-adapt-depfun.scala
Original file line number Diff line number Diff line change
@@ -1,23 +1,23 @@
trait Cap { def use(): Int }

def test1(io: Cap^): Unit = {
type Id[X] = [T] -> (op: X ->{io} T) -> T
class Id[X](val value: [T] -> (op: X ->{io} T) -> T)

val x: Id[Cap]^{io} = ???
x(cap => cap.use()) // ok
x.value(cap => cap.use()) // ok
}

def test2(io: Cap^): Unit = {
type Id[X] = [T] -> (op: (x: X) ->{io} T) -> T
class Id[X](val value: [T] -> (op: (x: X) ->{io} T) -> T)

val x: Id[Cap^{io}] = ???
x(cap => cap.use())
x.value(cap => cap.use())
// should work when the expected type is a dependent function
}

def test3(io: Cap^): Unit = {
type Id[X] = [T] -> (op: (x: X) ->{} T) -> T
class Id[X](val value: [T] -> (op: (x: X) ->{} T) -> T)

val x: Id[Cap^{io}] = ???
x(cap => cap.use()) // error
x.value(cap => cap.use()) // error
}
8 changes: 4 additions & 4 deletions tests/neg-custom-args/captures/box-adapt-typefun.scala
Original file line number Diff line number Diff line change
@@ -1,13 +1,13 @@
trait Cap { def use(): Int }

def test1(io: Cap^): Unit = {
type Op[X] = [T] -> X -> Unit
class Op[X](val value: [T] -> X -> Unit)
val f: [T] -> (Cap^{io}) -> Unit = ???
val op: Op[Cap^{io}] = f // error
val op: Op[Cap^{io}] = Op(f) // was error, now ok
}

def test2(io: Cap^): Unit = {
type Lazy[X] = [T] -> Unit -> X
class Lazy[X](val value: [T] -> Unit -> X)
val f: Lazy[Cap^{io}] = ???
val test: [T] -> Unit -> (Cap^{io}) = f // error
val test: [T] -> Unit -> (Cap^{io}) = f.value // error
}
12 changes: 6 additions & 6 deletions tests/neg-custom-args/captures/capt1.check
Original file line number Diff line number Diff line change
Expand Up @@ -36,15 +36,15 @@
-- Error: tests/neg-custom-args/captures/capt1.scala:34:16 -------------------------------------------------------------
34 | val z2 = h[() -> Cap](() => x) // error // error
| ^^^^^^^^^
| Type variable X of method h cannot be instantiated to () -> box C^ since
| the part box C^ of that type captures the root capability `cap`.
| Type variable X of method h cannot be instantiated to () -> (ex$15: caps.Exists) -> C^{ex$15} since
| the part C^{ex$15} of that type captures the root capability `cap`.
-- Error: tests/neg-custom-args/captures/capt1.scala:34:30 -------------------------------------------------------------
34 | val z2 = h[() -> Cap](() => x) // error // error
| ^
| reference (x : C^) is not included in the allowed capture set {}
| of an enclosing function literal with expected type () -> box C^
| reference (x : C^) is not included in the allowed capture set {}
| of an enclosing function literal with expected type () -> (ex$15: caps.Exists) -> C^{ex$15}
-- Error: tests/neg-custom-args/captures/capt1.scala:36:13 -------------------------------------------------------------
36 | val z3 = h[(() -> Cap) @retains(x)](() => x)(() => C()) // error
| ^^^^^^^^^^^^^^^^^^^^^^^
| Type variable X of method h cannot be instantiated to box () ->{x} Cap since
| the part Cap of that type captures the root capability `cap`.
| Type variable X of method h cannot be instantiated to box () ->{x} (ex$20: caps.Exists) -> C^{ex$20} since
| the part C^{ex$20} of that type captures the root capability `cap`.
2 changes: 1 addition & 1 deletion tests/neg-custom-args/captures/explain-under-approx.check
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
| Found: Future[Int]{val a: (async : Async)}^{async}
| Required: Future[Int]^{col.futs*}
|
| Note that reference ex$25.type
| Note that reference ex$22.type
| cannot be included in outer capture set {cap}
|
| longer explanation available when compiling with `-explain`
Expand Down
4 changes: 2 additions & 2 deletions tests/neg-custom-args/captures/i15922.scala
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@


trait Cap { def use(): Int }
type Id[X] = [T] -> (op: X => T) -> T
def mkId[X](x: X): Id[X] = [T] => (op: X => T) => op(x)
class Id[+X](val value: [T] -> (op: X => T) -> T)
def mkId[X](x: X): Id[X] = Id([T] => (op: X => T) => op(x))

def withCap[X](op: (Cap^) => X): X = {
val cap: Cap^ = new Cap { def use() = { println("cap is used"); 0 } }
Expand Down
6 changes: 3 additions & 3 deletions tests/neg-custom-args/captures/i16725.scala
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,11 @@ class IO extends caps.Capability:
def brewCoffee(): Unit = ???
def usingIO[T](op: IO => T): T = ???

type Wrapper[T] = [R] -> (f: T => R) -> R
def mk[T](x: T): Wrapper[T] = [R] => f => f(x)
class Wrapper[T](val value: [R] -> (f: T => R) -> R)
def mk[T](x: T): Wrapper[T] = Wrapper([R] => f => f(x))
def useWrappedIO(wrapper: Wrapper[IO]): () -> Unit =
() =>
wrapper: io => // error
wrapper.value: io => // error
io.brewCoffee()
def main(): Unit =
val escaped = usingIO(io => useWrappedIO(mk(io))) // error
Expand Down
2 changes: 1 addition & 1 deletion tests/neg-custom-args/captures/i19330.check
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,6 @@
22 | val bad: bar.T = foo(bar) // error
| ^^^^^^^^
| Found: () => Logger^
| Required: () ->{fresh} Logger^{fresh}
| Required: () ->{fresh} (ex$9: caps.Exists) -> Logger^{ex$9}
|
| longer explanation available when compiling with `-explain`
8 changes: 4 additions & 4 deletions tests/neg-custom-args/captures/i21401.check
Original file line number Diff line number Diff line change
Expand Up @@ -11,8 +11,8 @@
-- Error: tests/neg-custom-args/captures/i21401.scala:16:66 ------------------------------------------------------------
16 | val leaked: [R, X <: Boxed[IO^] -> R] -> (op: X) -> R = usingIO[Res](mkRes) // error
| ^^^
| Type variable R of method usingIO cannot be instantiated to Res since
| the part box IO^ of that type captures the root capability `cap`.
| Type variable R of method usingIO cannot be instantiated to [R, X <: Boxed[box IO^] -> R] => (op: X) -> R since
| the part box IO^ of that type captures the root capability `cap`.
-- Error: tests/neg-custom-args/captures/i21401.scala:17:29 ------------------------------------------------------------
17 | val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error
| ^^^^^^^^^^
Expand All @@ -21,8 +21,8 @@
-- Error: tests/neg-custom-args/captures/i21401.scala:17:52 ------------------------------------------------------------
17 | val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) // error // error
| ^^^^^^^^^^^^^^^^^^^^^^^^
|Type variable X of value leaked cannot be instantiated to Boxed[box IO^] -> (ex$18: caps.Exists) -> Boxed[box IO^{ex$18}] since
|the part box IO^{ex$18} of that type captures the root capability `cap`.
|Type variable X of value leaked cannot be instantiated to Boxed[box IO^] -> (ex$20: caps.Exists) -> Boxed[box IO^{ex$20}] since
|the part box IO^{ex$20} of that type captures the root capability `cap`.
-- Error: tests/neg-custom-args/captures/i21401.scala:18:21 ------------------------------------------------------------
18 | val y: IO^{x*} = x.unbox // error
| ^^^^^^^
Expand Down
2 changes: 1 addition & 1 deletion tests/neg/cc-ex-conformance.scala
Original file line number Diff line number Diff line change
Expand Up @@ -21,5 +21,5 @@ def Test =
val ex3: EX3 = ???
val ex4: EX4 = ???
val _: EX4 = ex3 // ok
val _: EX4 = ex4
val _: EX4 = ex4 // error (???) Probably since we also introduce existentials on expansion
val _: EX3 = ex4 // error
24 changes: 12 additions & 12 deletions tests/neg/existential-mapping.check
Original file line number Diff line number Diff line change
Expand Up @@ -33,56 +33,56 @@
-- [E007] Type Mismatch Error: tests/neg/existential-mapping.scala:21:30 -----------------------------------------------
21 | val _: A^ -> (x: C^) -> C = x5 // error
| ^^
| Found: (x5 : A^ -> (ex$27: caps.Exists) -> Fun[C^{ex$27}])
| Found: (x5 : A^ -> (x: C^) -> (ex$27: caps.Exists) -> C^{ex$27})
| Required: A^ -> (x: C^) -> C
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/existential-mapping.scala:24:30 -----------------------------------------------
24 | val _: A^ -> (x: C^) => C = x6 // error
| ^^
| Found: (x6 : A^ -> (ex$33: caps.Exists) -> (x: C^) ->{fresh} C^{ex$33})
| Required: A^ -> (ex$36: caps.Exists) -> (x: C^) ->{ex$36} C
| Found: (x6 : A^ -> (ex$36: caps.Exists) -> (x: C^) ->{ex$36} (ex$35: caps.Exists) -> C^{ex$35})
| Required: A^ -> (ex$39: caps.Exists) -> (x: C^) ->{ex$39} C
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/existential-mapping.scala:27:25 -----------------------------------------------
27 | val _: (x: C^) => C = y1 // error
| ^^
| Found: (y1 : (x: C^) ->{fresh} (ex$38: caps.Exists) -> C^{ex$38})
| Found: (y1 : (x: C^) ->{fresh} (ex$41: caps.Exists) -> C^{ex$41})
| Required: (x: C^) ->{fresh} C
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/existential-mapping.scala:30:20 -----------------------------------------------
30 | val _: C^ => C = y2 // error
| ^^
| Found: (y2 : C^ ->{fresh} (ex$42: caps.Exists) -> C^{ex$42})
| Found: (y2 : C^ ->{fresh} (ex$45: caps.Exists) -> C^{ex$45})
| Required: C^ ->{fresh} C
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/existential-mapping.scala:33:30 -----------------------------------------------
33 | val _: A^ => (x: C^) => C = y3 // error
| ^^
| Found: (y3 : A^ ->{fresh} (ex$47: caps.Exists) -> (x: C^) ->{ex$47} (ex$46: caps.Exists) -> C^{ex$46})
| Required: A^ ->{fresh} (ex$50: caps.Exists) -> (x: C^) ->{ex$50} C
| Found: (y3 : A^ ->{fresh} (ex$50: caps.Exists) -> (x: C^) ->{ex$50} (ex$49: caps.Exists) -> C^{ex$49})
| Required: A^ ->{fresh} (ex$53: caps.Exists) -> (x: C^) ->{ex$53} C
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/existential-mapping.scala:36:25 -----------------------------------------------
36 | val _: A^ => C^ => C = y4 // error
| ^^
| Found: (y4 : A^ ->{fresh} (ex$53: caps.Exists) -> C^ ->{ex$53} (ex$52: caps.Exists) -> C^{ex$52})
| Required: A^ ->{fresh} (ex$56: caps.Exists) -> C^ ->{ex$56} C
| Found: (y4 : A^ ->{fresh} (ex$56: caps.Exists) -> C^ ->{ex$56} (ex$55: caps.Exists) -> C^{ex$55})
| Required: A^ ->{fresh} (ex$59: caps.Exists) -> C^ ->{ex$59} C
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/existential-mapping.scala:39:30 -----------------------------------------------
39 | val _: A^ => (x: C^) -> C = y5 // error
| ^^
| Found: (y5 : A^ ->{fresh} (ex$58: caps.Exists) -> Fun[C^{ex$58}])
| Found: (y5 : A^ ->{fresh} (x: C^) -> (ex$61: caps.Exists) -> C^{ex$61})
| Required: A^ ->{fresh} (x: C^) -> C
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/existential-mapping.scala:42:30 -----------------------------------------------
42 | val _: A^ => (x: C^) => C = y6 // error
| ^^
| Found: (y6 : A^ ->{fresh} (ex$64: caps.Exists) -> (x: C^) ->{fresh} C^{ex$64})
| Required: A^ ->{fresh} (ex$67: caps.Exists) -> (x: C^) ->{ex$67} C
| Found: (y6 : A^ ->{fresh} (ex$70: caps.Exists) -> (x: C^) ->{ex$70} (ex$69: caps.Exists) -> C^{ex$69})
| Required: A^ ->{fresh} (ex$73: caps.Exists) -> (x: C^) ->{ex$73} C
|
| longer explanation available when compiling with `-explain`
Original file line number Diff line number Diff line change
Expand Up @@ -6,19 +6,17 @@ object u extends Unit

type Top = Any^

type Wrapper[+T] = [X] -> (op: T ->{cap} X) -> X
class Wrapper[+T](val value: [X] -> (op: T ->{cap} X) -> X)

def test =

def wrapper[T](x: T): Wrapper[T] =
def wrapper[T](x: T): Wrapper[T] = Wrapper:
[X] => (op: T ->{cap} X) => op(x)

def strictMap[A <: Top, B <: Top](mx: Wrapper[A])(f: A ->{cap} B): Wrapper[B] =
mx((x: A) => wrapper(f(x)))
mx.value((x: A) => wrapper(f(x)))

def force[A](thunk: Unit ->{cap} A): A = thunk(u)

def forceWrapper[A](@use mx: Wrapper[Unit ->{cap} A]): Wrapper[A] =
// Γ ⊢ mx: Wrapper[□ {cap} Unit => A]
// `force` should be typed as ∀(□ {cap} Unit -> A) A, but it can not
strictMap[Unit ->{mx*} A, A](mx)(t => force[A](t)) // error // should work
strictMap[Unit ->{mx*} A, A](mx)(t => force[A](t)) // was error when Wrapper was an alias type

0 comments on commit eae9c07

Please sign in to comment.