In System F à la Church, can we automatize type inference for the for-all elimination?
I'm not really sure I've understood the question. 
First, I try to reduce your problem to the following unification problem: 

Given a system F type τ(X) with a free (type) variable X, and a type σ.
Is it possible to find a type γ such that τ(γ) = σ ?

Here is a pseudo-code (with an exception raised when not unifiable) for 
solving this problem. 

unify (X, σ) = σ
unify (Y, Y) = Y
unify (τ₁ → τ₂, σ₁ → σ₂) = unify(τ₁,σ₁) → unify(τ₂,σ₂)
unify (∀Y.τ(Y), ∀Y.σ(Y)) = ∀Y.unify(τ(Y),σ(Y)) (with Y a fresh variable)
unify (_,_) = raise Not_unifiable


You can prove (by induction) that γ = τ(unify(τ(X),σ) works if and 
only an exception is not raised. 

Now for your problem you can take 

f (ΛX.t) (r) = match type of t with "τ₁ → τ₂" =&gt; unify (τ₁, type of r) | _ =&gt; fail end


(of course your function f should take as argument a context if your terms are open).