Polymorphic-typed var adds unnecessary effects to function call, but non-generic var does not

[fhackett]

I can't seem to pass a generic-typed var to a function without nonsensical effects getting added. This seems specifically tied to a bad interaction between typing and var, as I demonstrate below.

Here is a simple way to reproduce the situation:

fun test-fun(init: a, body: a -> <> ()): <> () {
  var foo := init
  body(foo)
}

Koka (version 2.4.0, Feb 6 2022, libc x64 (gcc)) complains like this:

test.kk(2,48): error: effects do not match
  context        : fun test-fun(init: a, body: a -> <> ()): <> () {
                   ...
                   }
  term           :                                                {
                   ...
                   }
  inferred effect: <div|_e>
  expected effect: (<>)

I'm not sure why this code might diverge; I'm just reading a var once.

If I free up the effects as e instead, it explains a different reason involving the var's state effect:

fun test-fun(init: a, body: a -> e ()): e () {
  var foo := init
  body(foo)
}

test.kk(4, 3): error: effects do not match
  context        :   body(foo)
  term           :   body
  inferred effect: <local<_h>|_e1>
  expected effect: $e
  because        : effect cannot be subsumed

This also doesn't make sense, because I'm not leaking the local at all. I don't even need it in this minimized code; it could be a val (and it would work if I did that).

The same problem happens even when just calling some other polymorphic function, rather than a polymorphic argument:

fun nom-nom(_: a): <> () {}

fun test-fun(init: a): <> () {
  var foo := init
  nom-nom(foo)
}

Changing var to val prevents all these errors, and so does changing a to int.

[TimWhiting]

I'm guessing it is because inference treats all references to the same variable the same, not distinguishing between the assignment vs reading context. However it is not clear to me why this doesn't work:

fun test-fun(init: int, body: int -> e ()): e () {
  var foo := init
  val foo2 = foo + 1
  body(foo2)
}

Because foo2 obviously contains a different value than foo, and is not a mutable reference, it only captured the value of a mutable reference at one point in time.

[TimWhiting]

Note that this works

fun test-fun(init: a, body: a -> <> ()): <> () {
  val foo = ref(init)
  body(!foo)
}