Repository: effekt-lang/effekt (scala)

Issue:
Incorrectly applies tail resumption optimization under var scope
Effekt's optimizations are currently not semantics-preserving for the following program:

<details>

```scala
effect flip(): Bool

def all{prog: => Unit / {flip}} = {
  try {
    prog()
  } with flip {
    resume(true)
    resume(false)
  }
}

interface State[T] {
  def get(): T
  def set(x: T): Unit
}

interface allocate {
  def fresh[T, R](init: T){k: {State[T]} => R}: R
}

def newRegion[T]{prog: {r: allocate} => T}: T = {
  try {
    prog{r}
  } with r: allocate {
    def fresh[T, R](init) = {
      var x = init
      def s = new State[T] {
        def get() = x
        def set(y) = {
          x = y
        }
      }
      resume{{k} => k{s}}
    }
  }
}

def main() = {
  newRegion { {r} =>
    all {
      with def x = r.fresh(0)
      if (do flip()) {
        x.set(3)
      } else {
      }
      println(x.get())
    }
  }
}
```

</details >

with optimizations:

```console
> effekt regions.effekt
3
0
```

without optimizations:

```console
> effekt regions.effekt --no-optimize
3
3
```

Pull request:
Fixes #1153.

Patch:
diff --git a/effekt/shared/src/main/scala/effekt/core/optimizer/RemoveTailResumptions.scala b/effekt/shared/src/main/scala/effekt/core/optimizer/RemoveTailResumptions.scala
index c29bb2795..16dde427e 100644
--- a/effekt/shared/src/main/scala/effekt/core/optimizer/RemoveTailResumptions.scala
+++ b/effekt/shared/src/main/scala/effekt/core/optimizer/RemoveTailResumptions.scala
@@ -33,9 +33,12 @@ object RemoveTailResumptions {
       case Stmt.Match(scrutinee, clauses, default) => !freeInExpr(scrutinee) && clauses.forall {
         case (_, BlockLit(tparams, cparams, vparams, bparams, body)) => tailResumptive(k, body)
       } && default.forall { stmt => tailResumptive(k, stmt) }
-      case Stmt.Region(BlockLit(tparams, cparams, vparams, bparams, body)) => tailResumptive(k, body)
+      case Stmt.Region(BlockLit(tparams, cparams, vparams, bparams, body)) => false
       case Stmt.Alloc(id, init, region, body) => tailResumptive(k, body) && !freeInExpr(init)
-      case Stmt.Var(ref, init, capture, body) => tailResumptive(k, body) && !freeInExpr(init)
+      // Conceptually, a mutable variable definition can be seen as a handler for get and put operations.
+      // Treating this as tail-resumptive leads to a failure of semantics preservation.
+      // See https://github.com/effekt-lang/effekt/issues/1153 for an example.
+      case Stmt.Var(ref, init, capture, body) => false
       case Stmt.Get(ref, annotatedCapt, tpe, id, body) => tailResumptive(k, body)
       case Stmt.Put(ref, annotatedCapt, value, body) => tailResumptive(k, body) && !freeInExpr(value)
       case Stmt.Reset(BlockLit(tparams, cparams, vparams, bparams, body)) => false
diff --git a/examples/pos/issue1153.check b/examples/pos/issue1153.check
new file mode 100644
index 000000000..08a81a932
--- /dev/null
+++ b/examples/pos/issue1153.check
@@ -0,0 +1,2 @@
+3
+3
\ No newline at end of file
diff --git a/examples/pos/issue1153.effekt b/examples/pos/issue1153.effekt
new file mode 100644
index 000000000..004ada3fa
--- /dev/null
+++ b/examples/pos/issue1153.effekt
@@ -0,0 +1,49 @@
+effect flip(): Bool
+
+def all{prog: => Unit / {flip}} = {
+  try {
+    prog()
+  } with flip {
+    resume(true)
+    resume(false)
+  }
+}
+
+interface State[T] {
+  def get(): T
+  def set(x: T): Unit
+}
+
+interface allocate {
+  def fresh[T, R](init: T){k: {State[T]} => R}: R
+}
+
+def newRegion[T]{prog: {r: allocate} => T}: T = {
+  try {
+    prog{r}
+  } with r: allocate {
+    def fresh[T, R](init) = {
+      var x = init
+      def s = new State[T] {
+        def get() = x
+        def set(y) = {
+          x = y
+        }
+      }
+      resume{{k} => k{s}}
+    }
+  }
+}
+
+def main() = {
+  newRegion { {r} =>
+    all {
+      with def x = r.fresh(0)
+      if (do flip()) {
+        x.set(3)
+      } else {
+      }
+      println(x.get())
+    }
+  }
+}


Test patch:
diff --git a/effekt/jvm/src/test/scala/effekt/ChezSchemeTests.scala b/effekt/jvm/src/test/scala/effekt/ChezSchemeTests.scala
index 4dfe21c78..db68b1f3f 100644
--- a/effekt/jvm/src/test/scala/effekt/ChezSchemeTests.scala
+++ b/effekt/jvm/src/test/scala/effekt/ChezSchemeTests.scala
@@ -27,6 +27,7 @@ abstract class ChezSchemeTests extends EffektTests {
     examplesDir / "pos" / "object",
     examplesDir / "pos" / "type_omission_op.effekt",
     examplesDir / "pos" / "issue972.effekt",
+    examplesDir / "pos" / "issue1153.effekt",
 
     // filesystem operations and bytearrays are not yet supported in our Chez backend
     examplesDir / "benchmarks" / "input_output" / "word_count_ascii.effekt",