[spectec] Clean up IL semantics and elaborator (WIP)

[rossberg]

This PR cleans up and tightens SpecTec IL scoping and validation and revamps the frontend elaborator accordingly.

The relevant tweaks to the IL are as follows (see also the diff on il/ast.ml):

• Binders are renamed to quantifiers and share the same AST type with parameters.
• Dependent tuple types (x1:t1,...,xN:tN)now bind just variables, not expressions. Furthermore, these variables are properly locally scoped. That implies that they no longer show up in outer binder lists. They scope over field types to the right as expected.
• As a special case, when a tuple type occurs as the parameter of a variant or record constructor, its names also scope over any premises of that arm. For example, in syntax t = C(a : t, b : u(a)) -- if $p(a, b), the variables a and b scope over the premise.
• Consequently, it is no longer necessary that the binders list of variant and record constructors scopes over their parameter type and can instead be treated solely as an existential quantifier for the free variables in the premises. As such, it moves to the right of the parameter and can depend on it, as in syntax t = C(a : t, b : u(a)) {c : v(b)} -- if $f(a, b) = c.
• Iteration variables (both i and j in e^(i<n){j <- k} are now properly locally scoped (this was a bit ambiguous before). That implies that they also no longer show up in outer binder lists.

The net effect of these changes is that all scoping now is much more standard and there no longer is any duplication between "binders" and parameters. As a concrete example, this e.g. is how the elaboration of the type name simplifies:

 syntax name =
-  | `%`{`char*` : char*}(char*{char <- `char*`} : char*)
+  | `%`(`char*` : char*)
     -- if (|$utf8(char*{char <- `char*`})| < (2 ^ 32))

There are only very few cases left where quantifiers on variants actually still show up (for example, the SUBNORM constructor for floats). Note that quantifiers remain heavily used for function definitions and their argument patterns.

• In addition to the above, the internal representation of mixfix operators changes from a list of atoms to a tree of atoms, in order to preserve knowledge about precedences (needed in the elaborator). Backends that do not construct/deconstruct mixops should be unaffected.

Currently there still is a test failure on the AL interpreter.