Implement with directly rather than via desugaring

[philandstuff]

I found it confusing to implement the recent with
optimizations (#1052) because with expressions are currently neither
pure sugar nor first-class expressions.

Also, there is arguably still scope for pathological behaviour, since
an abstract function like

\(r : {a : {b : {c : Natural}} }) -> r with a.b.x = 1 with a.b.y = 2

will be evaluated to a function which potentially evaluates r 6
times (in an implementation which does not evaluate arguments before
passing them to a function).

This commit defines type inference and beta-normalization for with
expressions directly, rather than via a desugaring step. As a
side-effect, desugaring of abstract with expressions no longer
happens; they are left as plain with expressions. This is a
breaking change.

There is another consideration, which is there are currently a number
of simplifications for right-biased record merge expressions which the
current with-desugaring can piggyback on. For example, currently:

(e with k = v).k

evaluates to v, because of the simplification of expressions of the
form (l // { k = v, rs... }).k. This commit does not attempt to
preserve those simplifications, but we could introduce some
with-simplifications in later commits if desired.

[Nadrieril]

Also, there is arguably still scope for pathological behaviour, since
an abstract function like

\(r : {a : {b : {c : Natural}} }) -> r with a.b.x = 1 with a.b.y = 2

will be evaluated to a function which potentially evaluates r 6
times (in an implementation which does not evaluate arguments before
passing them to a function).

That's not a very convincing argument: the same would happen with

\(f: Int -> Int) -> Natural/fold 6 Natural f 0

That said, I find the new rules much shorted and clearer than the desugaring, so I'm weakly in favor of this change (weakly because I'd have to implement it ^^)

[Gabriella439]

Looks great! Just a few minor suggestions

[philandstuff]

Ok I've updated the PR to allow { a = 5 } with b.c = 10 to typecheck and evaluate to { a = 5, b = { c = 10 } }. I've also updated the tests to reflect the new judgment rules, and removed the old WithUnderscore tests which were based on the old desugaring.

I've also made a corresponding change to the dhall-golang implementation: philandstuff/dhall-golang#53

[Gabriella439]

I also made the matching change in the Haskell implementation here: dhall-lang/dhall-haskell#2055

[Gabriella439]

@philandstuff: I believe this is clear to merge