Is it possible to make this function generic?

[codehz]

I'm trying to make a collector but I'm running into a problem where I can't make the function generic (it is only works when I specify the final type)

module ctx-yield

import std/core/types

effect<a> fun yield(x: a): ()

fun traverse(xs: list<a>): yield<a> (){
  match xs {
    Cons(x,xx) -> { yield(x); traverse(xx) }
    Nil        -> ()
  }
}

// If I change the <int> to <a>, the type checking will failed
fun collect-arr(action: () -> yield<int> ()): list<int> {
  var acc := ctx _
  handle(action) fun yield(i) {
    acc := acc ++ ctx Cons(i, _)
  }
  acc ++. Nil;
}


pub fun main() {
  var collected := collect-arr {
    [1,2,3].traverse
    yield(5)
  }
  collected.show.println()
}

the error is

effects do not match
context        : fun collect-arr(action: () -> yield<a> ()): list<a> {
                 ...
                 }
term           :                                                     {
                 ...
                 }
inferred effect: <div|_e>
expected effect: total

[codehz]

Ok, I found a way is to add div to type

fun collect-arr(action: () -> <div, yield<a>>()): div list<a> {
  var acc := ctx _
  handle(action) fun yield(i) {
    acc := acc ++ ctx Cons(i, _)
  }
  acc ++. Nil;
}

but the question is, why they behavior differently?

[TimWhiting]

You don't actually have to add div to the function argument type in this case. Just the result type.

fun collect-arr(action: () -> yield<a> ()): div list<a> {
  var acc := ctx _
  handle(action) fun yield(i) {
    acc := acc ++ ctx Cons(i, _)
  }
  acc ++. Nil;
}

There is no change in behavior of the program. The div effect signifies that something can diverge (not terminate). It doesn't say that it must diverge, it is just saying that in pathological cases it might.

However, in this particular case it seems to be an issue with local variable inference. You can switch it to explicitly use a heap allocated reference, and it can infer a non-divergent type:

fun collect-arr(action: () -> yield<a> ()): list<a>
  val acc = ref(ctx _)
  with handler 
    fun yield(i)
      acc := !acc ++ ctx Cons(i, _)
    return(_)
      !acc ++. Nil
  action()

The reason it mistakenly adds divergence I believe is due to the translation of local variables in connection with the following statements from std/core/types.kk

// The predicate `:hdiv<h,a,e>` signifies that if the type `:a` contains a reference to `:h`,
// then the effect `:e` must contain the divergent effect (`:div`). This constraint is generated
// when reading from the heap (see `(!)`) and is necessary to catch cases where code can diverge
// by storing self referential functions in the heap.
pub type hdiv :: (H,V,E) -> P

// Read the value of a local variable.
pub inline extern local-get : forall<a,s,e> (v: local-var<s,a>) -> <local<s>|e> a with(hdiv<s,a,e>)

I feel like this statement doesn't apply, which is why the ref() works, but it seems like local variables sometimes don't do as well during inference.