MacWilliams identity for Hamming weight enumerators

For every type $F$ equipped with a field structure, a finite enumeration, and decidable equality; every type $\iota$ equipped with a finite enumeration and decidable equality; and every $F$-linear subspace $C\subseteq F^\iota$, let $q=\#F$, $n=\#\iota$, $w(c)=\#\{i\in\iota:c_i\ne0\}$, and define the integer-coefficient polynomial in the two variables $X_0,X_1$ by $W_D(X_0,X_1)=\sum_{d\in D}X_0^{n-w(d)}X_1^{w(d)}$. Define $C^\perp=\{d\in F^\iota:\sum_{i\in\iota}c_i d_i=0\text{ for every }c\in C\}$, where the sum and products are in $F$. The assertion is the following equality in $\mathbb Z[X_0,X_1]$:

More literally, $|C|$ on the left is first computed as the natural-number cardinality of the subtype $C$, cast to $\mathbb Z$, embedded as a constant polynomial, and then multiplied by $W_{C^\perp}$; on the right, $q-1$ is first natural-number subtraction $\#F-1$, then cast to $\mathbb Z$ and embedded as a constant polynomial, and the displayed replacement of $X_0$ and $X_1$ is the coefficient-preserving polynomial-algebra homomorphism sending $X_0$ to $X_0+(q-1)X_1$ and $X_1$ to $X_0-X_1$. The exponent $n-w(c)$ is likewise natural-number subtraction, which would return $0$ if $w(c)>n$, although here $w(c)\le n$ because it counts a subset of $\iota$; similarly, a field is nonempty (indeed has at least two elements), so the natural subtraction $q-1$ does not underflow. No assumption requires $\iota$ to be nonempty or $C$ to be nonzero, proper, or of positive dimension: the statement includes the zero and full codes and the case $\iota=\varnothing$, in which $n=0$, the word space and every code or dual code have one element, every weight is $0$, and both enumerator polynomials are the constant polynomial $1$.