Type compatibility error message, when reading from .cfg

[Kukovec]

• Tests added for any new code
• Ran make fmt-fix (or had formatting run automatically on all files edited)
• Documentation added for any new functionality
• Entries added to ./unreleased/ for any new functionality

This PR adds an additional type validation check to any CONSTANT overwritten from a .cfg file. Since the typechecking pass precedes the configuration pass, it was otherwise possible to introduce type-inconsistencies, by overwriting a constant declared with type A with a value of type B, which would only fail at the cell-introduction level, with cryptic error messages.

72aaea0 adds support for literals of uninterpreted types within .cfg files (+ tests and some cleanup to use the typed builder smoothly)

closes #2750

[codecov-commenter]

Codecov Report

Merging #2757 (64671f3) into main (c877256) will decrease coverage by 0.02%.
The diff coverage is 52.77%.

❗ Current head 64671f3 differs from pull request most recent head fb952ff. Consider uploading reports for the commit fb952ff to get more accurate results

@@            Coverage Diff             @@
##             main    #2757      +/-   ##
==========================================
- Coverage   78.85%   78.83%   -0.02%     
==========================================
  Files         464      464              
  Lines       15878    15882       +4     
  Branches     2545     2589      +44     
==========================================
+ Hits        12520    12521       +1     
- Misses       3358     3361       +3     

Files	Coverage Δ
...at/forsyte/apalache/tla/pp/TlcConfigImporter.scala	80.48% <88.23%> (-1.34%)	⬇️
...apalache/tla/passes/pp/ConfigurationPassImpl.scala	34.88% <33.33%> (-1.83%)	⬇️
.../forsyte/apalache/infra/tlc/config/TlcConfig.scala	65.85% <10.00%> (-3.38%)	⬇️

... and 2 files with indirect coverage changes

📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more

[thpani]

closes #2750

afaiu from #2750 (comment), we still don't parse uninterpreted type literals from TLC configs, so I'm not sure this actually "closes" the issue. We should check with @konnov what the expected outcome of that issue is, or split it into subtasks, where one is preventing the exception (addressed here), and the other is support for the provided spec.

Also, please add a PR description.

[Kukovec]

I don't think we'll ever support ULs in .cfg, mainly because .cfg is not Apalache native. As for supporting the spec, given the cfg as it is provided, the cleanest solution is to replace PROC with an alias to Str, since that's the only way you can use TLC's model values.

[konnov]

Looks good! I just left one comment. Thanks for fixing this!

[konnov]

What is the difference between ConfigModelValue and ConfigStrValue now? It looks like ConfigStrValue handles model values too.

[Kukovec]

ConfigModelValue is what you get when TLC model values are parsed (e.g. a and b in Producers = {a,b}).
ConfigStrValue is what you get when a "-value is parsed (e.g. "abc" or "1_OF_X")

[thpani]

Looks great!

Amazing that it now works with uninterpreted types