effekt-lang / effekt

A research language with effect handlers and lightweight effect polymorphism
https://effekt-lang.org
MIT License
304 stars 14 forks source link

References escape their region when using `var` #512

Open phischu opened 3 weeks ago

phischu commented 3 weeks ago

Consider the following program where we allocate a mutable variable x in a region r1, and return a closure that contains it.

interface Ref[T] {
  def get(): T
}

def main() = {
  var myref =
    region r1 {
      var x in r1 = "hoho";
      new Ref[String] {
        def get() = x
      }
    }
  println(myref.get())
}

This program is accepted but it should not. When changing var myref to val myref it is rejected, which is good.

b-studios commented 3 weeks ago

One bit of additional information: the inferred type of the returned ref is Ref[String] at {r1}, which is correct. So my conjecture is that simply the wellformedness check is buggy:

https://github.com/effekt-lang/effekt/blob/9e651118559e5980e7182a10e47abdbd9bf1b973/effekt/shared/src/main/scala/effekt/typer/Wellformedness.scala#L97-L109