Solution (source code)

= Solution

Add constants $c_1,\ldots,c_n$ and form $T\cup\{\varphi(c):\varphi\in p\}$. Every <finite set> has a model by consistency of the type. The <compactness theorem> gives a model $\mathcal M$ realizing the whole expanded theory, so $c^{\mathcal M}$ realizes $p$.

Apply the downward <Löwenheim-Skolem theorem> to the <countable> expanded language, retaining these finitely many named elements. The resulting <countable> <elementary substructure> still satisfies every formula of $p$ at the same tuple. Its reduct to the original language is a <countable> model of $T$ realizing $p$. Since $T$ has no finite models, this model is countably infinite.
$$
\boxed{\text{Every finite-arity type has a realization in a countable model of }T.}
$$