SolverSig: use an abstract type for O.tyvar

Currently the Output module signature used by SolverHi lets user provide their own ty type to represent elaborated types, but it defines

type tyvar = int

to directly inject solver-generated inference variable identifier as types.

There is a difference in abstraction level here: a signature such as mu : tyvar -> ty -> ty has a first parameter that is a low-level type fixed by the solver, and the second parameter that is a user-determined abstract type.

This lack of abstraction for type variables is problematic for users that would want to generate elaborated types on their own, without going through inference variables. For example, consider language-level support for parametrized type abbreviations:

type 'a cps = { run : 'r . ('a -> 'r) -> 'r }

If we want to reflect a user annotation of the form foo cps into a System F type ∀r. (〚foo〛→r)→r, we would want to generate a Forall quantifier for 'r. But how would the user pick a "fresh" nominal variable that is guaranteed to be distinct from those generated by the solver ? (There may be inference variables in scope used in foo).

Currently it is not possible for the user to generate System F binders that are guaranteed to be free of conflicts with solver-generated variables. The simple change in this commit makes this possible by making the tyvar type abstract, with an explicit conversion function between unique integers and user type variables.

This enables several possible strategies for users to implement a fresh_tyvar : unit -> tyvar on the side, that does not conflict with solver_tyvar. For example:

1. keep tyvar = int but store already-used identifiers in a hashtable that is used to provide a conflict-avoiding translation in `solver_tyvar.
2. use even numbers for solver variables and odd numbers for user variables
3. use type tyvar = Solver of int | User of ...

We could use approaches (1) and (2) above without the separation (with the conversion done purely on the client side), but we believe that enforcing the separation in the Output signature is the better design. It forces users to give a thought to their tyvar representation (it's easy to just use int and the identity), so they will know where to go change things if the need for user-side fresh variables arises. Without this API-level guidance, worse solution would be considered (our first idea when hitting this issue with @O_Olivier was to expose Inferno's fresh-identifier generator to clients).