purer constraints

This PR started from the observation that the syntax of raw constraints is mutable: it is not valid to run solve twice on the same constraint, the second run will explode with an error. This comes from the fact that (mutable) unification variables are embedded in the constraint syntax, and mutated during resolution. In particular, at the end of the first resolution those constraints have a rank (their final rank in the solution); on the second run, the solver expects existentially-bound variables to have no_rank and blows up. This is ugly!

The idea to avoid this was to introduce an indirection: inside the constraint syntax, have a pure representation of variables (just an integer, for example). During resolution, map those pure variables to unification variables. This sounds simple, but many aspects of the current implementation make it difficult:

• The "decoder" in SolverLo is provided independently of the solver, it works on any unification variable that was solved previously. This API needs to change if the solver has local state that is required to decode its solution.
• The write-once references used in the constraint syntax are very awkward to adapt. Should they now store pure variables to decode, or inference variables? In general it is hard or impossible to go back from an inference variable to a pure/syntactic variable name, so storing pure variables is difficult/impossible. Storing inference variables is also awkward, if we try to remove this type from the constraint syntax.

Finding solutions to these problem step by step led to an important change to the codebase: instead of having mutable constraints in SolverLo, and an immutable applicative interface on top of them in SolverHi, the SolverLo constraints are now both immutable and applicative, using a GADT. Write-once references are gone. Most of the SolverHi logic can then be removed, or becomes a thin renaming layer on top of SolverLo constraints. We could seriously consider removing the distinction in the future and having a single Solver module.

There is a performance impact to this change (mostly to the part that adds an indirection between pure variables and inference variables: now we have to lookup the inference variable in a hashtable). In my testing, running the random checks moves from about 3.0s to about 3.3s. I tried to understand better the performance profile, and concluded that this was not easily done without better profiling tools in place (I think we should consider using Landmarks if we are serious about Inferno's performances), and I think that it is not a priority right now.

This MR is correct and can be reviewed either as a whole or commit-per-commit, but I still marked it as a WIP for several reasons:

• This is an ambitious change that you probably want to discuss first.

• I think that we should consider merging SolverLo and SolverHi in a single Solver module, but before doing this tedious work I wanted to get your opinion on that. (If we do this, we don't technically need to expose the type of constraints to the outside world. Should we still expose it, because it is the soul of Inferno?)