Clean up "Eta reduction for data families" Noteswip/T17313

Before, there were two distinct Notes named
"Eta reduction for data families". This renames one of them to
"Implementing eta reduction for data families" to disambiguate the
two and fixes references in other parts of the codebase to ensure
that they are pointing to the right place.

Fixes #17313.

[ci skip]

7 files changed, 31 insertions, 21 deletions

diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs
index 06de44f65b..ea9a21d2aa 100644
--- a/compiler/GHC/Core/Coercion.hs
+++ b/compiler/GHC/Core/Coercion.hs
@@ -245,7 +245,7 @@ ppr_co_ax_branch ppr_rhs fam_tc branch
 
     -- Eta-expand LHS and RHS types, because sometimes data family
     -- instances are eta-reduced.
-    -- See Note [Eta reduction for data families] in GHC.Core.FamInstEnv.
+    -- See Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom.
     (ee_tvs, ee_lhs, ee_rhs) = etaExpandCoAxBranch branch
 
     pp_lhs = pprIfaceTypeApp topPrec (toIfaceTyCon fam_tc)
diff --git a/compiler/GHC/Core/Coercion/Axiom.hs b/compiler/GHC/Core/Coercion/Axiom.hs
index 9b8fb6e067..5dd99a4ac1 100644
--- a/compiler/GHC/Core/Coercion/Axiom.hs
+++ b/compiler/GHC/Core/Coercion/Axiom.hs
@@ -235,7 +235,7 @@ data CoAxBranch
     , cab_tvs      :: [TyVar]       -- Bound type variables; not necessarily fresh
     , cab_eta_tvs  :: [TyVar]       -- Eta-reduced tyvars
                                     -- See Note [CoAxBranch type variables]
-                                    -- cab_tvs and cab_lhs may be eta-reduded; see
+                                    -- cab_tvs and cab_lhs may be eta-reduced; see
                                     -- Note [Eta reduction for data families]
     , cab_cvs      :: [CoVar]       -- Bound coercion variables
                                     -- Always empty, for now.
@@ -443,9 +443,13 @@ looked like
 (See #9692, #14179, and #15845 for examples of what can go wrong if
 we don't eta-expand when showing things to the user.)
 
-(See also Note [Newtype eta] in GHC.Core.TyCon.  This is notionally separate
-and deals with the axiom connecting a newtype with its representation
-type; but it too is eta-reduced.)
+See also:
+
+* Note [Newtype eta] in GHC.Core.TyCon.  This is notionally separate
+  and deals with the axiom connecting a newtype with its representation
+  type; but it too is eta-reduced.
+* Note [Implementing eta reduction for data families] in TcInstDcls. This
+  describes the implementation details of this eta reduction happen.
 -}
 
 instance Eq (CoAxiom br) where
diff --git a/compiler/GHC/Core/FamInstEnv.hs b/compiler/GHC/Core/FamInstEnv.hs
index 8ac78035bd..0b58195be6 100644
--- a/compiler/GHC/Core/FamInstEnv.hs
+++ b/compiler/GHC/Core/FamInstEnv.hs
@@ -118,6 +118,7 @@ data FamInst  -- See Note [FamInsts and CoAxioms]
 
             , fi_tys    :: [Type]       --   The LHS type patterns
             -- May be eta-reduced; see Note [Eta reduction for data families]
+            -- in GHC.Core.Coercion.Axiom
 
             , fi_rhs :: Type         --   the RHS, with its freshened vars
             }
@@ -132,7 +133,8 @@ Note [Arity of data families]
 Data family instances might legitimately be over- or under-saturated.
 
 Under-saturation has two potential causes:
- U1) Eta reduction. See Note [Eta reduction for data families].
+ U1) Eta reduction. See Note [Eta reduction for data families] in
+     GHC.Core.Coercion.Axiom.
  U2) When the user has specified a return kind instead of written out patterns.
      Example:
 
@@ -160,8 +162,8 @@ Over-saturation is also possible:
 
       However, we require that any over-saturation is eta-reducible. That is,
       we require that any extra patterns be bare unrepeated type variables;
-      see Note [Eta reduction for data families]. Accordingly, the FamInst
-      is never over-saturated.
+      see Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom.
+      Accordingly, the FamInst is never over-saturated.
 
 Why can we allow such flexibility for data families but not for type families?
 Because data families can be decomposed -- that is, they are generative and
@@ -335,7 +337,7 @@ Then we get a data type for each instance, and an axiom:
    axiom ax8 a :: T Bool [a] ~ TBoolList a
 
 These two axioms for T, one with one pattern, one with two;
-see Note [Eta reduction for data families]
+see Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom
 
 Note [FamInstEnv determinism]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -479,7 +481,7 @@ irrelevant (clause 1 of compatible) or benign (clause 2 of compatible).
 Note [Compatibility of eta-reduced axioms]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In newtype instances of data families we eta-reduce the axioms,
-See Note [Eta reduction for data families] in GHC.Core.FamInstEnv. This means that
+See Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom. This means that
 we sometimes need to test compatibility of two axioms that were eta-reduced to
 different degrees, e.g.:
 
@@ -1057,7 +1059,7 @@ We handle data families and type families separately here:
  * For data family instances, though, we need to re-split for each
    instance, because the breakdown might be different for each
    instance.  Why?  Because of eta reduction; see
-   Note [Eta reduction for data families].
+   Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom.
 -}
 
 -- checks if one LHS is dominated by a list of other branches
diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs
index 11fd1cf5a9..e3044095bc 100644
--- a/compiler/GHC/Core/TyCon.hs
+++ b/compiler/GHC/Core/TyCon.hs
@@ -240,7 +240,7 @@ See also Note [Wrappers for data instance tycons] in GHC.Types.Id.Make
         DataFamInstTyCon T [Int] ax_ti
 
 * The axiom ax_ti may be eta-reduced; see
-  Note [Eta reduction for data families] in GHC.Core.FamInstEnv
+  Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom
 
 * Data family instances may have a different arity than the data family.
   See Note [Arity of data families] in GHC.Core.FamInstEnv
@@ -1100,8 +1100,9 @@ data AlgTyConFlav
                -- and R:T is the representation TyCon (ie this one)
                -- and a,b,c are the tyConTyVars of this TyCon
                --
-               -- BUT may be eta-reduced; see FamInstEnv
-               --     Note [Eta reduction for data families]
+               -- BUT may be eta-reduced; see
+               --     Note [Eta reduction for data families] in
+               --     GHC.Core.Coercion.Axiom
 
           -- Cached fields of the CoAxiom, but adjusted to
           -- use the tyConTyVars of this TyCon
diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs
index 40efd08652..506ae1a1fc 100644
--- a/compiler/typecheck/TcDeriv.hs
+++ b/compiler/typecheck/TcDeriv.hs
@@ -1312,7 +1312,7 @@ write it out
       return x = MkT [x]
       ... etc ...
 
-See Note [Eta reduction for data families] in GHC.Core.FamInstEnv
+See Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom
 
 %************************************************************************
 %*                                                                      *
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index e189c7d896..40bc3853d5 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -667,7 +667,7 @@ tcDataFamInstDecl mb_clsinfo
                                     new_or_data
 
        -- Eta-reduce the axiom if possible
-       -- Quite tricky: see Note [Eta-reduction for data families]
+       -- Quite tricky: see Note [Implementing eta reduction for data families]
        ; let (eta_pats, eta_tcbs) = eta_reduce fam_tc pats
              eta_tvs       = map binderVar eta_tcbs
              post_eta_qtvs = filterOut (`elem` eta_tvs) qtvs
@@ -761,7 +761,7 @@ tcDataFamInstDecl mb_clsinfo
        ; return (fam_inst, m_deriv_info) }
   where
     eta_reduce :: TyCon -> [Type] -> ([Type], [TyConBinder])
-    -- See Note [Eta reduction for data families] in GHC.Core.FamInstEnv
+    -- See Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom
     -- Splits the incoming patterns into two: the [TyVar]
     -- are the patterns that can be eta-reduced away.
     -- e.g.     T [a] Int a d c   ==>  (T [a] Int a, [d,c])
@@ -887,8 +887,8 @@ we actually have a place to put the regeneralised variables.
 Thus: skolemise away. cf. Inst.deeplySkolemise and TcUnify.tcSkolemise
 Examples in indexed-types/should_compile/T12369
 
-Note [Eta-reduction for data families]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Implementing eta reduction for data families]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
    data D :: * -> * -> * -> * -> *
 
@@ -906,7 +906,10 @@ and an axiom to connect them
 
 except that we'll eta-reduce the axiom to
   axiom AxDrep forall a b. D [(a,b]] = Drep a b
-There are several fiddly subtleties lurking here
+
+This is described at some length in Note [Eta reduction for data families]
+in GHC.Core.Coercion.Axiom. There are several fiddly subtleties lurking here,
+however, so this Note aims to describe these subtleties:
 
 * The representation tycon Drep is parameterised over the free
   variables of the pattern, in no particular order. So there is no
diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs
index d6972f8ec5..40e16d1305 100644
--- a/compiler/typecheck/TcSplice.hs
+++ b/compiler/typecheck/TcSplice.hs
@@ -2046,7 +2046,7 @@ reifyFamilyInstance is_poly_tvs (FamInst { fi_flavor = flavor
       DataFamilyInst rep_tc ->
         do { let -- eta-expand lhs types, because sometimes data/newtype
                  -- instances are eta-reduced; See #9692
-                 -- See Note [Eta reduction for data families] in GHC.Core.FamInstEnv
+                 -- See Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom
                  (ee_tvs, ee_lhs, _) = etaExpandCoAxBranch branch
                  fam'     = reifyName fam
                  dataCons = tyConDataCons rep_tc