I'm kind of wondering why we haven't seen any notable (unless I've missed something) languages with full unification escape from academia into wider use since Prolog -- I know on the academic side there is Oz, which is a very interesting language, but I don't get the impression that its seen much, if any, use in industry.

"Erlang has pattern matching, while Prolog has unification."

Ah, yes. My first reaction to seeing pattern matching in ML: "Hey, this is literally half of unification."