Switch to n-ary functions in the surface language and Core

[dougalm]

Follows up on #1240, #1243.

Big frontend change! So far the only Dex code I've updated is the prelude. I'll do the rest of the corpus in follow-up commits.

Main changes

• Application can be done with f(x,y). It can also be done with juxtaposition. Juxtaposition is really nice for type constructors (Ref h a vs Ref(h, s)) and for trailing continuations. Mixing the two styles is unconventional but it actually seems to work ok. Wiring up functions to their arguments is most of what programs do so it makes sense to offer some syntactic flexibility. In that spirit I also added | for left-application and kept $ for right application. These three sorts of "fancy application", |, $ and juxtaposition, work by extending the argument list of the original expression if it's an application. So x | f(y, z) w parses as f(x, y, z, w), and x | f y parses as f(x, y).
• Use x[i,j] for table indexing, and (finally!) use . for field access.
• Distinguish wholly-implicit functions from explicit functions with zero explicit args. The former can be applied to its implicit arguments just by mentioning it. The latter isn't fully applied until it's actually called like f(). We didn't need the distinction before because in the unary/curried world occurrence and nullary application are both written as f. We use ->> for the types of wholly implicit functions but we rarely need to use it.
• Adam proposed some really neat syntax for specifying unary constraints. Instead of something like {a:Type} [Ix a, Ord a], we write given (a|Ix|Ord), which both introduces the implicit argument a, and provides the two constraints on it. This only works for unary constraints but that's the most common case by far. And since the constraints constrain the type of a we don't have to give its type explicitly.
• Pun (,) for both types ((Int, Bool)) and terms ((1, True), with the ambiguity resolved during type inference. No more ampersand!
• Allow named arg application for implicit args, like coerce(to=Int, x). This means we don't need the "explicit" tag on methods anymore (it was always incomplete anyway).

I removed some features that were expensive to maintain relative to their utility:

• Automatic dictionary argument insertion (e.g. Ix). This feature really complicated the inference implementation. It was also a source of bugs (#860, #1229) and bad error messages. The benefit was that it saved us writing Ix in a few places. But that syntactic burden is much less now thanks to Adam's syntax for specifying constraints, see above.
• Handler inference. These were unimplemented beyond type inference anyway. And when we get around to implementing them who knows what else will have changed.
• Pattern-matching on product constructors in lambda arguments. N-ary functions complicate lambda patterns because they require decls between the binders. But they were already a syntactic headache, especially with type annotations. And nowadays we can project out components of a product with dot-based field access which is often nicer anyway.