AUTOMAP

[athas]

This PR adds a new type checker and a bunch of the infrastructure necessary for supporting AUTOMAP. There is a lot of work to do before it can even handle all programs, and even more before it is of sufficient quality to actually use. I can think of at least the following issues:

• The two-stage type checking is a bit buggy when it comes to propagating existential sizes in higher order functions from one to the other. It means that programs like x |> filter p |> length do not work.
• The type checker is about 3x slower than before, largely because of redundant work, but also because it is completely unoptimised. The new type checker is however possible to implement more efficiently than the old one.
• AUTOMAP-related type errors are atrocious.

AUTOMAP currently uses GLPK to solve the linear problems. This is not a dealbreaker, but it'd be worth considering whether we can get rid of it. The linear problems we produce and solve are pretty simple. At a minimum, we need to figure out how to link it statically.

I suspect we will start by merging a type checker that uses a vacuous AUTOMAP solver (essentially not allowing AUTOMAP), in order to get the supporting infrastructure into use, and then continue work on the solver.