"In pFG, the argument pBArg has been given a type (moreover a
monomorphic type) by the type signature for pFG itself. Why does
the definition of 'closed' require the variable to be let-bound?
Wouldn't lambda-bound with a type implicitly provided by an
explicit type signature for the lambda" be equally good?"
I think so, yes.
Full disclosure: before this thread, I had never looked closely at the MonoLocalBinds definition. For years, I was operating under a simpler premise: "a local binding group is closed if all variables free in the group are bound at top-level". That is, any binding group that capture variables from the local definition would not be generalized. This interpretation means that your definition within pFG1 would also not be generalized. But my working definition was too limited, as the manual explains.
Bottom line: I think you're right that we could do more generalization. I'm not sure how easy this would be to implement (I don't know how GHC tracks this information off the top of my head), but I do think it's worth filing a ticket to see if we can easily do better.
Good conversation! I've learned something here.
Thanks,
Richard