Constrain operator parameters by their type annotations

[shonfeder]

Closes #1177

Reviewing

The PR is smaller than it looks! Almost everything here is either generated by the parser generator or minor cleanup. Review by commit could be helpful.

The change

The new behavior is easiest to illustrate with reference to the operator
definition used in the regression test added here:

pure def foo(s: str): int = {
  val x = 1.in(s) // We SHOULD identify an error here, since s is annotated as a str
  val y = s + 1   // and NOT identify an error here, incorrectly expecting s to be a set
  y
}

Prior to this fix, typechecking locates the error at val y, because it is not
accounting for the constraint s : str before it begins solving constraints in
the body of the declaration:

error: [QNT000] Couldn't unify int and set
Trying to unify int and Set[int]
Trying to unify (int, int) => int and (Set[int], int) => _t2

4:         val y = s + 1   // and NOT identify an error here, incorrectly expecting s to be a set
                   ^^^^^

error: typechecking failed

With this fix, we now correctly account for the constraint on s, so we catch
the misuse at val x:

error: [QNT000] Couldn't unify set and str
Trying to unify Set[int] and str
Trying to unify (_t0, Set[_t0]) => bool and (int, str) => _t1

3:         val x = 1.in(s) // We SHOULD identify an error here, since s is annotated as a str
                   ^^^^^^^

error: typechecking failed

The fix is achieved primarily via a small improvement to the IR (which does not
impact the integration with Apalache): we add an optional typeAnnotation field
to QuintLambdaParams. This is a natural fix, since we are already parsing
these out together.

Along the way there was some minor cleanup and preparation for
#923

This change will also make it very easy to support selective annotation of parameters or return values, and to support annotating params of lambdas.

• Tests added for any new code
• Documentation added for any new functionality
• Entries added to the respective CHANGELOG.md for any new functionality
• Feature table on README.md updated for any listed functionality

[shonfeder]

We don't need this stack, because these are just string values we can grab directly.

[shonfeder]

These unwraps and asserts are just like the ones in all the exitType* methods: the grammar will not bring us to visit this context without these pre-requisites unless we've messed up something badly. It should have no impact on incremental parsing, unless we have a bigger problem that we want to know about.

[shonfeder]

The number is shifted because the type annotation in the param is now the first leaf we hit while parsing this example.

[bugarela]

Looks amazing ✨. I'm so happy you found such a simple fix here, really worth the time invested!

[shonfeder]

Thanks for the review and the fix!