[spectec] Incorrect front-end elaboration

[zilinc]

MWE:

;; .spectec source
syntax t =
  | ATOM nat? int  -- if (int < 2 /\ nat > 0)?

and it's elaborated into:

;; elab.spectec:1.1-2.47
syntax t =
  | ATOM(`nat?` : nat?, int : int) {`int?` : int?}
    -- (if ((int < (2 : nat <:> int)) /\ (nat > 0)))?{int <- `int?`, nat <- `nat?`}

The quantifier list of the type case and that of the side condition are both wrong. int? shouldn't be there.

(Credits to @maximelegoupil and @DCupello1)

The real use case is the STORE instruction in the Wasm specs. It was uncovered during the Wasm 2.0 proof.