Fix kind inference for data types. Again.

This patch fixes several aspects of kind inference for data type
declarations, especially data /instance/ declarations

Specifically

1. In kcConDecls/kcConDecl make it clear that the tc_res_kind argument
   is only used in the H98 case; and in that case there is no result
   kind signature; and hence no need for the disgusting splitPiTys in
   kcConDecls (now thankfully gone).

   The GADT case is a bit different to before, and much nicer.
   This is what fixes #18891.

   See Note [kcConDecls: kind-checking data type decls]

2. Do not look at the constructor decls of a data/newtype instance
   in tcDataFamInstanceHeader. See GHC.Tc.TyCl.Instance
   Note [Kind inference for data family instances].  This was a
   new realisation that arose when doing (1)

   This causes a few knock-on effects in the tests suite, because
   we require more information than before in the instance /header/.

   New user-manual material about this in "Kind inference in data type
   declarations" and "Kind inference for data/newtype instance
   declarations".

3. Minor improvement in kcTyClDecl, combining GADT and H98 cases

4. Fix #14111 and #8707 by allowing the header of a data instance
   to affect kind inferece for the the data constructor signatures;
   as described at length in Note [GADT return types] in GHC.Tc.TyCl

   This led to a modest refactoring of the arguments (and argument
   order) of tcConDecl/tcConDecls.

5. Fix #19000 by inverting the sense of the test in new_locs
   in GHC.Tc.Solver.Canonical.canDecomposableTyConAppOK.

2 files changed, 158 insertions, 85 deletions

diff --git a/docs/users_guide/9.2.1-notes.rst b/docs/users_guide/9.2.1-notes.rst
index 30a58175f4..283615b7a4 100644
--- a/docs/users_guide/9.2.1-notes.rst
+++ b/docs/users_guide/9.2.1-notes.rst
@@ -14,6 +14,11 @@ Language
   (Serrano et al, ICFP 2020).  More information here: :ref:`impredicative-polymorphism`.
   This replaces the old (undefined, flaky) behaviour of the :extension:`ImpredicativeTypes` extension.
 
+* Kind inference for data/newtype instance declarations is slightly
+  more restrictive than before.  See the user manual :ref:`kind-inference-data-family-instances`.
+  This is a breaking change, albeit a fairly obscure one that corrects a specification bug.
+
+
 Compiler
 ~~~~~~~~
 
diff --git a/docs/users_guide/exts/poly_kinds.rst b/docs/users_guide/exts/poly_kinds.rst
index 3cd9540a26..5b34ae10e4 100644
--- a/docs/users_guide/exts/poly_kinds.rst
+++ b/docs/users_guide/exts/poly_kinds.rst
@@ -130,8 +130,45 @@ This rule has occasionally-surprising consequences (see
 The kind-polymorphism from the class declaration makes ``D1``
 kind-polymorphic, but not so ``D2``; and similarly ``F1``, ``F2``.
 
+Kind inference in type signatures
+---------------------------------
+
+When kind-checking a type, GHC considers only what is written in that
+type when figuring out how to generalise the type's kind.
+
+For example,
+consider these definitions (with :extension:`ScopedTypeVariables`): ::
+
+  data Proxy a    -- Proxy :: forall k. k -> Type
+  p :: forall a. Proxy a
+  p = Proxy :: Proxy (a :: Type)
+
+GHC reports an error, saying that the kind of ``a`` should be a kind variable
+``k``, not ``Type``. This is because, by looking at the type signature
+``forall a. Proxy a``, GHC assumes ``a``'s kind should be generalised, not
+restricted to be ``Type``. The function definition is then rejected for being
+more specific than its type signature.
+
+.. _explicit-kind-quantification:
+
+Explicit kind quantification
+----------------------------
+
+Enabled by :extension:`PolyKinds`, GHC supports explicit kind quantification,
+as in these examples: ::
+
+  data Proxy :: forall k. k -> Type
+  f :: (forall k (a :: k). Proxy a -> ()) -> Int
+
+Note that the second example has a ``forall`` that binds both a kind ``k`` and
+a type variable ``a`` of kind ``k``. In general, there is no limit to how
+deeply nested this sort of dependency can work. However, the dependency must
+be well-scoped: ``forall (a :: k) k. ...`` is an error.
+
+
 .. _inferring-variable-order:
 
+
 Inferring the order of variables in a type/class declaration
 ------------------------------------------------------------
 
@@ -490,41 +527,92 @@ This also applies to GADT-style data instances: ::
       --   • In the data instance declaration for ‘T’
 
 
-Kind inference in closed type families
---------------------------------------
+Kind inference in data type declarations
+----------------------------------------
 
-Although all open type families are considered to have a complete
-user-supplied kind signature, we can relax this condition for closed
-type families, where we have equations on which to perform kind
-inference. GHC will infer kinds for the arguments and result types of a
-closed type family.
+Consider the declaration ::
 
-GHC supports *kind-indexed* type families, where the family matches both
-on the kind and type. GHC will *not* infer this behaviour without a
-complete user-supplied kind signature, as doing so would sometimes infer
-non-principal types. Indeed, we can see kind-indexing as a form
-of polymorphic recursion, where a type is used at a kind other than
-its most general in its own definition.
+  data T1 f a = MkT1 (f a)
+  data T2 f a where
+    MkT2 :: f a -> T f a
 
-For example: ::
+In both cases GHC looks at the data constructor declarations to
+give constraints on the kind of ``T``, yielding ::
 
-    type family F1 a where
-      F1 True  = False
-      F1 False = True
-      F1 x     = x
-    -- F1 fails to compile: kind-indexing is not inferred
+  T1, T2 :: forall k. (k -> Type) -> k -> Type
 
-    type family F2 (a :: k) where
-      F2 True  = False
-      F2 False = True
-      F2 x     = x
-    -- F2 fails to compile: no complete signature
+Consider the type ::
+
+  type G :: forall k. k -> Type
+  data G (a :: k) where
+    GInt    :: G Int
+    GMaybe  :: G Maybe
+
+This datatype ``G`` is GADT-like in both its kind and its type. Suppose you
+have ``g :: G a``, where ``a :: k``. Then pattern matching to discover that
+``g`` is in fact ``GMaybe`` tells you both that ``k ~ (Type -> Type)`` and
+``a ~ Maybe``. The definition for ``G`` requires that :extension:`PolyKinds`
+be in effect, but pattern-matching on ``G`` requires no extension beyond
+:extension:`GADTs`. That this works is actually a straightforward extension
+of regular GADTs and a consequence of the fact that kinds and types are the
+same.
+
+Note that the datatype ``G`` is used at different kinds in its body, and
+therefore that kind-indexed GADTs use a form of polymorphic recursion.
+It is thus only possible to use this feature if you have provided a
+complete user-supplied kind signature (CUSK)
+for the datatype (:ref:`complete-kind-signatures`), or a standalone
+kind signature (:ref:`standalone-kind-signatures`);
+in the case of ``G`` we both.
+If you wish to see the kind indexing explicitly, you can do so by enabling :ghc-flag:`-fprint-explicit-kinds` and querying ``G`` with GHCi's :ghci-cmd:`:info` command: ::
+
+  > :set -fprint-explicit-kinds
+  > :info G
+  type role G nominal nominal
+  type G :: forall k. k -> Type
+  data G @k a where
+    GInt   :: G @Type Int
+    GMaybe :: G @(Type -> Type) Maybe
+
+where you can see the GADT-like nature of the two constructors.
+
+.. _kind-inference-data-family-instances:
+
+Kind inference for data/newtype instance declarations
+-----------------------------------------------------
+
+Consider these declarations ::
+
+   data family T :: forall k. (k->Type) -> k -> Type
+
+   data instance T p q where
+      MkT :: forall r. r Int -> T r Int
+
+Here ``T`` has an invisible kind argument; and perhaps it is instantiated
+to ``Type`` in the instance, thus::
+
+   data instance T @Type (p :: Type->Type) (q :: Type) where
+      MkT :: forall r. r Int -> T r Int
+
+Or perhaps we intended the specialisation to be in the GADT data
+constructor, thus::
+
+   data instance T @k (p :: k->Type) (q :: k) where
+      MkT :: forall r. r Int -> T @Type r Int
+
+It gets more complicated if there are multiple constructors.  In
+general, there is no principled way to tell which type specialisation
+comes from the data instance, and which from the individual GADT data
+constructors.
+
+So GHC implements this rule: in data/newtype instance declararations
+(unlike ordinary data/newtype declarations) we do *not* look at the
+constructor declarations when inferring the shape of the instance
+header.  The principle is that *the instantiation of the data instance
+should be apparent from the header alone*.  This principle makes the
+program easier to understand, and avoids the swamp of complexity
+indicated above.
 
-    type family F3 (a :: k) :: k where
-      F3 True  = False
-      F3 False = True
-      F3 x     = x
-    -- OK
 
 Kind inference in class instance declarations
 ---------------------------------------------
@@ -555,43 +643,8 @@ infrastructure, and it's not clear the payoff is worth it. If you want
 to restrict ``b``\ 's kind in the instance above, just use a kind
 signature in the instance head.
 
-Kind inference in type signatures
----------------------------------
-
-When kind-checking a type, GHC considers only what is written in that
-type when figuring out how to generalise the type's kind.
-
-For example,
-consider these definitions (with :extension:`ScopedTypeVariables`): ::
-
-  data Proxy a    -- Proxy :: forall k. k -> Type
-  p :: forall a. Proxy a
-  p = Proxy :: Proxy (a :: Type)
-
-GHC reports an error, saying that the kind of ``a`` should be a kind variable
-``k``, not ``Type``. This is because, by looking at the type signature
-``forall a. Proxy a``, GHC assumes ``a``'s kind should be generalised, not
-restricted to be ``Type``. The function definition is then rejected for being
-more specific than its type signature.
-
-.. _explicit-kind-quantification:
-
-Explicit kind quantification
-----------------------------
-
-Enabled by :extension:`PolyKinds`, GHC supports explicit kind quantification,
-as in these examples: ::
-
-  data Proxy :: forall k. k -> Type
-  f :: (forall k (a :: k). Proxy a -> ()) -> Int
-
-Note that the second example has a ``forall`` that binds both a kind ``k`` and
-a type variable ``a`` of kind ``k``. In general, there is no limit to how
-deeply nested this sort of dependency can work. However, the dependency must
-be well-scoped: ``forall (a :: k) k. ...`` is an error.
-
-Implicit quantification in type synonyms and type family instances
-------------------------------------------------------------------
+Kind inference in type synonyms and type family instances
+---------------------------------------------------------
 
 Consider the scoping rules for type synonyms and type family instances, such as
 these::
@@ -706,29 +759,44 @@ kinds. Consequently, visible dependent quantifiers are rejected in any context
 that is unambiguously the type of a term. They are also rejected in the types
 of data constructors.
 
-Kind-indexed GADTs
-------------------
+Kind inference in closed type families
+--------------------------------------
 
-Consider the type ::
+Although all open type families are considered to have a complete
+user-supplied kind signature (:ref:`complete-kind-signatures`),
+we can relax this condition for closed
+type families, where we have equations on which to perform kind
+inference. GHC will infer kinds for the arguments and result types of a
+closed type family.
 
-  data G (a :: k) where
-    GInt    :: G Int
-    GMaybe  :: G Maybe
+GHC supports *kind-indexed* type families, where the family matches both
+on the kind and type. GHC will *not* infer this behaviour without a
+complete user-supplied kind signature or standalone kind
+signature (see :ref:`standalone-kind-signatures`),
+because doing so would sometimes infer
+non-principal types. Indeed, we can see kind-indexing as a form
+of polymorphic recursion, where a type is used at a kind other than
+its most general in its own definition.
 
-This datatype ``G`` is GADT-like in both its kind and its type. Suppose you
-have ``g :: G a``, where ``a :: k``. Then pattern matching to discover that
-``g`` is in fact ``GMaybe`` tells you both that ``k ~ (Type -> Type)`` and
-``a ~ Maybe``. The definition for ``G`` requires that :extension:`PolyKinds`
-be in effect, but pattern-matching on ``G`` requires no extension beyond
-:extension:`GADTs`. That this works is actually a straightforward extension
-of regular GADTs and a consequence of the fact that kinds and types are the
-same.
+For example: ::
 
-Note that the datatype ``G`` is used at different kinds in its body, and
-therefore that kind-indexed GADTs use a form of polymorphic recursion.
-It is thus only possible to use this feature if you have provided a
-complete user-supplied kind signature
-for the datatype (:ref:`complete-kind-signatures`).
+    type family F1 a where
+      F1 True  = False
+      F1 False = True
+      F1 x     = x
+    -- F1 fails to compile: kind-indexing is not inferred
+
+    type family F2 (a :: k) where
+      F2 True  = False
+      F2 False = True
+      F2 x     = x
+    -- F2 fails to compile: no complete signature
+
+    type family F3 (a :: k) :: k where
+      F3 True  = False
+      F3 False = True
+      F3 x     = x
+    -- OK
 
 Higher-rank kinds
 -----------------