Improve handling of data type return kindswip/T18300

Following a long conversation with Richard, this patch tidies up the
handling of return kinds for data/newtype declarations (vanilla,
family, and instance).

I have substantially edited the Notes in TyCl, so they would
bear careful reading.

Fixes #18300, #18357

In GHC.Tc.Instance.Family.newFamInst we were checking some Lint-like
properties with ASSSERT.  Instead Richard and I have added
a proper linter for axioms, and called it from lintGblEnv, which in
turn is called in tcRnModuleTcRnM

New tests (T18300, T18357) cause an ASSERT failure in HEAD.

1 files changed, 12 insertions, 6 deletions

diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs
index e7e5c9dc09..e72e5742a6 100644
--- a/compiler/GHC/Tc/Utils/Instantiate.hs
+++ b/compiler/GHC/Tc/Utils/Instantiate.hs
@@ -16,7 +16,7 @@ module GHC.Tc.Utils.Instantiate (
        instCall, instDFunType, instStupidTheta, instTyVarsWith,
        newWanted, newWanteds,
 
-       tcInstInvisibleTyBinders, tcInstInvisibleTyBinder,
+       tcInstInvisibleTyBindersN, tcInstInvisibleTyBinders, tcInstInvisibleTyBinder,
 
        newOverloadedLit, mkOverLit,
 
@@ -366,13 +366,19 @@ instStupidTheta orig theta
 *                                                                      *
 ********************************************************************* -}
 
--- | Instantiates up to n invisible binders
--- Returns the instantiating types, and body kind
-tcInstInvisibleTyBinders :: Int -> TcKind -> TcM ([TcType], TcKind)
+-- | Given ty::forall k1 k2. k, instantiate all the invisible forall-binders
+--   returning ty @kk1 @kk2 :: k[kk1/k1, kk2/k1]
+tcInstInvisibleTyBinders :: TcType -> TcKind -> TcM (TcType, TcKind)
+tcInstInvisibleTyBinders ty kind
+  = do { (extra_args, kind') <- tcInstInvisibleTyBindersN n_invis kind
+       ; return (mkAppTys ty extra_args, kind') }
+  where
+    n_invis = invisibleTyBndrCount kind
 
-tcInstInvisibleTyBinders 0 kind
+tcInstInvisibleTyBindersN :: Int -> TcKind -> TcM ([TcType], TcKind)
+tcInstInvisibleTyBindersN 0 kind
   = return ([], kind)
-tcInstInvisibleTyBinders n ty
+tcInstInvisibleTyBindersN n ty
   = go n empty_subst ty
   where
     empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ty))