According to the article Second-order and Higher-order Logic from the Stanford Encyclopedia of Philosophy,

there is no need to stop at second-order logic; one can keep going. [...] we can allow quantification over super-predicate symbols. And then we can keep going further.

We reach the level of type theory after ω steps.

I wonder what the expressive power of "$\omega$-order logic" is:

Can you give an example of two structures $\mathcal A$, $\mathcal B$ that satisfy the same $\omega$-order sentences but are not isomorphic?