Using dynamic array in spec

Hi colleagues, could you help me to figure out how to port attached TLA+ spec to Apalache?

I have a stack of structs but have hard time trying to specify Apalache type annotation for it.

I think problem is that I’m mixing functions, sequences and tuples which are all different for type checker. But I’m not sure how express stack using just one of them.

$ cat Test.tla
---- MODULE Test ----

EXTENDS
  Integers, Sequences

CONSTANTS
  \* @type: Int;
  N

VARIABLES
  \* @type: Seq({data : Int});
  stack

\* How to make this a stack's type for Apalache ?
Stack == UNION {[1..len -> [data : 1..3]] : len \in 0..N}

Init ==
  /\ stack = <<>>

Step ==
  /\ Len(stack) = 0
  /\ stack' = [stack EXCEPT ![Len(stack) + 1].data = 0]

Next ==
  /\ Step

Spec ==
  /\ Init
  /\ [][Next]_<<stack>>

Inv ==
  /\ stack \in Stack
  /\ \A i \in DOMAIN stack : stack[i].data = 0

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

$ cat Init.cfg
CONSTANTS
  N = 2

SPECIFICATION
  Spec

INVARIANT
  Inv

$ java -jar ./tla2tools.jar Test.tla
...
Model checking completed. No error has been found.

$ apalache-mc check --config=Test.cfg Test.tla
...
 > Running Snowcat .::.                                           I@16:12:53.664
[Test.tla:32:6-32:20]: An operator with the signature ((c, Set(c)) => Bool) cannot be applied to the provided arguments of type Seq({ data: Int }) and Set((Int -> { data: Int })) E@16:16:47.794