You want something called higher-order unification. For it to work you need totality checking. What you want is dependent types. Dependent types are sensible, n

You want something called higher-order unification. For it to work you need totality checking. What you want is dependent types. Dependent types are sensible, navigable, comprehensible, ah-what-I-wrote-last-week-is-understandable metaprogramming.