scala3
scala3 copied to clipboard
scala
Existential Capabilities
The design has changed quite a bit relative to https://github.com/scala/scala3/pull/20470. It is written up as a doc comment on object cc.Existentials.
scalac is crashing on opaque types aliasing a capability type
import language.experimental.captureChecking
trait A extends caps.Capability
object O:
opaque type B = A
Stack trace
Exception in thread "main" java.lang.AssertionError: assertion failed: RefinedType(TermRef(ThisType(TypeRef(NoPrefix,module class <empty>)),object O),B,AnnotatedType(TypeAlias(LazyRef(TypeRef(ThisType(TypeRef(NoPrefix,module class <empty>)),trait A))),CaptureAnnotation({TermRef(ThisType(TypeRef(ThisType(TypeRef(NoPrefix,module class scala)),module class caps$)),val cap)},false)))
at scala.runtime.Scala3RunTime$.assertFailed(Scala3RunTime.scala:8)
at dotty.tools.dotc.core.Types$RefinedType.<init>(Types.scala:3312)
at dotty.tools.dotc.core.Types$CachedRefinedType.<init>(Types.scala:3356)
unhandled exception while running cc on Test.scala
An unhandled exception was thrown in the compiler.
Please file a crash report here:
https://github.com/scala/scala3/issues/new/choose
For non-enriched exceptions, compile with -Xno-enrich-error-messages.
while compiling: Test.scala
during phase: cc
mode: Mode(ImplicitsEnabled)
library version: version 2.13.12
compiler version: version 3.5.1-RC1-bin-SNAPSHOT-git-5454526
settings: -classpath /home/nki/.cache/coursier/v1/https/repo1.maven.org/maven2/org/scala-lang/scala-library/2.13.12/scala-library-2.13.12.jar:/home/nki/Projects/dotty/library/../out/bootstrap/scala3-library-bootstrapped/scala-3.5.1-RC1-bin-SNAPSHOT-nonbootstrapped/scala3-library_3-3.5.1-RC1-bin-SNAPSHOT.jar -d /
at dotty.tools.dotc.core.Types$RefinedType$.apply(Types.scala:3365)
at dotty.tools.dotc.core.Types$RefinedType.derivedRefinedType(Types.scala:3326)
at dotty.tools.dotc.core.Types$TypeMap.derivedRefinedType(Types.scala:6200)
at dotty.tools.dotc.core.Types$TypeMap.mapOver(Types.scala:6322)
at dotty.tools.dotc.cc.Setup$$anon$4.recur(Setup.scala:304)
at dotty.tools.dotc.cc.Setup$$anon$4.apply(Setup.scala:329)
at dotty.tools.dotc.core.Types$DeepTypeMap.mapClassInfo(Types.scala:6411)
at dotty.tools.dotc.core.Types$DeepTypeMap.mapClassInfo(Types.scala:6406)
at dotty.tools.dotc.core.Types$TypeMap.mapOver(Types.scala:6351)
at dotty.tools.dotc.cc.Setup$$anon$4.recur(Setup.scala:304)
at dotty.tools.dotc.cc.Setup$$anon$4.apply(Setup.scala:329)
at dotty.tools.dotc.cc.Setup.dotty$tools$dotc$cc$Setup$$transformExplicitType(Setup.scala:332)
at dotty.tools.dotc.cc.Setup.mappedInfo$1(Setup.scala:114)
at dotty.tools.dotc.cc.Setup.transformSym(Setup.scala:121)
at dotty.tools.dotc.core.DenotTransformers$SymTransformer.transform(DenotTransformers.scala:72)
at dotty.tools.dotc.core.DenotTransformers$SymTransformer.transform$(DenotTransformers.scala:67)
at dotty.tools.dotc.cc.Setup.transform(Setup.scala:53)
at dotty.tools.dotc.core.Denotations$SingleDenotation.goForward$1(Denotations.scala:833)
at dotty.tools.dotc.core.Denotations$SingleDenotation.current(Denotations.scala:879)
at dotty.tools.dotc.core.Types$NamedType.computeDenot(Types.scala:2551)
at dotty.tools.dotc.core.Types$NamedType.denot(Types.scala:2514)
at dotty.tools.dotc.ast.Trees$DenotingTree.denot(Trees.scala:258)
at dotty.tools.dotc.ast.Trees$Tree.symbol(Trees.scala:147)
at dotty.tools.dotc.ast.tpd$.localOwner(tpd.scala:597)
at dotty.tools.dotc.ast.tpd$.localCtx(tpd.scala:601)
at dotty.tools.dotc.ast.Trees$Instance$TreeAccumulator.foldOver(Trees.scala:1753)
at dotty.tools.dotc.ast.Trees$Instance$TreeTraverser.traverseChildren(Trees.scala:1799)
at dotty.tools.dotc.cc.CheckCaptures$$anon$2.traverse(CheckCaptures.scala:673)
at dotty.tools.dotc.ast.Trees$Instance$TreeTraverser.apply(Trees.scala:1798)
at dotty.tools.dotc.ast.Trees$Instance$TreeTraverser.apply(Trees.scala:1798)
at dotty.tools.dotc.ast.Trees$Instance$TreeAccumulator.fold$1(Trees.scala:1662)
at dotty.tools.dotc.ast.Trees$Instance$TreeAccumulator.apply(Trees.scala:1664)
at dotty.tools.dotc.ast.Trees$Instance$TreeAccumulator.foldOver(Trees.scala:1763)
at dotty.tools.dotc.ast.Trees$Instance$TreeTraverser.traverseChildren(Trees.scala:1799)
at dotty.tools.dotc.cc.CheckCaptures$$anon$2.traverse(CheckCaptures.scala:673)
at dotty.tools.dotc.cc.CheckCaptures$CaptureChecker.checkUnit(CheckCaptures.scala:1251)
at dotty.tools.dotc.transform.Recheck.run(Recheck.scala:158)
at dotty.tools.dotc.cc.CheckCaptures.run(CheckCaptures.scala:193)
at dotty.tools.dotc.core.Phases$Phase.runOn$$anonfun$1(Phases.scala:380)
at scala.runtime.function.JProcedure1.apply(JProcedure1.java:15)
at scala.runtime.function.JProcedure1.apply(JProcedure1.java:10)
at scala.collection.immutable.List.foreach(List.scala:333)
at dotty.tools.dotc.core.Phases$Phase.runOn(Phases.scala:373)
at dotty.tools.dotc.transform.Recheck.runOn(Recheck.scala:162)
at dotty.tools.dotc.Run.runPhases$1$$anonfun$1(Run.scala:343)
at scala.runtime.function.JProcedure1.apply(JProcedure1.java:15)
at scala.runtime.function.JProcedure1.apply(JProcedure1.java:10)
at scala.collection.ArrayOps$.foreach$extension(ArrayOps.scala:1323)
at dotty.tools.dotc.Run.runPhases$1(Run.scala:336)
at dotty.tools.dotc.Run.compileUnits$$anonfun$1(Run.scala:384)
at dotty.tools.dotc.Run.compileUnits$$anonfun$adapted$1(Run.scala:396)
at dotty.tools.dotc.util.Stats$.maybeMonitored(Stats.scala:69)
at dotty.tools.dotc.Run.compileUnits(Run.scala:396)
at dotty.tools.dotc.Run.compileSources(Run.scala:282)
at dotty.tools.dotc.Run.compile(Run.scala:267)
at dotty.tools.dotc.Driver.doCompile(Driver.scala:37)
at dotty.tools.dotc.Driver.process(Driver.scala:201)
at dotty.tools.dotc.Driver.process(Driver.scala:169)
at dotty.tools.dotc.Driver.process(Driver.scala:181)
at dotty.tools.dotc.Driver.main(Driver.scala:211)
at dotty.tools.dotc.Main.main(Main.scala)
Strange compiler error on this code
import language.experimental.captureChecking
trait Suspend:
type Suspension
def resume(s: Suspension): Unit
trait Async(val support: Suspend) extends caps.Capability
class CancelSuspension(ac: Async, suspension: ac.support.Suspension):
ac.support.resume(suspension)
gives
-- [E007] Type Mismatch Error: Test.scala:11:20 --------------------------------
11 | ac.support.resume(suspension)
| ^^^^^^^^^^
|Found: ((CancelSuspension.this.ac : Async^)^{CancelSuspension.this.suspension*})#
| support.Suspension
|Required: CancelSuspension.this.ac.support.Suspension
|
| longer explanation available when compiling with `-explain`
1 error found
The error doesn't come up if Async does not extend Capability and CancelSuspension takes Async^ instead.
Reach capabilities being widened into cap:
//> using scala 3.5.1-RC1-bin-SNAPSHOT
import language.experimental.captureChecking
class Box[T](items: Seq[T^]):
def getOne: T^{items*} = ???
object Box:
def getOne[T](items: Seq[T^]): T^{items*} =
Box(items).getOne
gives
-- Error: /tmp/tmp.yIHCJZJOce/test.scala:9:15 ----------------------------------
9 | Box(items).getOne
| ^^^^^^^^^^^^^^^^^
|The expression's type (box T^?)^ is not allowed to capture the root capability `cap`.
|This usually means that a capability persists longer than its allowed lifetime.
1 error found
Similar to the above, simplified from gears
//> using scala 3.5.1-RC1-bin-SNAPSHOT
import language.experimental.captureChecking
trait Future[+T]:
def await: T
trait Channel[T]:
def read(): Either[Nothing, T]
class Collector[T](val futures: Seq[Future[T]^]):
val results: Channel[Future[T]^{futures*}] = ???
end Collector
extension [T](fs: Seq[Future[T]^])
def awaitAll =
val collector = Collector(fs)
// val ch = collector.results // also errors
val fut: Future[T]^{fs*} = collector.results.read().right.get // found ...^{caps.cap}
Compiling project (Scala 3.5.1-RC1-bin-SNAPSHOT, JVM (21))
[error] ./main.scala:19:32
[error] Found: Future[box T^?]^{caps.cap?}
[error] Required: Future[T]^{fs*}
[error] val fut: Future[T]^{fs*} = collector.results.read().right.get // found ...^{caps.cap}
[error] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
@natsukagami I noted that the last example typechecks if the type of collector is given explicitly:
val collector: Collector[T]{val futures: Seq[Future[T]^{fs*}]}
= Collector(fs)
An unsound snippet that should not have compiled:
import language.experimental.captureChecking
// Some capabilities that should be used locally
trait Async:
// some method
def read(): Unit
def usingAsync[X](op: Async^ => X): X = ???
case class Box[+T](get: T)
def useBoxedAsync(x: Box[Async^]): Unit = x.get.read()
def test(): Unit =
val f: Box[Async^] => Unit = useBoxedAsync
def boom(x: Async^): () ->{f} Unit =
() => f(Box(x))
val leaked = usingAsync[() ->{f} Unit](boom)
leaked() // scope violation
Functions like usingBoxedAsync should not type-check, as x.get.read() is charging {x*} to the closure of usingBoxedAsync, which should be rejected.
@Linyxus I need some more explanations why this is unsound. The typeckecked example is here:
@SourceFile("leak-problem.scala") final module class leak-problem$package()
extends Object() {
private[this] type $this = leak-problem$package.type
private def writeReplace(): AnyRef =
new scala.runtime.ModuleSerializationProxy(
classOf[leak-problem$package.type])
def usingAsync[X](op: Async^ => X): X = ???
def useBoxedAsync(x: Box[box Async^]): Unit = x.Async.read()
def test(): Unit =
{
val f: Box[box Async^] => Unit =
{
def $anonfun(x: Box[box Async^]^?): Unit = useBoxedAsync(x)
closure($anonfun)
}
def boom(x: Async^): () ->{f} Unit =
{
def $anonfun(): Unit =
{
f.apply(Box.apply[box Async^{x}](x))
}
closure($anonfun)
}
val leaked: () ->{f} Unit =
usingAsync[box () ->{f} Unit](
{
def $anonfun(x: Async^): () ->{f} Unit = boom(x)
closure($anonfun)
}
)
leaked.apply()
}
}
There's not a single reach capability in that program.
The reach capability appears in the expression x.get.read(), since x's type is Box[Async^] and the type parameter of Box is covariant, it gets reach-refined to Box[Async^{x*}].
I have a modified version of this snippet which better shows the problem:
import language.experimental.captureChecking
// Some capabilities that should be used locally
trait Async:
// some method
def read(): Unit
def usingAsync[X](op: Async^ => X): X = ???
case class Box[+T](get: T)
def useBoxedAsync(x: Box[Async^]): Unit =
val t0 = x
val t1 = x.get
t1.read()
def test(): Unit =
val f: Box[Async^] => Unit = useBoxedAsync
def boom(x: Async^): () ->{f} Unit =
() => f(Box(x))
val leaked = usingAsync[() ->{f} Unit](boom)
leaked() // scope violation
The tree after cc:
def useBoxedAsync(x: Box[box Async^]): Unit =
{
val t0: Box[box Async^{x*}]^? = x
val t1: Async^{x*} = x.Async
t1.read()
}
Some weird interaction between caps, opaque types and inlines...
//> using scala 3.6.0-RC1-bin-SNAPSHOT
import language.experimental.captureChecking
trait Async extends caps.Capability:
def group: Int
object Async:
inline def current(using async: Async): async.type = async
opaque type Spawn <: Async = Async
def blocking[T](f: Spawn ?=> T): T = ???
def main() =
Async.blocking:
val a = Async.current.group
gives
-- Error: test.scala:15:25 -----------------------------------------------------
15 | val a = Async.current.group
| ^
|The expression's type box ((contextual$1 : Async.Spawn^) & $proxy1.Spawn)^ is not allowed to capture the root capability `cap`.
|This usually means that a capability persists longer than its allowed lifetime.
Making Spawn not opaque or making current not-inline would make the code compile.
//> using scala 3.6.0-RC1-bin-SNAPSHOT
import language.experimental.captureChecking
trait Source[+T]
def race[T](@caps.unboxed sources: Seq[Source[T]^]): Source[T]^{sources*} = ???
def raceTwo[T](src1: Source[T]^, src2: Source[T]^): Source[T]^{} = race(Seq(src1, src2))
this compiles and returns a Source that does not capture src1 and src2.
Seems to not work with spread parameters
//> using scala 3.6.0-RC1-bin-SNAPSHOT
import language.experimental.captureChecking
trait Source[+T]
def race[T](@caps.unbox sources: (Source[T]^)*): Source[T]^{sources*} = ???
def raceTwo[T](src1: Source[T]^, src2: Source[T]^): Source[T]^{} =
// race(Seq(src1, src2)*) // this fails
race(src1, src2) // this compiles
Inline functions capturing a parameter on the result will fail if passed a pure argument:
//> using scala 3.6.0-RC1-bin-SNAPSHOT
import language.experimental.captureChecking
trait Listener[+T]
inline def consume[T](f: T => Unit): Listener[T]^{f} = ???
val consumePure = consume(_ => ())
errors with
-- Error: test.scala:7:50 ------------------------------------------------------
7 |inline def consume[T](f: T => Unit): Listener[T]^{f} = ???
| ^
|(f$proxy1 : (x$0: Any) ->? Unit) cannot be tracked since its capture set is empty
@natsukagami Latest problems should be fixed now. Let's see what you come up with next!
Not sure if this is a bug, but how should programmers deal with the following:
import language.experimental.captureChecking // compiles just fine *without* this import
trait DSL:
type Now[+A]
def lam[A,B](fun: Now[A] => Now[B]): Now[A => B]
def app[A,B](fun: Now[A => B], arg: Now[A]): Now[B]
def prog[A](e: Now[A]): Now[A]
def test =
prog[Int => Int]:
lam(x => x)
With capture checking enabled, the meaning of => is changed to be a tracked type and we get the following error:
-- [E007] Type Mismatch Error: local/dsl.scala:14:12 ---------------------------
13 | prog[Int => Int]:
14 | lam(x => x)
| ^
| Found: DSL.this.Now[box Int => Int]
| Required: DSL.this.Now[Int => Int]
|
| Note that the expected type DSL.this.Now[Int => Int]
| is the previously inferred result type of method test
| which is also the type seen in separately compiled sources.
| The new inferred type DSL.this.Now[box Int => Int]
| must conform to this type.
The problem is the explicit type annotation Int => Int, and there is no way to express in the surface syntax (that I'm aware of) we want prog[box Int => Int]. A rather drastic way to get it to compile under capture checking is making all the arrows in the file pure ->.
Edit: Simplifying test to def test: Now[Int => Int] = lam(x => x) compiles properly. So perhaps type applications such as prog[Int => Int] aren't handled correctly?
Edit2: If we ascribe Any to test, the example compiles again with capture checking:
def test : Any =
prog[Int => Int]:
lam(x => x)
Simply importing language.experimental.captureChecking appears to break conformance checks:
import language.experimental.captureChecking
trait Dsl:
sealed trait Nat
case object Zero extends Nat
case class Succ[N <: Nat](n: N) extends Nat
type Stable[+l <: Nat, +b <: Nat, +A]
type Now[+l <: Nat, +b <: Nat, +A]
type Box[+A]
def stable[l <: Nat, b <: Nat, A](e: Stable[l, b, A]): Now[l, b, Box[A]]
def program[A](prog: Now[Zero.type, Zero.type, A]): Now[Zero.type, Zero.type, A]
//val conforms: Zero.type <:< Nat = summon
// ^ need to uncomment this line to compile with captureChecking enabled
def test =
program:
val v : Stable[Zero.type, Zero.type, Int] = ???
stable(v)
// ^
// Type argument Dsl.this.Zero.type does not conform to upper bound Dsl.this.Nat
//> using scala 3.6.0-RC1-bin-SNAPSHOT
import language.experimental.captureChecking
trait Async extends caps.Capability
class Future[+T](x: () => T)(using val a: Async)
class Collector[T](val futs: Seq[Future[T]^]):
def add(fut: Future[T]^{futs*}) = ???
def main() =
given async: Async = ???
val futs = (1 to 20).map(x => Future(() => x))
val col: Collector[Int] { val futs: Seq[Future[Int]^{async}] } = Collector(futs)
col.add(Future(() => 25))
gives
-- [E007] Type Mismatch Error: Test.scala:15:10 --------------------------------
15 | col.add(Future(() => 25))
| ^^^^^^^^^^^^^^^^
| Found: Future[Int]{val a: (async : Async^)}^{async}
| Required: Future[Int]
|
| longer explanation available when compiling with `-explain`
It doesn't work even with the explicit annotation on Collector.
@bracevac
-- [E007] Type Mismatch Error: local/dsl.scala:14:12 ---------------------------
13 | prog[Int => Int]:
14 | lam(x => x)
| ^
| Found: DSL.this.Now[box Int => Int]
| Required: DSL.this.Now[Int => Int]
|
| Note that the expected type DSL.this.Now[Int => Int]
| is the previously inferred result type of method test
| which is also the type seen in separately compiled sources.
| The new inferred type DSL.this.Now[box Int => Int]
| must conform to this type.
Here it simply requires that you need to give an explicit type to test. It could be Any or it could be Now[Int => Int]. Both work.
@natsukagami The latest example you have is not supposed to compile. What I could do is add some way to give a hint why it failed:
15 | col.add(Future(() => 25)) // error
| ^^^^^^^^^^^^^^^^
|Found: Future[Int]{val a: (async : Async^)}^{async}
|Required: Future[Int]^{}
|
|Note that a capability Collector.this.futs* in a capture set appearing in contravariant position
|was mapped to col.futs* which is not a capability. Therefore, it was under-approximated to the empty set.
@bracevac Your latest problem should be fixed with last commit.
Simply importing language.experimental.captureChecking appears to break conformance checks
The conformance check was done by the capture checker. And that is run only if the language import is present. So that explains it. But it was still a bug since no error should have been issued.
@natsukagami For the latest example, maybe you could try explicit capture set polymorphism?
@bracevac I think it would be good to get this merged soon. We are getter further and further away from the main branch, in a good way.