Fix our dear #693 type checker bug

[bugarela]

Hello

This fixes #693!

The problem was: even though type variables for parameters are free, we were failing to keep track of this fact after substitutions. So, considering the example:

val b(x: int -> str): int = val c = x.keys() { 1 }

Suppose x has type variable t0, which is free. Once we analyze x.keys(), we'll perform a unification and apply substitutions, resulting in t0 being replaced by t1 -> t2 (since x has to be a map in order for it to be an argument for keys()). However, since t1 and t2 are not free names, when we exit the let definition, the types are quantified, and we loose track that those types are related to the parameter type.

The solution is to make sure that, in a substitution like t0 |-> t1 -> t2, if t0 is a free variable, then t1 and t2 also have to be free.

Also, I found another small bug in the integration with Apalache due to the different representation of row types between quint and apalache. The Apalache representation doesn't allow nested rows (that is, a concrete row in the tail). This also adds a small fix for that.

• 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

[bugarela]

This specific case seems different from the others. I'll look at it in a separate issue (to be created). Every other FIXME of this kind has been removed 😄

[thpani]

This is amazing, great work!

Changes to the typechecker LGTM.

Could you explain where we need the row type simplifier?
afaik, nested rows are already flattened on the Apalache side:
https://github.com/informalsystems/apalache/blob/315d43ad3afca3ed3abbb5e8f2610e3bd9bc9929/tla-io/src/main/scala/at/forsyte/apalache/io/quint/QuintTypeConverter.scala#L60-L73

I've also pushed a small commit to get rid of a reference to #693 in one of the RFCs.

[bugarela]

Could you explain where we need the row type simplifier? afaik, nested rows are already flattened on the Apalache side: https://github.com/informalsystems/apalache/blob/315d43ad3afca3ed3abbb5e8f2610e3bd9bc9929/tla-io/src/main/scala/at/forsyte/apalache/io/quint/QuintTypeConverter.scala#L60-L73

Interesting, I didn't realize we are already doing this in Apalache.

So... I've added this simplification step because I was hitting an error where Apalache complained about mismatching row types, something like "expected Var or Empty, found Row", which I instantly interpreted as nested rows and jumped to a fix. However, I can't reproduce that anymore 🤔. Perhaps it was caused by some intermediate state of my other fix or something like that.

While trying to decide if this simplification is worth keeping, I noticed we do similar processes both before printing rows and before unifying rows. So I'll extract it from this PR and just add it in a separate cleanup PR accounting for all these scenarios.

[thpani]

Excellent, LGTM!