The motivation behind this change is to add support for "modules" to
Dhall, which are just large records that users can import bundling both
terms and types.

Users can already import terms and types separately and users can already
bundle terms into a single import using a record, but before this change
they cannot bundle types in the same way.  The reason why is that the
typing judgments for record types and record literals forbid records
with type-valued fields.  This change removes that restrictions,
allowing records to store types and type-level functions for fields.

For consistency, this change also loosens the same restriction for union
alternatives.

For example, after this change the following becomes a valid Dhall record:

```haskell
{ x = True, y = Bool, z = List } : { x : Bool, y : Type, z : Type → Type }
```

... and this is a valid `merge` expression:

```haskell
merge
{ x = λ(a : Type) → a
, y = λ(f : Type → Type) → f Bool
}
< x = Bool | y : Type → Type >
```

The practical benefit of this change is to improve the usability and
speed of Dhall programs.  This allows users to shorten their programs by
consolidate their import list into a single import, which in turn speeds
up program interpretation by reducing the number of HTTP requests.

This change preserves soundness, which consists of the following four
rules:

* Type-checking should never diverge
* If a term type-checks, then normalizing that term should never diverge
* Normalizing an inferred type should never diverge
* Normalization doesn't change a term's type

Here is the informal proof of the above soundness properties for the
modified typing judgements:

*   Type-checking should never diverge

    By induction, both newly added type-checking rules still recurse on a
    strictly smaller input expression so type-checking still always
    terminates.

*   If a term type-checks, then normalizing that term should never diverge

    By induction, each field or alternative is type-checked, which means that
    each field or alternative is safe to normalize, which in turn means that
    the record or union is safe to normalize.

*   Normalizing an inferred type should never diverge

    By induction, the inferred type of each field or alternative is safe
    to normalize, therefore the inferred type of the record or union is
    safe to normalize.

*   Normalization doesn't change a term's type

    By induction, if normalizing the type of each field or alternative
    doesn't change their type then normalizing the record or union
    doesn't change its type.

Note that the records are still not dependent records (i.e. the type of
a field cannot depend on the value of another field) since fields are
not ordered.