Based on #138

This PR adds a new mode constraint solver to the type checker. The new solver supports morphisms between mode axes. An example of such morphisms is unique_to_linear :

u2l unique = once
u2l shared = many

The new solver allows us to apply such morphisms to mode variables, and use the resulted variables in submode constraints. All morphisms needs to be monotone and having appropriate left/right adjoint for the solver to work. We slightly extend the solver so that antitone morphisms can also work with some limitations.

Some other notable features/changes:

• In light of the incoming seven hundred mode axes, and how costy it would be to call submode m0.x m1.x for each axis x, we introduce the product object in the category so that submoding relation can be expressed on the product as a whole. Note that axes of opposite polarities can't be product together. As a result, currently locality and linearity are packed into the product object, while uniqueness (being of negative polarity) is standalone.
• Previously the 3-valued locality is represented as its image into the 2-valued locality via mappings. It is now natively represented, together with all mappings between 2- and 3-values in a chain of adjunction.
• After talking to @stedolan , vlower is no longer compressed. It was compressed in the hope for an optimization - but that optimization turned out to be hard to implement in ocaml. Compressing vlower would also cause explosion problem once morphisms are introduced.
• As before, the lower bound of variables are not precise, but updated on demand. The original update method no longer works with morphisms in circular paths. The update method we adopt is to repreat submode_vc until it succeeds.
• There was a circular dependency between mode.ml and types.ml. Previously (in the uniqueness PR) it was solved by preceeding type definitions which has became dirtier with bigger types. This is now solved by solver.ml having its own implementation of logging (which is minimalistic).