[BUG] StackOverflow in TypeUnifer when in annotation using type variable and sets in record fields

[shonfeder]

Description

Type checking a spec with a type annotation on an operator taking a type variable to a record with a value whose type is the set of elements of that variable produces a stack overflow.

Input specification

------------------- MODULE scratch -----------------------

EXTENDS Integers, FiniteSets

\* @type: (a) => [f: Set(a)];
Optional(x) == [f |-> x]


============================================================

The command line parameters used to run the tool

apalache-mc typecheck scratch.tla

Expected behavior

It should check the type.

Log files

PASS #1: TypeCheckerSnowcat                                       I@13:41:58.840
 > Running Snowcat .::.                                           I@13:41:58.840
(Please report an issue at: [https://github.com/informalsystems/apalache/issues],java.lang.StackOverflowError)
Unhandled exception                                               E@13:41:58.971
java.lang.StackOverflowError: null
	at at.forsyte.apalache.tla.typecheck.etc.TypeUnifier.compute(TypeUnifier.scala:67)
	at at.forsyte.apalache.tla.typecheck.etc.TypeUnifier.compute(TypeUnifier.scala:121)
	at at.forsyte.apalache.tla.typecheck.etc.TypeUnifier.insert(TypeUnifier.scala:221)
	at at.forsyte.apalache.tla.typecheck.etc.TypeUnifier.compute(TypeUnifier.scala:90)
	at at.forsyte.apalache.tla.typecheck.etc.TypeUnifier.compute(TypeUnifier.scala:121)
	at at.forsyte.apalache.tla.typecheck.etc.TypeUnifier.insert(TypeUnifier.scala:221)
	at at.forsyte.apalache.tla.typecheck.etc.TypeUnifier.compute(TypeUnifier.scala:90)
	at at.forsyte.apalache.tla.typecheck.etc.TypeUnifier.compute(TypeUnifier.scala:121)
	at at.forsyte.apalache.tla.typecheck.etc.TypeUnifier.insert(TypeUnifier.scala:221)
[snip]

System information

• Apalache version [apalache-mc version]: 0.15.12-SNAPSHOT build v0.15.11-12-g28ed4e6-dirty
• OS [e.g. Ubuntu Linux or Mac OS, and the current version]: Linux system76-pc 5.11.0-7614-generic #15~1622578982~20.10~383c0a9~dev-Ubuntu SMP Wed Jun 2 00:50:39 U x86_64 x86_64 x86_64 GNU/Linux
• JDK version [e.g. OpenJDK 0.8.0]: openjdk 11.0.11 2021-04-20

[konnov]

Wow! :)

[konnov]

Sorry @shonfeder , I took this one from you and fixed it :)

[shonfeder]

I'll remember that! ;)