Pattern unification is a simplified form of higher-order unification in which existential variables only appear applied to distinct universal variables. Thus, for instance, an equation such as $M \,x\, y\, z = t$ can be solved by $M = \lambda x y z.t$, assuming various side conditions hold (e.g. its RHS is in scope for $M$, has a rigid head, and contains no occurrences of $M$). Unlike full higher-order unification, pattern unification has most-general unifiers and a fairly well-known algorithm to find them.
It seems to be fairly well-known that the "universal variables" occurring as arguments of an existential variable in a pattern unification equation can also be eta-expanded forms of variables. For instance, $M \, x \, (\lambda u.y\, u)\,z = t$ is equivalent to $M \, x \, y \, z = t$ and has the same solutions. Often this is handled in algorithms by eta-contracting the arguments of $M$, which is slightly odd (since in most other contexts it seems better to treat eta-equivalence through expansion) but seems to mostly work.
However, what about something like $M \, x\, (\lambda uv. y\, v\, u)\, z = t$? Here the variable $y$ is not just eta-expanded, but its two arguments are swapped. But in the presence of eta-conversion, knowing the value of $\lambda uv. y\, v\, u$ is equivalent to knowing the value of $y$, and so the above equation has the solution $M = \lambda x y' z. t[y \mapsto (\lambda uv. y'\, v\, u)]$. Has anyone considered extending pattern unification to include cases like this?