I haven't thought through the consequences of this fully, but it does seem plausible.
It says we must generalise over some ‘a’, but which ‘a’? What type does (\@a (\x. x)) have?
My understanding of Eric's idea is that GHC would give (\x.x) the type (alpha -> alpha), as usual. Then (\ @a (\x.x)) gets the type forall a. alpha -> alpha. Later, we might solve for alpha or generalize over it, perhaps leading a type like forall b a. b -> b.
But someone would need to write down a type system.
I agree here. I think we'd need more Medium Thought (not quite Hard Thought) before committing to this plan, but it still seems plausible.
Richard