Short answer

• A uniform, easy-to-check sufficient condition is: α must be part of a definable retraction. That is, there is a pure term β0 with β0 ∘ α ≡βη id. Then for every g and f = M(α) g we can take β = β0 and get g = M(β) f. Your two positive examples are exactly of this kind: one is an isomorphism (argument swap) and the other is a section with a definable left-inverse (a ↦ eval-at-a, left-inverse y ↦ y I).
• In the absence of such a retraction, there is in general no way to “invert” α by a pure term, even for a single given f = M(α) g. In particular, the intuitive idea that “higher type complexity of g than of f” would suffice is false.

A general necessary condition (and how to get counterexamples) Pure terms are invariant under arbitrary renamings of base-type elements. Concretely, in any full set-theoretic model with infinite base types, any family of bijections π on the base sets induces an automorphism of the whole model; the denotation of a pure term commutes with these automorphisms (equivariance). This gives an immediate necessary condition:

• If g = M(β) f for some pure β, then every automorphism of the model that fixes f must also fix g.

Equivalently, thinking in “support” terms, the set of base elements that g can depend on (its support) must be contained in the support of f. This yields a robust way to manufacture counterexamples: choose α that “forgets information” so that f depends on fewer base elements than g; then no pure β can recover g from f.

A concrete counterexample with g of higher type than f Let o be a base type (an infinite set), and consider

• A = (o → o) → o,
• B = o,
• α = λg. g I : A → B, where I = λx. x.

Pick any g ∈ A whose value depends on its argument in a way that involves more base elements than just g I. For instance (and such g exist in a full model), choose g that distinguishes its input h by looking at how h acts on two different atoms a ≠ b and returns different results accordingly. Then f = M(α) g = g I is just a single element v ∈ o; f is fixed by every permutation of o that fixes v, but by construction g is not fixed by some permutation that fixes v (it still permutes the other atoms g depends on). By the equivariance argument above, no pure β can satisfy M(β) f = g for this g. Thus even with g at higher type than f, inversion can fail.

Why your examples behave as they do

• Argument swap is an isomorphism; it has a pure inverse (itself).
• a ↦ eval-at-a is a section: β0 = λy. y I is a pure left-inverse, so β0 ∘ α = id and inversion works for every a uniformly.
• λx y. x discards the second argument; many different g map to the same f, and there is no way for a pure β to recover the lost information.

What can be said in general

• The strongest uniform condition you can expect is exactly that α splits (there is a pure β0 with β0 ∘ α ≡ id). This is both sufficient and, if you want the inversion to work for all g, necessary.
• For a single given pair (f, g) with f = M(α) g, the exact necessary-and-sufficient condition is tautological: g must lie in the “definable closure” of f, i.e., there must exist some pure term β with g = M(β) f. Equivariance gives a practical necessary check: any automorphism fixing f must fix g.
• Type complexity alone does not control invertibility. One can have g at strictly higher type than f and still be unable to recover g, as shown above.

References and context This topic connects to definable retractions/isomorphisms between simple types in the simply typed λ-calculus. There is a substantial literature classifying when a type is a (definable) retract of another. Your positive cases correspond to known definable isomorphisms/sections; outside those, in full models there will typically be many g for which inversion is impossible due to the equivariance constraint.