report an error when a type annotation is too general

[konnov]

Closes #2102. This PR adds a small test in EtcTypeChecker that ensures that a polymorphic type annotation is as precise as the inferred principal type.

• The new version of the type checker has found a bug in the type annotation of ReduceSet of __rewire_finite_sets_ext_in_apalache.tla. Due to the incorrect order of arguments, the type was more specific. This is actually a bug in the community modules.

• Also, it found a bug in our type annotation of FoldLeft in SequencesExt. This is purely a bug in the type annotation, not propagated to the community modules.

• 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

[codecov-commenter]

Codecov Report

Merging #2109 (17681c0) into main (ef2a18e) will increase coverage by 0.00%.
The diff coverage is 83.33%.

@@           Coverage Diff           @@
##             main    #2109   +/-   ##
=======================================
  Coverage   76.98%   76.98%           
=======================================
  Files         425      425           
  Lines       13769    13778    +9     
  Branches     1881     1884    +3     
=======================================
+ Hits        10600    10607    +7     
- Misses       3169     3171    +2     

Impacted Files	Coverage Δ
...te/apalache/tla/typecheck/etc/EtcTypeChecker.scala	84.33% <83.33%> (-0.38%)	⬇️
...he/io/annotations/parser/CommentPreprocessor.scala	96.70% <0.00%> (-1.10%)	⬇️
...a/at/forsyte/apalache/tla/lir/TlaLevelFinder.scala	95.83% <0.00%> (+2.08%)	⬆️

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

[shonfeder]

A few small suggestions on comments, and some questions (for my own edification) on the tests.

[shonfeder]

For my own edification: I don't know how to read the body of this lambda. What is ((c, c) => c) x d? It looks like it's applying an implication to two arguments? Or is that only on the type level? But then what's the labmda doing? And how does F end up being typed as the identify function?

[konnov]

This expression is written in the syntax of EtcExpr, a lambda calculus over types. The body of the lambda is an application of x and d to a type, which in this case is an operator of two arguments of type c and returns type c.

[konnov]

It is an identity from the types of view.

[shonfeder]

Thank you for explaining. It helps a lot. So is the lambda here a type-level lambda? It seems like it's kind of mixing type level syntax with pseudo-TNT syntax, or am I just totally missing the thread here :D?

It is an identity from the types of view.

So, we are maybe getting outside the scope of this PR, but one thing that I think is throwing me off here is that, afaik, it is not possible to write an operator that actually has type a => a and also relies on some constant d that comes from outside the operator.

The only way we can write an operator of type a => a is if we treat the provided argument as fully abstract, because we can't know anything about the value of type a, since we don't know what type it is (or, equivalently, it must work for any type). So afaik, there would be no way of having a d available that could work for any possible type for application to (c, c) => c. afaiu, This is why (in a HM-ish type system) any function with type a => a must be (isomorphic to) the identity function.

The fact that this test is going through makes me think that either our type inference is off, or we're constructing type here that shouldn't actually be possible to assign to any expression (or else I am just quite confused about what is going on here). But in any of these three cases, it seems like we might be looking to either fix the test, fix the type inference, or fix my understanding :)

[shonfeder]

Same question here: I may be being dense, but I don't understand how it is that F here turns out to be the identity function. Is (c, c) => c somehow the k combinator?

[konnov]

It's the same thing again. We have a lambda that applies an operator of type (c, c) => c) to x and d. We are interested not in the structure of this operator, but only in its type.

[shonfeder]

That helps a bit, but the annotation here is really quite confusing, imo, as it seems to be mixing up value and type level syntax. Would this comment convey the same thing but within using types to stand in for expressions?

Suggested change

	// @type: a => a;
	// let F == lambda x \in Set(a): ((c, c) => c) x d
	// @type: (c, c) => c;
	// let G(a, b) = a
	// @type: a => a;
	// let F == lambda x \in Set(a): G x d

In any case, I can see that this comment is not change by this PR, so it should be outside the scope of the PR. You've cleared up my confusion, thanks.

The part of this that should perhaps be addressed (at least in discussion) is described in #2109 (comment).

[shonfeder]

Marking this OK for merge, as we can followup with any needed fixes to testing or inference or docs.