Unintuitive Effect Inference Behavior with println in Functions Using Polymorphic Effects

[chtenb]

Take the following code

pub fun take-exn(i : () -> exn int) : exn int i()
pub fun get() : e int 42

The following will compile

pub fun main()
  val f = get
  val str = f().show
  // println(str)
  take-exn(f)

However, when uncommenting the println, the compiler will complain that

repro.kk(3, 3): error: effects do not match context : val str = f().show println(str) term : val str = f().show println(str) inferred effect: <exn,console|_e> expected effect: exn

I can't see the logic in that, and I think it's a bug.

[TimWhiting]

Ignore this: I misread the issue the first time. Real answer in follow-up comments.

The println function requires the console effect to be handled. (It doesn't make sense to use println when in a context that doesn't have a console to print to). However, if you don't want to reannotate all of your function's effects - i.e. console is not meant to be part of the function, and you are only printing for debugging purposes, there is a function called trace that is meant for debugging - which doesn't emit any effect.

[chtenb]

I'm not sure I follow. The main() function has access to the console effect. If I comment the take-exn call instead, and leave the println uncommented it works.

[TimWhiting]

Sorry, I completely read the signatures wrong. This is partially related to #401.

Daan has told me that he does not let-generalize functions due to this paper: https://dl.acm.org/doi/abs/10.1145/1708016.1708023

However, he said he will revisit that issue. In particular I think that opening the effect row should be allowed, even if the rest of the type stays monomorphic.

[TimWhiting]

To work around it you can provide an explicit annotation for now:

pub fun main()
  val f  : forall<e> () -> e int = get
  val str = f().show
  println(str)
  take-exn(f)
  ()

The issue is that koka infers this:

pub fun main()
  val f  : some<e> () -> e int = get
  val str = f().show
  println(str)
  take-exn(f)
  ()

Which doesn't unify