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

exception Unreachable

fun('a)
    nth_safe(x::xs, n) = if (n = 0) then x else nth_safe(xs, n-1)
  | nth_safe _ = raise Unreachable
where nth_safe <| {l:nat}{n:nat | n < l} 'a list(l) * int(n) -> 'a