Solution (source code)

= Solution

A primitive eighth root satisfies $\zeta_8=(1+i)/\sqrt2$, while $i=\zeta_8^2$ and $\sqrt2=\zeta_8+\zeta_8^{-1}$. Thus $K=\mathbb Q(i,\sqrt2)$. The real elements of $\mathbb Q(i)$ are rational, so it does not contain $\sqrt2$. The tower law gives
$$
\boxed{[K:\mathbb Q]=2\cdot2=4}.
$$