… as permitted by dhall-lang/dhall-lang#1052

… as permitted by dhall-lang/dhall-lang#1052

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.

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.

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.

* Implement `with` directly rather than via desugaring

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.

* small tweaks

* oops, remove duplicate alpha-normalization rule

* Update standard/beta-normalization.md

Co-authored-by: Gabriel Gonzalez <Gabriel439@gmail.com>

* Update standard/type-inference.md

Co-authored-by: Gabriel Gonzalez <Gabriel439@gmail.com>

* fix type inference rule

as caught by @Nadrieril

* better mnemonic variable names

as caught by @Gabriel439

* Allow creation of intermediate records

also tidy up the judgments a bit, add tests for the new judgments,
remove tests for the old desugaring behaviour.

* Update standard/type-inference.md

Co-authored-by: Gabriel Gonzalez <Gabriel439@gmail.com>

* Update standard/type-inference.md

Co-authored-by: Gabriel Gonzalez <Gabriel439@gmail.com>

* Add a test for partially-abstract `with` expressions

This caught a bug in dhall-golang.

Co-authored-by: Gabriel Gonzalez <Gabriel439@gmail.com>