0. How to read this document

The grammar is in EBNF: | is a choice, [ ] may be there or not, { } may come zero or more times, and text in quotes is written as it is.

Inside a type in the rules and in the prose, a capital letter, alone or with a digit, such as A, T, E, N, or P1, stands for any type, and a lowercase letter, alone or with a digit, such as a, r, or b1, stands for a type variable. A letter followed by an index, i, j, k, m, or n, as in Ti, Qi, ai, an, or bm, is that letter with that index, and stands for the same kind of thing as the letter alone. Outside a type, the letters keep the sense that the text gives them: in §4.8, for example, C is a constructor, e an expression, and r an expression or a name. This is notation of this document, not i syntax: in i code, a type variable is an UpName that is declared as a type parameter (§4.7), as in <A>(A) -> A.

These words have a fixed sense in this document:

Compile error: the compiler does not take the program and makes no output.
Stop: the program ends at once while it is running. The host gets a message (§11.7). In a test, a stop makes that test fail, and the other tests go on.
Error: a value raised through the service Fail in place of a normal value (§9.3). An error is not a compile error.
Host: the system that runs the compiled Wasm module, for example a web browser or Wasmtime.
Type constructor: a type name with a fixed number of parameters. List has one parameter; Int has none.
Program source: all modules but the library modules (§2.1). Built-in names (§12) are not in the program source.
Not fixed: this document does not say which result is given. A compiler may give any result that keeps to the stated rules, but the same compiled module gives the same result every time.