NamedFieldPuns/RecordWildCards "only if ... not ... bound at top level"

What does "[not] bound at top level" mean wrt NamedFieldPuns/RecordWildCards?

(I suspect this is either a bug or a mis-documentation.) GHC Users' guide 15.5.4 re NamedFieldPuns and 15.5.5 re RecordWildCards 'More details', fourth bullet.

{-# LANGUAGE  NamedFieldPuns, RecordWildCards  #-}

module ConfusingRecSyntax  where

    data T a = MkT{ fooT :: Int, barT :: a }
    
    someT = MkT{ fooT = 5, barT = (+ 1) }
    
    otherT MkT{ fooT } = MkT{ barT, .. }          -- barT not bound on lhs
    -- infer  otherT :: T a1 -> T (T a2 -> a2)
    
    gnaa = barT (otherT someT) someT 5             -- yields 6

The Users' guide says

• When record wildcards are use in record construction, a field f is initialised only if f is in scope, and is not imported or bound at top level. For example, f can be bound by an enclosing pattern match or let/where-binding.

In that equation for otherT, there's no pattern match or let/where binding for barT. So GHC falls back to the top-level binding (field selector) in the decl data T.

Strictly speaking, it's the NamedFieldPun that's using this top-level binding; but § 15.5.4 is unspecific about where it gets its binding from.

Proposed improvements or changes

§ 15.5.4 should use the same wording as 15.5.5 about the binding; both should be more explicit that "not ... bound at top level" doesn't apply for record selector top-level functions.

Or

GHC's behaviour is wrong: that use of barT should be rejected/warned

warning: [-Wmissing-fields]
* Fields of `MkT' not initialised: barT

Environment

• GHC version used: 8.10.7, Windows 64-bit (x86_64) (libgmp)