Communicating missing matches

[schicks]

Koka infers an exn effect when a pattern match is incomplete. This makes sense, but does make it hard compared to other languages with pattern matching to use the compiler errors to determine what is missing. For example;

type integral {
  Infinity
  Undefined
  Integer( i : int )
}

fun divide (a: integral, b: integral): integral {
    match ((a, b)) {
        (Undefined, _) -> Undefined
        (_, Undefined) -> Undefined
        (Infinity, Infinity) -> Undefined
        (Infinity, Integer(_)) -> Infinity
        (Integer(_), Infinity) -> Integer(0)
        (Integer(num), Integer(div)) -> if (num % div == 0) then Integer(num / div) else Undefined
    }
}

The compiler complains here with this message;

context        : fun divide (a: integral, b: integral): integral {
                   ...
                   }
  term           :                                                 {
                   ...
                   }
  inferred effect: <exn|_e>
  expected effect: (<>)

I can't actually see what pattern I'm missing here. That makes it much harder to eliminate the exception effect and make sure the code is sound. Is there a way to get the compiler to expect a match statement to be complete? It feels to me like ideally the compiler would just require matches to be exhaustive, and to get back to the current behavior you could just add a catchall pattern that would throw.

[anfelor]

I can confirm that the exn effect is not inferred anymore if a match on _ is appended. But I also think you are not missing any pattern here, so this seems to be a bug.

[schicks]

So the fact that this particular match has a bug wasn't quite my point. What I was getting at was that requiring matches to be exhaustive and letting users throw an exception in a catchall case if they wanted the current behavior would be more flexible and allow the compiler to be more helpful to the user.

[anfelor]

I agree, it would be better to fail to compile if a match isn't exhaustive (or give a compile-time warning). But it is also a bug, because the match is exhaustive here and the compiler seems not to notice.