Help! Two extremely similar functions, yet one is forced to be div

[AZMCode]

I have been trying to create a small generator library for my own use, and I found that one piece of code I was writing, and encountering errors with, was very similar to an example within the documentation, yet wasn't working as well.

This is the code I've been writing:

pub effect<a> fun yield(item: a): ()

pub fun into-list<a,e>(gen: () -> <yield<a>|e> ()): e list<a>
  var l := []
  with handler
    fun yield(item) l := Cons(item,l)
    return(_) l.reverse
  gen()

This fails with the error message:

generator.kk(6,36): error: effects do not match
  context        :                                    l
  term           :                                    l
  inferred effect: <div|_e1>
  expected effect: $e

Adding the div effect both to the parameter and the return seems to work but..

A similar piece of code copied straight from the documentation, works perfectly fine without it

effect fun emit( msg : string ) : ()

fun emit-collect( action : () -> <emit|e> () ) : e string
  var lines := []
  with handler
    return(x)     lines.reverse.join("\n") 
    fun emit(msg) lines := Cons(msg,lines)   
  action()

Why is the div effect being forced on my version of the code, but not on the documentation's?
The only perceivable difference I can think of is the fact that I'm returning a list and not a string, as well as the fact my effect is generic, but I don't see how either of those would make my function possibly diverge

[TimWhiting]

Divergence inference is rather conservative. Koka still has room for improvement in this area, and this particular issue seems worth looking into. However, annotating with divergence isn't the end of the world. In general it is hard(impossible) to determine if a program will ever diverge (the halting problem). That doesn't mean that for certain programs it can't be done, but that in general you will likely end up having to annotate divergence, even where you know as a programmer that it will never diverge. Program analyzers are getting better at figuring out some invariants similar to humans, but there is definitely more work to be done.

[AZMCode]

Thanks for the tip!
I understand this can be done if it's absolutely necessary and no invariants are broken, but I also understand these kind of escape hatches to the protections set by the language should only be used as a last resort. Hopefully the divergence checker can detect these edge cases better.

[AZMCode]

@chtenb Thanks for the pointer!

[chtenb]

Or in some situations you can mark arguments to recursive calls as decreasing using unsafe-decreasing, which can be a clean way to hint the termination checker.

[AZMCode]

I'm guessing it doesn't apply in this exact situation though, as I can see no recursion happening

[chtenb]

Yeah, I meant in general