I think you meant (\x -> x) :: forall a. a -> a? Yes it is equivalent, one is just more “filled in”.
Not sure what you mean, do you mean \ @_ x -> x? That might be accepted in some contexts. There are some type checking questions unrelated to name resolution to work out, however.
I am interested in the concepts / theory but not when I am actually programming (i.e. I don’t want to have write
@everywhere just to satisfy my theorist side).
OK!
That the bit I I still don’t understand but I’ll trust you on that. If it is necessary, then it is. I’m still voting for implicit parameter and I think you understand my reasoning.
I just want to emphasize that optional != leaky implementation detail. There is no real upper bound to how much of your program a clever language implementation might be able to figure out / guess on it’s own. The point of this explicit stuff isn’t that GHC is lost and confused, but that the human might be lost an confused. Of course, this is a matter of opinion.
It is fine if you continue to like it :).