Warning unused-top-binds complains if not all projections from a data type are used

Summary

Warning unused-top-binds complains if not all projections from a data type are used. I'd expect a warning only if none of the projections is used.

Steps to reproduce

{-# OPTIONS_GHC -Wall #-}

module WarnUnusedProjection (match, project) where

data D = D { f1 :: Int, f2 :: Bool }

match :: D -> Int
match (D i b) = if b then i else 0

project :: D -> Int
project = f1

Expected behavior and discussion

I get the warning

WarnUnusedProjection.hs:5:25: warning: [-Wunused-top-binds]
    Defined but not used: ‘f2’
  |
5 | data D = D { f1 :: Int, f2 :: Bool }
  |                         ^^

I expect no warning.

I could silence this warning in several ways:

1. Prefix f2 with an underscore.
2. Introduce an artificial use of f2 into my code, like writing match with a record match.
3. Export f2.

Option 1 is not feasible, it does not look good if some projections are prefixed by an underscore and some not. I could of course always prefix all record field names by an underscore to prevent such a warning, but this has aesthetic issues.

Option 2 is what I did to silence the warning, but I'd prefer there wasn't a warning in this case in the first place.

Option 3 is probably what prevents abundant occurrence of this warning in the Agda code base, since we rarely write export lists, thus, all projections are exported by default.

I often give names to record field to document their intended purpose, not necessarily only to use the corresponding projections.

Alternatives to fix this issue:

1. The warning should only be thrown if none of the projections are used.
2. unused-top-binds does not include projections at all. Instead there is a new warning unused-projections that is off by default and not included in unused-top-binds.

Environment

• GHC version used: 8.6.4