Is there a way to mark while as non divergent?

[ov7a]

Consider the following code to compare two vectors:

  var i := some_end
  var j := some_other_end
  while { (i >= some_start) && (data.at(i) == other_data.at(j)) }
     i := i - 1
     j := j - 1
  ...   

while always has div effect. However, in this case, I know that it must end. How do I tell koka compiler that? I don't want to pass around div.

One solution might be to re-implement while as a recursive call with pretend-decreasing, but that feels like an overkill...

Another solution is to use unsafe-total, but it removes other effects as well

[TimWhiting]

Use, pretend-no-div:

koka/lib/std/core/undiv.kk

Line 24 in 0bee513

pub fun pretend-no-div( action : () -> <div|e> a ) : e a

[ov7a]

Oops, I was one step away from it. Thanks!