This is just an expansion of Emil Jerabek's comments above; I've made it CW to avoid reputation gain, and will delete this if he posts an answer of his own.

Craig interpolation can be rephrased as a "syntactic separation" property: the statement $$\varphi\models\psi$$ can be rephrased as $$\emptyset\models\exists\mathfrak{R}(\varphi[\mathfrak{R}])\rightarrow\exists\mathfrak{S}(\varphi[\mathfrak{S}])$$ for some appropriate objects $\mathfrak{R},\mathfrak{S}$ corresponding to the uncommon parts of the languages of $\varphi,\psi$ respectively. Now if our "base logic" is first-order then this is broadly speaking where the story ends, but using second-order logic as our "base" gives us a lot more power.

Specifically, since we can pin down $\mathcal{N}=(\mathbb{N};+,\times)$ up to isomorphism, we can "localize" the syntactic separation result above into a separation result for sets of natural numbers: if "fully-second-order" logic had the Craig interpolation property then any two disjoint $\Sigma^2_1$ subsets of $\mathcal{N}$ could be separated by a second-order-definable set of naturals, but this is impossible (by Tarski) since the usual-second-order theory of $\mathcal{N}$ is $\Delta^2_1$.

This raises a natural follow-up question:

• Is there a "reasonably natural" and "not too strong" extension of second-order logic which has the interpolation property for second-order languages?

The point of the "not too strong" requirement is that there is an obvious extension of $\mathsf{SOL}$ which has the interpolation property for second-order languages - third-order logic (which then loses interpolation for third-order languages, and so forth)!