Currently in solver.ml there is Solver_mono which can handle monotone morphisms. Based on that, there are two polarized solvers Positive and Negative, used for comonadic and monadic axes respectively. The intention is such that user code (mode.ml) doesn't need to think about the flipping. This has two issues:

• It turns out that mode.ml still needs to think about the flipping in some definitions but not all of them. This mixture, and the fact that both mode.ml and solver.ml handles flipping, makes the code more confusing.
• Positive.t and Negative.t are different types and complicates type polymorphism. In particular, Value.Axis.t is a complicated GADT.

So we remove both Positive and Negative, and let mode.ml to be the only file that cares about flipping. We move some code such that the flipping are concentrated to fewer places.

The downside is that code that uses mode might see (Uniqueness.Const.t, allowed * disallowed) mode instead of (disallowed * allowed) Uniqueness.t. The two types are the same, but ideally we want to show the latter.

Review

Please review by commit.