(*
 * This simple examples shows that dependent types can help eliminate
 * unreachable matching clauses, and therefore speed up the code.
 *)

exception Unreachable

fun('a,'b)
    zip_safe(nil, nil) = nil
  | zip_safe(x::xs, y::ys) = (x, y)::zip_safe(xs, ys)
  | zip_safe _ = raise Unreachable (* we can verify that this is indeed unreachable *)
where zip_safe <| {n:nat} 'a list(n) * 'b list(n) -> ('a * 'b) list(n)