TODO

Performance and Software Architecture

In Generalization, it would be possible to merge rank and generic into a single field. This can wait until the code is stable. (Try it and benchmark.)

Remove the ~rectypes label and use a variant type.
Offer an n-ary conjunction that produces a list as its semantic value: that is, a list combinator of type 'a co list -> 'a list co. Do the same for option. These combinators could be defined in terms of CPure, CConj, and CMap, but I would favor making them primitive, so as to avoid intermediate allocations.
Simplify the treatment of names in constraints. Treat term variables and type variables in the same way, if possible. Treat all binding sites (CExist, CLet, etc.) in the same way, if possible. Let the user decide whether to pick a fresh name or use a predetermined name. Avoid a design that would require multiple name transformations (i.e., composing multiple environment lookups).
Can we remove the redundancy between instance and `instance_? (See next item.)
Introduce a combinator ignore : 'a co -> unit co that allows the solver to solve a constraint without computing its semantic value. This could be marginally useful, e.g., by allowing Alice to package type inference and elaboration together, as a black box of type F.term co, and allowing Bob to pay only the cost of type inference, assuming he does not need elaboration. Also, it could remove the need for a primitive instance_ combinator, as instance_ x ty would correspond to ignore (instance x ty).
Introduce a forall combinator so as to make it easy to express ∀α.c.

Attach exploitable information to the exception VariableScopeEscape.
Introduce more powerful combinators to handle errors in a programmatic way. Change the type 'a co to ('a, 'b) co? Introduce a CCatch construct to allow recovering after an error? (Think about Merlin, where type inference and elaboration are allowed to continue.) In a conjunction, distinguish an error in the left branch (producing just an error) and an error in the right branch (producing a value and an error)? Offer a way of decoding types after an error has occurred.
Better distinguish between decoding in normal mode (where the decoder discovers generic variables only) and decoding in error mode (where the decoder does not discover any generic variables, but may find flexible and rigid variables). In the latter case, when decoding a variable, offer sensible ways of naming this variable; this may require a reverse lookup in an environment (beware of shadowing).

Document that decoding takes place after the unifier is done; decoding is performed either during elaboration or after the unifier has encountered an error.

Improve the coverage of the test suite. Add explicit negative test cases.
Run the random tests in parallel. (Parameterize TestMLRandom with the number and size of the tests, with the rectypes flag, etc., and run multiple instances in parallel.)

Introduce a dynamic check to ensure that the unifier never runs after the decoder has been invoked.

Include ranges in System F terms, and have the type-checker print the relevant range when a type error occurs.
The decoders are careful to perform as much sharing as possible, but the conversion of nominal types to de Bruijn types causes this sharing to be lost.