SolverSig: use an abstract type for O.tyvar

See merge request !7

Use n-ary products in the client to expose programming difficulties

See merge request !6

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 need 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 was to
expose Inferno's fresh-identifier generator to clients).

There is no principal way to type (Proj<3> t) without type-based
disambiguation, as we do not know (at constraint-generation time) what
is the arity of the tuple type of t.

Note: to avoid ambiguities, n-ary product types are printed with
braces as delimiters: `{a * b * c}` is a ternary product, distinct
from `a * {b * c}`, `{a}` is distinct from `a`, and `{}` is the unit
type (empty product).

Gabriel Scherer authored Jun 11, 2020 and POTTIER Francois committed Jun 12, 2020

This will make it easier to write pure-system-F tests.

Gabriel Scherer authored May 08, 2020 and POTTIER Francois committed Jun 12, 2020

The tests as selected take 0.6s on my machine, and they should help
catch some simple mistakes.

Gabriel Scherer authored May 03, 2020 and POTTIER Francois committed Jun 12, 2020

Naming convention:
- TestFoo: a bunch of tests to execute
- CheckFoo: definitions of interesting properties to check (in tests)
  and helper functions to check them

remove the BEGIN/END comment markers

See merge request !5