Haskell port of Tobias Nipkow's LICS 1993 paper on Higher-Order Pattern Unification using the Unbound libirary.
The main function runs the Example 3.2 in Nipkow's paper.
The code here is trying to do a bit more than the paper. The code of the paper only describs solving the unification problem of a single pair of higher-order patterns. However, what we almost always want is to solve a conjuction of unification pairs where some of the logic variables are shared among them.