Add textual information for Record and Union diff

[TristanCacqueray]

This change improves error messages when argument types are wrong.

Fixes #1846

[TristanCacqueray]

Example:

$ dhall <<< '<a | b>.a : { a : Bool }'

Use "dhall --explain" for detailed errors

Error: Expression doesn't match annotation

- { … : … } (a record)
+ < … : … > (an union)

[TristanCacqueray]

New examples:

$ dhall <<< '<a | b>.a : { a : Bool }'
Error: Expression doesn't match annotation

- { … : … } (a record type)
+ < … : … > (a union type)

$ dhall <<< '<a | b>.a : { a = Bool }'
Error: Expression doesn't match annotation

- { … = … } (a record)
+ < … : … > (a union type)

$ dhall <<< '{ a : Bool } : { a = Bool }'
Error: Expression doesn't match annotation

- { … = … } (a record)
+ Type

[Gabriella439]

I think all you need to do to fix the build failure is to update the doctest in src/Dhall/Deriving.hs to reflect the new error message

[timbertson]

Should this be "a union"? It's talking about an instance of a union type, I think?

[Gabriella439]

@timbertson: No, this is a union type. A union value is of the form UnionType.Alternative x

[timbertson]

Thanks! Don't suppose you could add "(a function)" to the Lam skeleton too? I think that's rendered as … → … which is a bit less cryptic but could still benefit from some words imo.

[TristanCacqueray]

@timbertson last commit adds "(a function)" message to Lam, though that doesn't work well:

$ dhall <<< '(\(a : Bool) -> a) : Bool'
Error: Expression doesn't match annotation

- Bool
+ … → …

$ dhall <<< 'Bool : (\(a : Bool) -> a)'
Error: Expression doesn't match annotation

- λ(… : …) → … (a function)
+ Type

And that wouldn't work for return type:

$ dhall <<< '(\(a : Bool) -> 42) : forall (a : Bool) -> Bool'
Error: Expression doesn't match annotation

  …
→ - Bool
  + Natural

I guess "(a function)" needs to be added to Pi instead, but I'm not entirely sure why it shouldn't be "(a function type)" :)

[sjakobi]

(a function) seems fine to me for Lam. And for consistency, Pi should get (a function type).

Thanks BTW – I think this will make some errors much easier to understand! :)

[sjakobi]

BTW, Hydra OOM'd again (error 137), with GHC 8.4.3. This has been happening repeatedly in the last few days, possibly due to more contributions during ZuriHac.

I'm wondering though whether it might be time to upgrade to a machine with more RAM. If costs are an issue, maybe it could be financed from the donations?

[Gabriella439]

@sjakobi: Cost would be an issue 🙂. I currently pay $40 / month for a Linode with 8 GB of RAM. The next tier with 16 GB would be $80 / month, which would consume a significant fraction of our donation budget.

I would personally wait to see if it's still a problem now that Zurihac's over

[sjakobi]

Sure. Of course we could also look at cheaper providers, as for example static-haskell-nix did, but it's all work that isn't strictly necessary when the existing server can mostly shoulder the load.

[sjakobi]

@Gabriel439 I believe the OOM'ing Hydra job needs to be restarted: https://hydra.dhall-lang.org/build/61554/nixlog/2