How to define eta-equivalence for F-omega types?
The first approach is subsumed by the second, sort of (because the first approach is slightly broken).

One should never consider expressions with free variables without explicitly specifying a context in which they appear (this is a lesson one learns as soon as one wants to formalize $\forall$ and $\exists$ that are allowed to range over possibly empty types or sets).

In a single-sorted theory, equations without context $t_1 = t_2$ can always be equipped with a context $\Gamma \vdash t_1 = t_2 : S$ where $S$ is the single sort and $\Gamma = x_1 : S, \ldots, x_n : S$, with $x_i$ being the free variables in $t_1$ and $t_2$.

Leaving the context implicit like that is not quite right. For example, what if I want to write down an equation that involves $x_1$ and $x_2$ in a context which also mentions $x_3$? You might think that sort of thing is going to be useless, but it isn't, not if $x_3$ could come from an empty type.

Also, as soon as you think about categorical semantics you will see that it makes little sense to have bare equations without contexts.

So I would advise you to put your equations in contexts, and then use the shorter form as an abbreviation. One reference where everything is done explicitly in a context all the time is Bart Jacob's "Categorical Logic and Type Theory", Chapter 8 is about polymorphic type theory and might be of particular interest to you.