Inline functions that do mutation rejected as ghost

[vkuncak]

It seems useful to make use of inline functions and assume they will be mostly taken care by Scala compiler.

Do we expect that something like this should work, or do we wish that the inline function is treated as a function?

object InvalidInvariantCopy {
  case class MyClass(var x: BigInt, var y: BigInt, var isValid: Boolean = true) {
    require(x <= y)    
  }

  inline def changeMyClass(m: MyClass)(inline body: => Unit): Unit =
    m.isValid = false
    body
    m.isValid = true

  def inc(m: MyClass): Unit =
    changeMyClass(m):
      m.x += 1
      m.y += 1
}

In any case, currently it reports

info Running phase AntiAliasing                               
Test.scala:6:14: error: Ghost function changeMyClass cannot have effect on non-ghost state: m.isValid
             inline def changeMyClass(m: MyClass)(inline body: => Unit): Unit =
                        ^

[mario-bucev]

What a strange error, I've checked against an older commit and the same error appears, at least it's not from #1476...

[vkuncak]

The intention of having user-defined change blocks using inline seems doomed, but it helped uncover this. Trying to make things ghost also confused me. It seems that marking an entire class ghost does not make its mutable fields ghost, but only methods defined in it (if any)? Do we have examples of people putting ghost on a class?

[mario-bucev]

changeMyClass is annotated with @ghost here because it is "an erased value or an erased inline method or field" according to the doc of isEffectivelyErased. This check has been added here when we could use erased as a replacement for @ghost. Note that this check to isEffectivelyErased has no equivalent in the Scala 2 frontend. I think it is safe to allow inline method, since this check was surely meant to only include erased.