Fix #17021 by checking more return kinds

All the details are in new Note [Datatype return kinds] in
TcTyClsDecls.

Test case: typecheck/should_fail/T17021{,b}
           typecheck/should_compile/T17021a

Updates haddock submodule

10 files changed, 396 insertions, 184 deletions

diff --git a/compiler/GHC/Core/Coercion/Axiom.hs b/compiler/GHC/Core/Coercion/Axiom.hs
index c6861d8590..b2a66033ac 100644
--- a/compiler/GHC/Core/Coercion/Axiom.hs
+++ b/compiler/GHC/Core/Coercion/Axiom.hs
@@ -198,6 +198,17 @@ axiom as a whole, and they are computed only when the final axiom is built.
 
 During serialization, the list is converted into a list of the indices
 of the branches.
+
+Note [CoAxioms are homogeneous]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+All axioms must be *homogeneous*, meaning that the kind of the LHS must
+match the kind of the RHS. In practice, this means:
+
+  Given a CoAxiom { co_ax_tc = ax_tc },
+  for every branch CoAxBranch { cab_lhs = lhs, cab_rhs = rhs }:
+    typeKind (mkTyConApp ax_tc lhs) `eqType` typeKind rhs
+
+This is checked in FamInstEnv.mkCoAxBranch.
 -}
 
 -- | A 'CoAxiom' is a \"coercion constructor\", i.e. a named equality axiom.
@@ -233,6 +244,7 @@ data CoAxBranch
     , cab_roles    :: [Role]        -- See Note [CoAxBranch roles]
     , cab_lhs      :: [Type]        -- Type patterns to match against
     , cab_rhs      :: Type          -- Right-hand side of the equality
+                                    -- See Note [CoAxioms are homogeneous]
     , cab_incomps  :: [CoAxBranch]  -- The previous incompatible branches
                                     -- See Note [Storing compatibility]
     }
diff --git a/compiler/GHC/Core/FamInstEnv.hs b/compiler/GHC/Core/FamInstEnv.hs
index c8e5a7a4f9..10dc63eb50 100644
--- a/compiler/GHC/Core/FamInstEnv.hs
+++ b/compiler/GHC/Core/FamInstEnv.hs
@@ -638,13 +638,16 @@ 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 lhs rhs roles loc
-  = CoAxBranch { cab_tvs     = tvs'
+mkCoAxBranch tvs eta_tvs cvs ax_tc lhs rhs roles loc
+  = -- See Note [CoAxioms are homogeneous] in Core.Coercion.Axiom
+    ASSERT( typeKind (mkTyConApp ax_tc lhs) `eqType` typeKind rhs )
+    CoAxBranch { cab_tvs     = tvs'
                , cab_eta_tvs = eta_tvs'
                , cab_cvs     = cvs'
                , cab_lhs     = tidyTypes env lhs
@@ -698,7 +701,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 lhs_tys rhs_ty
+    branch = mkCoAxBranch tvs eta_tvs cvs fam_tc lhs_tys rhs_ty
                           (map (const Nominal) tvs)
                           (getSrcSpan ax_name)
 
@@ -716,7 +719,7 @@ mkNewTypeCoAxiom name tycon tvs roles rhs_ty
             , co_ax_tc       = tycon
             , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
   where
-    branch = mkCoAxBranch tvs [] [] (mkTyVarTys tvs) rhs_ty
+    branch = mkCoAxBranch tvs [] [] tycon (mkTyVarTys tvs) rhs_ty
                           roles (getSrcSpan name)
 
 {-
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index b22705eb6f..92e9a25a6f 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -1388,7 +1388,8 @@ lintInTy ty
   = addLoc (InType ty) $
     do  { ty' <- applySubstTy ty
         ; k  <- lintType ty'
-        ; lintKind k  -- The kind returned by lintType is already
+        ; addLoc (InKind ty' k) $
+          lintKind k  -- The kind returned by lintType is already
                       -- a LintedKind but we also want to check that
                       -- k :: *, which lintKind does
         ; return (ty', k) }
@@ -2278,6 +2279,7 @@ data LintLocInfo
   | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
   | TopLevelBindings
   | InType Type         -- Inside a type
+  | InKind Type Kind    -- Inside a kind
   | InCo   Coercion     -- Inside a coercion
 
 initL :: DynFlags -> LintFlags -> [Var]
@@ -2533,6 +2535,8 @@ dumpLoc TopLevelBindings
   = (noSrcLoc, Outputable.empty)
 dumpLoc (InType ty)
   = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
+dumpLoc (InKind ty ki)
+  = (noSrcLoc, text "In the kind of" <+> parens (ppr ty <+> dcolon <+> ppr ki))
 dumpLoc (InCo co)
   = (noSrcLoc, text "In the coercion" <+> quotes (ppr co))
 
diff --git a/compiler/GHC/Core/Unify.hs b/compiler/GHC/Core/Unify.hs
index fa188fc022..8719746f67 100644
--- a/compiler/GHC/Core/Unify.hs
+++ b/compiler/GHC/Core/Unify.hs
@@ -355,8 +355,8 @@ types are apart. This has practical consequences for the ability for closed
 type family applications to reduce. See test case
 indexed-types/should_compile/Overlap14.
 
-Note [Unifying with skolems]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Unification with skolems]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 If we discover that two types unify if and only if a skolem variable is
 substituted, we can't properly unify the types. But, that skolem variable
 may later be instantiated with a unifyable type. So, we return maybeApart
diff --git a/compiler/GHC/Hs/Utils.hs b/compiler/GHC/Hs/Utils.hs
index b3a327c4c6..d7f37dac86 100644
--- a/compiler/GHC/Hs/Utils.hs
+++ b/compiler/GHC/Hs/Utils.hs
@@ -498,8 +498,21 @@ nlHsTyVar x   = noLoc (HsTyVar noExtField NotPromoted (noLoc x))
 nlHsFunTy a b = noLoc (HsFunTy noExtField (parenthesizeHsType funPrec a) b)
 nlHsParTy t   = noLoc (HsParTy noExtField t)
 
-nlHsTyConApp :: IdP (GhcPass p) -> [LHsType (GhcPass p)] -> LHsType (GhcPass p)
-nlHsTyConApp tycon tys  = foldl' nlHsAppTy (nlHsTyVar tycon) tys
+nlHsTyConApp :: LexicalFixity -> IdP (GhcPass p)
+             -> [LHsTypeArg (GhcPass p)] -> LHsType (GhcPass p)
+nlHsTyConApp fixity tycon tys
+  | Infix <- fixity
+  , HsValArg ty1 : HsValArg ty2 : rest <- tys
+  = foldl' mk_app (noLoc $ HsOpTy noExtField ty1 (noLoc tycon) ty2) rest
+  | otherwise
+  = foldl' mk_app (nlHsTyVar tycon) tys
+  where
+    mk_app :: LHsType (GhcPass p) -> LHsTypeArg (GhcPass p) -> LHsType (GhcPass p)
+    mk_app fun@(L _ (HsOpTy {})) arg = mk_app (noLoc $ HsParTy noExtField fun) arg
+      -- parenthesize things like `(A + B) C`
+    mk_app fun (HsValArg ty) = noLoc (HsAppTy noExtField fun (parenthesizeHsType appPrec ty))
+    mk_app fun (HsTypeArg _ ki) = noLoc (HsAppKindTy noSrcSpan fun (parenthesizeHsType appPrec ki))
+    mk_app fun (HsArgPar _) = noLoc (HsParTy noExtField fun)
 
 nlHsAppKindTy ::
   LHsType (GhcPass p) -> LHsKind (GhcPass p) -> LHsType (GhcPass p)
diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs
index 24dbe364b2..1a52bcc966 100644
--- a/compiler/GHC/HsToCore/Expr.hs
+++ b/compiler/GHC/HsToCore/Expr.hs
@@ -1044,10 +1044,13 @@ mk_fail_msg dflags pat = "Pattern match failure in do expression at " ++
 
 dsHsVar :: Id -> DsM CoreExpr
 dsHsVar var
-               -- See Wrinkle in Note [Detecting forced eta expansion]
-  = ASSERT2(null (badUseOfLevPolyPrimop var ty), ppr var $$ ppr ty)
-    return (varToCoreExpr var)   -- See Note [Desugaring vars]
+  | let bad_tys = badUseOfLevPolyPrimop var ty
+  , not (null bad_tys)
+  = do { levPolyPrimopErr (ppr var) ty bad_tys
+       ; return unitExpr }  -- return something eminently safe
 
+  | otherwise
+  = return (varToCoreExpr var)   -- See Note [Desugaring vars]
   where
     ty = idType var
 
@@ -1134,6 +1137,8 @@ This invariant is checked in dsExpr.
 With that representation invariant, we simply look inside every HsWrap
 to see if its body is an HsVar whose Id hasNoBinding. Then, we look
 at the wrapped type. If it has any levity polymorphic arguments, reject.
+Because we might have an HsVar without a wrapper, we check in dsHsVar
+as well. typecheck/should_fail/T17021 triggers this case.
 
 Interestingly, this approach does not look to see whether the Id in
 question will be eta expanded. The logic is this:
@@ -1144,20 +1149,6 @@ question will be eta expanded. The logic is this:
     argument. If its wrapped type contains levity polymorphic arguments, reject.
 So, either way, we're good to reject.
 
-Wrinkle
-~~~~~~~
-Currently, all levity-polymorphic Ids are wrapped in HsWrap.
-
-However, this is not set in stone, in the future we might make
-instantiation more lazy.  (See "Visible type application", ESOP '16.)
-If we spot a levity-polymorphic hasNoBinding Id without a wrapper,
-then that is surely a problem. In this case, we raise an assertion failure.
-This failure can be changed to a call to `levPolyPrimopErr` in the future,
-if we decide to change instantiation.
-
-We can just check HsVar and HsConLikeOut for RealDataCon, since
-we don't have levity-polymorphic pattern synonyms. (This might change
-in the future.)
 -}
 
 -- | Takes an expression and its instantiated type. If the expression is an
diff --git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs
index 1b46b98636..a780f4688e 100644
--- a/compiler/typecheck/FamInst.hs
+++ b/compiler/typecheck/FamInst.hs
@@ -183,13 +183,14 @@ newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc })
            -- Note [Linting type synonym applications].
            case lintTypes dflags tcvs' (rhs':lhs') of
              Nothing       -> pure ()
-             Just fail_msg -> pprPanic "Core Lint error" (vcat [ fail_msg
-                                                               , ppr fam_tc
-                                                               , ppr subst
-                                                               , ppr tvs'
-                                                               , ppr cvs'
-                                                               , ppr lhs'
-                                                               , ppr rhs' ])
+             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
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index ac15c36201..8d47f4b329 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -54,7 +54,6 @@ module TcHsType (
         typeLevelMode, kindLevelMode,
 
         kindGeneralizeAll, kindGeneralizeSome, kindGeneralizeNone,
-        checkExpectedKind_pp,
 
         -- Sort-checking kinds
         tcLHsKindSig, checkDataKindSig, DataSort(..),
@@ -400,7 +399,7 @@ tcHsTypeApp wc_ty kind
                setXOptM LangExt.PartialTypeSignatures $
                -- See Note [Wildcards in visible type application]
                tcNamedWildCardBinders sig_wcs $ \ _ ->
-               tcCheckLHsType hs_ty kind
+               tcCheckLHsType hs_ty (TheKind kind)
        -- We do not kind-generalize type applications: we just
        -- instantiate with exactly what the user says.
        -- See Note [No generalization in type application]
@@ -466,10 +465,11 @@ tcHsOpenTypeNC   ty = do { ek <- newOpenTypeKind
 tcHsLiftedTypeNC ty = tc_lhs_type typeLevelMode ty liftedTypeKind
 
 -- Like tcHsType, but takes an expected kind
-tcCheckLHsType :: LHsType GhcRn -> Kind -> TcM TcType
+tcCheckLHsType :: LHsType GhcRn -> ContextKind -> TcM TcType
 tcCheckLHsType hs_ty exp_kind
   = addTypeCtxt hs_ty $
-    tc_lhs_type typeLevelMode hs_ty exp_kind
+    do { ek <- newExpectedKind exp_kind
+       ; tc_lhs_type typeLevelMode hs_ty ek }
 
 tcLHsType :: LHsType GhcRn -> TcM (TcType, TcKind)
 -- Called from outside: set the context
@@ -1431,27 +1431,18 @@ checkExpectedKind :: HasDebugCallStack
                   -> TcKind             -- ^ the expected kind
                   -> TcM TcType
 -- Just a convenience wrapper to save calls to 'ppr'
-checkExpectedKind hs_ty ty act exp
-  = checkExpectedKind_pp (ppr hs_ty) ty act exp
-
-checkExpectedKind_pp :: HasDebugCallStack
-                     => SDoc               -- ^ The thing we are checking
-                     -> TcType             -- ^ type we're checking
-                     -> TcKind             -- ^ the known kind of that type
-                     -> TcKind             -- ^ the expected kind
-                     -> TcM TcType
-checkExpectedKind_pp pp_hs_ty ty act_kind exp_kind
+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
 
        ; let origin = TypeEqOrigin { uo_actual   = act_kind'
                                    , uo_expected = exp_kind
-                                   , uo_thing    = Just pp_hs_ty
+                                   , uo_thing    = Just (ppr hs_ty)
                                    , uo_visible  = True } -- the hs_ty is visible
 
        ; traceTc "checkExpectedKindX" $
-         vcat [ pp_hs_ty
+         vcat [ ppr hs_ty
               , text "act_kind':" <+> ppr act_kind'
               , text "exp_kind:" <+> ppr exp_kind ]
 
@@ -1473,7 +1464,6 @@ checkExpectedKind_pp pp_hs_ty ty act_kind exp_kind
       n_act_invis_bndrs = invisibleTyBndrCount act_kind
       n_to_inst         = n_act_invis_bndrs - n_exp_invis_bndrs
 
-
 ---------------------------
 tcHsMbContext :: Maybe (LHsContext GhcRn) -> TcM [PredType]
 tcHsMbContext Nothing    = return []
@@ -2909,7 +2899,7 @@ Hence using zonked_kinds when forming tvs'.
 
 -----------------------------------
 etaExpandAlgTyCon :: [TyConBinder]
-                  -> Kind
+                  -> Kind   -- must be zonked
                   -> TcM ([TyConBinder], Kind)
 -- GADT decls can have a (perhaps partial) kind signature
 --      e.g.  data T a :: * -> * -> * where ...
@@ -2919,6 +2909,7 @@ etaExpandAlgTyCon :: [TyConBinder]
 -- Never emits constraints.
 -- It's a little trickier than you might think: see
 -- Note [TyConBinders for the result kind signature of a data type]
+-- See Note [Datatype return kinds] in TcTyClsDecls
 etaExpandAlgTyCon tc_bndrs kind
   = do  { loc     <- getSrcSpanM
         ; uniqs   <- newUniqueSupply
@@ -2987,6 +2978,8 @@ data DataSort
 -- 1. @TYPE r@ (for some @r@), or
 --
 -- 2. @k@ (where @k@ is a bare kind variable; see #12369)
+--
+-- See also Note [Datatype return kinds] in TcTyClsDecls
 checkDataKindSig :: DataSort -> Kind -> TcM ()
 checkDataKindSig data_sort kind = do
   dflags <- getDynFlags
@@ -2995,11 +2988,11 @@ checkDataKindSig data_sort kind = do
     pp_dec :: SDoc
     pp_dec = text $
       case data_sort of
-        DataDeclSort     DataType -> "data type"
-        DataDeclSort     NewType  -> "newtype"
-        DataInstanceSort DataType -> "data instance"
-        DataInstanceSort NewType  -> "newtype instance"
-        DataFamilySort            -> "data family"
+        DataDeclSort     DataType -> "Data type"
+        DataDeclSort     NewType  -> "Newtype"
+        DataInstanceSort DataType -> "Data instance"
+        DataInstanceSort NewType  -> "Newtype instance"
+        DataFamilySort            -> "Data family"
 
     is_newtype :: Bool
     is_newtype =
@@ -3042,8 +3035,8 @@ checkDataKindSig data_sort kind = do
 
     err_msg :: DynFlags -> SDoc
     err_msg dflags =
-      sep [ (sep [ text "Kind signature on" <+> pp_dec <+>
-                   text "declaration has non-" <>
+      sep [ (sep [ pp_dec <+>
+                   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) ])
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index 39d0cdb0ca..e5c805a275 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -688,6 +688,8 @@ tcDataFamInstDecl mb_clsinfo
        -- NB: we can do this after eta-reducing the axiom, because if
        --     we did it before the "extra" tvs from etaExpandAlgTyCon
        --     would always be eta-reduced
+       --
+       -- See also Note [Datatype return kinds] in TcTyClsDecls
        ; (extra_tcbs, final_res_kind) <- etaExpandAlgTyCon full_tcbs res_kind
        ; checkDataKindSig (DataInstanceSort new_or_data) final_res_kind
        ; let extra_pats  = map (mkTyVarTy . binderVar) extra_tcbs
@@ -797,7 +799,7 @@ tcDataFamInstHeader
 -- Here the "header" is the bit before the "where"
 tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
                     hs_ctxt hs_pats m_ksig hs_cons new_or_data
-  = do { (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty)))
+  = do { (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty, lhs_applied_kind)))
             <- pushTcLevelM_                                $
                solveEqualities                              $
                bindImplicitTKBndrs_Q_Skol imp_vars          $
@@ -815,8 +817,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
 
-                  ; lhs_ty <- checkExpectedKind_pp pp_lhs lhs_ty lhs_kind res_kind
-                  ; return (stupid_theta, lhs_ty) }
+                  -- See Note [Datatype return kinds] in TcTyClsDecls, 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
+                  ; _ <- unifyKind (Just (unLoc hs_lhs)) lhs_applied_kind res_kind
+
+                  ; return ( stupid_theta
+                           , lhs_applied_ty
+                           , lhs_applied_kind ) }
 
        -- See TcTyClsDecls Note [Generalising in tcFamTyPatsGuts]
        -- This code (and the stuff immediately above) is very similar
@@ -829,10 +840,10 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
        ; qtvs <- quantifyTyVars dvs
 
        -- Zonk the patterns etc into the Type world
-       ; (ze, qtvs)   <- zonkTyBndrs qtvs
-              -- See Note [Unifying data family kinds] about the discardCast
-       ; lhs_ty       <- zonkTcTypeToTypeX ze (discardCast lhs_ty)
-       ; stupid_theta <- zonkTcTypesToTypesX ze stupid_theta
+       ; (ze, qtvs)       <- zonkTyBndrs qtvs
+       ; lhs_ty           <- zonkTcTypeToTypeX ze lhs_ty
+       ; stupid_theta     <- zonkTcTypesToTypesX ze stupid_theta
+       ; lhs_applied_kind <- zonkTcTypeToTypeX ze lhs_applied_kind
 
        -- Check that type patterns match the class instance head
        -- The call to splitTyConApp_maybe here is just an inlining of
@@ -840,12 +851,10 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
        ; pats <- case splitTyConApp_maybe lhs_ty of
            Just (_, pats) -> pure pats
            Nothing -> pprPanic "tcDataFamInstHeader" (ppr lhs_ty)
-       ; return (qtvs, pats, typeKind lhs_ty, stupid_theta) }
-          -- See Note [Unifying data family kinds] about why we need typeKind here
+       ; return (qtvs, pats, lhs_applied_kind, stupid_theta) }
   where
     fam_name  = tyConName fam_tc
     data_ctxt = DataKindCtxt fam_name
-    pp_lhs    = pprHsFamInstLHS fam_name mb_bndrs hs_pats fixity hs_ctxt
     exp_bndrs = mb_bndrs `orElse` []
 
     -- See Note [Implementation of UnliftedNewtypes] in TcTyClsDecls, wrinkle (2).
@@ -863,7 +872,11 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
            ; lvl <- getTcLevel
            ; (subst, _tvs') <- tcInstSkolTyVarsAt lvl False emptyTCvSubst tvs
              -- Perhaps surprisingly, we don't need the skolemised tvs themselves
-           ; return (substTy subst inner_kind) }
+           ; let final_kind = substTy subst inner_kind
+           ; checkDataKindSig (DataInstanceSort new_or_data) $
+               snd $ tcSplitPiTys final_kind
+             -- See Note [Datatype return kinds], end of point (4)
+           ; return final_kind }
 
 {- Note [Result kind signature for a data family instance]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -874,36 +887,6 @@ we actually have a place to put the regeneralised variables.
 Thus: skolemise away. cf. Inst.deeplySkolemise and TcUnify.tcSkolemise
 Examples in indexed-types/should_compile/T12369
 
-Note [Unifying data family kinds]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When we kind-check a newtype instance with -XUnliftedNewtypes, we must
-unify the kind of the data family with any declared kind in the instance
-declaration. For 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
-
-We end up unifying `TYPE (Interpret 'Red)` (the kind of Foo, instantiated
-with 'Red) and `TYPE IntRep` (the declared kind of the instance). This
-unification succeeds, resulting in a coercion. The big question: what to
-do with this coercion? Answer: nothing! A kind annotation on a newtype instance
-is always redundant (except, perhaps, in that it helps guide unification). We
-have a definitive kind for the data family from the data family declaration,
-and so we learn nothing really new from the kind signature on an instance.
-We still must perform this unification (done in the call to checkExpectedKind
-toward the beginning of tcDataFamInstHeader), but the result is unhelpful. If there
-is a cast, it will wrap the lhs_ty, and so we just drop it before splitting the
-lhs_ty to reveal the underlying patterns. Because of the potential of dropping
-a cast like this, we just use typeKind in the result instead of propagating res_kind
-from above.
-
-This Note is wrinkle (3) in Note [Implementation of UnliftedNewtypes] in TcTyClsDecls.
-
 Note [Eta-reduction for data families]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
@@ -936,7 +919,8 @@ There are several fiddly subtleties lurking here
   tycon Drep.  The kind of D says it takes 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
+  So, with etaExpandAlgTyCon we make up some extra TyConBinders.
+  See point (3) in Note [Datatype return kinds] in TcTyClsDecls.
 
 * The result kind in the instance might be a polykind, like this:
      data family DP a :: forall k. k -> *
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index b265315c04..e85f471432 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -39,7 +39,7 @@ import TcTyDecls
 import TcClassDcl
 import {-# SOURCE #-} TcInstDcls( tcInstDecls1 )
 import TcDeriv (DerivInfo(..))
-import TcUnify ( unifyKind, checkTvConstraints )
+import TcUnify ( checkTvConstraints )
 import TcHsType
 import ClsInst( AssocInstInfo(..) )
 import TcMType
@@ -1324,7 +1324,7 @@ getInitialKind strategy
         ; tc <- kcDeclHeader strategy name flav ktvs $
                 case m_sig of
                   Just ksig -> TheKind <$> tcLHsKindSig ctxt ksig
-                  Nothing -> dataDeclDefaultResultKind new_or_data
+                  Nothing -> return $ dataDeclDefaultResultKind new_or_data
         ; return [tc] }
 
 getInitialKind InitialKindInfer (FamDecl { tcdFam = decl })
@@ -1439,13 +1439,10 @@ have before standalone kind signatures:
 -}
 
 -- See Note [Data declaration default result kind]
-dataDeclDefaultResultKind :: NewOrData -> TcM ContextKind
-dataDeclDefaultResultKind new_or_data = do
-  -- See Note [Implementation of UnliftedNewtypes]
-  unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes
-  return $ case new_or_data of
-    NewType | unlifted_newtypes -> OpenKind
-    _ -> TheKind liftedTypeKind
+dataDeclDefaultResultKind :: NewOrData -> ContextKind
+dataDeclDefaultResultKind NewType  = OpenKind
+  -- See Note [Implementation of UnliftedNewtypes], point <Error Messages>.
+dataDeclDefaultResultKind DataType = TheKind liftedTypeKind
 
 {- Note [Data declaration default result kind]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1466,13 +1463,14 @@ accept D4:
   data D4 :: Type -> Type where
     MkD4 :: ... -> D4 param
 
-However, there's a twist: when -XUnliftedNewtypes are enabled, we must relax
-the assumed result kind to (TYPE r) for newtypes:
+However, there's a twist: for newtypes, we must relax
+the assumed result kind to (TYPE r):
 
   newtype D5 where
     MkD5 :: Int# -> D5
 
-dataDeclDefaultResultKind takes care to produce the appropriate result kind.
+See Note [Implementation of UnliftedNewtypes], STEP 1 and it's sub-note
+<Error Messages>.
 -}
 
 ---------------------------------
@@ -1544,7 +1542,7 @@ kcTyClDecl (DataDecl { tcdLName    = (L _ name)
 
 kcTyClDecl (SynDecl { tcdLName = L _ name, tcdRhs = rhs }) _tycon
   = bindTyClTyVars name $ \ _ _ res_kind ->
-    discardResult $ tcCheckLHsType rhs res_kind
+    discardResult $ tcCheckLHsType rhs (TheKind res_kind)
         -- NB: check against the result kind that we allocated
         -- in inferInitialKinds.
 
@@ -1571,38 +1569,15 @@ kcTyClDecl (XTyClDecl nec)                      _ = noExtCon nec
 
 -------------------
 
--- | Unify the kind of the first type provided with the newtype's kind, if
--- -XUnliftedNewtypes is enabled and the NewOrData indicates Newtype. If there
--- is more than one type provided, do nothing: the newtype is in error, and this
--- will be caught in validity checking (which will give a better error than we can
--- here.)
-unifyNewtypeKind :: DynFlags
-                 -> NewOrData
-                 -> [LHsType GhcRn]   -- user-written argument types, should be just 1
-                 -> [TcType]          -- type-checked argument types, should be just 1
-                 -> TcKind            -- expected kind of newtype
-                 -> TcM [TcType]      -- casted argument types (should be just 1)
-                                      --  result = orig_arg |> kind_co
-                                      -- where kind_co :: orig_arg_ki ~N expected_ki
-unifyNewtypeKind dflags NewType [hs_ty] [tc_ty] ki
-  | xopt LangExt.UnliftedNewtypes dflags
-  = do { traceTc "unifyNewtypeKind" (ppr hs_ty $$ ppr tc_ty $$ ppr ki)
-       ; co <- unifyKind (Just (unLoc hs_ty)) (typeKind tc_ty) ki
-       ; return [tc_ty `mkCastTy` co] }
-  -- See comments above: just do nothing here
-unifyNewtypeKind _ _ _ arg_tys _ = return arg_tys
-
 -- Type check the types of the arguments to a data constructor.
 -- This includes doing kind unification if the type is a newtype.
 -- See Note [Implementation of UnliftedNewtypes] for why we need
 -- the first two arguments.
 kcConArgTys :: NewOrData -> Kind -> [LHsType GhcRn] -> TcM ()
 kcConArgTys new_or_data res_kind arg_tys = do
-  { arg_tc_tys <- mapM (tcHsOpenType . getBangType) arg_tys
+  { let exp_kind = getArgExpKind new_or_data res_kind
+  ; mapM_ (flip tcCheckLHsType exp_kind . getBangType) arg_tys
     -- See Note [Implementation of UnliftedNewtypes], STEP 2
-  ; dflags <- getDynFlags
-  ; discardResult $
-      unifyNewtypeKind dflags new_or_data arg_tys arg_tc_tys res_kind
   }
 
 kcConDecls :: NewOrData
@@ -1842,20 +1817,20 @@ What follows is a high-level overview of the implementation of the
 proposal.
 
 STEP 1: Getting the initial kind, as done by inferInitialKind. We have
-two sub-cases (assuming we have a newtype and -XUnliftedNewtypes is enabled):
+two sub-cases:
 
-* With a CUSK: no change in kind-checking; the tycon is given the kind
+* With a SAK/CUSK: no change in kind-checking; the tycon is given the kind
   the user writes, whatever it may be.
 
-* Without a CUSK: If there is no kind signature, the tycon is given
-  a kind `TYPE r`, for a fresh unification variable `r`.
+* Without a SAK/CUSK: If there is no kind signature, the tycon is given
+  a kind `TYPE r`, for a fresh unification variable `r`. We do this even
+  when -XUnliftedNewtypes is not on; see <Error Messages>, below.
 
 STEP 2: Kind-checking, as done by kcTyClDecl. This step is skipped for CUSKs.
 The key function here is kcConDecl, which looks at an individual constructor
-declaration. In the unlifted-newtypes case (i.e., -XUnliftedNewtypes and,
-indeed, we are processing a newtype), we call unifyNewtypeKind, which is a
-thin wrapper around unifyKind, unifying the kind of the one argument and the
-result kind of the newtype tycon.
+declaration. When we are processing a newtype (but whether or not -XUnliftedNewtypes
+is enabled; see <Error Messages>, below), we generate a correct ContextKind
+for the checking argument types: see getArgExpKind.
 
 Examples of newtypes affected by STEP 2, assuming -XUnliftedNewtypes is
 enabled (we use r0 to denote a unification variable):
@@ -1878,10 +1853,11 @@ component of the kind for checking in kcConDecl, so we call etaExpandAlgTyCon
 in kcTyClDecl.
 
 STEP 3: Type-checking (desugaring), as done by tcTyClDecl. The key function
-here is tcConDecl. Once again, we must call unifyNewtypeKind, for two reasons:
+here is tcConDecl. Once again, we must use getArgExpKind to ensure that the
+representation type's kind matches that of the newtype, for two reasons:
 
   A. It is possible that a GADT has a CUSK. (Note that this is *not*
-     possible for H98 types. Recall that CUSK types don't go through
+     possible for H98 types.) Recall that CUSK types don't go through
      kcTyClDecl, so we might not have done this kind check.
   B. We need to produce the coercion to put on the argument type
      if the kinds are different (for both H98 and GADT).
@@ -1897,11 +1873,32 @@ newtype N :: TYPE (F Int) where
 We really need to have the argument to MkN be (Int |> TYPE (sym axF)), where
 axF :: F Int ~ LiftedRep. That way, the argument kind is the same as the
 newtype kind, which is the principal correctness condition for newtypes.
-This call to unifyNewtypeKind is what produces that coercion.
+
+Wrinkle: Consider (#17021, typecheck/should_fail/T17021)
+
+    type family Id (x :: a) :: a where
+      Id x = x
+
+    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.
+
+  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
+  important that even after dropping the cast, the type's kind has the form
+  TYPE r. This is guaranteed by restrictions on the kinds of datatypes.
+  For example, a declaration like `newtype T :: Id Type` is rejected: a
+  newtype's final kind always has the form TYPE r, just as we want.
 
 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:
 
 1. In tcFamDecl1, we suppress a tcIsLiftedTypeKind check if
    UnliftedNewtypes is on. This allows us to write things like:
@@ -1923,7 +1920,7 @@ the H98 syntax doesn't permit a kind signature on the newtype itself.
    we use that kind signature.
 
 3. A data family and its newtype instance may be declared with slightly
-   different kinds. See Note [Unifying data family kinds] in TcInstDcls.
+   different kinds. See point 7 in Note [Datatype return kinds].
 
 There's also a change in the renamer:
 
@@ -1936,6 +1933,36 @@ There's also a change in the renamer:
 For completeness, it was also necessary to make coerce work on
 unlifted types, resolving #13595.
 
+<Error Messages>: It's tempting to think that the expected kind for a newtype
+constructor argument when -XUnliftedNewtypes is *not* enabled should just be Type.
+But this leads to difficulty in suggesting to enable UnliftedNewtypes. Here is
+an example:
+
+  newtype A = MkA Int#
+
+If we expect the argument to MkA to have kind Type, then we get a kind-mismatch
+error. The problem is that there is no way to connect this mismatch error to
+-XUnliftedNewtypes, and suggest enabling the extension. So, instead, we allow
+the A to type-check, but then find the problem when doing validity checking (and
+where we get make a suitable error message). One potential worry is
+
+  {-# LANGUAGE PolyKinds #-}
+  newtype B a = MkB a
+
+This turns out OK, because unconstrained RuntimeReps default to LiftedRep, just
+as we would like. Another potential problem comes in a case like
+
+  -- no UnliftedNewtypes
+
+  data family D :: k
+  newtype instance D = MkD Any
+
+Here, we want inference to tell us that k should be instantiated to Type in
+the instance. With the approach described here (checking for Type only in
+the validity checker), that will not happen. But I cannot think of a non-contrived
+example that will notice this lack of inference, so it seems better to improve
+error messages than be able to infer this instantiation.
+
 -}
 
 tcTyClDecl :: RolesInfo -> LTyClDecl GhcRn -> TcM (TyCon, [DerivInfo])
@@ -2285,6 +2312,177 @@ 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 TcHsType.
+
+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. Note that we do *not* do type family reduction here.
+   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
+
+     type Arrow = (->)
+     data T7 :: Arrow Bool Type               -- good
+
+     type family ARROW where
+       ARROW = (->)
+     data T8 :: ARROW Bool Type               -- bad
+
+     type Star = Type
+     data T9 :: Bool -> Star                  -- good
+
+     type family F a where
+       F Int  = Bool
+       F Bool = Type
+     data T10 :: Bool -> F Bool               -- bad
+
+   This check is done in checkDataKindSig. For data declarations, this
+   call is in tcDataDefn; for data instances, this call is in tcDataFamInstDecl.
+
+   However, 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 in tc_kind_sig within tcDataFamInstHeader. 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. TcHsType.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].
+
 -}
 
 {- *********************************************************************
@@ -2313,6 +2511,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
   --   data family D a :: forall k. Type -> k
   -- 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
   ; tc_rep_name <- newTyConRepName tc_name
@@ -2445,7 +2644,7 @@ tcTySynRhs roles_info tc_name hs_ty
        ; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env))
        ; rhs_ty <- pushTcLevelM_   $
                    solveEqualities $
-                   tcCheckLHsType hs_ty res_kind
+                   tcCheckLHsType hs_ty (TheKind res_kind)
        ; rhs_ty <- zonkTcTypeToType rhs_ty
        ; let roles = roles_info tc_name
              tycon = buildSynTyCon tc_name binders res_kind roles rhs_ty
@@ -2471,6 +2670,7 @@ tcDataDefn err_ctxt roles_info tc_name
        -- But it does no harm to bring them into scope
        -- over GADT ConDecls as well; and it's awkward not to
     do { gadt_syntax <- dataDeclChecks tc_name new_or_data ctxt cons
+         -- see Note [Datatype return kinds]
        ; (extra_bndrs, final_res_kind) <- etaExpandAlgTyCon tycon_binders res_kind
 
        ; tcg_env <- getGblEnv
@@ -2566,7 +2766,7 @@ kcTyFamInstEqn tc_fam_tc
          bindImplicitTKBndrs_Q_Tv imp_vars $
          bindExplicitTKBndrs_Q_Tv AnyKind (mb_expl_bndrs `orElse` []) $
          do { (_fam_app, res_kind) <- tcFamTyPats tc_fam_tc hs_pats
-            ; tcCheckLHsType hs_rhs_ty res_kind }
+            ; tcCheckLHsType hs_rhs_ty (TheKind res_kind) }
              -- Why "_Tv" here?  Consider (#14066
              --  type family Bar x y where
              --      Bar (x :: a) (y :: b) = Int
@@ -2613,7 +2813,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 [] [] pats rhs_ty
+       ; return (mkCoAxBranch qtvs [] [] fam_tc pats rhs_ty
                               (map (const Nominal) qtvs)
                               loc) }
 
@@ -2703,7 +2903,7 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty
                        -- Ensure that the instance is consistent with its
                        -- parent class (#16008)
                      ; addConsistencyConstraints mb_clsinfo lhs_ty
-                     ; rhs_ty <- tcCheckLHsType hs_rhs_ty rhs_kind
+                     ; rhs_ty <- tcCheckLHsType hs_rhs_ty (TheKind rhs_kind)
                      ; return (lhs_ty, rhs_ty) }
 
        -- See Note [Generalising in tcTyFamInstEqnGuts]
@@ -2948,15 +3148,11 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data
               solveEqualities                           $
               bindExplicitTKBndrs_Skol explicit_tkv_nms $
               do { ctxt <- tcHsMbContext hs_ctxt
-                 ; btys <- tcConArgs hs_args
+                 ; let exp_kind = getArgExpKind new_or_data res_kind
+                 ; btys <- tcConArgs exp_kind hs_args
                  ; field_lbls <- lookupConstructorFields (unLoc name)
                  ; let (arg_tys, stricts) = unzip btys
-                 ; dflags <- getDynFlags
-                 ; final_arg_tys <-
-                     unifyNewtypeKind dflags new_or_data
-                                      (hsConDeclArgTys hs_args)
-                                      arg_tys res_kind
-                 ; return (ctxt, final_arg_tys, field_lbls, stricts)
+                 ; return (ctxt, arg_tys, field_lbls, stricts)
                  }
 
          -- exp_tvs have explicit, user-written binding sites
@@ -3032,17 +3228,20 @@ 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
-                 ; btys <- tcConArgs hs_args
+                 ; 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
+                   -- See Note [Datatype return kinds]
+                 ; let exp_kind = getArgExpKind new_or_data (typeKind res_ty)
+                 ; btys <- tcConArgs exp_kind hs_args
                  ; let (arg_tys, stricts) = unzip btys
-                 ; res_ty <- tcHsOpenType hs_res_ty
-                   -- See Note [Implementation of UnliftedNewtypes]
-                 ; dflags <- getDynFlags
-                 ; final_arg_tys <-
-                     unifyNewtypeKind dflags new_or_data
-                                      (hsConDeclArgTys hs_args)
-                                      arg_tys (typeKind res_ty)
                  ; field_lbls <- lookupConstructorFields name
-                 ; return (ctxt, final_arg_tys, res_ty, field_lbls, stricts)
+                 ; return (ctxt, arg_tys, res_ty, field_lbls, stricts)
                  }
        ; imp_tvs <- zonkAndScopedSort imp_tvs
        ; let user_tvs = imp_tvs ++ exp_tvs
@@ -3102,6 +3301,16 @@ tcConDecl _ _ _ _ _ _ (ConDeclGADT _ _ _ (XLHsQTyVars nec) _ _ _ _)
   = noExtCon nec
 tcConDecl _ _ _ _ _ _ (XConDecl nec) = noExtCon nec
 
+-- | 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,
+-- it is OpenKind for datatypes and liftedTypeKind.
+-- Why do we not check for -XUnliftedNewtypes? See point <Error Messages>
+-- in Note [Implementation of UnliftedNewtypes]
+getArgExpKind :: NewOrData -> Kind -> ContextKind
+getArgExpKind NewType res_ki = TheKind res_ki
+getArgExpKind DataType _     = OpenKind
+
 tcConIsInfixH98 :: Name
              -> HsConDetails (LHsType GhcRn) (Located [LConDeclField GhcRn])
              -> TcM Bool
@@ -3124,16 +3333,19 @@ tcConIsInfixGADT con details
                         ; return (con `elemNameEnv` fix_env) }
                | otherwise -> return False
 
-tcConArgs :: HsConDeclDetails GhcRn
+tcConArgs :: ContextKind  -- expected kind of arguments
+                          -- always OpenKind for datatypes, but unlifted newtypes
+                          -- might have a specific kind
+          -> HsConDeclDetails GhcRn
           -> TcM [(TcType, HsSrcBang)]
-tcConArgs (PrefixCon btys)
-  = mapM tcConArg btys
-tcConArgs (InfixCon bty1 bty2)
-  = do { bty1' <- tcConArg bty1
-       ; bty2' <- tcConArg bty2
+tcConArgs exp_kind (PrefixCon btys)
+  = mapM (tcConArg exp_kind) btys
+tcConArgs exp_kind (InfixCon bty1 bty2)
+  = do { bty1' <- tcConArg exp_kind bty1
+       ; bty2' <- tcConArg exp_kind bty2
        ; return [bty1', bty2'] }
-tcConArgs (RecCon fields)
-  = mapM tcConArg btys
+tcConArgs exp_kind (RecCon fields)
+  = mapM (tcConArg exp_kind) btys
   where
     -- We need a one-to-one mapping from field_names to btys
     combined = map (\(L _ f) -> (cd_fld_names f,cd_fld_type f))
@@ -3143,13 +3355,12 @@ tcConArgs (RecCon fields)
     (_,btys) = unzip exploded
 
 
-tcConArg :: LHsType GhcRn -> TcM (TcType, HsSrcBang)
-tcConArg bty
+tcConArg :: ContextKind  -- expected kind for args; always OpenKind for datatypes,
+                         -- but might be an unlifted type with UnliftedNewtypes
+         -> LHsType GhcRn -> TcM (TcType, HsSrcBang)
+tcConArg exp_kind bty
   = do  { traceTc "tcConArg 1" (ppr bty)
-        ; arg_ty <- tcHsOpenType (getBangType bty)
-             -- Newtypes can't have unboxed types, but we check
-             -- that in checkValidDataCon; this tcConArg stuff
-             -- doesn't happen for GADT-style declarations
+        ; arg_ty <- tcCheckLHsType (getBangType bty) exp_kind
         ; traceTc "tcConArg 2" (ppr bty)
         ; return (arg_ty, getBangStrictness bty) }