[FEATURE] Overhaul error message treatment

[shonfeder]

During our retro last week, we discussed some ways we could change the error messaging and user-error handling that would improve learnability and user feedback, and perhaps even improve our development cycle. The two key points discussed were:

• Elm/Rust-like error messages, that include built in documentation and heuristics to suggest fixes
  • An example of an unclear error messages on the types: [FEATURE] Overhaul error message treatment #943
• Semi-automating bug reports for any implementation errors. This would at least involve generating a bug report that a user could paste into an issue. But perhaps we could even automate opening an issue?
• Clear indication when the error comes from a dependency, rather than from Apalache. (E.g, [BUG] GLIBC 2.27 not working with z3 4.8.12 #1006)

[konnov]

If you working on this right now, check #1127. It's related to error messages. I am going to use to produce message about unsupported operators.

[shonfeder]

Related to #802

[shonfeder]

As points of reference for the state of the art, the most lauded error messaging I'm aware of are in:

• Rust: https://rustfest.global/session/5-the-anatomy-of-error-messages-in-rust/
• and Elm: https://elm-lang.org/news/compiler-errors-for-humans

[shonfeder]

This should be a valuable resource in helping guide our design: https://web.eecs.umich.edu/~akamil/papers/iticse19.pdf

[thpani]

Related: #1654

[shonfeder]

See https://github.com/informalsystems/apalache/pull/1717/files#r868375855

Where I suggest:

- [Bug874.tla:4:17-4:27]: Cannot apply ["a" ↦ 2] to the argument "b" in (["a" ↦ 2])["b"].
+ [Bug874.tla:4:17-4:27]: Cannot access nonexistent field "b" in record ["a" ↦ 2] in (["a" ↦ 2])["b"].

This should go with a more systematic treatment of composing phrasing for errors on particular kinds of values.