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 051b4d8f3b5b..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)
 
@@ -1581,7 +1579,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
@@ -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/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/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/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/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) ||
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
 
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 <empty>
  6 |      boundary[Unit]: l2 ?=>
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/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/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-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/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`
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/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)
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 = "<none>"
+
+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)