I think the explanation for how propagation works is too detailed for a user manual. I think the first thing in that section should really just be a couple examples of when propagatedBuildInputs is needed and not needed. I think the detailed explanation of exactly how dependencies are propagated and in what way should be saved for a different document. Maybe a wiki page?
I do not think that the Nixpkgs manual is a user manual; for a long time it was called Nixpkgs development manual, but it also has accumulated some user-oriented notes that had no better place to go.
And of course there are notes for maintainers of normal packages there, and there are things for people who debug core parts (e.g. when wanting to fix cross-compilation to minor platforms), and these are also not always well-separated.
But this approach takes the problem out of the papercut scope, I guess…