Turing Completeness + Dataflow Unification = Arbitrarily invertible (pure, nonrecursive) functions? Assume we are working in a Turing-complete, referentially-transparent, higher-order language that supports arbitrary dataflow unification.  Shouldn't it then be possible to construct the following function (using Haskell-like syntax, because that's what I'm most familiar with)?

-- Takes an arbitrary pure function and constructs its inverse.  
-- If the passed-in function is recursive, the result is not guaranteed to terminate
invert :: (a -&gt; b) -&gt; b -&gt; a
invert f r = declare a in let r =|= f a in a


(if =|= is the dataflow unification operator).

Is this indeed possible in such a language?  If so, why haven't people leapt at this before?  If not, where did my reasoning go wrong?
Dataflow unification behaves as you expect on first-order data (numbers, booleans, lists, trees, etc.) but can fail for higher-order data such as functions. In general, unifying functions requires using full higher-order unification, which has terrible performance, up to and including frequent failure to terminate (as it must, since otherwise it would solve the halting problem).  

Higher-order logic languages such as $\lambda$-Prolog and Curry typically use restricted forms of higher-order unification, to get better efficiency at the price of completeness.