question about type systems

a.ml

type exp =
  | Int of int
  | Succ of exp

(* This is what we want to write: *)
(* let rec step (e : exp) : exp option = *)
(*   match e with *)
(*   | Int _ -> None *)
(*   | Succ (Int i) -> Some (Int (i + 1)) *)
(*   | Succ e -> Some (Succ (step e)) *)
(*                       ^^^^^^^^ *)
(* Error: This expression has type exp option *)
(*        but an expression was expected of type exp *)

(* ... but it gives us a type error *)

(* So then we have to write: *)
let rec step (e : exp) : exp option =
  match e with
  | Int _ -> None
  | Succ (Int i) -> Some (Int (i + 1))
  | Succ e -> match step e with
              | Some e' -> Some (Succ e')
              | None -> None
(*            ^^^^^^^^^^^^^^ *)
(* But we know ^this^ is unreachable because the only thing which
could step to `None` is `Int i` which is matched by the preceding
case *)

(* So then something like *)

exception Unreachable

let rec step (e : exp) : exp option =
  match e with
  | Int _ -> None
  | Succ (Int i) -> Some (Int (i + 1))
  | Succ e -> match step e with
              | Some e' -> Some (Succ e')
              | None -> raise Unreachable

(* Or "better" yet *)
let unsafe (arg : 'a option) : arg =
  match arg with
  | Some v -> v
  | None -> raise Unreachable

let rec step (e : exp) : exp option =
  match e with
  | Int _ -> None
  | Succ (Int i) -> Some (Int (i + 1))
  | Succ e -> Some (Succ (unsafe (step e)))

(* So is this:
   1 - the wrong use of types
   2 - a deficiency of the type system
   3 - a feature of the type system
   4 - something else *)

(* And are there type systems which could know that code is unreachable *)