wyvernlang/wyvern

Effect bound for branch is not computed conservatively

Opened this issue · 1 comments

Assume that the function fun : Unit -> Unit has an effect {system.FFI}, the following code compiles

def foo() : {} Unit
  val x : Unit = if (1>0)
      fun()
    else
      unit
  unit

However, the function foo should have the effect annotation {system.FFI}

The solution I'd like to see for this is as follows:

  • make the underlying if() function effect-parametric
  • implement inference of effect parameters by using the effect bound of the actual function parameters. Scala does something similar (there's a talk and I think a paper by Odersky and colleagues)