Draft: Scheme names

This MR is for discussion rather than ready for inclusion.

It implements the idea of separating "term variables" (in the client) from "scheme variables" (in the solver), with the client keeping a mapping from term variables to scheme variables.

This change would also be useful to introduce rigid variables, which naturally come with a form of let-abstraction that is not bound to a term variable. (For example, (<term> : 'a. <type>) in the source term binds a polymorphic scheme.) Our current rigid-variable prototype has separate instance combinators for instances named by term variables and those coming from rigid-lets, which is unpleasant.

I have mixed feelings about the result:

• I like the fact that the solver is less coupled to the input language
• I hoped that we could remove a kind of environment in the solver (by having the user pass schemes around directly), but in fact we cannot

There are things in the API that could be changed in various ways (I'm not sure which is best):

• the user-visible type of let* combinators could be changed to be more CPS-style
• or, conversely, it could return the decoded scheme instead of having a separate scheme_witness combinator

(My temptation would be to go full-CPS, as we learned that it works better for exists:

(* in master *)
  val let1: tevar -> (variable -> 'a co) -> 'b co ->
            (scheme * tyvar list * 'a * 'b) co

(* in this PR *)
  val scheme_witness : scheme_variable -> O.scheme co
  val let1: (variable -> 'a co) -> (scheme_variable -> 'b co) ->
            (tyvar list * 'a * 'b) co

(* but we could also do *)
  val scheme_witness : scheme_variable -> O.scheme co
  val let1: (variable -> 'a co)
         -> (scheme_variable * (tyvar list * 'a) co -> 'b co)
         -> 'b co