Multiplicity polymorphism: unification up to

[aspiwack]

Depends on #59

In #59, unification of multiplicity polynomials is done syntactically (in particular (p + q) + r will not unify with p + (q + r)). This won't be comfortable in the long run, so we need to add some domain-specific knowledge to multiplicity unification.

The goal is to have unification up to all semiring laws, or at least a sufficient approximation. In particular q*(p + (1*r + s)) should unify with (q*p +q*r) + q*s. In AC unification, the hard part is splitting:

p + q unifies with a+b+c in one of two ways: either p = x+y and q=z or p=x and q=y+z (for x,y,z any permutation of a,b,c).

We may choose to be imprecise with regard to splitting to make implementation easier. This is yet to be decided.