Decidable higher-order matching for the second-order fragment.

Higher-order matching is the task of finding a substitution σ such that σ(s) ≡βη t for two given terms s and t where t is _ground (contains no free variables). General higher-order matching is decidable (Stirling 2009) but impractical to implement; this module restricts to Huet's second-order fragment, where every variable and constant in the problem has a type of order at most 2.

Termination is guaranteed by a structural argument on the multi-set of right-hand sides: every imitation step strictly decreases the total size of the targets, and every projection step eliminates a flex variable without introducing new ones (for order-1 flex arguments) or introduces strictly-smaller-order metas (for order-2 flex arguments). No depth bound is needed.

Inputs that violate the second-order or ground-target preconditions raise ArgumentError.