A 'textbook' unification algorithm

[h0nzZik]

I was inspired by this code and the associated paper. But the specification of when the algorithm is supposed to fail is weird there:

Inductive UnifyFailure : list_constr -> Prop :=
  | occ_fail  : forall v t lc, occurs v t -> UnifyFailure (((var v), t) :: lc)
  | occ_fail'  : forall v t lc, occurs v t -> UnifyFailure ((t, (var v)) :: lc)
  | con_app   : forall l r lc, UnifyFailure ((con,(arr l r)) :: lc)
  | app_con   : forall l r lc, UnifyFailure (((arr l r), con) :: lc)
  | app_left  : forall l l' r r' lc, UnifyFailure ((l,l') :: lc) -> UnifyFailure (((arr l r), (arr l' r')) :: lc)
  | app_right  : forall l l' r r' lc, UnifyFailure ((l,l') :: (r, r') :: lc) -> UnifyFailure (((arr l r), (arr l' r')) :: lc)
  | constr_rec : forall t t' l, UnifyFailure l -> UnifyFailure ((t,t') :: l)
  | subs_rec : forall t t' s l, UnifyFailure (apply_subst_constraint s l) -> UnifyFailure ((t,t') :: l).

With such a definition, one is not able to prove the completeness lemma I wanted.
However, with my definition (unify_failure), it works:

Lemma unify_failure_is_severe
  {Σ : StaticModel}
  (es : list eqn)
:
  unify_failure es ->
  ~ exists s : SubT,
    is_unifier_of s es
.

I wonder why the paper didn't contain any result like that - the specification UnifyFailure is not very helpful in saying why the algorithm should fail. Why would anyone take it as a specification?
That said, it was definitely easier to take the paper and this inductive as a starting point than starting from scratch.