apalache
apalache copied to clipboard
[FEATURE] Improve error messages around type annotations
- [ ] 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: #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 theStr
prefix.
- Currently
- [ ] 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.
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
.