Higher-order pattern unification (Miller 1991).

A higher-order pattern is a βη-normal term in which every free variable F occurs only in applications of the form $F(x_1, \dots, x_n)$ where the arguments $x_1, \dots, x_n$ are pairwise distinct bound variables. Unification over the pattern fragment is decidable and unitary: when a unifier exists it is unique up to α-renaming, so this entry point returns either a single most-general unifier or :error.

The implementation realises Miller's algorithm with four rules:

• decomposition of rigid-rigid pairs whose heads agree,
• inversion of a flex–rigid pair $F(\bar x) \overset{?}{=} t$, with pruning of any nested flex application whose arguments would otherwise reach a binder outside $\{\bar x\}$,
• alias for flex–flex pairs with the same head — bind the variable to a fresh meta over the positions on which the two argument lists agree,
• intersection for flex–flex pairs with distinct heads — bind both variables to a fresh meta applied to the bound variables they share.

Termination is by structural recursion on the work-list; no depth bound is needed.

Use ShotUn.pattern_unify/1 as the public entry point. Inputs containing non-pattern terms raise ArgumentError.