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.

13 files changed, 651 insertions, 346 deletions

diff --git a/compiler/GHC/Core/Coercion/Axiom.hs b/compiler/GHC/Core/Coercion/Axiom.hs
index 4ecbb6cc3d..7046273ae5 100644
--- a/compiler/GHC/Core/Coercion/Axiom.hs
+++ b/compiler/GHC/Core/Coercion/Axiom.hs
@@ -184,9 +184,10 @@ Note [Storing compatibility]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 During axiom application, we need to be aware of which branches are compatible
 with which others. The full explanation is in Note [Compatibility] in
-FamInstEnv. (The code is placed there to avoid a dependency from CoAxiom on
-the unification algorithm.) Although we could theoretically compute
-compatibility on the fly, this is silly, so we store it in a CoAxiom.
+GHc.Core.FamInstEnv. (The code is placed there to avoid a dependency from
+GHC.Core.Coercion.Axiom on the unification algorithm.) Although we could
+theoretically compute compatibility on the fly, this is silly, so we store it
+in a CoAxiom.
 
 Specifically, each branch refers to all other branches with which it is
 incompatible. This list might well be empty, and it will always be for the
@@ -233,8 +234,8 @@ data CoAxBranch
     { cab_loc      :: SrcSpan       -- Location of the defining equation
                                     -- See Note [CoAxiom locations]
     , cab_tvs      :: [TyVar]       -- Bound type variables; not necessarily fresh
-    , cab_eta_tvs  :: [TyVar]       -- Eta-reduced tyvars
                                     -- See Note [CoAxBranch type variables]
+    , cab_eta_tvs  :: [TyVar]       -- Eta-reduced tyvars
                                     -- cab_tvs and cab_lhs may be eta-reduced; see
                                     -- Note [Eta reduction for data families]
     , cab_cvs      :: [CoVar]       -- Bound coercion variables
diff --git a/compiler/GHC/Core/DataCon.hs b/compiler/GHC/Core/DataCon.hs
index 60a7052643..cc4b84faa9 100644
--- a/compiler/GHC/Core/DataCon.hs
+++ b/compiler/GHC/Core/DataCon.hs
@@ -425,7 +425,7 @@ data DataCon
                 -- NB: for a data instance, the original user result type may
                 -- differ from the DataCon's representation TyCon.  Example
                 --      data instance T [a] where MkT :: a -> T [a]
-                -- The OrigResTy is T [a], but the dcRepTyCon might be :T123
+                -- The dcOrigResTy is T [a], but the dcRepTyCon might be R:TList
 
         -- Now the strictness annotations and field labels of the constructor
         dcSrcBangs :: [HsSrcBang],
@@ -1576,4 +1576,3 @@ splitDataProductType_maybe ty
   = Just (tycon, ty_args, con, dataConInstArgTys con ty_args)
   | otherwise
   = Nothing
-
diff --git a/compiler/GHC/Core/FamInstEnv.hs b/compiler/GHC/Core/FamInstEnv.hs
index 8408bc5406..4a685ba096 100644
--- a/compiler/GHC/Core/FamInstEnv.hs
+++ b/compiler/GHC/Core/FamInstEnv.hs
@@ -640,16 +640,13 @@ that Note.
 mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars
              -> [TyVar] -- Extra eta tyvars
              -> [CoVar] -- possibly stale covars
-             -> TyCon   -- family/newtype TyCon (for error-checking only)
              -> [Type]  -- LHS patterns
              -> Type    -- RHS
              -> [Role]
              -> SrcSpan
              -> CoAxBranch
-mkCoAxBranch tvs eta_tvs cvs ax_tc lhs rhs roles loc
-  = -- See Note [CoAxioms are homogeneous] in "GHC.Core.Coercion.Axiom"
-    ASSERT( typeKind (mkTyConApp ax_tc lhs) `eqType` typeKind rhs )
-    CoAxBranch { cab_tvs     = tvs'
+mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc
+  = CoAxBranch { cab_tvs     = tvs'
                , cab_eta_tvs = eta_tvs'
                , cab_cvs     = cvs'
                , cab_lhs     = tidyTypes env lhs
@@ -703,7 +700,7 @@ mkSingleCoAxiom role ax_name tvs eta_tvs cvs fam_tc lhs_tys rhs_ty
             , co_ax_implicit = False
             , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
   where
-    branch = mkCoAxBranch tvs eta_tvs cvs fam_tc lhs_tys rhs_ty
+    branch = mkCoAxBranch tvs eta_tvs cvs lhs_tys rhs_ty
                           (map (const Nominal) tvs)
                           (getSrcSpan ax_name)
 
@@ -721,7 +718,7 @@ mkNewTypeCoAxiom name tycon tvs roles rhs_ty
             , co_ax_tc       = tycon
             , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
   where
-    branch = mkCoAxBranch tvs [] [] tycon (mkTyVarTys tvs) rhs_ty
+    branch = mkCoAxBranch tvs [] [] (mkTyVarTys tvs) rhs_ty
                           roles (getSrcSpan name)
 
 {-
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index e7385be78f..32abec0521 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -8,13 +8,12 @@ See Note [Core Lint guarantee].
 -}
 
 {-# LANGUAGE CPP #-}
-{-# LANGUAGE ViewPatterns #-}
-{-# LANGUAGE ScopedTypeVariables, DeriveFunctor #-}
+{-# LANGUAGE ViewPatterns, ScopedTypeVariables, DeriveFunctor, MultiWayIf #-}
 
 module GHC.Core.Lint (
     lintCoreBindings, lintUnfolding,
     lintPassResult, lintInteractiveExpr, lintExpr,
-    lintAnnots, lintTypes,
+    lintAnnots, lintAxioms,
 
     -- ** Debug output
     endPass, endPassIO,
@@ -36,7 +35,7 @@ import GHC.Types.Literal
 import GHC.Core.DataCon
 import GHC.Builtin.Types.Prim
 import GHC.Builtin.Types ( multiplicityTy )
-import GHC.Tc.Utils.TcType ( isFloatingTy )
+import GHC.Tc.Utils.TcType ( isFloatingTy, isTyFamFree )
 import GHC.Types.Var as Var
 import GHC.Types.Var.Env
 import GHC.Types.Var.Set
@@ -56,9 +55,10 @@ import GHC.Types.RepType
 import GHC.Core.TyCo.Rep   -- checks validity of types/coercions
 import GHC.Core.TyCo.Subst
 import GHC.Core.TyCo.FVs
-import GHC.Core.TyCo.Ppr ( pprTyVar )
+import GHC.Core.TyCo.Ppr ( pprTyVar, pprTyVars )
 import GHC.Core.TyCon as TyCon
 import GHC.Core.Coercion.Axiom
+import GHC.Core.Unify
 import GHC.Types.Basic
 import GHC.Utils.Error as Err
 import GHC.Data.List.SetOps
@@ -76,7 +76,7 @@ import GHC.Driver.Session
 import Control.Monad
 import GHC.Utils.Monad
 import Data.Foldable      ( toList )
-import Data.List.NonEmpty ( NonEmpty )
+import Data.List.NonEmpty ( NonEmpty(..), groupWith )
 import Data.List          ( partition )
 import Data.Maybe
 import GHC.Data.Pair
@@ -1587,18 +1587,6 @@ lintIdBndr top_lvl bind_site id thing_inside
 %************************************************************************
 -}
 
-lintTypes :: DynFlags
-          -> [TyCoVar]   -- Treat these as in scope
-          -> [Type]
-          -> Maybe MsgDoc -- Nothing => OK
-lintTypes dflags vars tys
-  | isEmptyBag errs = Nothing
-  | otherwise       = Just (pprMessageBag errs)
-  where
-    (_warns, errs) = initL dflags (defaultLintFlags dflags) vars linter
-    linter = lintBinders LambdaBind vars $ \_ ->
-             mapM_ lintType tys
-
 lintValueType :: Type -> LintM LintedType
 -- Types only, not kinds
 -- Check the type, and apply the substitution to it
@@ -1617,7 +1605,7 @@ checkTyCon tc
   = checkL (not (isTcTyCon tc)) (text "Found TcTyCon:" <+> ppr tc)
 
 -------------------
-lintType :: LintedType -> LintM LintedType
+lintType :: Type -> LintM LintedType
 
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism]
@@ -2342,6 +2330,175 @@ lintCoercion (HoleCo h)
   = do { addErrL $ text "Unfilled coercion hole:" <+> ppr h
        ; lintCoercion (CoVarCo (coHoleCoVar h)) }
 
+{-
+************************************************************************
+*                                                                      *
+              Axioms
+*                                                                      *
+************************************************************************
+-}
+
+lintAxioms :: DynFlags
+           -> [CoAxiom Branched]
+           -> WarnsAndErrs
+lintAxioms dflags axioms
+  = initL dflags (defaultLintFlags dflags) [] $
+    do { mapM_ lint_axiom axioms
+       ; let axiom_groups = groupWith coAxiomTyCon axioms
+       ; mapM_ lint_axiom_group axiom_groups }
+
+lint_axiom :: CoAxiom Branched -> LintM ()
+lint_axiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches
+                       , co_ax_role = ax_role })
+  = addLoc (InAxiom ax) $
+    do { mapM_ (lint_branch tc) branch_list
+       ; extra_checks }
+  where
+    branch_list = fromBranches branches
+
+    extra_checks
+      | isNewTyCon tc
+      = do { CoAxBranch { cab_tvs     = tvs
+                        , cab_eta_tvs = eta_tvs
+                        , cab_cvs     = cvs
+                        , cab_roles   = roles
+                        , cab_lhs     = lhs_tys }
+              <- case branch_list of
+               [branch] -> return branch
+               _        -> failWithL (text "multi-branch axiom with newtype")
+           ; let ax_lhs = mkInfForAllTys tvs $
+                          mkTyConApp tc lhs_tys
+                 nt_tvs = takeList tvs (tyConTyVars tc)
+                    -- axiom may be eta-reduced: Note [Newtype eta] in GHC.Core.TyCon
+                 nt_lhs = mkInfForAllTys nt_tvs $
+                          mkTyConApp tc (mkTyVarTys nt_tvs)
+                 -- See Note [Newtype eta] in GHC.Core.TyCon
+           ; lintL (ax_lhs `eqType` nt_lhs)
+                   (text "Newtype axiom LHS does not match newtype definition")
+           ; lintL (null cvs)
+                   (text "Newtype axiom binds coercion variables")
+           ; lintL (null eta_tvs)  -- See Note [Eta reduction for data families]
+                                   -- which is not about newtype axioms
+                   (text "Newtype axiom has eta-tvs")
+           ; lintL (ax_role == Representational)
+                   (text "Newtype axiom role not representational")
+           ; lintL (roles `equalLength` tvs)
+                   (text "Newtype axiom roles list is the wrong length." $$
+                    text "roles:" <+> sep (map ppr roles))
+           ; lintL (roles == takeList roles (tyConRoles tc))
+                   (vcat [ text "Newtype axiom roles do not match newtype tycon's."
+                         , text "axiom roles:" <+> sep (map ppr roles)
+                         , text "tycon roles:" <+> sep (map ppr (tyConRoles tc)) ])
+           }
+
+      | isFamilyTyCon tc
+      = do { if | isTypeFamilyTyCon tc
+                  -> lintL (ax_role == Nominal)
+                           (text "type family axiom is not nominal")
+
+                | isDataFamilyTyCon tc
+                  -> lintL (ax_role == Representational)
+                           (text "data family axiom is not representational")
+
+                | otherwise
+                  -> addErrL (text "A family TyCon is neither a type family nor a data family:" <+> ppr tc)
+
+           ; mapM_ (lint_family_branch tc) branch_list }
+
+      | otherwise
+      = addErrL (text "Axiom tycon is neither a newtype nor a family.")
+
+lint_branch :: TyCon -> CoAxBranch -> LintM ()
+lint_branch ax_tc (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
+                              , cab_lhs = lhs_args, cab_rhs = rhs })
+  = lintBinders LambdaBind (tvs ++ cvs) $ \_ ->
+    do { let lhs = mkTyConApp ax_tc lhs_args
+       ; lhs' <- lintType lhs
+       ; rhs' <- lintType rhs
+       ; let lhs_kind = typeKind lhs'
+             rhs_kind = typeKind rhs'
+       ; lintL (lhs_kind `eqType` rhs_kind) $
+         hang (text "Inhomogeneous axiom")
+            2 (text "lhs:" <+> ppr lhs <+> dcolon <+> ppr lhs_kind $$
+               text "rhs:" <+> ppr rhs <+> dcolon <+> ppr rhs_kind) }
+
+-- these checks do not apply to newtype axioms
+lint_family_branch :: TyCon -> CoAxBranch -> LintM ()
+lint_family_branch fam_tc br@(CoAxBranch { cab_tvs     = tvs
+                                         , cab_eta_tvs = eta_tvs
+                                         , cab_cvs     = cvs
+                                         , cab_roles   = roles
+                                         , cab_lhs     = lhs
+                                         , cab_incomps = incomps })
+  = do { lintL (isDataFamilyTyCon fam_tc || null eta_tvs)
+               (text "Type family axiom has eta-tvs")
+       ; lintL (all (`elemVarSet` tyCoVarsOfTypes lhs) tvs)
+               (text "Quantified variable in family axiom unused in LHS")
+       ; lintL (all isTyFamFree lhs)
+               (text "Type family application on LHS of family axiom")
+       ; lintL (all (== Nominal) roles)
+               (text "Non-nominal role in family axiom" $$
+                text "roles:" <+> sep (map ppr roles))
+       ; lintL (null cvs)
+               (text "Coercion variables bound in family axiom")
+       ; forM_ incomps $ \ br' ->
+           lintL (not (compatible_branches br br')) $
+           text "Incorrect incompatible branch:" <+> ppr br' }
+
+lint_axiom_group :: NonEmpty (CoAxiom Branched) -> LintM ()
+lint_axiom_group (_  :| []) = return ()
+lint_axiom_group (ax :| axs)
+  = do { lintL (isOpenFamilyTyCon tc)
+               (text "Non-open-family with multiple axioms")
+       ; let all_pairs = [ (ax1, ax2) | ax1 <- all_axs
+                                      , ax2 <- all_axs ]
+       ; mapM_ (lint_axiom_pair tc) all_pairs }
+  where
+    all_axs = ax : axs
+    tc      = coAxiomTyCon ax
+
+lint_axiom_pair :: TyCon -> (CoAxiom Branched, CoAxiom Branched) -> LintM ()
+lint_axiom_pair tc (ax1, ax2)
+  | Just br1@(CoAxBranch { cab_tvs = tvs1
+                         , cab_lhs = lhs1
+                         , cab_rhs = rhs1 }) <- coAxiomSingleBranch_maybe ax1
+  , Just br2@(CoAxBranch { cab_tvs = tvs2
+                         , cab_lhs = lhs2
+                         , cab_rhs = rhs2 }) <- coAxiomSingleBranch_maybe ax2
+  = lintL (compatible_branches br1 br2) $
+    vcat [ hsep [ text "Axioms", ppr ax1, text "and", ppr ax2
+                , text "are incompatible" ]
+         , text "tvs1 =" <+> pprTyVars tvs1
+         , text "lhs1 =" <+> ppr (mkTyConApp tc lhs1)
+         , text "rhs1 =" <+> ppr rhs1
+         , text "tvs2 =" <+> pprTyVars tvs2
+         , text "lhs2 =" <+> ppr (mkTyConApp tc lhs2)
+         , text "rhs2 =" <+> ppr rhs2 ]
+
+  | otherwise
+  = addErrL (text "Open type family axiom has more than one branch: either" <+>
+             ppr ax1 <+> text "or" <+> ppr ax2)
+
+compatible_branches :: CoAxBranch -> CoAxBranch -> Bool
+-- True <=> branches are compatible. See Note [Compatibility] in GHC.Core.FamInstEnv.
+compatible_branches (CoAxBranch { cab_tvs = tvs1
+                                , cab_lhs = lhs1
+                                , cab_rhs = rhs1 })
+                    (CoAxBranch { cab_tvs = tvs2
+                                , cab_lhs = lhs2
+                                , cab_rhs = rhs2 })
+  = -- we need to freshen ax2 w.r.t. ax1
+    -- do this by pretending tvs1 are in scope when processing tvs2
+    let in_scope       = mkInScopeSet (mkVarSet tvs1)
+        subst0         = mkEmptyTCvSubst in_scope
+        (subst, _)     = substTyVarBndrs subst0 tvs2
+        lhs2'          = substTys subst lhs2
+        rhs2'          = substTy  subst rhs2
+    in
+    case tcUnifyTys (const BindMe) lhs1 lhs2' of
+      Just unifying_subst -> substTy unifying_subst rhs1  `eqType`
+                             substTy unifying_subst rhs2'
+      Nothing             -> True
 
 {-
 ************************************************************************
@@ -2539,6 +2696,7 @@ data LintLocInfo
   | TopLevelBindings
   | InType Type         -- Inside a type
   | InCo   Coercion     -- Inside a coercion
+  | InAxiom (CoAxiom Branched)   -- Inside a CoAxiom
 
 initL :: DynFlags -> LintFlags -> [Var]
        -> LintM a -> WarnsAndErrs    -- Warnings and errors
@@ -2822,6 +2980,34 @@ dumpLoc (InType ty)
   = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
 dumpLoc (InCo co)
   = (noSrcLoc, text "In the coercion" <+> quotes (ppr co))
+dumpLoc (InAxiom ax)
+  = (getSrcLoc ax_name, text "In the coercion axiom" <+> ppr ax_name <+> dcolon <+> pp_ax)
+  where
+    CoAxiom { co_ax_name     = ax_name
+            , co_ax_tc       = tc
+            , co_ax_role     = ax_role
+            , co_ax_branches = branches } = ax
+    branch_list = fromBranches branches
+
+    pp_ax
+      | [branch] <- branch_list
+      = pp_branch branch
+
+      | otherwise
+      = braces $ vcat (map pp_branch branch_list)
+
+    pp_branch (CoAxBranch { cab_tvs = tvs
+                          , cab_cvs = cvs
+                          , cab_lhs = lhs_tys
+                          , cab_rhs = rhs_ty })
+      = sep [ brackets (pprWithCommas pprTyVar (tvs ++ cvs)) <> dot
+            , ppr (mkTyConApp tc lhs_tys)
+            , text "~_" <> pp_role ax_role
+            , ppr rhs_ty ]
+
+    pp_role Nominal          = text "N"
+    pp_role Representational = text "R"
+    pp_role Phantom          = text "P"
 
 pp_binders :: [Var] -> SDoc
 pp_binders bs = sep (punctuate comma (map pp_binder bs))
diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs
index aa5c3460b0..e4f31e9fe0 100644
--- a/compiler/GHC/Core/TyCon.hs
+++ b/compiler/GHC/Core/TyCon.hs
@@ -293,7 +293,14 @@ See also Note [Wrappers for data instance tycons] in GHC.Types.Id.Make
     Indeed the latter type is unknown to the programmer.
 
   - There *is* an instance for (T Int) in the type-family instance
-    environment, but it is only used for overlap checking
+    environment, but it is looked up (via tcLookupDataFamilyInst)
+    in can_eq_nc (via tcTopNormaliseNewTypeTF_maybe) when trying to
+    solve representational equalities like
+         T Int ~R# Bool
+    Here we look up (T Int), convert it to R:TInt, and then unwrap the
+    newtype R:TInt.
+
+    It is also looked up in reduceTyFamApp_maybe.
 
   - It's fine to have T in the LHS of a type function:
     type instance F (T a) = [a]
@@ -1251,34 +1258,21 @@ example,
 
    newtype T a = MkT (a -> a)
 
-the NewTyCon for T will contain nt_co = CoT where CoT t : T t ~ t -> t.
-
-In the case that the right hand side is a type application
-ending with the same type variables as the left hand side, we
-"eta-contract" the coercion.  So if we had
-
-   newtype S a = MkT [a]
-
-then we would generate the arity 0 axiom CoS : S ~ [].  The
-primary reason we do this is to make newtype deriving cleaner.
+the NewTyCon for T will contain nt_co = CoT where CoT :: forall a. T a ~ a -> a.
 
-In the paper we'd write
-        axiom CoT : (forall t. T t) ~ (forall t. [t])
-and then when we used CoT at a particular type, s, we'd say
-        CoT @ s
-which encodes as (TyConApp instCoercionTyCon [TyConApp CoT [], s])
+We might also eta-contract the axiom: see Note [Newtype eta].
 
 Note [Newtype eta]
 ~~~~~~~~~~~~~~~~~~
 Consider
         newtype Parser a = MkParser (IO a) deriving Monad
-Are these two types equal (to Core)?
+Are these two types equal (that is, does a coercion exist between them)?
         Monad Parser
         Monad IO
 which we need to make the derived instance for Monad Parser.
 
 Well, yes.  But to see that easily we eta-reduce the RHS type of
-Parser, in this case to ([], Froogle), so that even unsaturated applications
+Parser, in this case to IO, so that even unsaturated applications
 of Parser will work right.  This eta reduction is done when the type
 constructor is built, and cached in NewTyCon.
 
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 1ab1986d74..5bb11a9ee7 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -70,7 +70,6 @@ module GHC.Core.Type (
         getRuntimeRep_maybe, kindRep_maybe, kindRep,
 
         mkCastTy, mkCoercionTy, splitCastTy_maybe,
-        discardCast,
 
         userTypeError_maybe, pprUserTypeErrorTy,
 
@@ -1402,20 +1401,6 @@ tyConBindersTyCoBinders = map to_tyb
     to_tyb (Bndr tv (NamedTCB vis)) = Named (Bndr tv vis)
     to_tyb (Bndr tv (AnonTCB af))   = Anon af (tymult (varType tv))
 
--- | Drop the cast on a type, if any. If there is no
--- cast, just return the original type. This is rarely what
--- you want. The CastTy data constructor (in "GHC.Core.TyCo.Rep") has the
--- invariant that another CastTy is not inside. See the
--- data constructor for a full description of this invariant.
--- Since CastTy cannot be nested, the result of discardCast
--- cannot be a CastTy.
-discardCast :: Type -> Type
-discardCast (CastTy ty _) = ASSERT(not (isCastTy ty)) ty
-  where
-  isCastTy CastTy{} = True
-  isCastTy _        = False
-discardCast ty            = ty
-
 
 {-
 --------------------------------------------------------------------
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 0d1bc6cceb..9ee420d4ca 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -46,7 +46,8 @@ module GHC.Tc.Gen.HsType (
         tcNamedWildCardBinders,
         tcHsLiftedType,   tcHsOpenType,
         tcHsLiftedTypeNC, tcHsOpenTypeNC,
-        tcInferLHsType, tcInferLHsTypeUnsaturated, tcCheckLHsType,
+        tcInferLHsTypeKind, tcInferLHsType, tcInferLHsTypeUnsaturated,
+        tcCheckLHsType,
         tcHsMbContext, tcHsContext, tcLHsPredType,
         failIfEmitsConstraints,
         solveEqualities, -- useful re-export
@@ -77,6 +78,7 @@ import GHC.Tc.Types.Origin
 import GHC.Core.Predicate
 import GHC.Tc.Types.Constraint
 import GHC.Tc.Utils.Env
+import GHC.Tc.Utils.Instantiate( tcInstInvisibleTyBinders )
 import GHC.Tc.Utils.TcMType
 import GHC.Tc.Validity
 import GHC.Tc.Utils.Unify
@@ -87,7 +89,7 @@ import GHC.Core.TyCo.Rep
 import GHC.Core.TyCo.Ppr
 import GHC.Tc.Errors      ( reportAllUnsolved )
 import GHC.Tc.Utils.TcType
-import GHC.Tc.Utils.Instantiate ( tcInstInvisibleTyBinders, tcInstInvisibleTyBinder )
+import GHC.Tc.Utils.Instantiate ( tcInstInvisibleTyBindersN, tcInstInvisibleTyBinder )
 import GHC.Core.Type
 import GHC.Builtin.Types.Prim
 import GHC.Types.Name.Env
@@ -617,12 +619,11 @@ tcHsOpenType, tcHsLiftedType,
   tcHsOpenTypeNC, tcHsLiftedTypeNC :: LHsType GhcRn -> TcM TcType
 -- Used for type signatures
 -- Do not do validity checking
-tcHsOpenType ty   = addTypeCtxt ty $ tcHsOpenTypeNC ty
-tcHsLiftedType ty = addTypeCtxt ty $ tcHsLiftedTypeNC ty
+tcHsOpenType   hs_ty = addTypeCtxt hs_ty $ tcHsOpenTypeNC hs_ty
+tcHsLiftedType hs_ty = addTypeCtxt hs_ty $ tcHsLiftedTypeNC hs_ty
 
-tcHsOpenTypeNC   ty = do { ek <- newOpenTypeKind
-                         ; tcLHsType ty ek }
-tcHsLiftedTypeNC ty = tcLHsType ty liftedTypeKind
+tcHsOpenTypeNC   hs_ty = do { ek <- newOpenTypeKind; tcLHsType hs_ty ek }
+tcHsLiftedTypeNC hs_ty = tcLHsType hs_ty liftedTypeKind
 
 -- Like tcHsType, but takes an expected kind
 tcCheckLHsType :: LHsType GhcRn -> ContextKind -> TcM TcType
@@ -632,15 +633,24 @@ tcCheckLHsType hs_ty exp_kind
        ; tcLHsType hs_ty ek }
 
 tcInferLHsType :: LHsType GhcRn -> TcM TcType
--- Called from outside: set the context
 tcInferLHsType hs_ty
-  = addTypeCtxt hs_ty $
-    do { (ty, _kind) <- tc_infer_lhs_type (mkMode TypeLevel) hs_ty
+  = do { (ty,_kind) <- tcInferLHsTypeKind hs_ty
        ; return ty }
 
+tcInferLHsTypeKind :: LHsType GhcRn -> TcM (TcType, TcKind)
+-- Called from outside: set the context
+-- Eagerly instantiate any trailing invisible binders
+tcInferLHsTypeKind lhs_ty@(L loc hs_ty)
+  = addTypeCtxt lhs_ty $
+    setSrcSpan loc     $  -- Cover the tcInstInvisibleTyBinders
+    do { (res_ty, res_kind) <- tc_infer_hs_type (mkMode TypeLevel) hs_ty
+       ; tcInstInvisibleTyBinders res_ty res_kind }
+  -- See Note [Do not always instantiate eagerly in types]
+
 -- Used to check the argument of GHCi :kind
 -- Allow and report wildcards, e.g. :kind T _
 -- Do not saturate family applications: see Note [Dealing with :kind]
+-- Does not instantiate eagerly; See Note [Do not always instantiate eagerly in types]
 tcInferLHsTypeUnsaturated :: LHsType GhcRn -> TcM (TcType, TcKind)
 tcInferLHsTypeUnsaturated hs_ty
   = addTypeCtxt hs_ty $
@@ -674,6 +684,19 @@ to switch off saturation.
 So tcInferLHsTypeUnsaturated does a little special case for top level
 applications.  Actually the common case is a bare variable, as above.
 
+Note [Do not always instantiate eagerly in types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Terms are eagerly instantiated. This means that if you say
+
+  x = id
+
+then `id` gets instantiated to have type alpha -> alpha. The variable
+alpha is then unconstrained and regeneralized. But we cannot do this
+in types, as we have no type-level lambda. So, when we are sure
+that we will not want to regeneralize later -- because we are done
+checking a type, for example -- we can instantiate. But we do not
+instantiate at variables, nor do we in tcInferLHsTypeUnsaturated,
+which is used by :kind in GHCi.
 
 ************************************************************************
 *                                                                      *
@@ -1648,14 +1671,14 @@ saturateFamApp :: TcType -> TcKind -> TcM (TcType, TcKind)
 --     tcTypeKind ty = kind
 --
 -- If 'ty' is an unsaturated family application with trailing
--- invisible arguments, instanttiate them.
+-- invisible arguments, instantiate them.
 -- See Note [saturateFamApp]
 
 saturateFamApp ty kind
   | Just (tc, args) <- tcSplitTyConApp_maybe ty
   , mustBeSaturated tc
   , let n_to_inst = tyConArity tc - length args
-  = do { (extra_args, ki') <- tcInstInvisibleTyBinders n_to_inst kind
+  = do { (extra_args, ki') <- tcInstInvisibleTyBindersN n_to_inst kind
        ; return (ty `mkTcAppTys` extra_args, ki') }
   | otherwise
   = return (ty, kind)
@@ -1712,7 +1735,7 @@ checkExpectedKind :: HasDebugCallStack
 checkExpectedKind hs_ty ty act_kind exp_kind
   = do { traceTc "checkExpectedKind" (ppr ty $$ ppr act_kind)
 
-       ; (new_args, act_kind') <- tcInstInvisibleTyBinders n_to_inst act_kind
+       ; (new_args, act_kind') <- tcInstInvisibleTyBindersN n_to_inst act_kind
 
        ; let origin = TypeEqOrigin { uo_actual   = act_kind'
                                    , uo_expected = exp_kind
@@ -1763,6 +1786,7 @@ tc_lhs_pred mode pred = tc_lhs_type mode pred constraintKind
 tcTyVar :: TcTyMode -> Name -> TcM (TcType, TcKind)
 -- See Note [Type checking recursive type and class declarations]
 -- in GHC.Tc.TyCl
+-- This does not instantiate. See Note [Do not always instantiate eagerly in types]
 tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
   = do { traceTc "lk1" (ppr name)
        ; thing <- tcLookup name
@@ -3293,12 +3317,18 @@ data DataSort
 -- 2. @k@ (where @k@ is a bare kind variable; see #12369)
 --
 -- See also Note [Datatype return kinds] in "GHC.Tc.TyCl"
-checkDataKindSig :: DataSort -> Kind -> TcM ()
-checkDataKindSig data_sort kind = do
-  dflags <- getDynFlags
-  traceTc "checkDataKindSig" (ppr kind)
-  checkTc (is_TYPE_or_Type dflags || is_kind_var) (err_msg dflags)
+checkDataKindSig :: DataSort -> Kind  -- any arguments in the kind are stripped off
+                 -> TcM ()
+checkDataKindSig data_sort kind
+  = do { dflags <- getDynFlags
+       ; traceTc "checkDataKindSig" (ppr kind)
+       ; checkTc (is_TYPE_or_Type dflags || is_kind_var)
+                 (err_msg dflags) }
   where
+    res_kind = snd (tcSplitPiTys kind)
+       -- Look for the result kind after
+       -- peeling off any foralls and arrows
+
     pp_dec :: SDoc
     pp_dec = text $
       case data_sort of
@@ -3335,16 +3365,19 @@ checkDataKindSig data_sort kind = do
            -- have return kind `TYPE r` unconditionally (#16827).
 
     is_TYPE :: Bool
-    is_TYPE = tcIsRuntimeTypeKind kind
+    is_TYPE = tcIsRuntimeTypeKind res_kind
+
+    is_Type :: Bool
+    is_Type = tcIsLiftedTypeKind res_kind
 
     is_TYPE_or_Type :: DynFlags -> Bool
     is_TYPE_or_Type dflags | tYPE_ok dflags = is_TYPE
-                           | otherwise      = tcIsLiftedTypeKind kind
+                           | otherwise      = is_Type
 
     -- In the particular case of a data family, permit a return kind of the
     -- form `:: k` (where `k` is a bare kind variable).
     is_kind_var :: Bool
-    is_kind_var | is_data_family = isJust (tcGetCastedTyVar_maybe kind)
+    is_kind_var | is_data_family = isJust (tcGetCastedTyVar_maybe res_kind)
                 | otherwise      = False
 
     err_msg :: DynFlags -> SDoc
@@ -3353,7 +3386,7 @@ checkDataKindSig data_sort kind = do
                    text "has non-" <>
                    (if tYPE_ok dflags then text "TYPE" else ppr liftedTypeKind)
                  , (if is_data_family then text "and non-variable" else empty) <+>
-                   text "return kind" <+> quotes (ppr kind) ])
+                   text "return kind" <+> quotes (ppr res_kind) ])
           , if not (tYPE_ok dflags) && is_TYPE && is_newtype &&
                not (xopt LangExt.UnliftedNewtypes dflags)
             then text "Perhaps you intended to use UnliftedNewtypes"
diff --git a/compiler/GHC/Tc/Instance/Family.hs b/compiler/GHC/Tc/Instance/Family.hs
index 698cfa682e..9be5c4675b 100644
--- a/compiler/GHC/Tc/Instance/Family.hs
+++ b/compiler/GHC/Tc/Instance/Family.hs
@@ -18,7 +18,6 @@ import GHC.Driver.Types
 import GHC.Core.FamInstEnv
 import GHC.Core.InstEnv( roughMatchTcs )
 import GHC.Core.Coercion
-import GHC.Core.Lint
 import GHC.Tc.Types.Evidence
 import GHC.Iface.Load
 import GHC.Tc.Utils.Monad
@@ -162,34 +161,13 @@ addressed yet.
 newFamInst :: FamFlavor -> CoAxiom Unbranched -> TcM FamInst
 -- Freshen the type variables of the FamInst branches
 newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc })
-  = ASSERT2( tyCoVarsOfTypes lhs `subVarSet` tcv_set, text "lhs" <+> pp_ax )
-    ASSERT2( lhs_kind `eqType` rhs_kind, text "kind" <+> pp_ax $$ ppr lhs_kind $$ ppr rhs_kind )
-    -- We used to have an assertion that the tyvars of the RHS were bound
-    -- by tcv_set, but in error situations like  F Int = a that isn't
-    -- true; a later check in checkValidFamInst rejects it
-    do { (subst, tvs') <- freshenTyVarBndrs tvs
+  = do {
+         -- Freshen the type variables
+         (subst, tvs') <- freshenTyVarBndrs tvs
        ; (subst, cvs') <- freshenCoVarBndrsX subst cvs
-       ; dflags <- getDynFlags
        ; let lhs'     = substTys subst lhs
              rhs'     = substTy  subst rhs
-             tcvs'    = tvs' ++ cvs'
-       ; ifErrsM (return ()) $ -- Don't lint when there are errors, because
-                               -- errors might mean TcTyCons.
-                               -- See Note [Recover from validity error] in GHC.Tc.TyCl
-         when (gopt Opt_DoCoreLinting dflags) $
-           -- Check that the types involved in this instance are well formed.
-           -- Do /not/ expand type synonyms, for the reasons discussed in
-           -- Note [Linting type synonym applications].
-           case lintTypes dflags tcvs' (rhs':lhs') of
-             Nothing       -> pure ()
-             Just fail_msg -> pprPanic "Core Lint error in newFamInst" $
-                              vcat [ fail_msg
-                                   , ppr fam_tc
-                                   , ppr subst
-                                   , ppr tvs'
-                                   , ppr cvs'
-                                   , ppr lhs'
-                                   , ppr rhs' ]
+
        ; return (FamInst { fi_fam      = tyConName fam_tc
                          , fi_flavor   = flavor
                          , fi_tcs      = roughMatchTcs lhs
@@ -199,10 +177,6 @@ newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc })
                          , fi_rhs      = rhs'
                          , fi_axiom    = axiom }) }
   where
-    lhs_kind = tcTypeKind (mkTyConApp fam_tc lhs)
-    rhs_kind = tcTypeKind rhs
-    tcv_set  = mkVarSet (tvs ++ cvs)
-    pp_ax    = pprCoAxiom axiom
     CoAxBranch { cab_tvs = tvs
                , cab_cvs = cvs
                , cab_lhs = lhs
diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs
index 5ef192befe..0145c6c776 100644
--- a/compiler/GHC/Tc/Module.hs
+++ b/compiler/GHC/Tc/Module.hs
@@ -268,6 +268,14 @@ tcRnModuleTcRnM hsc_env mod_sum
                             then tcRnHsBootDecls hsc_src local_decls
                             else {-# SCC "tcRnSrcDecls" #-}
                                  tcRnSrcDecls explicit_mod_hdr local_decls export_ies
+
+               ; whenM (goptM Opt_DoCoreLinting) $
+                 do { let (warns, errs) = lintGblEnv (hsc_dflags hsc_env) tcg_env
+                    ; mapBagM_ (addWarn NoReason) warns
+                    ; mapBagM_ addErr errs
+                    ; failIfErrsM }  -- if we have a lint error, we're only
+                                     -- going to get in deeper trouble by proceeding
+
                ; setGblEnv tcg_env
                  $ do { -- Process the export list
                         traceRn "rn4a: before exports" empty
@@ -2896,7 +2904,7 @@ pprTcGblEnv (TcGblEnv { tcg_type_env  = type_env,
                 pprUFM (imp_dep_mods imports) (ppr . sort)
          , text "Dependent packages:" <+>
                 ppr (S.toList $ imp_dep_pkgs imports)]
-  where         -- The use of sort is just to reduce unnecessary
+                -- The use of sort is just to reduce unnecessary
                 -- wobbling in testsuite output
 
 ppr_rules :: [LRuleDecl GhcTc] -> SDoc
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index efdb1bdfd0..013892ee6e 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -1791,6 +1791,272 @@ and take the wired-in information.  That avoids complications.
 e.g. the need to make the data constructor worker name for
      a constraint tuple match the wired-in one
 
+Note [Datatype return kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+There are several poorly lit corners around datatype/newtype return kinds.
+This Note explains these.  We cover data/newtype families and instances
+in Note [Data family/instance return kinds].
+
+data    T a :: <kind> where ...   -- See Point DT4
+newtype T a :: <kind> where ...   -- See Point DT5
+
+DT1 Where this applies: Only GADT syntax for data/newtype/instance declarations
+    can have declared return kinds. This Note does not apply to Haskell98
+    syntax.
+
+DT2 Where these kinds come from: The return kind is part of the TyCon kind, gotten either
+     by checkInitialKind (standalone kind signature / CUSK) or
+     inferInitialKind. It is extracted by bindTyClTyVars in tcTyClDecl1. It is
+     then passed to tcDataDefn.
+
+DT3 Eta-expansion: Any forall-bound variables and function arguments in a result kind
+    become parameters to the type. That is, when we say
+
+     data T a :: Type -> Type where ...
+
+    we really mean for T to have two parameters. The second parameter
+    is produced by processing the return kind in etaExpandAlgTyCon,
+    called in tcDataDefn.
+
+    See also Note [TyConBinders for the result kind signatures of a data type]
+    in GHC.Tc.Gen.HsType.
+
+DT4 Datatype return kind restriction: A data type return kind must end
+    in a type that, after type-synonym expansion, yields `TYPE LiftedRep`. By
+    "end in", we mean we strip any foralls and function arguments off before
+    checking.
+
+    Examples:
+      data T1 :: Type                          -- good
+      data T2 :: Bool -> Type                  -- good
+      data T3 :: Bool -> forall k. Type        -- strange, but still accepted
+      data T4 :: forall k. k -> Type           -- good
+      data T5 :: Bool                          -- bad
+      data T6 :: Type -> Bool                  -- bad
+
+    Exactly the same applies to data instance (but not data family)
+    declarations.  Examples
+      data instance D1 :: Type                 -- good
+      data instance D2 :: Bool -> Type         -- good
+
+    We can "look through" type synonyms
+      type Star = Type
+      data T7 :: Bool -> Star                  -- good (synonym expansion ok)
+      type Arrow = (->)
+      data T8 :: Arrow Bool Type               -- good (ditto)
+
+    But we specifically do *not* do type family reduction here.
+      type family ARROW where
+        ARROW = (->)
+      data T9 :: ARROW Bool Type               -- bad
+
+      type family F a where
+        F Int  = Bool
+        F Bool = Type
+      data T10 :: Bool -> F Bool               -- bad
+
+    The /principle/ here is that in the TyCon for a data type or data instance,
+    we must be able to lay out all the type-variable binders, one by one, until
+    we reach (TYPE xx).  There is no place for a cast here.  We could add one,
+    but let's not!
+
+    This check is done in checkDataKindSig. For data declarations, this
+    call is in tcDataDefn; for data instances, this call is in tcDataFamInstDecl.
+
+DT5 Newtype return kind restriction.
+    If -XUnliftedNewtypes is not on, then newtypes are treated just
+    like datatypes --- see (4) above.
+
+    If -XUnliftedNewtypes is on, then a newtype return kind must end in
+    TYPE xyz, for some xyz (after type synonym expansion). The "xyz"
+    may include type families, but the TYPE part must be visible
+    /without/ expanding type families (only synonyms).
+
+    This kind is unified with the kind of the representation type (the
+    type of the one argument to the one constructor). See also steps
+    (2) and (3) of Note [Implementation of UnliftedNewtypes].
+
+    The checks are done in the same places as for datatypes.
+    Examples (assume -XUnliftedNewtypes):
+
+      newtype N1 :: Type                       -- good
+      newtype N2 :: Bool -> Type               -- good
+      newtype N3 :: forall r. Bool -> TYPE r   -- good
+
+      type family F (t :: Type) :: RuntimeRep
+      newtype N4 :: forall t -> TYPE (F t)     -- good
+
+      type family STAR where
+        STAR = Type
+      newtype N5 :: Bool -> STAR               -- bad
+
+Note [Data family/instance return kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Within this note, understand "instance" to mean data or newtype
+instance, and understand "family" to mean data family. No type
+families or classes here. Some examples:
+
+data family T a :: <kind>          -- See Point DF56
+
+data    instance T [a] :: <kind> where ...   -- See Point DF2
+newtype instance T [a] :: <kind> where ...   -- See Point DF2
+
+Here is the Plan for Data Families:
+
+DF0 Where these kinds come from:
+
+    Families: The return kind is either written in a standalone signature
+     or extracted from a family declaration in getInitialKind.
+     If a family declaration is missing a result kind, it is assumed to be
+     Type. This assumption is in getInitialKind for CUSKs or
+     get_fam_decl_initial_kind for non-signature & non-CUSK cases.
+
+   Instances: The data family already has a known kind. The return kind
+     of an instance is then calculated by applying the data family tycon
+     to the patterns provided, as computed by the typeKind lhs_ty in the
+     end of tcDataFamInstHeader. In the case of an instance written in GADT
+     syntax, there are potentially *two* return kinds: the one computed from
+     applying the data family tycon to the patterns, and the one given by
+     the user. This second kind is checked by the tc_kind_sig function within
+     tcDataFamInstHeader. See also DF3, below.
+
+DF1 In a data/newtype instance, we treat the kind of the /data family/,
+    once instantiated, as the "master kind" for the representation
+    TyCon.  For example:
+        data family T1 :: Type -> Type -> Type
+        data instance T1 Int :: F Bool -> Type where ...
+    The "master kind" for the representation TyCon R:T1Int comes
+    from T1, not from the signature on the data instance.  It is as
+    if we declared
+        data R:T1Int :: Type -> Type where ...
+     See Note [Liberalising data family return kinds] for an alternative
+     plan.  But this current plan is simple, and ensures that all instances
+     are simple instantiations of the master, without strange casts.
+
+     An example with non-trivial instantiation:
+        data family T2 :: forall k. Type -> k
+        data instance T2 :: Type -> Type -> Type where ...
+     Here 'k' gets instantiated with (Type -> Type), driven by
+     the signature on the 'data instance'. (See also DT3 of
+     Note [Datatype return kinds] about eta-expansion, which applies here,
+     too; see tcDataFamInstDecl's call of etaExpandAlgTyCon.)
+
+     A newtype example:
+
+       data Color = Red | Blue
+       type family Interpret (x :: Color) :: RuntimeRep where
+         Interpret 'Red = 'IntRep
+         Interpret 'Blue = 'WordRep
+       data family Foo (x :: Color) :: TYPE (Interpret x)
+       newtype instance Foo 'Red :: TYPE IntRep where
+         FooRedC :: Int# -> Foo 'Red
+
+    Here we get that Foo 'Red :: TYPE (Interpret Red), and our
+    representation newtype looks like
+         newtype R:FooRed :: TYPE (Interpret Red) where
+            FooRedC :: Int# -> R:FooRed
+    Remember: the master kind comes from the /family/ tycon.
+
+DF2 /After/ this instantiation, the return kind of the master kind
+    must obey the usual rules for data/newtype return kinds (DT4, DT5)
+    of Note [Datatype return kinds].  Examples:
+        data family T3 k :: k
+        data instance T3 Type where ...          -- OK
+        data instance T3 (Type->Type) where ...  -- OK
+        data instance T3 (F Int) where ...       -- Not OK
+
+DF3 Any kind signatures on the data/newtype instance are checked for
+    equality with the master kind (and hence may guide instantiation)
+    but are otherwise ignored. So in the T1 example above, we check
+    that (F Int ~ Type) by unification; but otherwise ignore the
+    user-supplied signature from the /family/ not the /instance/.
+
+    We must be sure to instantiate any trailing invisible binders
+    before doing this unification.  See the call to tcInstInvisibleBinders
+    in tcDataFamInstHeader. For example:
+       data family D :: forall k. k
+       data instance D :: Type               -- forall k. k   <:  Type
+       data instance D :: Type -> Type       -- forall k. k   <:  Type -> Type
+         -- NB: these do not overlap
+    we must instantiate D before unifying with the signature in the
+    data instance declaration
+
+DF4 We also (redundantly) check that any user-specified return kind
+    signature in the data instance also obeys DT4/DT5.  For example we
+    reject
+        data family T1 :: Type -> Type -> Type
+        data instance T1 Int :: Type -> F Int
+    even if (F Int ~ Type).  We could omit this check, because we
+    use the master kind; but it seems more uniform to check it, again
+    with checkDataKindSig.
+
+DF5 Data /family/ return kind restrictions. Consider
+       data family D8 a :: F a
+    where F is a type family.  No data/newtype instance can instantiate
+    this so that it obeys the rules of DT4 or DT5.  So GHC proactively
+    rejects the data /family/ declaration if it can never satisfy (DT4)/(DT5).
+    Remember that a data family supports both data and newtype instances.
+
+    More precisely, the return kind of a data family must be either
+        * TYPE xyz (for some type xyz) or
+        * a kind variable
+    Only in these cases can a data/newtype instance possibly satisfy (DT4)/(DT5).
+    This is checked by the call to checkDataKindSig in tcFamDecl1.  Examples:
+
+      data family D1 :: Type              -- good
+      data family D2 :: Bool -> Type      -- good
+      data family D3 k :: k               -- good
+      data family D4 :: forall k -> k     -- good
+      data family D5 :: forall k. k -> k  -- good
+      data family D6 :: forall r. TYPE r  -- good
+      data family D7 :: Bool -> STAR      -- bad (see STAR from point 5)
+
+DF6 Two return kinds for instances: If an instance has two return kinds,
+    one from the family declaration and one from the instance declaration
+    (see point DF3 above), they are unified. More accurately, we make sure
+    that the kind of the applied data family is a subkind of the user-written
+    kind. GHC.Tc.Gen.HsType.checkExpectedKind normally does this check for types, but
+    that's overkill for our needs here. Instead, we just instantiate any
+    invisible binders in the (instantiated) kind of the data family
+    (called lhs_kind in tcDataFamInstHeader) with tcInstInvisibleTyBinders
+    and then unify the resulting kind with the kind written by the user.
+    This unification naturally produces a coercion, which we can drop, as
+    the kind annotation on the instance is redundant (except perhaps for
+    effects of unification).
+
+    This all is Wrinkle (3) in Note [Implementation of UnliftedNewtypes].
+
+Note [Liberalising data family return kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Could we allow this?
+   type family F a where { F Int = Type }
+   data family T a :: F a
+   data instance T Int where
+      MkT :: T Int
+
+In the 'data instance', T Int :: F Int, and F Int = Type, so all seems
+well.  But there are lots of complications:
+
+* The representation constructor R:TInt presumably has kind Type.
+  So the axiom connecting the two would have to look like
+       axTInt :: T Int ~ R:TInt |> sym axFInt
+  and that doesn't match expectation in DataFamInstTyCon
+  in AlgTyConFlav
+
+* The wrapper can't have type
+     $WMkT :: Int -> T Int
+  because T Int has the wrong kind.  It would have to be
+     $WMkT :: Int -> (T Int) |> axFInt
+
+* The code for $WMkT would also be more complicated, needing
+  two coherence coercions. Try it!
+
+* Code for pattern matching would be complicated in an
+  exactly dual way.
+
+So yes, we could allow this, but we currently do not. That's
+why we have DF2 in Note [Data family/instance return kinds].
+
 Note [Implementation of UnliftedNewtypes]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Expected behavior of UnliftedNewtypes:
@@ -1867,11 +2133,12 @@ Wrinkle: Consider (#17021, typecheck/should_fail/T17021)
     newtype T :: TYPE (Id LiftedRep) where
       MkT :: Int -> T
 
-  In the type of MkT, we must end with (Int |> TYPE (sym axId)) -> T, never Int -> (T |>
-  TYPE axId); otherwise, the result type of the constructor wouldn't match the
-  datatype. However, type-checking the HsType T might reasonably result in
-  (T |> hole). We thus must ensure that this cast is dropped, forcing the
-  type-checker to add one to the Int instead.
+  In the type of MkT, we must end with (Int |> TYPE (sym axId)) -> T,
+  never Int -> (T |> TYPE axId); otherwise, the result type of the
+  constructor wouldn't match the datatype. However, type-checking the
+  HsType T might reasonably result in (T |> hole). We thus must ensure
+  that this cast is dropped, forcing the type-checker to add one to
+  the Int instead.
 
   Why is it always safe to drop the cast? This result type is type-checked by
   tcHsOpenType, so its kind definitely looks like TYPE r, for some r. It is
@@ -1883,7 +2150,7 @@ Wrinkle: Consider (#17021, typecheck/should_fail/T17021)
 Note that this is possible in the H98 case only for a data family, because
 the H98 syntax doesn't permit a kind signature on the newtype itself.
 
-There are also some changes for deailng with families:
+There are also some changes for dealing with families:
 
 1. In tcFamDecl1, we suppress a tcIsLiftedTypeKind check if
    UnliftedNewtypes is on. This allows us to write things like:
@@ -1905,7 +2172,7 @@ There are also some changes for deailng with families:
    we use that kind signature.
 
 3. A data family and its newtype instance may be declared with slightly
-   different kinds. See point 7 in Note [Datatype return kinds].
+   different kinds. See point DF6 in Note [Data family/instance return kinds]
 
 There's also a change in the renamer:
 
@@ -2292,187 +2559,6 @@ Since the LHS of an associated type family default is always just variables,
 it won't contain any tycons. Accordingly, the patterns used in the substitution
 won't actually be knot-tied, even though we're in the knot. This is too
 delicate for my taste, but it works.
-
-Note [Datatype return kinds]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-There are several poorly lit corners around datatype/newtype return kinds.
-This Note explains these. Within this note, always understand "instance"
-to mean data or newtype instance, and understand "family" to mean data
-family. No type families or classes here. Some examples:
-
-data    T a :: <kind> where ...   -- See Point 4
-newtype T a :: <kind> where ...   -- See Point 5
-
-data family T a :: <kind>          -- See Point 6
-
-data    instance T [a] :: <kind> where ...   -- See Point 4
-newtype instance T [a] :: <kind> where ...   -- See Point 5
-
-1. Where this applies: Only GADT syntax for data/newtype/instance declarations
-   can have declared return kinds. This Note does not apply to Haskell98
-   syntax.
-
-2. Where these kinds come from: Return kinds are processed through several
-   different code paths:
-
-   Data/newtypes: The return kind is part of the TyCon kind, gotten either
-     by checkInitialKind (standalone kind signature / CUSK) or
-     inferInitialKind. It is extracted by bindTyClTyVars in tcTyClDecl1. It is
-     then passed to tcDataDefn.
-
-   Families: The return kind is either written in a standalone signature
-     or extracted from a family declaration in getInitialKind.
-     If a family declaration is missing a result kind, it is assumed to be
-     Type. This assumption is in getInitialKind for CUSKs or
-     get_fam_decl_initial_kind for non-signature & non-CUSK cases.
-
-   Instances: The data family already has a known kind. The return kind
-     of an instance is then calculated by applying the data family tycon
-     to the patterns provided, as computed by the typeKind lhs_ty in the
-     end of tcDataFamInstHeader. In the case of an instance written in GADT
-     syntax, there are potentially *two* return kinds: the one computed from
-     applying the data family tycon to the patterns, and the one given by
-     the user. This second kind is checked by the tc_kind_sig function within
-     tcDataFamInstHeader.
-
-3. Eta-expansion: Any forall-bound variables and function arguments in a result kind
-   become parameters to the type. That is, when we say
-
-     data T a :: Type -> Type where ...
-
-   we really mean for T to have two parameters. The second parameter
-   is produced by processing the return kind in etaExpandAlgTyCon,
-   called in tcDataDefn for data/newtypes and in tcDataFamInstDecl
-   for instances. This is true for data families as well, though their
-   arity only matters for pretty-printing.
-
-   See also Note [TyConBinders for the result kind signatures of a data type]
-   in GHC.Tc.Gen.HsType.
-
-4. Datatype return kind restriction: A data/data-instance return kind must end
-   in a type that, after type-synonym expansion, yields `TYPE LiftedRep`. By
-   "end in", we mean we strip any foralls and function arguments off before
-   checking: this remaining part of the type is returned from etaExpandAlgTyCon.
-
-   Examples:
-     data T1 :: Type                          -- good
-     data T2 :: Bool -> Type                  -- good
-     data T3 :: Bool -> forall k. Type        -- strange, but still accepted
-     data T4 :: forall k. k -> Type           -- good
-     data T5 :: Bool                          -- bad
-     data T6 :: Type -> Bool                  -- bad
-
-   Exactly the same applies to data instance (but not data family)
-   declarations.  Examples
-     data instance D1 :: Type                 -- good
-     data instance D2 :: Boool -> Type        -- good
-
-   We can "look through" type synonyms
-     type Star = Type
-     data T7 :: Bool -> Star                  -- good (synonym expansion ok)
-     type Arrow = (->)
-     data T8 :: Arrow Bool Type               -- good (ditto)
-
-   But we specifically do *not* do type family reduction here.
-     type family ARROW where
-       ARROW = (->)
-     data T9 :: ARROW Bool Type               -- bad
-
-     type family F a where
-       F Int  = Bool
-       F Bool = Type
-     data T10 :: Bool -> F Bool               -- bad
-
-   The /principle/ here is that in the TyCon for a data type or data instance,
-   we must be able to lay out all the type-variable binders, one by one, until
-   we reach (TYPE xx).  There is no place for a cast here.  We could add one,
-   but let's not!
-
-   This check is done in checkDataKindSig. For data declarations, this
-   call is in tcDataDefn; for data instances, this call is in tcDataFamInstDecl.
-
-4a  Because data instances in GADT syntax can have two return kinds (see
-    point (2) above), we must check both return kinds. The user-written return
-    kind is checked by the call to checkDataKindSig in tcDataFamInstDecl. Examples:
-
-     data family D (a :: Nat) :: k     -- good (see Point 6)
-
-     data instance D 1 :: Type         -- good
-     data instance D 2 :: F Bool       -- bad
-
-5. Newtype return kind restriction: If -XUnliftedNewtypes is on, then
-   a newtype/newtype-instance return kind must end in TYPE xyz, for some
-   xyz (after type synonym expansion). The "xyz" may include type families,
-   but the TYPE part must be visible with expanding type families (only synonyms).
-   This kind is unified with the kind of the representation type (the type
-   of the one argument to the one constructor). See also steps (2) and (3)
-   of Note [Implementation of UnliftedNewtypes].
-
-   If -XUnliftedNewtypes is not on, then newtypes are treated just like datatypes.
-
-   The checks are done in the same places as for datatypes.
-   Examples (assume -XUnliftedNewtypes):
-
-     newtype N1 :: Type                       -- good
-     newtype N2 :: Bool -> Type               -- good
-     newtype N3 :: forall r. Bool -> TYPE r   -- good
-
-     type family F (t :: Type) :: RuntimeRep
-     newtype N4 :: forall t -> TYPE (F t)     -- good
-
-     type family STAR where
-       STAR = Type
-     newtype N5 :: Bool -> STAR               -- bad
-
-6. Family return kind restrictions: The return kind of a data family must
-   be either TYPE xyz (for some xyz) or a kind variable. The idea is that
-   instances may specialise the kind variable to fit one of the restrictions
-   above. This is checked by the call to checkDataKindSig in tcFamDecl1.
-   Examples:
-
-     data family D1 :: Type              -- good
-     data family D2 :: Bool -> Type      -- good
-     data family D3 k :: k               -- good
-     data family D4 :: forall k -> k     -- good
-     data family D5 :: forall k. k -> k  -- good
-     data family D6 :: forall r. TYPE r  -- good
-     data family D7 :: Bool -> STAR      -- bad (see STAR from point 5)
-
-7. Two return kinds for instances: If an instance has two return kinds,
-   one from the family declaration and one from the instance declaration
-   (see point (2) above), they are unified. More accurately, we make sure
-   that the kind of the applied data family is a subkind of the user-written
-   kind. GHC.Tc.Gen.HsType.checkExpectedKind normally does this check for types, but
-   that's overkill for our needs here. Instead, we just instantiate any
-   invisible binders in the (instantiated) kind of the data family
-   (called lhs_kind in tcDataFamInstHeader) with tcInstInvisibleTyBinders
-   and then unify the resulting kind with the kind written by the user.
-   This unification naturally produces a coercion, which we can drop, as
-   the kind annotation on the instance is redundant (except perhaps for
-   effects of unification).
-
-   Example:
-
-      data Color = Red | Blue
-      type family Interpret (x :: Color) :: RuntimeRep where
-        Interpret 'Red = 'IntRep
-        Interpret 'Blue = 'WordRep
-      data family Foo (x :: Color) :: TYPE (Interpret x)
-      newtype instance Foo 'Red :: TYPE IntRep where
-        FooRedC :: Int# -> Foo 'Red
-
-   Here we get that Foo 'Red :: TYPE (Interpret Red) and we have to
-   unify the kind with TYPE IntRep.
-
-   Example requiring subkinding:
-
-      data family D :: forall k. k
-      data instance D :: Type               -- forall k. k   <:  Type
-      data instance D :: Type -> Type       -- forall k. k   <:  Type -> Type
-        -- NB: these do not overlap
-
-   This all is Wrinkle (3) in Note [Implementation of UnliftedNewtypes].
-
 -}
 
 {- *********************************************************************
@@ -2502,8 +2588,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
   -- When UnliftedNewtypes is enabled, we loosen this restriction
   -- on the return kind. See Note [Implementation of UnliftedNewtypes], wrinkle (1).
   -- See also Note [Datatype return kinds]
-  ; let (_, final_res_kind) = splitPiTys res_kind
-  ; checkDataKindSig DataFamilySort final_res_kind
+  ; checkDataKindSig DataFamilySort res_kind
   ; tc_rep_name <- newTyConRepName tc_name
   ; let inj   = Injective $ replicate (length binders) True
         tycon = mkFamilyTyCon tc_name binders
@@ -2798,7 +2883,7 @@ tcTyFamInstEqn fam_tc mb_clsinfo
                                       hs_pats hs_rhs_ty
        -- Don't print results they may be knot-tied
        -- (tcFamInstEqnGuts zonks to Type)
-       ; return (mkCoAxBranch qtvs [] [] fam_tc pats rhs_ty
+       ; return (mkCoAxBranch qtvs [] [] pats rhs_ty
                               (map (const Nominal) qtvs)
                               loc) }
 
@@ -3170,8 +3255,8 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data
        }
 
 tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data
-  -- NB: don't use res_kind here, as it's ill-scoped. Instead, we get
-  -- the res_kind by typechecking the result type.
+  -- NB: don't use res_kind here, as it's ill-scoped. Instead,
+  -- we get the res_kind by typechecking the result type.
           (ConDeclGADT { con_g_ext = implicit_tkv_nms
                        , con_names = names
                        , con_qvars = explicit_tkv_nms
@@ -3188,16 +3273,12 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data
               bindImplicitTKBndrs_Skol implicit_tkv_nms $
               bindExplicitTKBndrs_Skol explicit_tkv_nms $
               do { ctxt <- tcHsMbContext cxt
-                 ; casted_res_ty <- tcHsOpenType hs_res_ty
-                 ; res_ty <- if not debugIsOn then return $ discardCast casted_res_ty
-                             else case splitCastTy_maybe casted_res_ty of
-                               Just (ty, _) -> do unlifted_nts <- xoptM LangExt.UnliftedNewtypes
-                                                  MASSERT( unlifted_nts )
-                                                  MASSERT( new_or_data == NewType )
-                                                  return ty
-                               _ -> return casted_res_ty
+                 ; (res_ty, res_kind) <- tcInferLHsTypeKind hs_res_ty
+                         -- See Note [GADT return kinds]
+
                    -- See Note [Datatype return kinds]
-                 ; let exp_kind = getArgExpKind new_or_data (typeKind res_ty)
+                 ; let exp_kind = getArgExpKind new_or_data res_kind
+
                  ; btys <- tcConArgs exp_kind hs_args
                  ; let (arg_tys, stricts) = unzip btys
                  ; field_lbls <- lookupConstructorFields name
@@ -3252,6 +3333,20 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data
        ; mapM buildOneDataCon names
        }
 
+{- Note [GADT return kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+   type family Star where Star = Type
+   data T :: Type where
+      MkT :: Int -> T
+
+If, for some stupid reason, tcInferLHsTypeKind on the return type of
+MkT returned (T |> ax, Star), then the return-type check in
+checkValidDataCon would reject the decl (although of course there is
+nothing wrong with it).  We are implicitly requiring tha
+tcInferLHsTypeKind doesn't any gratuitous top-level casts.
+-}
+
 -- | Produce an "expected kind" for the arguments of a data/newtype.
 -- If the declaration is indeed for a newtype,
 -- then this expected kind will be the kind provided. Otherwise,
@@ -3924,11 +4019,16 @@ checkValidDataCon dflags existential_ok tc con
               , ppr orig_res_ty <+> dcolon <+> ppr (tcTypeKind orig_res_ty)])
 
 
-        ; checkTc (isJust (tcMatchTy res_ty_tmpl orig_res_ty))
+        ; checkTc (isJust (tcMatchTyKi res_ty_tmpl orig_res_ty))
                   (badDataConTyCon con res_ty_tmpl)
             -- Note that checkTc aborts if it finds an error. This is
             -- critical to avoid panicking when we call dataConDisplayType
             -- on an un-rejiggable datacon!
+            -- Also NB that we match the *kind* as well as the *type* (#18357)
+            -- However, if the kind is the only thing that doesn't match, the
+            -- error message is terrible.  E.g. test T18357b
+            --    type family Star where Star = Type
+            --    newtype T :: Type where MkT :: Int -> (T :: Star)
 
         ; traceTc "checkValidDataCon 2" (ppr data_con_display_type)
 
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index dc8aeb1962..fbcb2e0363 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -704,7 +704,6 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env
 
        -- Check the result kind; it may come from a user-written signature.
        -- See Note [Datatype return kinds] in GHC.Tc.TyCl point 4(a)
-       ; checkDataKindSig (DataInstanceSort new_or_data) final_res_kind
        ; let extra_pats  = map (mkTyVarTy . binderVar) extra_tcbs
              all_pats    = pats `chkAppend` extra_pats
              orig_res_ty = mkTyConApp fam_tc all_pats
@@ -713,10 +712,12 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env
        ; traceTc "tcDataFamInstDecl" $
          vcat [ text "Fam tycon:" <+> ppr fam_tc
               , text "Pats:" <+> ppr pats
-              , text "visibliities:" <+> ppr (tcbVisibilities fam_tc pats)
+              , text "visiblities:" <+> ppr (tcbVisibilities fam_tc pats)
               , text "all_pats:" <+> ppr all_pats
               , text "ty_binders" <+> ppr ty_binders
               , text "fam_tc_binders:" <+> ppr (tyConBinders fam_tc)
+              , text "res_kind:" <+> ppr res_kind
+              , text "final_res_kind:" <+> ppr final_res_kind
               , text "eta_pats" <+> ppr eta_pats
               , text "eta_tcbs" <+> ppr eta_tcbs ]
 
@@ -734,9 +735,9 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env
                      NewType  -> ASSERT( not (null data_cons) )
                                  mkNewTyConRhs rep_tc_name rec_rep_tc (head data_cons)
 
-              ; let axiom  = mkSingleCoAxiom Representational axiom_name
-                                 post_eta_qtvs eta_tvs [] fam_tc eta_pats
-                                 (mkTyConApp rep_tc (mkTyVarTys post_eta_qtvs))
+              ; let ax_rhs = mkTyConApp rep_tc (mkTyVarTys post_eta_qtvs)
+                    axiom  = mkSingleCoAxiom Representational axiom_name
+                                 post_eta_qtvs eta_tvs [] fam_tc eta_pats ax_rhs
                     parent = DataFamInstTyCon axiom fam_tc all_pats
 
                       -- NB: Use the full ty_binders from the pats. See bullet toward
@@ -851,13 +852,17 @@ tcDataFamInstHeader
 tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
                     hs_ctxt hs_pats m_ksig hs_cons new_or_data
   = do { traceTc "tcDataFamInstHeader {" (ppr fam_tc <+> ppr hs_pats)
-       ; (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty, res_kind)))
+       ; (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty, master_res_kind, instance_res_kind)))
             <- pushTcLevelM_                                $
                solveEqualities                              $
                bindImplicitTKBndrs_Q_Skol imp_vars          $
                bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $
                do { stupid_theta <- tcHsContext hs_ctxt
                   ; (lhs_ty, lhs_kind) <- tcFamTyPats fam_tc hs_pats
+                  ; (lhs_applied_ty, lhs_applied_kind)
+                      <- tcInstInvisibleTyBinders lhs_ty lhs_kind
+                      -- See Note [Data family/instance return kinds]
+                      -- in GHC.Tc.TyCl point (DF3)
 
                   -- Ensure that the instance is consistent
                   -- with its parent class
@@ -869,21 +874,17 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
                   -- Add constraints from the data constructors
                   ; kcConDecls new_or_data res_kind hs_cons
 
-                  -- See Note [Datatype return kinds] in GHC.Tc.TyCl, point (7).
-                  ; (lhs_extra_args, lhs_applied_kind)
-                      <- tcInstInvisibleTyBinders (invisibleTyBndrCount lhs_kind)
-                                                  lhs_kind
-                  ; let lhs_applied_ty = lhs_ty `mkTcAppTys` lhs_extra_args
-                        hs_lhs         = nlHsTyConApp fixity (getName fam_tc) hs_pats
+                  -- Check that the result kind of the TyCon applied to its args
+                  -- is compatible with the explicit signature (or Type, if there
+                  -- is none)
+                  ; let hs_lhs = nlHsTyConApp fixity (getName fam_tc) hs_pats
                   ; _ <- unifyKind (Just (unLoc hs_lhs)) lhs_applied_kind res_kind
-                    -- Check that the result kind of the TyCon applied to its args
-                    -- is compatible with the explicit signature (or Type, if there
-                    -- is none)
 
                   ; traceTc "tcDataFamInstHeader" $
                     vcat [ ppr fam_tc, ppr m_ksig, ppr lhs_applied_kind, ppr res_kind ]
                   ; return ( stupid_theta
                            , lhs_applied_ty
+                           , lhs_applied_kind
                            , res_kind ) }
 
        -- See GHC.Tc.TyCl Note [Generalising in tcFamTyPatsGuts]
@@ -900,13 +901,17 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
        ; (ze, qtvs)   <- zonkTyBndrs qtvs
        ; lhs_ty       <- zonkTcTypeToTypeX ze lhs_ty
        ; stupid_theta <- zonkTcTypesToTypesX ze stupid_theta
-       ; res_kind     <- zonkTcTypeToTypeX ze res_kind
+       ; master_res_kind   <- zonkTcTypeToTypeX ze master_res_kind
+       ; instance_res_kind <- zonkTcTypeToTypeX ze instance_res_kind
 
        -- We check that res_kind is OK with checkDataKindSig in
        -- tcDataFamInstDecl, after eta-expansion.  We need to check that
        -- it's ok because res_kind can come from a user-written kind signature.
        -- See Note [Datatype return kinds], point (4a)
 
+       ; checkDataKindSig (DataInstanceSort new_or_data) master_res_kind
+       ; checkDataKindSig (DataInstanceSort new_or_data) instance_res_kind
+
        -- Check that type patterns match the class instance head
        -- The call to splitTyConApp_maybe here is just an inlining of
        -- the body of unravelFamInstPats.
@@ -914,7 +919,7 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
            Just (_, pats) -> pure pats
            Nothing -> pprPanic "tcDataFamInstHeader" (ppr lhs_ty)
 
-       ; return (qtvs, pats, res_kind, stupid_theta) }
+       ; return (qtvs, pats, master_res_kind, stupid_theta) }
   where
     fam_name  = tyConName fam_tc
     data_ctxt = DataKindCtxt fam_name
@@ -973,7 +978,7 @@ 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
   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
+  in the right order.  So, if the /patterns/ of the family instance
   are eta-reducible, we re-order Drep's parameters to put the
   eta-reduced type variables last.
 
diff --git a/compiler/GHC/Tc/Types.hs b/compiler/GHC/Tc/Types.hs
index ce2e5faead..f99f99d1a5 100644
--- a/compiler/GHC/Tc/Types.hs
+++ b/compiler/GHC/Tc/Types.hs
@@ -79,7 +79,10 @@ module GHC.Tc.Types(
 
         -- Role annotations
         RoleAnnotEnv, emptyRoleAnnotEnv, mkRoleAnnotEnv,
-        lookupRoleAnnot, getRoleAnnots
+        lookupRoleAnnot, getRoleAnnots,
+
+        -- Linting
+        lintGblEnv
   ) where
 
 #include "HsVersions.h"
@@ -93,6 +96,7 @@ import GHC.Tc.Types.Evidence
 import GHC.Core.Type
 import GHC.Core.TyCon  ( TyCon, tyConKind )
 import GHC.Core.PatSyn ( PatSyn )
+import GHC.Core.Lint   ( lintAxioms )
 import GHC.Types.Id         ( idType, idName )
 import GHC.Types.FieldLabel ( FieldLabel )
 import GHC.Core.UsageEnv
@@ -1738,3 +1742,16 @@ lookupRoleAnnot = lookupNameEnv
 getRoleAnnots :: [Name] -> RoleAnnotEnv -> [LRoleAnnotDecl GhcRn]
 getRoleAnnots bndrs role_env
   = mapMaybe (lookupRoleAnnot role_env) bndrs
+
+{- *********************************************************************
+*                                                                      *
+                  Linting a TcGblEnv
+*                                                                      *
+********************************************************************* -}
+
+-- | Check the 'TcGblEnv' for consistency. Currently, only checks
+-- axioms, but should check other aspects, too.
+lintGblEnv :: DynFlags -> TcGblEnv -> (Bag SDoc, Bag SDoc)
+lintGblEnv dflags tcg_env = lintAxioms dflags axioms
+  where
+    axioms = typeEnvCoAxioms (tcg_type_env tcg_env)
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))