Type.TypeVar.subNew.KindMismatch

[anfelor]

Koka v. 2.1.9 fails while compiling this merge function:

module haskell-sort

alias elem = int

fun merge(as_ : list<elem>, bs_ : list<elem>) : <exn,div> list<elem> {
    match(as_, bs_) {
        (Cons(a, as'), Cons(b, bs')) {
            if(a > b) then Cons(b, merge(as_, bs'))
            else Cons(a, merge(as', bs_))
        }
        (Nil, _) -> bs_
        (_, Nil) -> as_
    }
}

with:

failure during code generation:
  *** internal compiler error: Type.TypeVar.subNew.KindMismatch: 3(1::KCon V |-> std/core/list::KApp (KApp (KCon (->)) (KCon V)) (KCon V)<(syn:haskell-sort/elem::KCon V<>[std/core/types/int::KCon V]),>)(2::KCon V |-> std/core/list::KApp (KApp (KCon (->)) (KCon V)) (KCon V)<(syn:haskell-sort/elem::KCon V<>[std/core/types/int::KCon V]),>)(3::KCon E |-> std/core/types/handled::KApp (KApp (KCon (->)) (KCon HX)) (KCon X)<std/core/exn::KCon HX,>)

Notice also, that Koka inferred both the exn and div effect even though there is no good reason for this. Replacing as_ and bs_ in the branches by the matched terms does not change the error message.

[anfelor]

I could work around this by splitting the match into two nested matches.

[TimWhiting]

This is fixed?

[anfelor]

Yes, this is fixed. Koka continues to infer an unnecessary div effect since it can not see that this recursion is well-founded, but that is also common even for the much more advanced heuristics used in proof assistants so it does not seem to be worth the effort of fixing. Unfortunately, Koka also infers an exn effect since it can not see that the pattern matches are exhaustive. That would be worth fixing, but requires a discussion on which algorithm from the literature we should adopt.