Two distinct Notes named "Eta reduction for data families"

I noticed recently that there are two places in the code base named Note [Eta reduction for data families], but with entirely different contents. One is in CoAxiom:

Note [Eta reduction for data families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this
   data family T a b :: *
   newtype instance T Int a = MkT (IO a) deriving( Monad )
We'd like this to work.

From the 'newtype instance' you might think we'd get:
   newtype TInt a = MkT (IO a)
   axiom ax1 a :: T Int a ~ TInt a   -- The newtype-instance part
   axiom ax2 a :: TInt a ~ IO a      -- The newtype part

But now what can we do?  We have this problem
   Given:   d  :: Monad IO
   Wanted:  d' :: Monad (T Int) = d |> ????
What coercion can we use for the ???

Solution: eta-reduce both axioms, thus:
   axiom ax1 :: T Int ~ TInt
   axiom ax2 :: TInt ~ IO
Now
   d' = d |> Monad (sym (ax2 ; ax1))

----- Bottom line ------

For a CoAxBranch for a data family instance with representation
TyCon rep_tc:

  - cab_tvs (of its CoAxiom) may be shorter
    than tyConTyVars of rep_tc.

  - cab_lhs may be shorter than tyConArity of the family tycon
       i.e. LHS is unsaturated

  - cab_rhs will be (rep_tc cab_tvs)
       i.e. RHS is un-saturated

  - This eta reduction happens for data instances as well
    as newtype instances. Here we want to eta-reduce the data family axiom.

  - This eta-reduction is done in TcInstDcls.tcDataFamInstDecl.

But for a /type/ family
  - cab_lhs has the exact arity of the family tycon

There are certain situations (e.g., pretty-printing) where it is necessary to
deal with eta-expanded data family instances. For these situations, the
cab_eta_tvs field records the stuff that has been eta-reduced away.
So if we have
    axiom forall a b. F [a->b] = D b a
and cab_eta_tvs is [p,q], then the original user-written definition
looked like
    axiom forall a b p q. F [a->b] p q = D b a p q
(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 TyCon.  This is notionally separate
and deals with the axiom connecting a newtype with its representation
type; but it too is eta-reduced.)

And the other is in TcInstDcls:

Note [Eta-reduction for data families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
   data D :: * -> * -> * -> * -> *

   data instance D [(a,b)] p q :: * -> * where
      D1 :: blah1
      D2 :: blah2

Then we'll generate a representation data type
  data Drep a b p q z where
      D1 :: blah1
      D2 :: blah2

and an axiom to connect them
  axiom AxDrep forall a b p q z. D [(a,b]] p q z = Drep a b p q z

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

* The representation tycon Drep is parameerised over the free
  variables of the pattern, in no particular order. So there is no
  guarantee that 'p' and 'q' will come last in Drep's parameters, and
  in the right order.  So, if the /patterns/ of the family insatance
  are eta-redcible, we re-order Drep's parameters to put the
  eta-reduced type variables last.

* Although we eta-reduce the axiom, we eta-/expand/ the representation
  tycon Drep.  The kind of D says it takses four arguments, but the
  data instance header only supplies three.  But the AlgTyCOn for Drep
  itself must have enough TyConBinders so that its result kind is Type.
  So, with etaExpandAlgTyCon we make up some extra TyConBinders

* The result kind in the instance might be a polykind, like this:
     data family DP a :: forall k. k -> *
     data instance DP [b] :: forall k1 k2. (k1,k2) -> *

  So in type-checking the LHS (DP Int) we need to check that it is
  more polymorphic than the signature.  To do that we must skolemise
  the siganture and istantiate the call of DP.  So we end up with
     data instance DP [b] @(k1,k2) (z :: (k1,k2)) where

  Note that we must parameterise the representation tycon DPrep over
  'k1' and 'k2', as well as 'b'.

  The skolemise bit is done in tc_kind_sig, while the instantiate bit
  is done by tcFamTyPats.

* Very fiddly point.  When we eta-reduce to
     axiom AxDrep forall a b. D [(a,b]] = Drep a b

  we want the kind of (D [(a,b)]) to be the same as the kind of
  (Drep a b).  This ensures that applying the axiom doesn't change the
  kind.  Why is that hard?  Because the kind of (Drep a b) depends on
  the TyConBndrVis on Drep's arguments. In particular do we have
    (forall (k::*). blah) or (* -> blah)?

  We must match whatever D does!  In #15817 we had
      data family X a :: forall k. * -> *   -- Note: a forall that is not used
      data instance X Int b = MkX

  So the data instance is really
      data istance X Int @k b = MkX

  The axiom will look like
      axiom    X Int = Xrep

  and it's important that XRep :: forall k * -> *, following X.

  To achieve this we get the TyConBndrVis flags from tcbVisibilities,
  and use those flags for any eta-reduced arguments.  Sigh.

* The final turn of the knife is that tcbVisibilities is itself
  tricky to sort out.  Consider
      data family D k :: k
  Then consider D (forall k2. k2 -> k2) Type Type
  The visibilty flags on an application of D may affected by the arguments
  themselves.  Heavy sigh.  But not truly hard; that's what tcbVisibilities
  does.

This is rather confusing. I suggest that either:

1. The two Notes be combined into one Note.
2. The two Notes be given different names to set them apart.