Use level checking for Fresh instances #23101

odersky · 2025-05-05T14:50:37Z

This PR changes the way we treat fresh instances. Instead of disallowing all of them when instantiating type parameters (as well as in a number of other situations), we allow them but check that inner fresh instances do not get widened to outer ones. This makes code like this one compile

class Ref extends Mutable:
  var x = 0
  def get: Int = x
  mut def put(y: Int): Unit = x = y

class Pair[+X, +Y](val fst: X, val snd: Y)

def twoRefs1(): Pair[Ref^, Ref^] =
  Pair(Ref(), Ref())

Previously, that would not work since the X and Y variables of Pair would be instantiated to Ref^, which was not allowed.

The PR also implements lots of improvements to error diagnostics.

We now disambiguate different instances of ^, cap, or =>.
We explain for each such instances what it represents exactly.
We also turn this on for override errors (not necessarily limited to capture checking).

Refactor to avoid generating refsText ahead of time. We need to keep the original capture sets or tree lists so that we can record them as seen.

- Map cap to Result in their original types (was Fresh before) - Map Result to Fresh on access

Turn level checking on under the useFreshLevels config option (which is on by default)

Fall back to previous scheme if there is no recording in Seen. That way, we see what we expect when turning on Ycc-verbose and other printing options.

…bles. The check was not working properly before, which meant that problems went undetected. To make things work again, we need two additional fixes - A more detailed treatment of result mapping for inferred types. In these, we map root.Fresh to root.Result only if the original inferred type was dependent. AppliedType functions are also mapped to RefinedType functions in setup, but this should not count for fresh to result mappings. - A fix in the Fresh to Result mapping of parameterless defs.

When printing types deriving from capability, do print their capture sets even if these are implied. This avoids confusing errors where a capability classes has two different implied Fresh instances which are both elided so the types look the same. Exception: When printing a singleton type (x: T) we do elide in T, since the usually the only part that matters is the `x`. But we don't do the elision under -Ycc-verbose or -explain.

We had the wrong condition in maxSubsumes before. We need to test for isStaticOwner instead of isStatic. The previous test made all fresh capabilities in global classes slip through the net.

odersky · 2025-05-09T09:45:14Z

Most of the added lines in this PR are in the tests. We have more tests and the existing neg tests explain the problem in more detail.

natsukagami

I also notice .check files missing for class-level-attack.scala and capt-capability.scala.

Otherwise seems good!

natsukagami · 2025-05-12T12:11:17Z

compiler/src/dotty/tools/dotc/cc/CaptureRef.scala

+    case _ =>
+      NoSymbol
+
+  final def adjustedOwner(using Context): Symbol =


Is this returning the owner representing the boundary of a level? I found only one use of this method, its name is a bit mysterious

natsukagami · 2025-05-12T12:14:55Z

compiler/src/dotty/tools/dotc/cc/CaptureRef.scala

            && !yIsExistential
-            && !y.isInstanceOf[TermParamRef]
+            && !y.isInstanceOf[ParamRef]


What's the reason for the TermParamRef -> ParamRef change? I tried changing it back and testCompilation captures still passes

natsukagami · 2025-05-12T12:16:33Z

compiler/src/dotty/tools/dotc/cc/CaptureSet.scala

@@ -183,7 +183,7 @@ sealed abstract class CaptureSet extends Showable:
   */
  def accountsFor(x: CaptureRef)(using ctx: Context)(using vs: VarState = VarState.Separate): Boolean =

-    def debugInfo(using Context) = i"$this accountsFor $x, which has capture set ${x.captureSetOfInfo}"
+    def debugInfo(using Context) = i"$this accountsFor $x"


Intentional removal?

natsukagami · 2025-05-12T13:38:30Z

compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala

      val argType = recheck(arg, freshenedFormal)
        .showing(i"recheck arg $arg vs $freshenedFormal = $result", capt)
      if formal.hasAnnotation(defn.UseAnnot) || formal.hasAnnotation(defn.ConsumeAnnot) then
-        // The @use and/or @consume annotation is added to `formal` by `prepareFunction`
+        // The @use and/or @consume annotation is added to `formal` by `prep areFunction`


Unintentional?

natsukagami · 2025-05-12T13:53:07Z

compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala

@@ -1261,8 +1277,7 @@ class CheckCaptures extends Recheck, SymTransformer:
          val msg = note match
            case CompareResult.LevelError(cs, ref) =>
              if ref.stripReadOnly.isCapOrFresh then
-                def capStr = if ref.isReadOnly then "cap.rd" else "cap"
-                i"""the universal capability `$capStr`
+                i"""the universa capability $ref


Suggested change

i"""the universa capability $ref

i"""the universal capability $ref

typo

natsukagami · 2025-05-12T14:44:30Z

compiler/src/dotty/tools/dotc/core/Types.scala

+                pdenot.meet(
+                  new JointRefDenotation(NoSymbol, rinfo, Period.allInRun(ctx.runId), pre, isRefinedMethod),
+                  pre,
+                  safeIntersection = ctx.base.pendingMemberSearches.contains(name))
+              pdenot.meet(
+                new JointRefDenotation(NoSymbol, rinfo, Period.allInRun(ctx.runId), pre, isRefinedMethod),
+                pre,
+                safeIntersection = ctx.base.pendingMemberSearches.contains(name))


pdenot.meet called twice, intentional?

natsukagami · 2025-05-12T15:02:30Z

tests/neg-custom-args/captures/box-adapt-contra.check

+   |        where:    =>  refers to the universal root capability
+   |                  cap is the universal root capability


This is still quite confusing I think, both are universal root capabilities

natsukagami · 2025-05-12T16:09:33Z

tests/neg-custom-args/captures/sep-pairs-2.scala

+def twoRefs3(): Pair[Ref^, Ref^] = // error but should work
+  val p = Pair(Ref(), Ref())
+  p


odersky added 11 commits May 1, 2025 14:34

Record level of current owner when creating Fresh instances

61668fc

Don't increase symLevel for blocks

4868498

Don't allow Fresh to subsume TypeParamRefs

543f64b

Introduce QualifiedCapability extractor

6fe59a1

Refactor printing of capturing types and function types

b630083

Refactor to avoid generating refsText ahead of time. We need to keep the original capture sets or tree lists so that we can record them as seen.

Explain root capabilities in error messages

c831b68

More detailed explanations where Fresh instances come from

0d55a9f

Refactor: Instead of purpose string, use Origin enum

18a5228

Implement level checking for Fresh roots

6056ae2

Disambiguate and explain override error messages

055c394

Fix root treatment of parameterless methods

d581e54

- Map cap to Result in their original types (was Fresh before) - Map Result to Fresh on access

odersky force-pushed the drop-disallow-fresh branch from 223b9c6 to 99a4c20 Compare May 5, 2025 18:11

odersky added 4 commits May 6, 2025 13:34

Turn level checking on under useFreshLevels config option

b6a77e6

Turn level checking on under the useFreshLevels config option (which is on by default)

Tweak printing in MessagePrinter

0ef14c3

Fall back to previous scheme if there is no recording in Seen. That way, we see what we expect when turning on Ycc-verbose and other printing options.

odersky force-pushed the drop-disallow-fresh branch from 99a4c20 to d7eb32a Compare May 7, 2025 12:00

Tighten level checking

806e2b5

We had the wrong condition in maxSubsumes before. We need to test for isStaticOwner instead of isStatic. The previous test made all fresh capabilities in global classes slip through the net.

odersky force-pushed the drop-disallow-fresh branch from d7eb32a to b58327d Compare May 8, 2025 16:24

Allow Fresh instances in disallowRootCapability

a178c04

odersky force-pushed the drop-disallow-fresh branch from b58327d to a178c04 Compare May 9, 2025 08:42

natsukagami self-assigned this May 9, 2025

natsukagami reviewed May 12, 2025

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Use level checking for Fresh instances #23101

Use level checking for Fresh instances #23101

odersky commented May 5, 2025 •

edited

Loading

odersky commented May 9, 2025

natsukagami left a comment

natsukagami May 12, 2025

natsukagami May 12, 2025

natsukagami May 12, 2025

natsukagami May 12, 2025

natsukagami May 12, 2025

natsukagami May 12, 2025

natsukagami May 12, 2025

natsukagami May 12, 2025

	i"""the universa capability $ref
	i"""the universal capability $ref

		\| where: => refers to the universal root capability
		\| cap is the universal root capability

Use level checking for Fresh instances #23101

Are you sure you want to change the base?

Use level checking for Fresh instances #23101

Conversation

odersky commented May 5, 2025 • edited Loading

odersky commented May 9, 2025

natsukagami left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

odersky commented May 5, 2025 •

edited

Loading