> To be honest, I am not sure what is meant by "pattern matching".

I'd say that "pattern matching" is unification, where there are no free variables on the right side and the left side is the "pattern" to match.

As Prolog code, something like

    ?- [X|Xs] = [a, b, c]

where X = a and Xs = [b, c] would be "pattern matching" the head and the tail of the list [a, b, c], but

    ?- [X|[b, c]] = [a|Xs]

where X = a and Xs = [b, c] would be "real" unification, if [X|[b, c]] would be valid syntax.

Oh, and both unification for type checking (inference) and pattern matching are compile time actions (or done before evaluating the generated functions).

A (simple) pattern match like

    match list with
      | head :: tail -> do_something(head, tail)
      | [] -> do_something_else()

is "compiled" to something like

    if list != []
      then do_something(head(list), tail(list)) 
      else do_something_else()