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

I suppose that those markers were used in scripts to produce output
for the Inferno paper. As far as I know, there is no plan to write
another paper on the same state-of-the-art literate-programming
technology, and those markers are slightly annoying for people reading
and, especially, modifying the code.

rename client/Client into client/Infer

See merge request !3

Nominal2Debruijn.concat : env -> env -> env

See merge request !2

We want to turn the client code into a Dune library called 'client',
separated from test binaries. Without the rename, as reported by
Olivier Martinot, dune complains about conflicting names.

This function will be useful to implement certain typing rules that
concatenate environments together. For example, in certain formulation
of pattern-matching, typing a pattern returns an environment fragment,
to be concatenated onto the current environment.