effect cannot be subsumed in recursive function call

[chtenb]

I'm trying to make a version of the many parser combinator that uses less stack space than the one provided in std. However, I'm getting a compiler error that I don't understand, and I can't get it to work. Here is the code.

pub fun many(p : parser<e,a>) : <div,parse|e> list<a>
  val (acc, rest) = many-rec(p, get-input(), [])
  set-input(rest)
  acc.reverse

fun many-rec(p : parser<e,a>, input : sslice, acc : list<a>) : <div,parse|e> (list<a>, sslice)
  match parse(input, p)
    ParseOk(x, rest) -> many-rec(p, rest, Cons(x, acc)) // This is were the compiler error happens
    ParseError(_, _) -> (acc, input)

// Below is the necessary code for full reproducation

pub alias parser<e,a> = () -> <parse|e> a

pub type parse-result<a> 
  ParseOk( result: a, rest : sslice )
  ParseError( msg : string, rest : sslice )

pub effect parse
  fun satisfy( pred : sslice -> total maybe<(a,sslice)> ) : maybe<a>
  ctl fail(msg : string) : a
  ctl pick() : bool
  fun get-input() : sslice
  fun set-input(s : sslice) : ()

pub fun parse( input0 : sslice, p : () -> <parse|e> a ) : e parse-result<a> 
  var input := input0
  handle p 
    return(x)
      ParseOk(x,input) 

    fun get-input()  
      input 
    
    fun set-input(s)  
      input := s

    final ctl fail(msg)     
      ParseError(msg,input) 

    fun satisfy(pred) 
      val inp = input
      val m   = fn() : total _ { pred(inp) }
      match m() 
        Just((x,cap)) -> { input := cap; Just(x) }
        Nothing       -> Nothing

    ctl pick() 
      val save = input;
      match resume(True)
        ParseOk(x1,rest1) -> ParseOk(x1,rest1)
        err1 -> 
          input := save
          match resume(False)   // todo: limit lookahead?
            ParseOk(x2,rest2) -> ParseOk(x2,rest2) 
            _err2 -> err1  // todo: merge or pick closest?

The message:

repro.kk(54,25): error: effects do not match
  context        :                         many-rec(p, rest, Cons(x, acc))
  term           :                         many-rec(p, rest, Cons(x, acc))
  inferred effect: $e
  expected effect: <div,parse|$e>
  because        : effect cannot be subsumed

I find this odd, because to me it seems that many-rec has effect div,parse, so I wouldn't know why it inferred $e at the call site.
However, this function does compile when I remove the effect variables e, and replace them with <>. Is this a bug in the compiler, or is there some fundamental limitation that I don't understand?

[anfelor]

This error happens due to effect inference. The compiler first encounters parse(input, p) which the effect e introduced by p : parser<e,a>. Koka then tries to unify e with the effect of the function <div,parse|e>. But clearly, they can not be unified: Remember that Koka functions can have the same effect multiple times and so <div,parse|e> is strictly bigger than e.

Here is how to fix it: Remove the parse effect from many-rec since there are no parsing combinators in this function. You can mask the div effect so that it does not apply to parse(input, p):

fun many-rec(p : parser<e,a>, input : sslice, acc : list<a>) : <div|e> (list<a>, sslice)
  match mask<div>
      parse(input, p)
    ParseOk(x, rest) -> many-rec(p, rest, Cons(x, acc))
    ParseError(_, _) -> (acc, input)

But then you have to pay attention in the many function. If you write a handler for code involving many, you want to handle the calls to get-input and set-input, but not any other parse effects that the effect e is instantiated to. And the parse effect hidden in the alias parser<e,a> = () -> <parse|e> a is already handled above by the calls to parse(input, p). Because of this, you have to wrap many-rec into another mask<parse>:

pub fun many(p : parser<e,a>) : <div,parse|e> list<a>
  val input = get-input()
  val (acc, rest) = mask<parse>
    many-rec(p, input, [])
  set-input(rest)
  acc.reverse

[chtenb]

Thanks for the explanation. You highlight several points that weren't clear to me from the documentation. It makes more sense now.
However, I cannot get your last suggestion to work, because my parse effect is actually polymorphic (parse<t>), which I left out for reasons of simplification. When masking it in the many function, like mask<parse<t>>, the compiler gives a kind mismatch:

error: Invalid type
  type context :                          parse<t>
  type         :                          parse
  inferred kind: V -> HX
  expected kind: k -> V
  because      : The type cannot be applied to those arguments

[anfelor]

Hi @chtenb, this is hard to debug without access to an mwe, but Koka only allows you to mask effect labels, such as parse even when the effect is defined as parse<t>. Does the same error occur if you keep the polymorphic parse<t> effect, but change the masks to be mask<parse>?

[chtenb]

I could swear I tried that yesterday, but doing it now it actually compiles without errors. Thanks for your response!