[spec] Slight simplification to Rectype_ok2 judgement

[rossberg]

Remove the redundant typeidx on the Rectype/Subtype_ok2 judgements.

@raoxiaojia, PTAL.

@zilinc, FYI.

[raoxiaojia]

The simplification looks correct to me.

I'm curious on the choice of type indices there for rectype_ok/ok2, which uses typeidx (bounded by 2^32-1) and nat respectively. Is this a deliberate choice to limit the number of subtypes in a module to 2^32-1? Note that the module definition itself doesn't have such a bound: it just says that a modules's types is a general sequence of rectype* instead of using the bounded sequence definition in spectec (list(rectype)). In fact, even the latter would not work, because that is only setting a bound on the number of rec groups but not the individual subtypes themselves, whereas using typeidx as the index in rectype_ok basically makes all types that appear at a position >=2^32 inaccessible (which seems intended).

[rossberg]

Yes, idx and list are used over nat and * where the domain or length is constrained in the AST, usually reflecting the binary format.

You are totally right about the abstract syntax of modules not doing that! That's an oversight, will fix. (FWIW, the binary format indeed applies the limit to the number of type groups. So you can define more than 2^32 types in a module, making the upper ones inaccessible by Wasm syntax. Doesn't really do any harm, though.)

[raoxiaojia]

Oops, I think there's some test expects that were not updated (frontend or sth).

[rossberg]

Yeah, on it, but I'm on the train and the connection is horrible.