Why not always eta-expanding block parameters implicitly

[thwfhk]

Sometimes we need to eta-expand block parameters to enable contextual effect polymorphism. For example,

effect Ask1(): Int
effect Ask2(): Int

def asks() = { do Ask1() + do Ask2() }

def hask1{f: => Int / {Ask1}} : Int =
  try {
    f()
  } with Ask1 { resume(40) }

def hask2{f: => Int / {Ask2}} : Int =
  try {
    f()
  } with Ask2 { resume(2) }

// def test1() = hask1{hask2{asks}}
// type error : Capture parameter count does not match () => Int / { Ask1, Ask2 } vs. () => Int / { Ask2 }

def test2() = hask1{hask2{() => asks()}}
// output : 42

// desugar of test2 ?
def test3() = hask1{
  def _asks() : Int / {Ask2} = asks()
  hask2{_asks}
}
// output : 42

Running test1 gives a type error. We need to eta-expand asks to let the type checker know that Ask2 should be handled by hask2. I'm wondering is there a reason why Effekt does not do this eta-expansion implicitly? Or, is there a well-typed example where eta-expanding its block parameters would give different results?

[b-studios]

Good point!

The compiler could (and should) eta-expand; we just did not implement it, yet.

[jiribenes]

I ran into this today again in a very similar setting:

interface Foo { def foo(): Int }
interface Bar { def bar(): Int }

def compile { prog: => Unit / Foo }: Unit = <>
def run { prog: => Unit / { Foo, Bar } }: Unit = compile { prog }
  // ERROR: requires manual eta-expansion into ↓ ^^^^^^^^^^^^^^^^
                                              // compile { () => prog() }

The error itself is: Capture parameter count does not match () => Unit / { Foo, Bar } vs. () => Unit / { Foo }