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

When @O_Olivier started working on implementing algebraic datatypes and records, we realized that it was difficult to use the exist combinator a dynamically-known number of times (for each element of a list, for example). We went into a few iterations to try to solve this issue, and we have a final proposal that we think makes it easier than the current API.

The current PR does not propose any change to the current API, but it exposes the problem by adding a simple client-language feature that requires creating dynamically-many inference variables: n-ary products, with Tuple ts as an introduction form (surface syntax (t1, t2, ...)), and LetProd(xs, ts, u) as an elimination form (surface syntax let (x1, x2, ...) = (t1, t2 ..) in u. The type-inference code for these two constructs is written in CPS style.

Remarks:

1. Prod(i,t) is removed from the ML language, because this form does not allow principal type inference for n-ary tuples (the arity of the tuple is not forced by the syntax, and there is no arity-polymorphic getter type). Currently the branch offers both Proj and LetProd on the System F side, because both are easy to type-check. (We could remove Proj if someone insisted.)
2. The inference rules for both constructs are written in a "generic" style, where the list-traversal functions take a continuation that expect the list of corresponding inference variables. We later found out that it is easier to write the code in a more "specialized" style where those traversals are specialized to the one continuation needed by the inference rule. Someone could instead argue that it's best to have the simplest possible code instead, and I would be happy to provide the simpler implementation if preferred.

For a concrete example of (2), the Tuple case currently reads as

      begin
        let rec traverse
            (ts : ML.term list)
            (k : variable list -> 'a co)
        : (F.nominal_term list * 'a) co =
          match ts with
          | [] ->
            map (fun r -> ([], r)) @@
            k []
          | t::ts ->
            exist_ @@ fun v ->
            map (fun (t', (ts', r)) -> (t'::ts', r)) @@
            hastype t v ^&
            traverse ts @@ fun vs ->
            k (v :: vs)
        in
        traverse ts @@ fun vs ->
        w --- product vs
      end <$$> fun (ts', ()) ->
      (* The System F term. *)
      F.Tuple ts'

the non-generic version, with the continuation inlined, reads as follows:

  | ML.Tuple ts ->
      let rec loop (acc : variable list) = function
        | t::ts ->
          exist_ @@ fun v ->
          hastype t v ^& loop (v :: acc) ts
          <$$> fun (t', ts') -> t'::ts'
        | [] ->
          let vs = List.rev acc in
          w --- product vs ^^ pure []
      in
      loop [] ts
      <$$> fun ts' -> F.Tuple ts'

I don't find this specialized approach very natural or modular, but it does result in simpler code.