Fix Paths Referencing Consumed Parameters

[bracevac]

Builds on #24424

Tasks

• Take a path's consume capabilities into account in consume check in checkUse.
• More neg tests.
• Improve the error message if possible.

[bracevac]

@odersky it seems to be stable now. I will add some more neg tests. Do you agree with the general direction, or should we try something else?

[bracevac]

I'm also surprised that reach capabilities would pop up where there are no boxes involved whatsoever.

[odersky]

Why do we need that? Would not the path root already contain the field consumed set?

[bracevac]

As discussed offline:

class B
class A(consume val b: B^)
class Holder(val a: A^)  // Note: NOT consume

def test =
  val b: B^ = B()
  val a = A(b) // b is gone
  val holder = Holder(a) // separation failure, but should be ok

At the end of checkUse, we can see b is consumed and know a clashes with b. To conclude that the use of a is ok, we also need to inspect its consume constructor parameter to see that it has consumed b, so we should ignore the clash.

[bracevac]

We came to the conclusion that the solution with fixing the logic at the end of checkUse is apparently not needed, and that instead we should tweak the logic around captureSetImpliedByFields to type something like A(b) where b is consumed as A{val b: B^{b}}^ instead of A{val b: B^{b}}^{b} as it is typed now, analogous to how consume methods work.

[odersky]

#24470 now contains code to require consume parameters to be covered by a fresh of the class. Can you rebase the tests here and see what they see with these changes?

[bracevac]

@odersky I only added the tests to #24470 here, and I'm seeing

-- Error: tests/pos-custom-args/captures/paths-simple-suffix-consume.scala:9:20 
9 |class A(consume val b: B^)
  |                    ^
  |A consume parameter is only allowed for classes producing a `cap` in their constructor.
  |This can be achieved by having the class extend caps.Separate.

and can't seem to be able to add extends caps.Separate:

-- [E008] Not Found Error: tests/pos-custom-args/captures/paths-simple-suffix-consume.scala:9:40 
9 |class A(consume val b: B^) extends caps.Separate
  |                                   ^^^^^^^^^^^^^
  |                                   type Separate is not a member of caps

It's missing?

[bracevac]

Spying at your test cases, I changed it to

class A(consume val b: B^) extends Mutable { var x: Int = 1 }

in tests/pos-custom-args/captures/paths-simple-suffix-consume.scala.
That seemed to help. However, I'm now getting

-- Error: tests/pos-custom-args/captures/paths-simple-suffix-consume.scala:19:12 
19 |  println(a.b)       // OK - consumed field
   |          ^^^
   |Separation failure: Illegal access to (a.b : B^{b²}), which was passed as a consume parameter to constructor of class A
   |on line 16 and therefore is no longer available.
   |
   |where:    b  is a value in class A
   |          b² is a value in method test1

But it should work, no?

Edit: When we check for a clash in checkUse, I see:

check use a.b, (a.b : B^{b}) clashes at (b,Argument(Ident(b),method <init>))
prefix = (a : A{val b: B^{b}}^)

The b field of a is still capturing the consumed b. Shouldn't we see

prefix = (a : A{val b: B^}^)

instead?