Skip to content

Separation checking does not work well for mutable variables with cap types #23889

@odersky

Description

@odersky

Compiler version

3.8.nightly

Minimized example

class B

def Test(consume b1: B^, consume b2: B^) =
  def f(): B^ = B()
  var x: B^ = f()
  x = b1 // error separation but should be OK

Output

-- Error: frozen-result.scala:6:6 ----------------------------------------------
6 |  x = b1 // error separation but should be OK
  |      ^^
  |Separation failure: Illegal access to {b1} which is hidden by the previous definition
  |of variable x with type B^{cap}.
  |This type hides capabilities  {cap², b1}
  |
  |where:    cap  is a fresh root capability in the type of variable x
  |          cap² is a fresh root capability created in variable x when instantiating method f's type (): B^{cap³}

Expectation

No error.

The problem is that we record all assigned right sides in the hidden set of x. Then separation checking of every right hand side except the first fails.

Metadata

Metadata

Assignees

No one assigned

    Labels

    stat: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