There is no type information at runtime at all in OCaml. Once the program has been typed, the program is translated into an untyped lambda-calculus and all type information is throw away. In particular, pattern matching is compiled into this untyped lambda-calculus using if/then/else (and switch statement, and exception and exceptions handlers, ...). The type system is sufficient to detect before this compilation if the pattern is total or if it need to add a failure case. In this case, the `Match_failure` is just a catch-all term in this conditional expression.

For instance

  let f x = match x with
  | [] -> ()

is translated into

    (is_empty/267 =
       (function x/269 : int
         (if x/269
           (raise (makeblock 0 (global Match_failure/18!) [0: "r.ml" 1 17]))
           1)))

where you can see the exception being build and raised in the `then` branch of the test. Contrarily, the total function

  let is_empty x = match x with
  | [] -> true
  | _ :: _ -> false

becomes

  (let (is_empty/267 = (function x/269 : int (if x/269 0 1)))

And since the function doesn't need to handle the failure case, it doesn't have that `(raise ...)` case.

Another important point is that type system information is only needed to check the exhautiveness of pattern matching in presence of GADTs. Otherwise the exhautiveness of pattern matching can be checked using syntatic criteria on the pattern matching and type definitions.