effekt-lang / effekt

A language with lexical effect handlers and lightweight effect polymorphism
https://effekt-lang.org
MIT License
321 stars 23 forks source link

Wrong effect inferred for effectful `while` header #601

Open marzipankaiser opened 3 weeks ago

marzipankaiser commented 3 weeks ago

The following program compiles without typer errors:

interface Foo { def foo(): Unit }

def bar(): Bool / Foo = {
  do foo()
  false
}

def fooo() = {
  while(bar() is true) {
      ()
    }
}

def main() = {
  fooo()
}

but crashes at runtime (in JS), because there is no handler for the do foo in the loop header. The type of fooo is shown (at least via LSP) as def fooo(): Unit / {}.

Adding a handler in main generates a warning that the handler is unused (but runs fine).

marzipankaiser commented 3 weeks ago

Note: I assume we just don't add the effects from the header of the while when checking in typer, so might be an easy fix.

b-studios commented 3 weeks ago

Yes, we just need to add guardEffs here: https://github.com/effekt-lang/effekt/blob/e0e5c60e3fdda4dbc693207a776ae60f41b0d292/effekt/shared/src/main/scala/effekt/Typer.scala#L122