Abstract ranks in the unifier

What this PR does is rather simple, but why I am proposing it requires more explanation.

What

To an Inferno beginner it may seem that Unifier and Generalization are nicely separated, independent modules providing services of interest to the solver: union-find / unification on one side, levels / generalization on the other. But in fact this rosy picture does not hold in reality:

• Generalization knows about the Unifier as it needs to manipulate (unifier) variables
• Unifier knows about Generalization as its variables carry a rank, which is updated by unification.

In the current codebase, Generalization depends on the Unifier (as a functor argument), but Unifier does not depend on Generalization (this would be a cyclic dependency). Instead the Unifier embeds the assumption that variables have ranks which are integers, and computes a min on unification. This is ugly: there is no reason that Unifier should know about ranks.

(Note: you would think that Generalization then encapsulates fresh-variable generation to set the rank correctly, but in fact it does not, it exposes a G.no_rank : int constant for the user to create variables, and then the solver sets it to the current rank during resolution. Ugh. Because the user creates unification variables, not the solver, we don't know at creation time what the right rank is anyway. Ugh again.)

What this MR does is to abstract the notion of ranks away in the Unifier. Unifier is now a functor parametrized on a type of ranks, with a merge functions to merge two ranks together during unification. Generalization decides that ranks are in fact integers by instantiating the Unifier module. (So instead of Unifier being an input of the Generalization.Make functor, it is now instantiated within the functor and returned bundled.)

A consequence of this change is that the user and the solver now have to go through Generalization to create new variables, which I think is actually the better design. (I have another MR in preparation that is going much farther in the direction of changing the way the solver and users deal with variables, stay tuned!)

Why

I worked on this MR as a preliminary step towards a very-experimental change to the solver as part of our work on "Frozen Constraints" with @omartino. (The change is to turn the generalization state, which is currently an array of variable regions, into a tree of variable regions; the notion of rank as an index into a linear array does not work anymore, and the "rank" becomes the region itself. Wow!) But of course I am not planning to propose this work-in-progress for upstreaming soon, so this MR happily remained in our experimental branch.

However, during our current work with @omartino on abbreviations/multiequations (trying to polish Carine Morel's implementation), we noticed that we are spending a lot of time fighting against circular dependencies between the various components of Inferno. Things that sound easy on paper are in fact very hard to implement, or refactorings very hard to perform, because of the tight interconnections between all the components.

The dependency-cycle involved in the present MR (between Unifier and Generalization) is not directly related to the issues we have with the multiequations code. But now I have the impression that any change that clarifies the dependencies between Inferno components, and reduces coupling between them, any such change is good to have, because it is going to avoid refactoring issues down the road.

This is why I am proposing the MR: it is just a small refactoring, there is no obvious/immediate need to have the logic upstream (except for the abstract sentiment of moving towards an objectively-better design). But I think that, sooner rather than later, it is going to make things simpler for us somewhere.