Add support for union alternatives without fields

[Gabriella439]

Fixes #224

This adds support for unions with empty alternatives that don't store any
values. In the simple case where the union has all empty alternatives it
degenerates to an enum.

For example:

let Role = < Wizard | Fighter | Rogue >

let show : Role → Text
    show =
        λ(x : Role)
      → merge { Wizard = "Wizard", Fighter = "Fighter", Rogue = "Rogue" } x

in  show Role.Wizard

However, these empty alternatives can be mixed with non-empty alternatives, too,
with handlers to match:

let Status = < Empty | NonEmpty : Text >

let concatSep
    : ∀(separator : Text) → ∀(elements : List Text) → Text
    =   λ(separator : Text)
      → λ(elements : List Text)
      → let status =
              List/fold
              Text
              elements
              Status
              (   λ(element : Text)
                → λ(status : Status)
                → merge
                  { Empty = Status.NonEmpty element
                  , NonEmpty =
                        λ(result : Text)
                      → Status.NonEmpty (element ++ separator ++ result)
                  }
                  status
              )
              Status.Empty

        in  merge
            { Empty = "", NonEmpty = λ(result : Text) → result }
            status

in  concatSep

Handlers for empty alternatives no longer have to bind unused arguments of
type {} and constructors for empty alternatives no longer have to take
an input of {=}.

[FintanH]

Fantastic!

[singpolyma]

Is the plan then to eventually normalize this syntax to the new syntax?

[Gabriella439]

@singpolyma: That's what I originally hoped, but the issue I ran into is that we can't (easily) do so because we don't have immediate access to the type of the selected alternative.

In other words, if we try to normalize < a = x > to < a : T >.a x we need to be able to infer the type T of x, but doing so would require interleaving type-checking and normalization.

It's still possible that dhall lint might do this since it's fine if it's implementation is more complicated

[f-f]

@Gabriel439 looks great! 👏

It's probably worth adding some parser and typecheck tests to verify that the new literal syntax also parses and typechecks correctly

[Gabriella439]

@f-f: Yes, I've almost got the matching change to the Haskell implementation ready so that I can use it to generate additional golden test results

[singpolyma]

In other words, if we try to normalize `< a = x >` to `< a : T >.a x` we need to be able to infer the type `T` of `x`, but doing so would require interleaving type-checking and normalization.

Ah, right, so we can require it in all cases. What about normalizing < a = (x : T) > to < a : T >.x -- this means that type annotating followed by normalizing would produce the desired result, at least.

[Gabriella439]

@singpolyma: In my view, the main goal of normalizing the deprecated syntax to the newer syntax is so that lazy users don't have to migrate their code manually. If they have to provide a type annotation to take advantage of the migration then it feels to me like they don't benefit much because they could have instead migrated their code directly.

However, I think in the common case most users won't need to migrate their code anyway because they are likely already using the Union.constructor syntax instead of using the deprecated union literal syntax (which is much less ergonomic).

[Gabriella439]

Matching change to the Haskell implementation up here: dhall-lang/dhall-haskell#863