Skip to content

Cannot define consume def in templates with caps.ExclusiveMutablity in the parents #24372

@hamzaremmal

Description

@hamzaremmal

Compiler version

3bea2f3

Minimized code

import scala.language.experimental.captureChecking
import scala.language.experimental.separationChecking

trait Foo extends caps.ExclusiveCapability:
  consume def sink: Unit = ()

Output

-- Error: test.scala:7:14 ------------------------------------------------------
7 |  consume def sink: Unit = ()
  |              ^
  |Update method sink must be declared in a class extending the `Mutable` trait.

Expectation

I understand that consume implies update in a Mutable context but it would be nice to be able to define consume def in an ExclusiveCapability context too (by definition of what an ExclusiveCapability is). As a workaround, one could do the following:

import scala.language.experimental.captureChecking
import scala.language.experimental.separationChecking

trait Foo extends caps.ExclusiveCapability
object Foo:
  extension (consume self: Foo)
    def sink: Unit = ()

def Test =
  val x: Foo^ = new Foo {}
  x.sink
  x.sink // error as expected

Metadata

Metadata

Assignees

Labels

itype:bugstat:needs triageEvery issue needs to have an "area" and "itype" label

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions