[Agda] Questions about unification

[Roman]

I wonder, why prune when you can just solve? Consider the flexRigid case

    U [vs] =?= t

where `vs` is a list of variables (not necessarily different). We
traverse `t` and check whether

  1) each variable in `t` occurs at least ones in `vs`. If not so,
then throw a "can't unify" error.
  2) each variable in `t` occurs exactly ones in `vs`.
    2.1) If so, we have a solution. I.e. this equation:

        U [x, y, w, w] =?= App (Var x) (Var y)

      gets solved by

        U [x, y, _, _] := App (Var x) (Var y)

      without any explicit pruning.
    2.2) If not so, then we can prune sometimes. E.g.

        U [x, y, w, w] =?= App (Var x) (Var w)

      results in pruning of `y` if the type of `w` doesn't depend on it.

Does this sound right?