Compiling TLA⁺ types into Go types.

Core.Go.Syntax is real Go rather than a statement layer parameterized over TLA⁺ types, so the translation is this pass's own work.

• Primitives go to the runtime's newtypes, not Go's builtins. Bool/Int/Str compile to tlaplus.Bool/tlaplus.Int/tlaplus.Str rather than bool/int/string, because every value in generated code has to implement Eq/Ord and Go forbids implementing an interface for a type declared in another package. Go.Typ's own .bool/.int/.str are still used by the pass, for the Go-level scaffolding a specification never sees — a branch function's guard bool, a scheduler's loop condition.
• Records compile to a struct with their fields sorted by name. TLA⁺ records are unordered, so [a ↦ 1, b ↦ 2] and [b ↦ 2, a ↦ 1] are the same value and must compile to the same Go type; a struct's fields are ordered, so a canonical order has to be imposed. Sorting also makes the tuple encoding fall out unchanged, proj1 … projn already being in order.
• Channel(τ) has no case. Channels are not first-class in Distributed PlusCal — one is never stored, passed, or placed in a data structure — so a channel type reaching this function means it turned up in an ordinary value position, which the well-formedness checks on channel declarations already rule out (Typ.isChannelLike, WellFormedness/ Declarations.lean). The channel declarations themselves don't come through here: they become the process's Network parameter, built by the process-wiring compilation.

partial def Network2Go.compileTyp {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] : ComputableTLAPlus.Typ → m Go.Typ

Compiles a TLA⁺ type into its Go representation.

Fails only on types that cannot appear in a value position by the time this pass runs — see the module doc for Channel(τ), and Core/ComputableTLAPlus/Syntax.lean for why no metavariable survives type checking.