Nested variant-wrapped record update compiles in Quint but fails in Apalache

[unthingable]

Summary

Quint accepts a record-spread update that replaces a nested field containing a variant-wrapped value, but compilation/verification fails in the Quint-to-Apalache path.

Reproducer

type Id = Id(str)
type Inner = { id: Id }
type State = { inner: Inner, flag: bool }

var state: State

action update = {
  state' = { ...state, inner: { id: Id("new") } }
}

Environment

• Quint 0.32.0
• Bundled Apalache 0.56.1

Actual result

Quint accepts the source, but the generated QuintIR/TLA+ is rejected with:

Operator EXCEPT cannot be applied to arguments of types:
(State record, <<Str>>, Snapshot)

The selector appears to be emitted as a one-element tuple (<<Str>>) in the failing update.

The same behavior occurs when using the concise record-update forms:

state' = state.with("inner", { id: Id("new") })
state' = with(state, "inner", { id: Id("new") })

Workaround

Introducing an explicit type boundary makes it compile:

action update = {
  val i: Inner = { id: Id("new") }
  state' = state.with("inner", i)
}

Expected result

The original concise update should compile and verify, or Quint should report a source-level type error explaining that the replacement needs an explicit type annotation.

This appears related to nested variant/open-row type inference during QuintIR export, but the exact ownership between Quint and Apalache is uncertain.