Note [Kind inference for data family instances]

Consider this GADT-style data type declaration, where I have used
fresh variables in the data constructor's type, to stress that c,d are
quite distinct from a,b.
   data T a b where
     MkT :: forall c d. c d -> T c d

Following Note [Inferring kinds for type declarations] in GHC.Tc.TyCl,
to infer T's kind, we initially give T :: kappa, a monomorpic kind,
gather constraints from the header and data constructors, and conclude
   T :: (kappa1 -> type) -> kappa1 -> Type
Then we generalise, giving
   T :: forall k. (k->Type) -> k -> Type

Now what about a data /instance/ decl
   data family T :: forall k. (k->Type) -> k -> Type

   data instance T p Int where ...

No doubt here! The poly-kinded T is instantiated with k=Type, so the
header really looks like
   data instance T @Type (p :: Type->Type) Int where ...

But what about this?
   data instance T p q where
      MkT :: forall r. r Int -> T r Int

So what kind do 'p' and 'q' have?  No clues from the header, but from
the data constructor we can clearly see that (r :: Type->Type).  Does
that mean that the /entire data instance/ is instantiated at Type,
like this?
   data instance T @Type (p :: Type->Type) (q :: Type) where
      ...

Not at all! This is a /GADT/-style decl, so the kind argument might
be specialised in this particular data constructor, thus:
   data instance T @k (p :: k->Type) (q :: k) where
     MkT :: forall (r :: Type -> Type).
            r Int -> T @Type r Int
(and perhaps specialised differently in some other data
constructor MkT2).

The key difference in this case and 'data T' at the top of this Note
is that we have no known kind for 'data T'. We thus forbid different
specialisations of T in its constructors, in an attempt to avoid
inferring polymorphic recursion. In data family T, however, there is
no problem with polymorphic recursion: we already /fully know/ T's
kind -- that came from the family declaration, and is not influenced
by the data instances -- and hence we /can/ specialise T's kind
differently in different GADT data constructors.

SHORT SUMMARY: In a data instance decl, it's not clear whether kind
constraints arising from the data constructors should be considered
local to the (GADT) data /constructor/ or should apply to the entire
data instance.

DESIGN CHOICE: In a data/newtype family instance declaration:
* We take account of the data constructors (via `kcConDecls`) for:
  * Haskell-98 style data instance declarations
  * All newtype instance declarations
  For Haskell-98 style declarations, there is no GADT refinement. And for
  GADT-style newtype declarations, no GADT matching is allowed anyway,
  so it's just a syntactic difference from Haskell-98.

* We /ignore/ the data constructors for:
  * GADT-style data instance declarations
  Here, the instance kinds are influenced only by the header.

This choice is implemented by the guarded call to `kcConDecls` in
`tcDataFamInstHeader`.

Observations:
* With `UnliftedNewtypes` or `UnliftedDatatypes`, looking at the data
  constructors is necessary to infer the kind of the result type for
  certain cases. Otherwise, additional kind signatures are required.
  Consider the following example in #25611:

    data family Fix :: (k -> Type) -> k
    newtype instance Fix f = In { out :: f (Fix f) }

  If we are not looking at the data constructors:
  * Without `UnliftedNewtypes`, it is accepted since `Fix f` is defaulted
    to `Type`.
  * But with `UnliftedNewtypes`, `Fix f` is defaulted to `TYPE r` where
    `r` is not scoped over the data constructor. Then the header `Fix f :: TYPE r`
    will fail to kind unify with `f (Fix f) :: Type`.

  Hence, we need to look at the data constructor to infer `Fix f :: Type`
  for this newtype instance.

This DESIGN CHOICE strikes a balance between well-rounded kind inference
and implementation simplicity. See #25611, #18891, and !4419 for more
discussion of this issue.

Kind inference for data types (Xie et al) https://arxiv.org/abs/1911.06153
takes a slightly different approach.