[FEATURE] Improve error messages around type annotations

[shonfeder]

• Missing annotations on VARIABLE's don't include line numbers:

PASS #1: TypeCheckerSnowcat                                       I@08:18:53.210
 > Running Snowcat .::.                                           I@08:18:53.210
Typing input error: Expected a type annotation for VARIABLE blockchain E@08:18:53.309
It took me 0 days  0 hours  0 min  0 sec                          I@08:18:53.310
Total time: 0.920 sec                                             I@08:18:53.310
EXITCODE: ERROR (255)

• Detect missing ; at end of line: Confusing error message on missing semicolon in type #954
• Detect incorrect tokens
  • Currently \* @type: [RM: String];= returns the confusing error that found =ing= when it exepted =], because it's not checking for the full token in the type, but just taking the Str prefix.
• Type aliases that aren't actually defined should raise a specific error reporting this mismatch
• TypeAlias declarations in invalid positions should raise an error (is that possible?)
• Format type errors. They are currently hard to read for nontrivial types, e.g.,

Expected ((Set((Int -> [Commits: Set(Str), header: [NextVS: Set(Str), VS: Set(Str), hight: Int, lastCommit: Set(Str), time: Int]])), [Commits: Set(Str), header: [NextVS: Set(Str), VS: Set(Str), hight: Int, lastCommit: Set(Str), time: Int]]) => [Commits: Set(Str), header: [NextVS: Set(Str), VS: Set(Str), hight: Int, lastCommit: Set(Str), time: Int]]) in LightStoreUpdateBlocks. Found: ((Set((Int -> [Commits: Set(Str), header: [NextVS: Set(Str), VS: Set(Str), hight: Int, lastCommit: Set(Str), time: Int]])), [Commits: Set(Str), header: [NextVS: Set(Str), VS: Set(Str), hight: Int, lastCommit: Set(Str), time: Int]]) => (a438 -> [Commits: Set(Str), header: [NextVS: Set(Str), VS: Set(Str), hight: Int, lastCommit: Set(Str), time: Int]])) E@10:53:12.003
[Lightclient_003_draft.tla:213:1-216:49]: Error when computing the type of LightStoreUpdateBlocks E@10:53:12.015

We should instead format something like

In LightStoreUpdateBlocks:

Expected:

    (Set(Int -> [Commits: Set(Str), header: [NextVS: Set(Str), VS: Set(Str), hight: Int, lastCommit: Set(Str), time: Int]]), [Commits: Set(Str), header: [NextVS: Set(Str), VS: Set(Str), hight: Int, lastCommit: Set(Str), time: Int]]) 
    => [Commits: Set(Str), header: [NextVS: Set(Str), VS: Set(Str), hight: Int, lastCommit: Set(Str), time: Int]]
   
   
Found:

    (Set(Int -> [Commits: Set(Str), header: [NextVS: Set(Str), VS: Set(Str), hight: Int, lastCommit: Set(Str), time: Int]]), [Commits: Set(Str), header: [NextVS: Set(Str), VS: Set(Str), hight: Int, lastCommit: Set(Str), time: Int]]) 
    => (a438 -> [Commits: Set(Str), header: [NextVS: Set(Str), VS: Set(Str), hight: Int, lastCommit: Set(Str), time: Int]])

Achieved via indentation, sensible line breaks, and removing redundant parens.

• Use typeAlias in scope instead of fully expanded type in type errors, but also report the full type of the alias at the end of the error. That would make errors like the previous much easier to read.

[konnov]

One issue is that the type checker is working at the level of EtcExpr, which lacks information about the original expressions. I think it makes sense to introduce another pass similar to ToEtcExpr that goes over TlaEx again and reports on errors by knowing the id of a problematic TlaEx.