From 133928c9e25be74f89b8c3933e1408fbcfe30277 Mon Sep 17 00:00:00 2001 From: odersky Date: Mon, 1 Dec 2025 18:52:18 +0100 Subject: [PATCH 1/6] Test for a new collection class hierarchy respecting mutability --- .../captures/mut-collections.scala | 51 +++++++++++++++++++ 1 file changed, 51 insertions(+) create mode 100644 tests/pos-custom-args/captures/mut-collections.scala diff --git a/tests/pos-custom-args/captures/mut-collections.scala b/tests/pos-custom-args/captures/mut-collections.scala new file mode 100644 index 000000000000..e1f6ebd7c040 --- /dev/null +++ b/tests/pos-custom-args/captures/mut-collections.scala @@ -0,0 +1,51 @@ +package colltestMut +import caps.* +import collection.*, mutable.*, immutable.* + +object collection: + trait Iterable[A]: + this: Iterable[A]^ => + type C[X] <: Iterable[X]^ + def map[B](f: A => B): C[B]^{f} = ??? + + trait View[A] extends Iterable[A]: + this: View[A]^ => + type C[X] = View[X]^{this} + + trait Seq[A] extends Iterable[A]: + this: Seq[A]^ => + override def map[B](f: A => B): C[B] = ??? + +object immutable: + import collection.* + trait Seq[A] extends Iterable[A], Pure: + type C[X] <: Seq[X] + + class List[A] extends Seq[A]: + type C[X] = List[X] + + +object mutable: + import collection.* + trait Seq[A] extends collection.Seq[A]: + this: Seq[A]^ => + type C[X] <: Seq[X]^ + + trait Buffer[A] extends Seq[A], Mutable: + this: Buffer[A]^ => + type C[X] = Buffer[X]^ + +class IO extends SharedCapability +class Ref extends Mutable + +object Test: + def test(io: IO, ref: Ref, f: Int => Int) = + val xs1: List[Int] = ??? + val ys1 = xs1.map(f) + val xs2: Buffer[Int]^ = ??? + val ys2 = xs2.map(f) + val xs3: Buffer[Int]^ = ??? + val zs3 = freeze(xs3) + val xs4: Buffer[Int]^ = ??? + val vs4: View[Int]^{xs4} = ??? + val ys4 = vs4.map(f) From e4227be2ad5d8229785656125bce579837204698 Mon Sep 17 00:00:00 2001 From: odersky Date: Tue, 2 Dec 2025 15:44:42 +0100 Subject: [PATCH 2/6] Make Array.copy work for capturing types --- library/src/scala/Array.scala | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/src/scala/Array.scala b/library/src/scala/Array.scala index e40d82b0ed17..4cf59c808f98 100644 --- a/library/src/scala/Array.scala +++ b/library/src/scala/Array.scala @@ -77,9 +77,9 @@ object Array { case _ => it.iterator.toArray[A] } - private def slowcopy(src : AnyRef, + private def slowcopy(src : AnyRef^, srcPos : Int, - dest : AnyRef, + dest : AnyRef^, destPos : Int, length : Int): Unit = { var i = srcPos @@ -107,7 +107,7 @@ object Array { * * @see `java.lang.System#arraycopy` */ - def copy(src: AnyRef, srcPos: Int, dest: AnyRef, destPos: Int, length: Int): Unit = { + def copy(src: AnyRef^, srcPos: Int, dest: AnyRef^, destPos: Int, length: Int): Unit = { val srcClass = src.getClass val destClass = dest.getClass if (srcClass.isArray && ((destClass eq srcClass) || From b3aa6b2c64eefe3a5c721e59cd95f34fd1e04a3d Mon Sep 17 00:00:00 2001 From: odersky Date: Tue, 2 Dec 2025 17:39:55 +0100 Subject: [PATCH 3/6] Use a better span for an anonymous class An anonymous class is expanded roughly to { class $anon{ ... }; new $anon } Previously the `new` part had a zero extent span at the end of the class. When used with significant indentation, this caused some puzzlement in error messages since one thought the last class definition was to blame. The span is now the whole anonymous class. --- .../src/dotty/tools/dotc/typer/Typer.scala | 6 +- tests/neg-custom-args/captures/capt1.check | 13 +-- tests/neg-custom-args/captures/capt1.scala | 4 +- .../captures/method-uses.scala | 4 +- .../captures/mut-iterator4.check | 23 ++---- .../captures/mut-iterator4.scala | 6 +- tests/neg/6570-1.check | 16 ++-- tests/neg/6570.check | 80 +++++++++---------- tests/neg/i13703.check | 8 +- 9 files changed, 78 insertions(+), 82 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala index 4b54419bd7a2..31d5a465b271 100644 --- a/compiler/src/dotty/tools/dotc/typer/Typer.scala +++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala @@ -1251,7 +1251,11 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer typedAhead(parent, tree => inferTypeParams(typedType(tree), pt)) val anon = tpnme.ANON_CLASS val clsDef = TypeDef(anon, templ1).withFlags(Final | Synthetic) - typed(cpy.Block(tree)(clsDef :: Nil, New(Ident(anon), Nil)), pt) + typed( + cpy.Block(tree)( + clsDef :: Nil, + New(Ident(anon), Nil).withSpan(tree.span)), + pt) case _ => var tpt1 = typedType(tree.tpt) val tsym = tpt1.tpe.underlyingClassRef(refinementOK = false).typeSymbol diff --git a/tests/neg-custom-args/captures/capt1.check b/tests/neg-custom-args/captures/capt1.check index 906991c4019e..a684c1463902 100644 --- a/tests/neg-custom-args/captures/capt1.check +++ b/tests/neg-custom-args/captures/capt1.check @@ -34,13 +34,14 @@ | Note that capability x is not included in capture set {}. | | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:28:40 ---------------------------------------- -28 | def m() = if x == null then y else y // error - | ^ - | Found: A^{x} - | Required: A +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:27:2 ----------------------------------------- +27 | new A: // error + | ^ + | Found: A^{x} + | Required: A | - | Note that capability x is not included in capture set {}. + | Note that capability x is not included in capture set {}. +28 | def m() = if x == null then y else y | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt1.scala:36:24 ---------------------------------------- diff --git a/tests/neg-custom-args/captures/capt1.scala b/tests/neg-custom-args/captures/capt1.scala index 01eda5e049f8..0d44d3171aa8 100644 --- a/tests/neg-custom-args/captures/capt1.scala +++ b/tests/neg-custom-args/captures/capt1.scala @@ -24,8 +24,8 @@ def h3(x: Cap): A = F(22) // error def h4(x: Cap, y: Int): A = - new A: - def m() = if x == null then y else y // error + new A: // error + def m() = if x == null then y else y def f1(c: Cap): () ->{c} c.type = () => c // ok diff --git a/tests/neg-custom-args/captures/method-uses.scala b/tests/neg-custom-args/captures/method-uses.scala index 576e227e5d74..6c3310d49f7f 100644 --- a/tests/neg-custom-args/captures/method-uses.scala +++ b/tests/neg-custom-args/captures/method-uses.scala @@ -23,8 +23,8 @@ def test3(xs: List[() => Unit]): () ->{xs*} Unit = () => def test4(xs: List[() => Unit]) = () => xs.head // error, ok under deferredReaches def test5(xs: List[() => Unit]) = new: - println(xs.head) // error, ok under deferredReaches // error + println(xs.head) // error, ok under deferredReaches def test6(xs: List[() => Unit]) = - val x= new { println(xs.head) } // error // error + val x= new { println(xs.head) } // error x diff --git a/tests/neg-custom-args/captures/mut-iterator4.check b/tests/neg-custom-args/captures/mut-iterator4.check index 9ab60ada56ce..fcf3c9c35916 100644 --- a/tests/neg-custom-args/captures/mut-iterator4.check +++ b/tests/neg-custom-args/captures/mut-iterator4.check @@ -1,29 +1,20 @@ -- Error: tests/neg-custom-args/captures/mut-iterator4.scala:9:26 ------------------------------------------------------ -9 | update def next() = f(Iterator.this.next()) // error // error +9 | update def next() = f(Iterator.this.next()) // error | ^^^^^^^^^^^^^ | Read-only method map accesses exclusive capability (Iterator.this : Iterator[T]^); | method map should be declared an update method to allow this. | | where: ^ refers to the universal root capability --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mut-iterator4.scala:9:47 --------------------------------- -9 | update def next() = f(Iterator.this.next()) // error // error - | ^ - |Found: Iterator[U^'s1]^{Iterator.this.rd, f, Iterator.this, cap} - |Required: Iterator[U]^{Iterator.this, f} - | - |Note that capability cap is not included in capture set {Iterator.this, f}. - | - |where: cap is a fresh root capability created in method map when constructing instance Object with (Iterator[U]^{cap².rd}) {...} - | - | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mut-iterator4.scala:23:34 -------------------------------- -23 | update def next() = f(it.next()) // error - | ^ - |Found: Iterator[U^'s2]^{it.rd, f, it, cap} +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mut-iterator4.scala:21:81 -------------------------------- +21 |def mappedIterator[T, U](it: Iterator[T]^, f: T => U): Iterator[U]^{it, f} = new Iterator: // error + | ^ + |Found: Iterator[U^'s1]^{it.rd, f, it, cap} |Required: Iterator[U]^{it, f} | |Note that capability cap is not included in capture set {it, f}. | |where: cap is a fresh root capability created in method mappedIterator when constructing instance Object with (Iterator[U]^{cap².rd}) {...} +22 | def hasNext = it.hasNext +23 | update def next() = f(it.next()) | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/mut-iterator4.scala b/tests/neg-custom-args/captures/mut-iterator4.scala index 72c60d26edfc..1d6716e5f82d 100644 --- a/tests/neg-custom-args/captures/mut-iterator4.scala +++ b/tests/neg-custom-args/captures/mut-iterator4.scala @@ -6,7 +6,7 @@ trait Iterator[T] extends Stateful: def map[U](f: T => U): Iterator[U]^{Iterator.this, f} = new Iterator: def hasNext = Iterator.this.hasNext - update def next() = f(Iterator.this.next()) // error // error + update def next() = f(Iterator.this.next()) // error end Iterator @@ -18,9 +18,9 @@ def listIterator[T](xs: List[T]): Iterator[T]^ = new Iterator[T]: current = xs1 x -def mappedIterator[T, U](it: Iterator[T]^, f: T => U): Iterator[U]^{it, f} = new Iterator: +def mappedIterator[T, U](it: Iterator[T]^, f: T => U): Iterator[U]^{it, f} = new Iterator: // error def hasNext = it.hasNext - update def next() = f(it.next()) // error + update def next() = f(it.next()) class IO extends SharedCapability: def write(x: Any): Unit = () diff --git a/tests/neg/6570-1.check b/tests/neg/6570-1.check index 0abf96e2d350..6e48c72d18c7 100644 --- a/tests/neg/6570-1.check +++ b/tests/neg/6570-1.check @@ -1,14 +1,14 @@ --- [E007] Type Mismatch Error: tests/neg/6570-1.scala:23:27 ------------------------------------------------------------ +-- [E007] Type Mismatch Error: tests/neg/6570-1.scala:23:14 ------------------------------------------------------------ 23 | def thing = new Trait1 {} // error - | ^ - | Found: Object with Trait1 {...} - | Required: N[Box[Int & String]] + | ^^^^^^^^^^^^^ + | Found: Object with Trait1 {...} + | Required: N[Box[Int & String]] | - | Note: a match type could not be fully reduced: + | Note: a match type could not be fully reduced: | - | trying to reduce N[Box[Int & String]] - | failed since selector Box[Int & String] - | is uninhabited (there are no values of that type). + | trying to reduce N[Box[Int & String]] + | failed since selector Box[Int & String] + | is uninhabited (there are no values of that type). | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg/6570-1.scala:36:54 ------------------------------------------------------------ diff --git a/tests/neg/6570.check b/tests/neg/6570.check index e849814449eb..3cfef5b70ac9 100644 --- a/tests/neg/6570.check +++ b/tests/neg/6570.check @@ -17,17 +17,17 @@ | x >: Int | | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg/6570.scala:29:29 -------------------------------------------------------------- +-- [E007] Type Mismatch Error: tests/neg/6570.scala:29:16 -------------------------------------------------------------- 29 | def thing = new Trait1 {} // error - | ^ - | Found: Object with Base.Trait1 {...} - | Required: Base.N[String & Int] + | ^^^^^^^^^^^^^ + | Found: Object with Base.Trait1 {...} + | Required: Base.N[String & Int] | - | Note: a match type could not be fully reduced: + | Note: a match type could not be fully reduced: | - | trying to reduce Base.N[String & Int] - | failed since selector String & Int - | is uninhabited (there are no values of that type). + | trying to reduce Base.N[String & Int] + | failed since selector String & Int + | is uninhabited (there are no values of that type). | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg/6570.scala:47:32 -------------------------------------------------------------- @@ -46,43 +46,43 @@ | a >: Int | | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg/6570.scala:51:29 -------------------------------------------------------------- +-- [E007] Type Mismatch Error: tests/neg/6570.scala:51:16 -------------------------------------------------------------- 51 | def thing = new Trait1 {} // error - | ^ - | Found: Object with Base.Trait1 {...} - | Required: Base.N[String & Int] + | ^^^^^^^^^^^^^ + | Found: Object with Base.Trait1 {...} + | Required: Base.N[String & Int] | - | Note: a match type could not be fully reduced: + | Note: a match type could not be fully reduced: | - | trying to reduce Base.N[String & Int] - | failed since selector String & Int - | is uninhabited (there are no values of that type). + | trying to reduce Base.N[String & Int] + | failed since selector String & Int + | is uninhabited (there are no values of that type). | | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg/6570.scala:69:29 -------------------------------------------------------------- +-- [E007] Type Mismatch Error: tests/neg/6570.scala:69:16 -------------------------------------------------------------- 69 | def thing = new Trait1 {} // error - | ^ - | Found: Object with Base.Trait1 {...} - | Required: Base.N[String & Int] + | ^^^^^^^^^^^^^ + | Found: Object with Base.Trait1 {...} + | Required: Base.N[String & Int] | - | Note: a match type could not be fully reduced: + | Note: a match type could not be fully reduced: | - | trying to reduce Base.N[String & Int] - | failed since selector String & Int - | is uninhabited (there are no values of that type). + | trying to reduce Base.N[String & Int] + | failed since selector String & Int + | is uninhabited (there are no values of that type). | | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg/6570.scala:86:29 -------------------------------------------------------------- +-- [E007] Type Mismatch Error: tests/neg/6570.scala:86:16 -------------------------------------------------------------- 86 | def thing = new Trait1 {} // error - | ^ - | Found: Object with Base.Trait1 {...} - | Required: Base.N[String & Int] + | ^^^^^^^^^^^^^ + | Found: Object with Base.Trait1 {...} + | Required: Base.N[String & Int] | - | Note: a match type could not be fully reduced: + | Note: a match type could not be fully reduced: | - | trying to reduce Base.N[String & Int] - | failed since selector String & Int - | is uninhabited (there are no values of that type). + | trying to reduce Base.N[String & Int] + | failed since selector String & Int + | is uninhabited (there are no values of that type). | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg/6570.scala:103:32 ------------------------------------------------------------- @@ -101,16 +101,16 @@ | t >: Int | | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg/6570.scala:107:29 ------------------------------------------------------------- +-- [E007] Type Mismatch Error: tests/neg/6570.scala:107:16 ------------------------------------------------------------- 107 | def thing = new Trait1 {} // error - | ^ - | Found: Object with Base.Trait1 {...} - | Required: Base.N[String & Int] + | ^^^^^^^^^^^^^ + | Found: Object with Base.Trait1 {...} + | Required: Base.N[String & Int] | - | Note: a match type could not be fully reduced: + | Note: a match type could not be fully reduced: | - | trying to reduce Base.N[String & Int] - | failed since selector String & Int - | is uninhabited (there are no values of that type). + | trying to reduce Base.N[String & Int] + | failed since selector String & Int + | is uninhabited (there are no values of that type). | | longer explanation available when compiling with `-explain` diff --git a/tests/neg/i13703.check b/tests/neg/i13703.check index a02bbdf407f7..c92349a476d1 100644 --- a/tests/neg/i13703.check +++ b/tests/neg/i13703.check @@ -1,7 +1,7 @@ --- [E007] Type Mismatch Error: tests/neg/i13703.scala:3:78 ------------------------------------------------------------- +-- [E007] Type Mismatch Error: tests/neg/i13703.scala:3:52 ------------------------------------------------------------- 3 |val f2: Foo { val i: Int; def i_=(x: Int): Unit } = new Foo { var i: Int = 0 } // error - | ^ - | Found: Object with Foo {...} - | Required: Foo{val i: Int; def i_=(x: Int): Unit} + | ^^^^^^^^^^^^^^^^^^^^^^^^^^ + | Found: Object with Foo {...} + | Required: Foo{val i: Int; def i_=(x: Int): Unit} | | longer explanation available when compiling with `-explain` From 13a62d67783d97248639f2f7ae924050c807f367 Mon Sep 17 00:00:00 2001 From: odersky Date: Tue, 2 Dec 2025 17:53:19 +0100 Subject: [PATCH 4/6] Show synthesizd tree for type mismatch errors in CC In capture checking, a type mismatch might happen for a synthesized tree (say from implicit search). It can be helpful to show this tree. Before capture checking a helpful message is less likely since we don't synthesize implicit trees that then don't match under the standard typing rules. --- compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala | 2 +- compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala | 9 ++++++++- tests/neg-custom-args/captures/boundary.check | 2 ++ 3 files changed, 11 insertions(+), 2 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 051b4d8f3b5b..72d1e11bb13c 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -1581,7 +1581,7 @@ class CheckCaptures extends Recheck, SymTransformer: * where local capture roots are instantiated to root variables. */ override def checkConformsExpr(actual: Type, expected: Type, tree: Tree, notes: List[Note])(using Context): Type = - try testAdapted(actual, expected, tree, notes: List[Note])(err.typeMismatch) + try testAdapted(actual, expected, tree, notes)(err.typeMismatch) catch case ex: AssertionError => println(i"error while checking $tree: $actual against $expected") throw ex diff --git a/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala b/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala index 76e55cda279f..89818820d575 100644 --- a/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala +++ b/compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala @@ -14,6 +14,7 @@ import config.Feature import reporting.* import Message.Note import collection.mutable +import cc.isCaptureChecking object ErrorReporting { @@ -190,7 +191,13 @@ object ErrorReporting { case _ => Nil - errorTree(tree, TypeMismatch(treeTp, expectedTp, Some(tree), notes ++ missingElse)) + def badTreeNote = + val span = tree.span + if tree.span.isZeroExtent && isCaptureChecking then + Note(i"\n\nThe error occurred for a synthesized tree: $tree") :: Nil + else Nil + + errorTree(tree, TypeMismatch(treeTp, expectedTp, Some(tree), notes ++ missingElse ++ badTreeNote)) } /** A subtype log explaining why `found` does not conform to `expected` */ diff --git a/tests/neg-custom-args/captures/boundary.check b/tests/neg-custom-args/captures/boundary.check index 0c440125a403..f7d2a06b32f0 100644 --- a/tests/neg-custom-args/captures/boundary.check +++ b/tests/neg-custom-args/captures/boundary.check @@ -45,6 +45,8 @@ | | Note that capability cap is not included in capture set {cap²}. | + | The error occurred for a synthesized tree: _ + | | where: ^ and cap² refer to the universal root capability | ^² and cap refer to a fresh root capability created in package 6 | boundary[Unit]: l2 ?=> From 8cb4bd4ca73ca165c0208fe39ca30887340911c1 Mon Sep 17 00:00:00 2001 From: odersky Date: Tue, 2 Dec 2025 18:14:45 +0100 Subject: [PATCH 5/6] Make Predef capture checked --- library/src/scala/Predef.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/src/scala/Predef.scala b/library/src/scala/Predef.scala index c97b2c761229..9ed2516d4f39 100644 --- a/library/src/scala/Predef.scala +++ b/library/src/scala/Predef.scala @@ -13,8 +13,8 @@ package scala import scala.language.`2.13` +import language.experimental.captureChecking import scala.language.implicitConversions - import scala.collection.{mutable, immutable, ArrayOps, StringOps}, immutable.WrappedString import scala.annotation.{experimental, implicitNotFound, publicInBinary, targetName, nowarn } import scala.annotation.meta.{ companionClass, companionMethod } @@ -552,7 +552,7 @@ object Predef extends LowPriorityImplicits { * `(A => A) <: (A => B)`. */ // $ to avoid accidental shadowing (e.g. scala/bug#7788) - implicit def $conforms[A]: A => A = <:<.refl + implicit def $conforms[A]: A -> A = <:<.refl.asInstanceOf // Extension methods for working with explicit nulls From 04278ba3410ebe3f98ffa573db699d28c87413d4 Mon Sep 17 00:00:00 2001 From: odersky Date: Wed, 3 Dec 2025 11:38:06 +0100 Subject: [PATCH 6/6] Make Arrays mutable types under separation checking --- .../src/dotty/tools/dotc/cc/CaptureOps.scala | 20 +- .../src/dotty/tools/dotc/cc/CaptureSet.scala | 28 ++- .../dotty/tools/dotc/cc/CheckCaptures.scala | 24 +-- .../src/dotty/tools/dotc/cc/Mutability.scala | 2 + compiler/src/dotty/tools/dotc/cc/Setup.scala | 12 +- .../src/dotty/tools/dotc/cc/ccConfig.scala | 5 +- .../tools/dotc/core/SymDenotations.scala | 2 +- .../dotty/tools/dotc/typer/TyperPhase.scala | 1 + .../captures/existential-mapping.check | 4 +- tests/neg-custom-args/captures/freeze.scala | 2 +- .../captures/mut-widen-empty.check | 12 ++ .../captures/mut-widen-empty.scala | 8 +- tests/new/test.scala | 45 ++--- .../captures/capt-depfun2.scala | 6 +- tests/pos-custom-args/captures/freeze.scala | 18 +- .../pos-custom-args/captures/mut-arrays.scala | 9 + tests/pos-custom-args/captures/ro-array.scala | 2 +- .../captures/sealed-value-class.scala | 6 +- tests/pos-custom-args/captures/steppers.scala | 13 +- .../colltest5/CollectionStrawManCC5_1.scala | 10 +- .../captures/minicheck-mutable.scala | 181 ++++++++++++++++++ 21 files changed, 328 insertions(+), 82 deletions(-) create mode 100644 tests/pos-custom-args/captures/mut-arrays.scala create mode 100644 tests/run-custom-args/captures/minicheck-mutable.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index af9a2abc7a9d..5c4bf9d4840d 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -553,10 +553,13 @@ extension (sym: Symbol) * - or it is a value class * - or it is an exception * - or it is one of Nothing, Null, or String + * Arrays are not pure under strict mutability even though their self type is declared pure + * in Arrays.scala. */ def isPureClass(using Context): Boolean = sym match case cls: ClassSymbol => - cls.pureBaseClass.isDefined || defn.pureSimpleClasses.contains(cls) + (cls.pureBaseClass.isDefined || defn.pureSimpleClasses.contains(cls)) + && !(cls == defn.ArrayClass && ccConfig.strictMutability) case _ => false @@ -588,8 +591,8 @@ extension (sym: Symbol) && !defn.isPolymorphicAfterErasure(sym) && !defn.isTypeTestOrCast(sym) - /** It's a parameter accessor that is not annotated @constructorOnly or @uncheckedCaptures - * and that is not a consume accessor. + /** It's a parameter accessor for a parameter that that is not annotated + * @constructorOnly or @uncheckedCaptures and that is not a consume parameter. */ def isRefiningParamAccessor(using Context): Boolean = sym.is(ParamAccessor) @@ -600,6 +603,17 @@ extension (sym: Symbol) && !param.hasAnnotation(defn.ConsumeAnnot) } + /** It's a parameter accessor that is tracked for capture checking. Excluded are + * accessors for parameters annotated with constructorOnly or @uncheckedCaptures. + */ + def isTrackedParamAccessor(using Context): Boolean = + sym.is(ParamAccessor) + && { + val param = sym.owner.primaryConstructor.paramNamed(sym.name) + !param.hasAnnotation(defn.ConstructorOnlyAnnot) + && !param.hasAnnotation(defn.UntrackedCapturesAnnot) + } + def hasTrackedParts(using Context): Boolean = !CaptureSet.ofTypeDeeply(sym.info).isAlwaysEmpty diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index d67e344830b1..b042abaa4c75 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -666,13 +666,33 @@ object CaptureSet: then i" under-approximating the result of mapping $ref to $mapped" else "" - private def capImpliedByCapability(parent: Type)(using Context): Capability = - if parent.derivesFromStateful then GlobalCap.readOnly else GlobalCap + private def capImpliedByCapability(parent: Type, sym: Symbol, variance: Int)(using Context): Capability = + // Since standard library classes are not compiled with separation checking, + // they treat Array as a Pure class. That means, no effort is made to distinguish + // between exclusive and read-only arrays. To compensate in code compiled under + // strict mutability, we treat contravariant arrays in signatures of stdlib + // members as read-only (so all arrays may be passed to them), and co- and + // invariant arrays as exclusive. + // TODO This scheme should also apply whenever code under strict mutability interfaces + // with code compiled without. To do that we will need to store in the Tasty format + // a flag whether code was compiled with separation checking on. This will have + // to wait until 3.10. + def isArrayFromScalaPackage = + parent.classSymbol == defn.ArrayClass + && ccConfig.strictMutability + && variance >= 0 + && sym.isContainedIn(defn.ScalaPackageClass) + if parent.derivesFromStateful && !isArrayFromScalaPackage + then GlobalCap.readOnly + else GlobalCap /* The same as {cap} but generated implicitly for references of Capability subtypes. + * @param parent the type to which the capture set will be attached + * @param sym the symbol carrying that type + * @param variance the variance in which `parent` appears in the type of `sym` */ - class CSImpliedByCapability(parent: Type)(using @constructorOnly ctx: Context) - extends Const(SimpleIdentitySet(capImpliedByCapability(parent))) + class CSImpliedByCapability(parent: Type, sym: Symbol, variance: Int)(using @constructorOnly ctx: Context) + extends Const(SimpleIdentitySet(capImpliedByCapability(parent, sym, variance))) /** A special capture set that gets added to the types of symbols that were not * themselves capture checked, in order to admit arbitrary corresponding capture diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 72d1e11bb13c..3e9313ab518f 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -1410,9 +1410,7 @@ class CheckCaptures extends Recheck, SymTransformer: // (3) Capture set of self type includes capture sets of parameters for param <- cls.paramGetters do - if !param.hasAnnotation(defn.ConstructorOnlyAnnot) - && !param.hasAnnotation(defn.UntrackedCapturesAnnot) - then + if param.isTrackedParamAccessor then withCapAsRoot: // OK? We need this here since self types use `cap` instead of `fresh` checkSubset(param.termRef.captureSet, thisSet, param.srcPos) @@ -2148,26 +2146,6 @@ class CheckCaptures extends Recheck, SymTransformer: checker.traverse(tree.nuType) end checkTypeParam - /** Under the unsealed policy: Arrays are like vars, check that their element types - * do not contains `cap` (in fact it would work also to check on array creation - * like we do under sealed). - */ - def checkArraysAreSealedIn(tp: Type, pos: SrcPos)(using Context): Unit = - val check = new TypeTraverser: - def traverse(t: Type): Unit = - t match - case AppliedType(tycon, arg :: Nil) if tycon.typeSymbol == defn.ArrayClass => - if !(pos.span.isSynthetic && ctx.reporter.errorsReported) - && !arg.typeSymbol.name.is(WildcardParamName) - then - disallowBadRootsIn(arg, NoSymbol, "Array", "have element type", "", pos) - traverseChildren(t) - case defn.RefinedFunctionOf(rinfo: MethodType) => - traverse(rinfo) - case _ => - traverseChildren(t) - check.traverse(tp) - /** Check that no uses refer to reach capabilities of parameters of enclosing * methods or classes. */ diff --git a/compiler/src/dotty/tools/dotc/cc/Mutability.scala b/compiler/src/dotty/tools/dotc/cc/Mutability.scala index e788d32dba9b..9c4b3fb40961 100644 --- a/compiler/src/dotty/tools/dotc/cc/Mutability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Mutability.scala @@ -10,6 +10,7 @@ import config.Printers.capt import config.Feature import ast.tpd.Tree import typer.ProtoTypes.LhsProto +import StdNames.nme /** Handling mutability and read-only access */ @@ -59,6 +60,7 @@ object Mutability: && !sym.field.hasAnnotation(defn.UntrackedCapturesAnnot) else true ) + || ccConfig.strictMutability && sym.name == nme.update && sym == defn.Array_update /** A read-only member is a lazy val or a method that is not an update method. */ def isReadOnlyMember(using Context): Boolean = diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala index 5c8c581f729c..1f688ce70277 100644 --- a/compiler/src/dotty/tools/dotc/cc/Setup.scala +++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala @@ -84,6 +84,16 @@ object Setup: case _ => false case _ => None + def patchArrayClass()(using Context): Unit = + if ccConfig.strictMutability then + val arrayCls = defn.ArrayClass.asClass + arrayCls.info match + case oldInfo: ClassInfo if !arrayCls.derivesFrom(defn.Caps_Mutable) => + arrayCls.info = oldInfo.derivedClassInfo( + declaredParents = oldInfo.declaredParents :+ defn.Caps_Mutable.typeRef) + arrayCls.invalidateBaseDataCache() + case _ => + end Setup import Setup.* @@ -425,7 +435,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: then normalizeCaptures(mapOver(t)) match case t1 @ CapturingType(_, _) => t1 - case t1 => CapturingType(t1, CaptureSet.CSImpliedByCapability(t1), boxed = false) + case t1 => CapturingType(t1, CaptureSet.CSImpliedByCapability(t1, sym, variance), boxed = false) else normalizeCaptures(mapFollowingAliases(t)) def innerApply(t: Type) = diff --git a/compiler/src/dotty/tools/dotc/cc/ccConfig.scala b/compiler/src/dotty/tools/dotc/cc/ccConfig.scala index 5ea8b17d8aaf..9823f68ba8b0 100644 --- a/compiler/src/dotty/tools/dotc/cc/ccConfig.scala +++ b/compiler/src/dotty/tools/dotc/cc/ccConfig.scala @@ -61,9 +61,12 @@ object ccConfig: def newScheme(using ctx: Context): Boolean = Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`) + /** Allow @use annotations */ def allowUse(using Context): Boolean = Feature.sourceVersion.stable.isAtMost(SourceVersion.`3.7`) - + /** Treat arrays as mutable types. Enabled under separation checking */ + def strictMutability(using Context): Boolean = + Feature.enabled(Feature.separationChecking) end ccConfig diff --git a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala index 3b198ea4dbaa..5e6dd471e304 100644 --- a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala +++ b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala @@ -1886,7 +1886,7 @@ object SymDenotations { myBaseTypeCache.nn } - private def invalidateBaseDataCache() = { + def invalidateBaseDataCache() = { baseDataCache.invalidate() baseDataCache = BaseData.None } diff --git a/compiler/src/dotty/tools/dotc/typer/TyperPhase.scala b/compiler/src/dotty/tools/dotc/typer/TyperPhase.scala index 264d0f170769..611784e0d40c 100644 --- a/compiler/src/dotty/tools/dotc/typer/TyperPhase.scala +++ b/compiler/src/dotty/tools/dotc/typer/TyperPhase.scala @@ -44,6 +44,7 @@ class TyperPhase(addRootImports: Boolean = true) extends Phase { val unit = ctx.compilationUnit try if !unit.suspended then ctx.profiler.onUnit(ctx.phase, unit): + if ctx.run.nn.ccEnabledSomewhere then cc.Setup.patchArrayClass() unit.tpdTree = ctx.typer.typedExpr(unit.untpdTree) typr.println("typed: " + unit.source) record("retained untyped trees", unit.untpdTree.treeSize) diff --git a/tests/neg-custom-args/captures/existential-mapping.check b/tests/neg-custom-args/captures/existential-mapping.check index 67f4afc25373..10f43e941e2e 100644 --- a/tests/neg-custom-args/captures/existential-mapping.check +++ b/tests/neg-custom-args/captures/existential-mapping.check @@ -1,10 +1,10 @@ -- Error: tests/neg-custom-args/captures/existential-mapping.scala:46:10 ----------------------------------------------- 46 | val z2: (x: A^) => Array[C^] = ??? // error | ^^^^^^^^^^^^^^^^^^^^ - | Array[C^] captures the root capability `cap` in invariant position. + | Array[C^]^{cap.rd} captures the root capability `cap` in invariant position. | This capability cannot be converted to an existential in the result type of a function. | - | where: ^ refers to the universal root capability + | where: ^ and cap refer to the universal root capability -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:9:25 --------------------------- 9 | val _: (x: C^) -> C = x1 // error | ^^ diff --git a/tests/neg-custom-args/captures/freeze.scala b/tests/neg-custom-args/captures/freeze.scala index 8f1a168fe2d2..81542f438c8e 100644 --- a/tests/neg-custom-args/captures/freeze.scala +++ b/tests/neg-custom-args/captures/freeze.scala @@ -1,7 +1,7 @@ import caps.* class Arr[T: reflect.ClassTag](len: Int) extends Mutable: - private val arr: Array[T] = new Array[T](len) + private val arr: Array[T]^ = new Array[T](len) def get(i: Int): T = arr(i) update def update(i: Int, x: T): Unit = arr(i) = x diff --git a/tests/neg-custom-args/captures/mut-widen-empty.check b/tests/neg-custom-args/captures/mut-widen-empty.check index b3ab5df59979..2a23fdeab58a 100644 --- a/tests/neg-custom-args/captures/mut-widen-empty.check +++ b/tests/neg-custom-args/captures/mut-widen-empty.check @@ -10,3 +10,15 @@ | where: ^ and cap refer to a fresh root capability classified as Unscoped in the type of value c | | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mut-widen-empty.scala:18:26 ------------------------------ +18 | val c: Array[String]^ = b // error + | ^ + | Found: (b : Array[String]^{}) + | Required: Array[String]^ + | + | Note that {cap} is an exclusive capture set of the stateful type Array[String]^, + | it cannot subsume a read-only capture set of the stateful type Array[String]^{}. + | + | where: ^ and cap refer to a fresh root capability classified as Unscoped in the type of value c + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/mut-widen-empty.scala b/tests/neg-custom-args/captures/mut-widen-empty.scala index 9e10c040a046..8ff95f210e10 100644 --- a/tests/neg-custom-args/captures/mut-widen-empty.scala +++ b/tests/neg-custom-args/captures/mut-widen-empty.scala @@ -1,7 +1,7 @@ import caps.* class Arr[T: reflect.ClassTag](len: Int) extends Mutable: - private val arr: Array[T] = new Array[T](len) + private val arr: Array[T]^ = new Array[T](len) def get(i: Int): T = arr(i) update def update(i: Int, x: T): Unit = arr(i) = x @@ -12,3 +12,9 @@ def test2 = val c: Arr[String]^ = b // error c(2) = "a" // boom! +def test3 = + val a = new Array[String](2) + val b: Array[String]^{} = ??? + val c: Array[String]^ = b // error + c(2) = "a" // boom! + diff --git a/tests/new/test.scala b/tests/new/test.scala index 4541893e0ffb..b9be7bc5b47b 100644 --- a/tests/new/test.scala +++ b/tests/new/test.scala @@ -1,27 +1,18 @@ -import caps.* - -class Ref[T](init: T) extends caps.Stateful, Unscoped: - var x = init - def get: T = x - update def put(y: T): Unit = x = y - -class File: - def read(): String = ??? - -def withFile[T](op: (f: File^) => T): T = - op(new File) - -def withFileAndRef[T](op: (f: File^, r: Ref[String]^) => T): T = - op(File(), Ref("")) - -def Test = -/* - withFileAndRef: (f, r: Ref[String]^) => - r.put(f.read()) -*/ - - withFileAndRef: (f, r) => - r.put(f.read()) - - - +import caps.unsafe.untrackedCaptures + +class ArrayBuffer[A] private (@untrackedCaptures initElems: Array[AnyRef]^, initLength: Int): + private var elems: Array[AnyRef]^ = initElems + private var start = 0 + private var end = initLength + + def +=(elem: A): this.type = + elems(end) = elem.asInstanceOf[AnyRef] + this + + override def toString = + val slice = elems.slice(start, end) + val wrapped = wrapRefArray(slice) + //val wrapped2 = collection.mutable.ArraySeq.ofRef(slice) + val str = wrapped.mkString(", ") + str + //s"ArrayBuffer(${elems.slice(start, end).mkString(", ")})" diff --git a/tests/pos-custom-args/captures/capt-depfun2.scala b/tests/pos-custom-args/captures/capt-depfun2.scala index 4451deb27c76..0affafa8bb48 100644 --- a/tests/pos-custom-args/captures/capt-depfun2.scala +++ b/tests/pos-custom-args/captures/capt-depfun2.scala @@ -3,9 +3,11 @@ import annotation.retains class C type Cap = C @retains[caps.cap.type] +class Arr[T] + class STR def f(consume y: Cap, consume z: Cap) = def g(): C @retains[y.type | z.type] = ??? - val ac: ((x: Cap) -> Array[STR @retains[x.type]]) = ??? - val dc: Array[? >: STR <: STR^]^{y, z} = ac(g()) // needs to be inferred + val ac: ((x: Cap) => Arr[STR @retains[x.type]]^{x}) = ??? + val dc: Arr[? >: STR <: STR^]^{y, z} = ac(g()) // needs to be inferred val ec = ac(y) diff --git a/tests/pos-custom-args/captures/freeze.scala b/tests/pos-custom-args/captures/freeze.scala index b979cb5cf193..3fe7f22e9d5f 100644 --- a/tests/pos-custom-args/captures/freeze.scala +++ b/tests/pos-custom-args/captures/freeze.scala @@ -2,7 +2,7 @@ import language.experimental.captureChecking import caps.* class Arr[T: reflect.ClassTag](len: Int) extends Mutable: - private val arr: Array[T] = new Array[T](len) + private val arr: Array[T]^ = new Array[T](len) def get(i: Int): T = arr(i) update def update(i: Int, x: T): Unit = arr(i) = x @@ -23,3 +23,19 @@ def test3 = val _: Arr[String]^{} = b b +def test4 = + val a = freeze: + val a = new Array[String](2) + a(0) = "1" + a(1) = "2" + a + val _: Array[String]^{} = a + +def test5 = + val a = new Array[String](2) + a(0) = "1" + a(1) = "2" + val b = freeze(a) + val _: Array[String]^{} = b + b + diff --git a/tests/pos-custom-args/captures/mut-arrays.scala b/tests/pos-custom-args/captures/mut-arrays.scala new file mode 100644 index 000000000000..270a37a49c23 --- /dev/null +++ b/tests/pos-custom-args/captures/mut-arrays.scala @@ -0,0 +1,9 @@ + + +def Test = + val a1 = new Array[Int](3) + val a2 = Array.fill(3)(0) + val a3 = a1 ++ a2 + + def f = () => a1(0) = 2 + def g = () => a1(0) diff --git a/tests/pos-custom-args/captures/ro-array.scala b/tests/pos-custom-args/captures/ro-array.scala index bcc4aa1be1c5..708331ca547d 100644 --- a/tests/pos-custom-args/captures/ro-array.scala +++ b/tests/pos-custom-args/captures/ro-array.scala @@ -2,7 +2,7 @@ import caps.* object Test class Arr[T: reflect.ClassTag](a: Async, len: Int) extends Stateful: - private val arr: Array[T] = new Array[T](len) + private val arr: Array[T]^ = new Array[T](len) def get(i: Int): T = arr(i) update def set(i: Int, x: T): Unit = arr(i) = x diff --git a/tests/pos-custom-args/captures/sealed-value-class.scala b/tests/pos-custom-args/captures/sealed-value-class.scala index 7d2a223be91f..a4850255315b 100644 --- a/tests/pos-custom-args/captures/sealed-value-class.scala +++ b/tests/pos-custom-args/captures/sealed-value-class.scala @@ -1,3 +1,3 @@ -class Ops[A](xs: Array[A]) extends AnyVal: - - def f(p: A => Boolean): Array[A] = xs +class Ops[A](xs: Array[A]^) extends AnyVal: + this: Ops[A]^ => + def f(p: A => Boolean): Array[A]^{this} = xs diff --git a/tests/pos-custom-args/captures/steppers.scala b/tests/pos-custom-args/captures/steppers.scala index 0d99e305bb22..756bb9def891 100644 --- a/tests/pos-custom-args/captures/steppers.scala +++ b/tests/pos-custom-args/captures/steppers.scala @@ -1,25 +1,26 @@ +import caps.unsafe.untrackedCaptures trait Stepper[+A] object Stepper: trait EfficientSplit -sealed trait StepperShape[-T, S <: Stepper[_]^] extends caps.Pure +sealed trait StepperShape[-T, S <: Stepper[?]^] extends caps.Pure trait IterableOnce[+A] extends Any: - def stepper[S <: Stepper[_]^{this}](implicit shape: StepperShape[A, S]): S = ??? + def stepper[S <: Stepper[?]^{this}](implicit shape: StepperShape[A, S]): S = ??? sealed abstract class ArraySeq[T] extends IterableOnce[T], caps.Pure: - def array: Array[_] + val array: Array[?] def sorted[B >: T](implicit ord: Ordering[B]): ArraySeq[T] = - val arr = array.asInstanceOf[Array[T]].sorted(ord.asInstanceOf[Ordering[Any]]).asInstanceOf[Array[T]] + val arr = array.asInstanceOf[Array[T]].sorted(using ord.asInstanceOf[Ordering[Any]]).asInstanceOf[Array[T]] ArraySeq.make(arr).asInstanceOf[ArraySeq[T]] object ArraySeq: def make[T](x: Array[T]): ArraySeq[T] = ??? - final class ofRef[T <: AnyRef](val array: Array[T]) extends ArraySeq[T], caps.Pure: - override def stepper[S <: Stepper[_]](implicit shape: StepperShape[T, S]): S & Stepper.EfficientSplit = ??? + final class ofRef[T <: AnyRef](@untrackedCaptures val array: Array[T]) extends ArraySeq[T], caps.Pure: + override def stepper[S <: Stepper[?]](implicit shape: StepperShape[T, S]): S & Stepper.EfficientSplit = ??? diff --git a/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala b/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala index 2de3ba603507..a5488b28d420 100644 --- a/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala +++ b/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala @@ -6,7 +6,7 @@ import scala.reflect.ClassTag import annotation.unchecked.{uncheckedVariance, uncheckedCaptures} import annotation.tailrec import caps.cap -import caps.unsafe.unsafeAssumeSeparate +import caps.unsafe.{unsafeAssumeSeparate, untrackedCaptures} import language.experimental.captureChecking @@ -295,12 +295,12 @@ object CollectionStrawMan5 { } /** Concrete collection type: ArrayBuffer */ - class ArrayBuffer[A] private (initElems: Array[AnyRef], initLength: Int) + class ArrayBuffer[A] private (@untrackedCaptures initElems: Array[AnyRef]^, initLength: Int) extends Seq[A] with SeqLike[A] with Builder[A, ArrayBuffer[A]] { - this: ArrayBuffer[A] => + //this: ArrayBuffer[A] => type C[X] = ArrayBuffer[X] def this() = this(new Array[AnyRef](16), 0) - private var elems: Array[AnyRef] = initElems + private var elems: Array[AnyRef]^ = initElems private var start = 0 private var end = initLength def apply(n: Int) = elems(start + n).asInstanceOf[A] @@ -358,7 +358,7 @@ object CollectionStrawMan5 { } } - class ArrayBufferView[A](val elems: Array[AnyRef], val start: Int, val end: Int) extends RandomAccessView[A] { + class ArrayBufferView[A](@untrackedCaptures val elems: Array[AnyRef]^, val start: Int, val end: Int) extends RandomAccessView[A] { this: ArrayBufferView[A] => def apply(n: Int) = elems(start + n).asInstanceOf[A] } diff --git a/tests/run-custom-args/captures/minicheck-mutable.scala b/tests/run-custom-args/captures/minicheck-mutable.scala new file mode 100644 index 000000000000..ca2050955f7c --- /dev/null +++ b/tests/run-custom-args/captures/minicheck-mutable.scala @@ -0,0 +1,181 @@ +// A mini typechecker to experiment with arena allocated contexts +import compiletime.uninitialized +import annotation.{experimental, tailrec, constructorOnly} +import collection.mutable +import caps.* +import caps.unsafe.{untrackedCaptures, unsafeDiscardUses} + +case class Symbol(name: String, initOwner: Symbol | Null) extends caps.Pure: + def owner = initOwner.nn + @untrackedCaptures private var myInfo: Type = uninitialized + def infoOrCompleter: Type = myInfo + def info: Type = + infoOrCompleter match + case completer: LazyType => + myInfo = NoType + completer.complete() + info + case NoType => + throw TypeError(s"cyclic reference involving $name") + case tp => + tp + def info_=(tp: Type) = myInfo = tp + def exists: Boolean = true + def orElse(alt: => Symbol): Symbol = this + +object NoSymbol extends Symbol("", null): + override def owner = assert(false, "NoSymbol.owner") + override def infoOrCompleter = NoType + override def exists: Boolean = false + override def orElse(alt: => Symbol): Symbol = alt + +abstract class Type extends caps.Pure: + def exists = true + def show: String +case class IntType()(using @constructorOnly c: Context) extends Type: + def show = "Int" +case class StringType()(using @constructorOnly c: Context) extends Type: + def show = "String" +case object NoType extends Type: + override def exists = false + def show = "" + +abstract class LazyType(using Context) extends Type: + def complete(): Unit = doComplete() + def doComplete()(using Context): Unit + def show = "?" + +enum Tree: + case Let(bindings: List[Binding], res: Tree) + case Ref(name: String) + case Add(x: Tree, y: Tree) + case Length(x: Tree) + case Lit(value: Any) + +case class Binding(name: String, rhs: Tree) + +class Scope: + private val elems = mutable.Map[String, Symbol]() + def enter(sym: Symbol)(using Context, Reporter^): Unit = + if elems.contains(sym.name) then + report.error(s"duplicate definition: ${sym.name}") + elems(sym.name) = sym + def lookup(name: String): Symbol = + elems.getOrElse(name, NoSymbol) + def elements: Iterator[Symbol] = elems.valuesIterator + +object EmptyScope extends Scope + +class TypeError(val msg: String) extends Exception + +class Reporter extends Stateful: + var errorCount = 0 + update def error(msg: -> String)(using Context) = + errorCount += 1 + println(s"ERROR: $msg") + +abstract class Context: + def outer: Context + def owner: Symbol + def scope: Scope + +class FreshContext(using val outer: Context) + (val owner: Symbol = outer.owner, val scope: Scope = outer.scope) extends Context + +object NoContext extends Context: + def outer = ??? + def owner = NoSymbol + def scope = EmptyScope + +def ctx(using c: Context): Context = c +def report(using r: Reporter^): r.type = r + +def withOwner[T](owner: Symbol)(op: Context ?=> T)(using Context): T = + op(using FreshContext(owner = owner)) + +def withScope[T](scope: Scope)(op: Context ?=> T)(using Context): T = + op(using FreshContext(scope = scope)) + +def typed(tree: Tree, expected: Type = NoType)(using Context, Reporter^): Type = + try + val tp = typedUnadapted(tree, expected) + if expected.exists && tp != expected then + report.error: + s"""Type error + | found : $tp + | expected: $expected + | for : $tree""".stripMargin + tp + catch case ex: TypeError => + report.error(ex.msg) + NoType + +import Tree.* +def typedUnadapted(tree: Tree, expected: Type = NoType)(using ctx: Context, rep: Reporter^): Type = tree match + case Let(bindings, res) => + withScope(Scope()): + for Binding(name, rhs) <- bindings do + val sym = Symbol(name, ctx.owner) + sym.info = new LazyType: + override def doComplete()(using Context) = + sym.info = withOwner(sym): + typed(rhs)(using ctx, unsafeDiscardUses(rep)) + ctx.scope.enter(sym) + for sym <- ctx.scope.elements do sym.info + typed(res, expected) + case Ref(name: String) => + def findIn(c: Context): Symbol = + val sym = c.scope.lookup(name) + if sym.exists || (c eq NoContext) then sym + else findIn(c.outer) + findIn(ctx).info + case Add(x: Tree, y: Tree) => + typed(x, IntType()) + typed(y, IntType()) + IntType() + case Length(x: Tree) => + typed(x, StringType()) + IntType() + case Lit(value: Any) => + value match + case value: Int => IntType() + case value: String => StringType() + case _ => + report.error(s"Int or String literal expected by $value found") + NoType + +object sugar: + extension (tree: Tree) + infix def where(bindings: Binding*) = Let(bindings.toList, tree) + def + (other: Tree) = Add(tree, other) + + extension (name: String) + def := (rhs: Tree) = Binding(name, rhs) + +import sugar.* + +val prog = + Ref("x") + Length(Ref("s")) where ( + "x" := Lit(1) + Length(Ref("s")), + "s" := Lit("abc")) + +val bad = Ref("x") + Ref("s") where ( + "x" := Lit(1), + "s" := Lit("abc")) + +val cyclic = + Ref("x") + Length(Ref("s")) where ( + "x" := Lit(1) + Ref("x"), + "s" := Lit("abc")) + +def compile(tree: Tree)(using Context) = + val reporter = Reporter() + val tp = typed(tree)(using ctx, reporter) + if reporter.errorCount == 0 then + println(s"OK $tp") + +@main def Test = + given Context = NoContext + compile(prog) + compile(bad) + compile(cyclic)