Quint verify fails while quint typechecks and simulation works on single constructor #2021

Summary

Declare a sum type with one constructor. Example: type T = D(str).

Quint typechecks the module. The simulator operates correctly. But quint verify fails in the Apalache pass when the module compares a value of this type with a value read from a record field.

Interestingly, a sum type with two constructors does not cause the failure.

Environment

• Quint 0.32.0
• Bundled Apalache 0.56.1 (build 70cdaf4)
• Node v22.20.0, macOS
• Reproduces on Temurin JDK 21.0.8 and on Homebrew OpenJDK 23.0.2

Example Module

module m {
  type T = D(str)
  pure val x: T = D("a")
  val contracts = { f: x }.f == x

  var n: int
  action init = n' = 0
  action step = n' = n
  val inv = true
}

quint typecheck and quint run accept this module. Note that contracts is not reachable from init, step, or inv.

Actual result

$ quint verify --invariant inv m.qnt
...
error: Expected RowT1(_, _) or VarT1(_), found: D(Str) | c

Expected result

quint verify should accept the module, or Quint should show an error at the source level.

Notes

There appears to be a duplicate issue, #1855, but it references a closed pull request that, presumably attempts to fix this. I'm adding this issue to note that the issue persists at the version noted above.