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 -> b) -> b -> 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.

StackExchange Computer Science Q#684, answer score: 7