Unify algorithm implemented in ocaml according to Alin Suciu's "Yet Another Efficient Unification Algorithm"

unify.ml

module type TERM = sig
  type t
  type tvar
  val var_opt : t -> tvar option
  val compare_var : tvar -> tvar -> int
  val same_functor : t -> t -> bool
  val args : t -> t list
end

module Make (Term : TERM) = struct
  module VarMap = Map.Make (struct
      type t = Term.tvar
      let compare = Term.compare_var
    end)
  exception Fail
  let unify sx sy =
    let bindings = ref VarMap.empty in
    let bind v t = bindings := VarMap.add v t !bindings in
    let rec loop sx sy =
      match sx, sy with
      | x :: sx, y :: sy -> (
          match Term.var_opt x, Term.var_opt y with
          | None, None -> (
              if Term.same_functor x y then
                let cons a b = b :: a in
                let sx = List.fold_left cons sx (Term.args x) in
                let sy = List.fold_left cons sy (Term.args y) in
                loop sx sy
              else raise Fail
            )
          | Some vx, None -> (
              match VarMap.find_opt vx !bindings with
              | Some x ->  (
                  match Term.var_opt x with
                  | Some vx -> bind vx y; loop sx sy
                  | None -> loop (x :: sx) (y :: sy)
                )
              | None -> bind vx y; loop sx sy
            )
          | None, Some vy -> (
              match VarMap.find_opt vy !bindings with
              | Some y -> (
                  match Term.var_opt y with
                  | Some vy -> bind vy x; loop sx sy
                  | None -> loop (x :: sx) (y :: sy)
                )
              | None -> bind vy x; loop sx sy
            )
          | Some vx, Some vy -> (
              match VarMap.find_opt vx !bindings, VarMap.find_opt vy !bindings with
              | None, None -> bind vx y; loop sx sy
              | Some x, None -> bind vy x; loop sx sy
              | None, Some y -> bind vx y; loop sx sy
              | Some x, Some y -> loop (x :: sx) (y :: sy)
            )
        )
      | [], [] -> ()
      | _ -> raise Fail
    in
    try loop sx sy; Ok (!bindings) with Fail -> Error ()
end