Treat isConstraintKind more consistently
[ghc.git] / compiler / typecheck / TcHsType.hs
index 125891f..c1ecd47 100644 (file)
@@ -6,6 +6,7 @@
 -}
 
 {-# LANGUAGE CPP, TupleSections, MultiWayIf, RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 
 module TcHsType (
         -- Type signatures
@@ -15,10 +16,10 @@ module TcHsType (
         funsSigCtxt, addSigCtxt, pprSigCtxt,
 
         tcHsClsInstType,
-        tcHsDeriv, tcHsVectInst,
+        tcHsDeriv, tcDerivStrategy,
         tcHsTypeApp,
         UserTypeCtxt(..),
-        tcImplicitTKBndrs, tcImplicitTKBndrsX,
+        tcImplicitTKBndrs, tcImplicitQTKBndrs,
         tcExplicitTKBndrs,
         kcExplicitTKBndrs, kcImplicitTKBndrs,
 
@@ -31,7 +32,7 @@ module TcHsType (
 
         -- Kind-checking types
         -- No kind generalisation, no checkValidType
-        kcLHsQTyVars, kcLHsTyVarBndrs,
+        kcLHsQTyVars,
         tcWildCardBinders,
         tcHsLiftedType,   tcHsOpenType,
         tcHsLiftedTypeNC, tcHsOpenTypeNC,
@@ -69,11 +70,10 @@ import TcIface
 import TcSimplify
 import TcType
 import TcHsSyn( zonkSigType )
-import Inst   ( tcInstBinders, tcInstBinder )
+import Inst   ( tcInstTyBinders, tcInstTyBinder )
 import TyCoRep( TyBinder(..) )  -- Used in tcDataKindSig
 import Type
 import Coercion
-import Kind
 import RdrName( lookupLocalRdrOcc )
 import Var
 import VarSet
@@ -99,7 +99,7 @@ import PrelNames hiding ( wildCardName )
 import qualified GHC.LanguageExtensions as LangExt
 
 import Maybes
-import Data.List ( partition, mapAccumR )
+import Data.List ( find, mapAccumR )
 import Control.Monad
 
 {-
@@ -213,7 +213,8 @@ tcHsSigType :: UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
 -- See Note [Recipe for checking a signature]
 tcHsSigType ctxt sig_ty
   = addSigCtxt ctxt (hsSigType sig_ty) $
-    do { kind <- case expectedKindInCtxt ctxt of
+    do { traceTc "tcHsSigType {" (ppr sig_ty)
+       ; kind <- case expectedKindInCtxt ctxt of
                     AnythingKind -> newMetaKindVar
                     TheKind k    -> return k
                     OpenKind     -> newOpenTypeKind
@@ -227,6 +228,7 @@ tcHsSigType ctxt sig_ty
                else tc_hs_sig_type         skol_info sig_ty kind
 
        ; checkValidType ctxt ty
+       ; traceTc "end tcHsSigType }" (ppr ty)
        ; return ty }
   where
     skol_info = SigTypeSkol ctxt
@@ -272,7 +274,7 @@ tc_hs_sig_type skol_info (HsIB { hsib_ext = HsIBRn { hsib_vars = sig_vars }
 tc_hs_sig_type _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type"
 
 -----------------
-tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], Class, [Type], [Kind])
+tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], (Class, [Type], [Kind]))
 -- Like tcHsSigType, but for the ...deriving( C t1 ty2 ) clause
 -- Returns the C, [ty1, ty2, and the kinds of C's remaining arguments
 -- E.g.    class C (a::*) (b::k->k)
@@ -289,9 +291,55 @@ tcHsDeriv hs_ty
        ; let (tvs, pred) = splitForAllTys ty
        ; let (args, _) = splitFunTys cls_kind
        ; case getClassPredTys_maybe pred of
-           Just (cls, tys) -> return (tvs, cls, tys, args)
+           Just (cls, tys) -> return (tvs, (cls, tys, args))
            Nothing -> failWithTc (text "Illegal deriving item" <+> quotes (ppr hs_ty)) }
 
+-- | Typecheck something within the context of a deriving strategy.
+-- This is of particular importance when the deriving strategy is @via@.
+-- For instance:
+--
+-- @
+-- deriving via (S a) instance C (T a)
+-- @
+--
+-- We need to typecheck @S a@, and moreover, we need to extend the tyvar
+-- environment with @a@ before typechecking @C (T a)@, since @S a@ quantified
+-- the type variable @a@.
+tcDerivStrategy
+  :: forall a.
+     UserTypeCtxt
+  -> Maybe (DerivStrategy GhcRn) -- ^ The deriving strategy
+  -> TcM ([TyVar], a) -- ^ The thing to typecheck within the context of the
+                      -- deriving strategy, which might quantify some type
+                      -- variables of its own.
+  -> TcM (Maybe (DerivStrategy GhcTc), [TyVar], a)
+     -- ^ The typechecked deriving strategy, all quantified tyvars, and
+     -- the payload of the typechecked thing.
+tcDerivStrategy user_ctxt mds thing_inside
+  = case mds of
+      Nothing -> boring_case Nothing
+      Just ds -> do (ds', tvs, thing) <- tc_deriv_strategy ds
+                    pure (Just ds', tvs, thing)
+  where
+    tc_deriv_strategy :: DerivStrategy GhcRn
+                      -> TcM (DerivStrategy GhcTc, [TyVar], a)
+    tc_deriv_strategy StockStrategy    = boring_case StockStrategy
+    tc_deriv_strategy AnyclassStrategy = boring_case AnyclassStrategy
+    tc_deriv_strategy NewtypeStrategy  = boring_case NewtypeStrategy
+    tc_deriv_strategy (ViaStrategy ty) = do
+      cls_kind <- newMetaKindVar
+      ty' <- checkNoErrs $
+             tc_hs_sig_type_and_gen (SigTypeSkol user_ctxt) ty cls_kind
+      let (via_tvs, via_pred) = splitForAllTys ty'
+      tcExtendTyVarEnv via_tvs $ do
+        (thing_tvs, thing) <- thing_inside
+        pure (ViaStrategy via_pred, via_tvs ++ thing_tvs, thing)
+
+    boring_case :: mds -> TcM (mds, [TyVar], a)
+    boring_case mds = do
+      (thing_tvs, thing) <- thing_inside
+      pure (mds, thing_tvs, thing)
+
 tcHsClsInstType :: UserTypeCtxt    -- InstDeclCtxt or SpecInstCtxt
                 -> LHsSigType GhcRn
                 -> TcM ([TyVar], ThetaType, Class, [Type])
@@ -301,29 +349,16 @@ tcHsClsInstType user_ctxt hs_inst_ty
     do { inst_ty <- tc_hs_sig_type_and_gen (SigTypeSkol user_ctxt) hs_inst_ty constraintKind
        ; checkValidInstance user_ctxt hs_inst_ty inst_ty }
 
--- Used for 'VECTORISE [SCALAR] instance' declarations
-tcHsVectInst :: LHsSigType GhcRn -> TcM (Class, [Type])
-tcHsVectInst ty
-  | let hs_cls_ty = hsSigType ty
-  , Just (L _ cls_name, tys) <- hsTyGetAppHead_maybe hs_cls_ty
-    -- Ignoring the binders looks pretty dodgy to me
-  = do { (cls, cls_kind) <- tcClass cls_name
-       ; (applied_class, _res_kind)
-           <- tcTyApps typeLevelMode hs_cls_ty (mkClassPred cls []) cls_kind tys
-       ; case tcSplitTyConApp_maybe applied_class of
-           Just (_tc, args) -> ASSERT( _tc == classTyCon cls )
-                               return (cls, args)
-           _ -> failWithTc (text "Too many arguments passed to" <+> ppr cls_name) }
-  | otherwise
-  = failWithTc $ text "Malformed instance type"
-
 ----------------------------------------------
 -- | Type-check a visible type application
 tcHsTypeApp :: LHsWcType GhcRn -> Kind -> TcM Type
 -- See Note [Recipe for checking a signature] in TcHsType
 tcHsTypeApp wc_ty kind
   | HsWC { hswc_ext = sig_wcs, hswc_body = hs_ty } <- wc_ty
-  = do { ty <- tcWildCardBindersX newWildTyVar Nothing sig_wcs $ \ _ ->
+  = do { ty <- solveLocalEqualities $
+               -- We are looking at a user-written type, very like a
+               -- signature so we want to solve its equalities right now
+               tcWildCardBindersX newWildTyVar Nothing sig_wcs $ \ _ ->
                tcCheckLHsType hs_ty kind
        ; ty <- zonkPromoteType ty
        ; checkValidType TypeAppCtxt ty
@@ -475,7 +510,7 @@ metavariable.
 In types, however, we're not so lucky, because *we cannot re-generalize*!
 There is no lambda. So, we must be careful only to instantiate at the last
 possible moment, when we're sure we're never going to want the lost polymorphism
-again. This is done in calls to tcInstBinders.
+again. This is done in calls to tcInstTyBinders.
 
 To implement this behavior, we use bidirectional type checking, where we
 explicitly think about whether we know the kind of the type we're checking
@@ -504,20 +539,35 @@ missing any patterns.
 
 Note [The tcType invariant]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If    tc_ty = tc_hs_type hs_ty exp_kind
-then
-      typeKind tc_ty = exp_kind
+(IT1) If    tc_ty = tc_hs_type hs_ty exp_kind
+      then  typeKind tc_ty = exp_kind
 without any zonking needed.  The reason for this is that in
 tcInferApps we see (F ty), and we kind-check 'ty' with an
 expected-kind coming from F.  Then, to make the resulting application
-well kinded --- see Note [Ensure well-kinded types] in TcType --- we
-need the kind-checked 'ty' to have exactly the kind that F expects,
+well kinded --- see Note [The well-kinded type invariant] in TcType ---
+we need the kind-checked 'ty' to have exactly the kind that F expects,
 with no funny zonking nonsense in between.
 
-The tcType invariant also applies to checkExpectedKind: if
-    (tc_ty, _, _) = checkExpectedKind ty act_ki exp_ki
-then
-    typeKind tc_ty = exp_ki
+The tcType invariant also applies to checkExpectedKind:
+
+(IT2) if
+        (tc_ty, _, _) = checkExpectedKind ty act_ki exp_ki
+      then
+        typeKind tc_ty = exp_ki
+
+These other invariants are all necessary, too, as these functions
+are used within tc_hs_type:
+
+(IT3) If (ty, ki) <- tc_infer_hs_type ..., then typeKind ty == ki.
+
+(IT4) If (ty, ki) <- tc_infer_hs_type ..., then zonk ki == ki.
+      (In other words, the result kind of tc_infer_hs_type is zonked.)
+
+(IT5) If (ty, ki) <- tcTyVar ..., then typeKind ty == ki.
+
+(IT6) If (ty, ki) <- tcTyVar ..., then zonk ki == ki.
+      (In other words, the result kind of tcTyVar is zonked.)
+
 -}
 
 ------------------------------------------
@@ -539,22 +589,21 @@ tc_infer_hs_type mode (HsTyVar _ _ (L _ tv)) = tcTyVar mode tv
 tc_infer_hs_type mode (HsAppTy _ ty1 ty2)
   = do { let (hs_fun_ty, hs_arg_tys) = splitHsAppTys ty1 [ty2]
        ; (fun_ty, fun_kind) <- tc_infer_lhs_type mode hs_fun_ty
-         -- A worry: what if fun_kind needs zoonking?
-         -- We used to zonk it here, but that got fun_ty and fun_kind
-         -- out of sync (see the precondition to tcTyApps), which caused
-         -- Trac #14873.  So I'm now zonking in tcTyVar, and not here.
-         -- Is that enough?  Seems so, but I can't see how to be certain.
+           -- NB: (IT4) of Note [The tcType invariant] ensures that fun_kind is zonked
        ; tcTyApps mode hs_fun_ty fun_ty fun_kind hs_arg_tys }
 
 tc_infer_hs_type mode (HsOpTy _ lhs lhs_op@(L _ hs_op) rhs)
   | not (hs_op `hasKey` funTyConKey)
   = do { (op, op_kind) <- tcTyVar mode hs_op
-         -- See "A worry" in the HsApp case
        ; tcTyApps mode (noLoc $ HsTyVar noExt NotPromoted lhs_op) op op_kind
                        [lhs, rhs] }
 
 tc_infer_hs_type mode (HsKindSig _ ty sig)
-  = do { sig' <- tc_lhs_kind (kindLevel mode) sig
+  = do { sig' <- tcLHsKindSig KindSigCtxt sig
+                 -- We must typecheck the kind signature, and solve all
+                 -- its equalities etc; from this point on we may do
+                 -- things like instantiate its foralls, so it needs
+                 -- to be fully determined (Trac #14904)
        ; traceTc "tc_infer_hs_type:sig" (ppr ty $$ ppr sig')
        ; ty' <- tc_lhs_type mode ty sig'
        ; return (ty', sig') }
@@ -569,7 +618,9 @@ tc_infer_hs_type mode (HsSpliceTy _ (HsSpliced _ _ (HsSplicedTy ty)))
   = tc_infer_hs_type mode ty
 
 tc_infer_hs_type mode (HsDocTy _ ty _) = tc_infer_lhs_type mode ty
-tc_infer_hs_type _    (XHsType (NHsCoreTy ty))  = return (ty, typeKind ty)
+tc_infer_hs_type _    (XHsType (NHsCoreTy ty))
+  = do { ty <- zonkTcType ty  -- (IT3) and (IT4) of Note [The tcType invariant]
+       ; return (ty, typeKind ty) }
 tc_infer_hs_type mode other_ty
   = do { kv <- newMetaKindVar
        ; ty' <- tc_hs_type mode other_ty kv
@@ -661,11 +712,11 @@ tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind
   = do { ctxt' <- tc_hs_context mode ctxt
 
          -- See Note [Body kind of a HsQualTy]
-       ; ty' <- if isConstraintKind exp_kind
+       ; ty' <- if tcIsConstraintKind exp_kind
                 then tc_lhs_type mode ty constraintKind
                 else do { ek <- newOpenTypeKind
                                 -- The body kind (result of the function)
-                                -- can be * or #, hence newOpenTypeKind
+                                -- can be TYPE r, for any r, hence newOpenTypeKind
                         ; ty' <- tc_lhs_type mode ty ek
                         ; checkExpectedKind (unLoc ty) ty' liftedTypeKind exp_kind }
 
@@ -677,12 +728,6 @@ tc_hs_type mode rn_ty@(HsListTy _ elt_ty) exp_kind
        ; checkWiredInTyCon listTyCon
        ; checkExpectedKind rn_ty (mkListTy tau_ty) liftedTypeKind exp_kind }
 
-tc_hs_type mode rn_ty@(HsPArrTy _ elt_ty) exp_kind
-  = do { MASSERT( isTypeLevel (mode_level mode) )
-       ; tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
-       ; checkWiredInTyCon parrTyCon
-       ; checkExpectedKind rn_ty (mkPArrTy tau_ty) liftedTypeKind exp_kind }
-
 -- See Note [Distinguishing tuple kinds] in HsTypes
 -- See Note [Inferring tuple kinds]
 tc_hs_type mode rn_ty@(HsTupleTy _ HsBoxedOrConstraintTuple hs_tys) exp_kind
@@ -765,13 +810,10 @@ tc_hs_type mode rn_ty@(HsIParamTy _ (L _ n) ty) exp_kind
        ; checkExpectedKind rn_ty (mkClassPred ipClass [n',ty'])
            constraintKind exp_kind }
 
-tc_hs_type mode rn_ty@(HsEqTy _ ty1 ty2) exp_kind
-  = do { (ty1', kind1) <- tc_infer_lhs_type mode ty1
-       ; (ty2', kind2) <- tc_infer_lhs_type mode ty2
-       ; ty2'' <- checkExpectedKind (unLoc ty2) ty2' kind2 kind1
-       ; eq_tc <- tcLookupTyCon eqTyConName
-       ; let ty' = mkNakedTyConApp eq_tc [kind1, ty1', ty2'']
-       ; checkExpectedKind rn_ty ty' constraintKind exp_kind }
+tc_hs_type _ rn_ty@(HsStarTy _ _) exp_kind
+  -- Desugaring 'HsStarTy' to 'Data.Kind.Type' here means that we don't have to
+  -- handle it in 'coreView' and 'tcView'.
+  = checkExpectedKind rn_ty liftedTypeKind liftedTypeKind exp_kind
 
 --------- Literals
 tc_hs_type _ rn_ty@(HsTyLit _ (HsNumTy _ n)) exp_kind
@@ -797,10 +839,6 @@ tc_hs_type _ (HsWildCardTy wc) exp_kind
          -- we still need it to establish Note [The tcType invariant]
        }
 
--- disposed of by renamer
-tc_hs_type _ ty@(HsAppsTy {}) _
-  = pprPanic "tc_hs_tyep HsAppsTy" (ppr ty)
-
 tcWildCardOcc :: HsWildCardInfo -> Kind -> TcM TcType
 tcWildCardOcc wc_info exp_kind
   = do { wc_tv <- tcLookupTyVar (wildCardName wc_info)
@@ -810,7 +848,7 @@ tcWildCardOcc wc_info exp_kind
 
 ---------------------------
 -- | Call 'tc_infer_hs_type' and check its result against an expected kind.
-tc_infer_hs_type_ek :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
+tc_infer_hs_type_ek :: HasDebugCallStack => TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
 tc_infer_hs_type_ek mode hs_ty ek
   = do { (ty, k) <- tc_infer_hs_type mode hs_ty
        ; checkExpectedKind hs_ty ty k ek }
@@ -820,9 +858,9 @@ tupKindSort_maybe :: TcKind -> Maybe TupleSort
 tupKindSort_maybe k
   | Just (k', _) <- splitCastTy_maybe k = tupKindSort_maybe k'
   | Just k'      <- tcView k            = tupKindSort_maybe k'
-  | isConstraintKind k = Just ConstraintTuple
-  | isLiftedTypeKind k = Just BoxedTuple
-  | otherwise          = Nothing
+  | tcIsConstraintKind k = Just ConstraintTuple
+  | tcIsLiftedTypeKind k   = Just BoxedTuple
+  | otherwise            = Nothing
 
 tc_tuple :: HsType GhcRn -> TcTyMode -> TupleSort -> [LHsType GhcRn] -> TcKind -> TcM TcType
 tc_tuple rn_ty mode tup_sort tys exp_kind
@@ -890,11 +928,13 @@ tcInferApps :: TcTyMode
 --    Reason: we will return a type application like (fun_ty arg1 ... argn),
 --            and that type must be well-kinded
 --            See Note [The tcType invariant]
+-- Postcondition: Result kind is zonked.
 tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
   = do { traceTc "tcInferApps {" (ppr orig_hs_ty $$ ppr orig_hs_args $$ ppr fun_ki)
-       ; stuff <- go 1 [] empty_subst fun_ty orig_ki_binders orig_inner_ki orig_hs_args
+       ; (f_args, args, res_k) <- go 1 [] empty_subst fun_ty orig_ki_binders orig_inner_ki orig_hs_args
        ; traceTc "tcInferApps }" empty
-       ; return stuff }
+       ; res_k <- zonkTcType res_k  -- nec'y to uphold (IT4) of Note [The tcType invariant]
+       ; return (f_args, args, res_k) }
   where
     empty_subst                      = mkEmptyTCvSubst $ mkInScopeSet $
                                        tyCoVarsOfType fun_ki
@@ -911,7 +951,10 @@ tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
 
       -- no user-written args left. We're done!
     go _ acc_args subst fun ki_binders inner_ki []
-      = return (fun, reverse acc_args, substTy subst $ mkPiTys ki_binders inner_ki)
+      = return ( fun
+               , reverse acc_args
+               , nakedSubstTy subst $ mkPiTys ki_binders inner_ki)
+                 -- nakedSubstTy: see Note [The well-kinded type invariant]
 
       -- The function's kind has a binder. Is it visible or invisible?
     go n acc_args subst fun (ki_binder:ki_binders) inner_ki
@@ -919,7 +962,7 @@ tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
       | isInvisibleBinder ki_binder
         -- It's invisible. Instantiate.
       = do { traceTc "tcInferApps (invis)" (ppr ki_binder $$ ppr subst)
-           ; (subst', arg') <- tcInstBinder mb_kind_info subst ki_binder
+           ; (subst', arg') <- tcInstTyBinder mb_kind_info subst ki_binder
            ; go n (arg' : acc_args) subst' (mkNakedAppTy fun arg')
                 ki_binders inner_ki all_args }
 
@@ -928,11 +971,15 @@ tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
       = do { traceTc "tcInferApps (vis)" (vcat [ ppr ki_binder, ppr arg
                                                , ppr (tyBinderType ki_binder)
                                                , ppr subst ])
+           ; let exp_kind = nakedSubstTy subst $ tyBinderType ki_binder
+                            -- nakedSubstTy: see Note [The well-kinded type invariant]
            ; arg' <- addErrCtxt (funAppCtxt orig_hs_ty arg n) $
-                     tc_lhs_type mode arg (substTy subst $ tyBinderType ki_binder)
+                     tc_lhs_type mode arg exp_kind
+           ; traceTc "tcInferApps (vis 1)" (vcat [ ppr exp_kind
+                                                 , ppr (typeKind arg') ])
            ; let subst' = extendTvSubstBinderAndInScope subst ki_binder arg'
            ; go (n+1) (arg' : acc_args) subst'
-                (mkNakedAppTy fun arg')
+                (mkNakedAppTy fun arg') -- See Note [The well-kinded type invariant]
                 ki_binders inner_ki args }
 
        -- We've run out of known binders in the functions's kind.
@@ -948,7 +995,7 @@ tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
            ; let new_in_scope = tyCoVarsOfTypes [arg_k, res_k]
                  subst'       = zapped_subst `extendTCvInScopeSet` new_in_scope
            ; go n acc_args subst'
-                (fun `mkNakedCastTy` co)
+                (fun `mkNakedCastTy` co)  -- See Note [The well-kinded type invariant]
                 [mkAnonBinder arg_k]
                 res_k all_args }
       where
@@ -968,16 +1015,18 @@ tcTyApps :: TcTyMode
          -> TcType               -- ^ Function (could be knot-tied)
          -> TcKind               -- ^ Function kind (zonked)
          -> [LHsType GhcRn]      -- ^ Args
-         -> TcM (TcType, TcKind) -- ^ (f args, result kind)
+         -> TcM (TcType, TcKind) -- ^ (f args, result kind)   result kind is zonked
 -- Precondition: see precondition for tcInferApps
 tcTyApps mode orig_hs_ty fun_ty fun_ki args
   = do { (ty', _args, ki') <- tcInferApps mode Nothing orig_hs_ty fun_ty fun_ki args
-       ; return (ty', ki') }
+       ; return (ty' `mkNakedCastTy` mkRepReflCo ki', ki') }
+          -- The mkNakedCastTy is for (IT3) of Note [The tcType invariant]
 
 --------------------------
 -- Like checkExpectedKindX, but returns only the final type; convenient wrapper
 -- Obeys Note [The tcType invariant]
-checkExpectedKind :: HsType GhcRn   -- type we're checking (for printing)
+checkExpectedKind :: HasDebugCallStack
+                  => HsType GhcRn   -- type we're checking (for printing)
                   -> TcType         -- type we're checking (might be knot-tied)
                   -> TcKind         -- the known kind of that type
                   -> TcKind         -- the expected kind
@@ -985,7 +1034,8 @@ checkExpectedKind :: HsType GhcRn   -- type we're checking (for printing)
 checkExpectedKind hs_ty ty act exp
   = fstOf3 <$> checkExpectedKindX Nothing (ppr hs_ty) ty act exp
 
-checkExpectedKindX :: Maybe (VarEnv Kind)  -- Possibly, instantiations for kind vars
+checkExpectedKindX :: HasDebugCallStack
+                   => Maybe (VarEnv Kind)  -- Possibly, instantiations for kind vars
                    -> SDoc                 -- HsType whose kind we're checking
                    -> TcType               -- the type whose kind we're checking
                    -> TcKind               -- the known kind of that type, k
@@ -1030,19 +1080,20 @@ checkExpectedKindX mb_kind_env pp_hs_ty ty act_kind exp_kind
 -- | Instantiate @n@ invisible arguments to a type. If @n <= 0@, no instantiation
 -- occurs. If @n@ is too big, then all available invisible arguments are instantiated.
 -- (In other words, this function is very forgiving about bad values of @n@.)
+-- Why zonk the result? So that tcTyVar can obey (IT6) of Note [The tcType invariant]
 instantiateTyN :: Maybe (VarEnv Kind)              -- ^ Predetermined instantiations
                                                    -- (for assoc. type patterns)
                -> Int                              -- ^ @n@
-               -> [TyBinder] -> TcKind             -- ^ its kind
-               -> TcM ([TcType], TcKind)   -- ^ The inst'ed type, new args, kind
+               -> [TyBinder] -> TcKind             -- ^ its kind (zonked)
+               -> TcM ([TcType], TcKind)   -- ^ The inst'ed type, new args, kind (zonked)
 instantiateTyN mb_kind_env n bndrs inner_ki
   | n <= 0
   = return ([], ki)
 
   | otherwise
-  = do { (subst, inst_args) <- tcInstBinders empty_subst mb_kind_env inst_bndrs
+  = do { (subst, inst_args) <- tcInstTyBinders empty_subst mb_kind_env inst_bndrs
        ; let rebuilt_ki = mkPiTys leftover_bndrs inner_ki
-             ki'        = substTy subst rebuilt_ki
+       ; ki' <- zonkTcType (substTy subst rebuilt_ki)
        ; traceTc "instantiateTyN" (vcat [ ppr ki
                                         , ppr n
                                         , ppr subst
@@ -1098,7 +1149,7 @@ tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
                           -- here because we are also maintaining
                           -- Note [The tcType invariant], so we don't just
                           -- want to zonk the kind, leaving the TyVar
-                          -- un-zonked  (Trac #114873)
+                          -- un-zonked  (Trac #14873)
                           do { ty <- zonkTcTyVar tv
                              ; return (ty, typeKind ty) }
 
@@ -1110,9 +1161,6 @@ tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
                                 ; tc <- get_loopy_tc name tc_tc
                                 ; handle_tyfams tc tc_tc }
                              -- mkNakedTyConApp: see Note [Type-checking inside the knot]
-                 -- NB: we really should check if we're at the kind level
-                 -- and if the tycon is promotable if -XNoTypeInType is set.
-                 -- But this is a terribly large amount of work! Not worth it.
 
            AGlobal (ATyCon tc)
              -> do { check_tc tc
@@ -1122,13 +1170,14 @@ tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
              -> do { data_kinds <- xoptM LangExt.DataKinds
                    ; unless (data_kinds || specialPromotedDc dc) $
                        promotionErr name NoDataKindsDC
-                   ; type_in_type <- xoptM LangExt.TypeInType
-                   ; unless ( type_in_type ||
-                              ( isTypeLevel (mode_level mode) &&
-                                isLegacyPromotableDataCon dc ) ||
-                              ( isKindLevel (mode_level mode) &&
-                                specialPromotedDc dc ) ) $
-                       promotionErr name NoTypeInTypeDC
+                   ; when (isFamInstTyCon (dataConTyCon dc)) $
+                       -- see Trac #15245
+                       promotionErr name FamDataConPE
+                   ; let (_, _, _, theta, _, _) = dataConFullSig dc
+                   ; case dc_theta_illegal_constraint theta of
+                       Just pred -> promotionErr name $
+                                    ConstrainedDataConPE pred
+                       Nothing   -> pure ()
                    ; let tc = promoteDataCon dc
                    ; return (mkNakedTyConApp tc [], tyConKind tc) }
 
@@ -1137,16 +1186,11 @@ tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
            _  -> wrongThingErr "type" thing name }
   where
     check_tc :: TyCon -> TcM ()
-    check_tc tc = do { type_in_type <- xoptM LangExt.TypeInType
-                     ; data_kinds   <- xoptM LangExt.DataKinds
+    check_tc tc = do { data_kinds   <- xoptM LangExt.DataKinds
                      ; unless (isTypeLevel (mode_level mode) ||
                                data_kinds ||
                                isKindTyCon tc) $
-                       promotionErr name NoDataKindsTC
-                     ; unless (isTypeLevel (mode_level mode) ||
-                               type_in_type ||
-                               isLegacyPromotableTyCon tc) $
-                       promotionErr name NoTypeInTypeTC }
+                       promotionErr name NoDataKindsTC }
 
     -- if we are type-checking a type family tycon, we must instantiate
     -- any invisible arguments right away. Otherwise, we get #11246
@@ -1156,22 +1200,32 @@ tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
     handle_tyfams tc tc_tc
       | mightBeUnsaturatedTyCon tc_tc || mode_unsat mode
                                          -- This is where mode_unsat is used
-      = do { traceTc "tcTyVar2a" (ppr tc_tc $$ ppr tc_kind)
-           ; return (mkNakedTyConApp tc [], tc_kind) }
+      = do { tc_kind <- zonkTcType (tyConKind tc_tc)   -- (IT6) of Note [The tcType invariant]
+           ; traceTc "tcTyVar2a" (ppr tc_tc $$ ppr tc_kind)
+           ; return (mkNakedTyConApp tc [] `mkNakedCastTy` mkRepReflCo tc_kind, tc_kind) }
+              -- the mkNakedCastTy ensures (IT5) of Note [The tcType invariant]
 
       | otherwise
-      = do { (tc_args, kind) <- instantiateTyN Nothing (length (tyConBinders tc_tc))
+      = do { tc_kind <- zonkTcType (tyConKind tc_tc)
+           ; let (tc_kind_bndrs, tc_inner_ki) = splitPiTysInvisible tc_kind
+           ; (tc_args, kind) <- instantiateTyN Nothing (length (tyConBinders tc_tc))
                                                tc_kind_bndrs tc_inner_ki
-           ; let tc_ty = mkNakedTyConApp tc tc_args
+           ; let is_saturated = tc_args `lengthAtLeast` tyConArity tc_tc
+                 tc_ty
+                   | is_saturated = mkNakedTyConApp tc tc_args `mkNakedCastTy` mkRepReflCo kind
+                      -- mkNakedCastTy is for (IT5) of Note [The tcType invariant]
+                   | otherwise    = mkNakedTyConApp tc tc_args
+                      -- if the tycon isn't yet saturated, then we don't want mkNakedCastTy,
+                      -- because that means we'll have an unsaturated type family
+                      -- We don't need it anyway, because we can be sure that the
+                      -- type family kind will accept further arguments (because it is
+                      -- not yet saturated)
            -- tc and tc_ty must not be traced here, because that would
            -- force the evaluation of a potentially knot-tied variable (tc),
            -- and the typechecker would hang, as per #11708
            ; traceTc "tcTyVar2b" (vcat [ ppr tc_tc <+> dcolon <+> ppr tc_kind
                                        , ppr kind ])
            ; return (tc_ty, kind) }
-      where
-        tc_kind                      = tyConKind tc_tc
-        (tc_kind_bndrs, tc_inner_ki) = splitPiTysInvisible tc_kind
 
     get_loopy_tc :: Name -> TyCon -> TcM TyCon
     -- Return the knot-tied global TyCon if there is one
@@ -1185,22 +1239,17 @@ tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
                 _                -> do { traceTc "lk1 (loopy)" (ppr name)
                                        ; return tc_tc } }
 
-tcClass :: Name -> TcM (Class, TcKind)
-tcClass cls     -- Must be a class
-  = do { thing <- tcLookup cls
-       ; case thing of
-           ATcTyCon tc -> return (aThingErr "tcClass" cls, tyConKind tc)
-           AGlobal (ATyCon tc)
-             | Just cls <- tyConClass_maybe tc
-             -> return (cls, tyConKind tc)
-           _ -> wrongThingErr "class" thing cls }
-
-
-aThingErr :: String -> Name -> b
--- The type checker for types is sometimes called simply to
--- do *kind* checking; and in that case it ignores the type
--- returned. Which is a good thing since it may not be available yet!
-aThingErr str x = pprPanic "AThing evaluated unexpectedly" (text str <+> ppr x)
+    -- We cannot promote a data constructor with a context that contains
+    -- constraints other than equalities, so error if we find one.
+    -- See Note [Constraints handled in types] in Inst.
+    dc_theta_illegal_constraint :: ThetaType -> Maybe PredType
+    dc_theta_illegal_constraint = find go
+      where
+        go :: PredType -> Bool
+        go pred | Just tc <- tyConAppTyCon_maybe pred
+                = not $  tc `hasKey` eqTyConKey
+                      || tc `hasKey` heqTyConKey
+                | otherwise = True
 
 {-
 Note [Type-checking inside the knot]
@@ -1366,7 +1415,6 @@ in the e2 example, we'll desugar the type, zonking the kind unification
 variables as we go.  When we encounter the unconstrained kappa, we
 want to default it to '*', not to (Any *).
 
-
 Help functions for type applications
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 -}
@@ -1553,67 +1601,51 @@ tcWildCardBindersX new_wc maybe_skol_info wc_names thing_inside
   where
     scope_tvs
       | Just info <- maybe_skol_info = scopeTyVars2 info
-      | otherwise                    = tcExtendTyVarEnv2
+      | otherwise                    = tcExtendNameTyVarEnv
 
 -- | Kind-check a 'LHsQTyVars'. If the decl under consideration has a complete,
 -- user-supplied kind signature (CUSK), generalise the result.
 -- Used in 'getInitialKind' (for tycon kinds and other kinds)
 -- and in kind-checking (but not for tycon kinds, which are checked with
--- tcTyClDecls). See also Note [Complete user-supplied kind signatures] in
--- HsDecls.
+-- tcTyClDecls). See Note [CUSKs: complete user-supplied kind signatures]
+-- in HsDecls.
 --
 -- This function does not do telescope checking.
 kcLHsQTyVars :: Name              -- ^ of the thing being checked
              -> TyConFlavour      -- ^ What sort of 'TyCon' is being checked
              -> Bool              -- ^ True <=> the decl being checked has a CUSK
              -> LHsQTyVars GhcRn
-             -> TcM (Kind, r)     -- ^ The result kind, possibly with other info
-             -> TcM (TcTyCon, r)  -- ^ A suitably-kinded TcTyCon
+             -> TcM Kind          -- ^ The result kind
+             -> TcM TcTyCon       -- ^ A suitably-kinded TcTyCon
 kcLHsQTyVars name flav cusk
   user_tyvars@(HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = kv_ns
                                            , hsq_dependent = dep_names }
                       , hsq_explicit = hs_tvs }) thing_inside
   | cusk
-  = do { typeintype <- xoptM LangExt.TypeInType
-       ; let m_kind
-               | typeintype = Nothing
-               | otherwise  = Just liftedTypeKind
-                 -- without -XTypeInType, default all kind variables to have kind *
-
-       ; (scoped_kvs, (tc_tvs, (res_kind, stuff)))
-           <- solveEqualities $
-              tcImplicitTKBndrsX newSkolemTyVar m_kind skol_info kv_ns $
-              kcLHsTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside
+  = do { (scoped_kvs, (tc_tvs, res_kind))
+           <- solveEqualities                    $
+              tcImplicitQTKBndrs skol_info kv_ns $
+              kcLHsQTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside
 
            -- Now, because we're in a CUSK, quantify over the mentioned
            -- kind vars, in dependency order.
-       ; tc_tvs  <- mapM zonkTcTyVarToTyVar tc_tvs
-       ; res_kind <- zonkTcType res_kind
+       ; let tc_binders_unzonked = zipWith mk_tc_binder hs_tvs tc_tvs
+       ; dvs  <- zonkTcTypeAndSplitDepVars (mkSpecForAllTys scoped_kvs $
+                                            mkTyConKind tc_binders_unzonked res_kind)
+       ; qkvs <- quantifyTyVars emptyVarSet dvs
+         -- don't call tcGetGlobalTyCoVars. For associated types, it gets the
+         -- tyvars from the enclosing class -- but that's wrong. We *do* want
+         -- to quantify over those tyvars.
+
+       ; scoped_kvs <- mapM zonkTcTyVarToTyVar scoped_kvs
+       ; tc_tvs     <- mapM zonkTcTyVarToTyVar tc_tvs
+       ; res_kind   <- zonkTcType res_kind
        ; let tc_binders = zipWith mk_tc_binder hs_tvs tc_tvs
-             qkvs = tyCoVarsOfTypeWellScoped (mkTyConKind tc_binders res_kind)
-                   -- the visibility of tvs doesn't matter here; we just
-                   -- want the free variables not to include the tvs
-
-          -- If there are any meta-tvs left, the user has
-          -- lied about having a CUSK. Error.
-       ; let (meta_tvs, good_tvs) = partition isMetaTyVar qkvs
-          -- skip this check for associated types. Why?
-          -- Any variables mentioned in the definition will get defaulted,
-          -- except those that appear in the class head. Defaulted vars do
-          -- not concern us here (they are fully determined). Variables from
-          -- the class head will be fully determined whenever the class has
-          -- a CUSK, and an associated family has a CUSK only when the enclosing
-          -- class has one. So skipping is safe. But why is it necessary?
-          -- It's possible that a class variable has too low a TcLevel to have
-          -- fully settled down by this point, and so this check will get
-          -- a false positive.
-       ; when (not_associated && not (null meta_tvs)) $
-         report_non_cusk_tvs (qkvs ++ tc_tvs)
 
           -- If any of the scoped_kvs aren't actually mentioned in a binder's
           -- kind (or the return kind), then we're in the CUSK case from
           -- Note [Free-floating kind vars]
-       ; let all_tc_tvs        = good_tvs ++ tc_tvs
+       ; let all_tc_tvs        = scoped_kvs ++ tc_tvs
              all_mentioned_tvs = mapUnionVarSet (tyCoVarsOfType . tyVarKind)
                                                 all_tc_tvs
                                  `unionVarSet` tyCoVarsOfType res_kind
@@ -1621,8 +1653,9 @@ kcLHsQTyVars name flav cusk
                                            scoped_kvs
        ; reportFloatingKvs name flav all_tc_tvs unmentioned_kvs
 
-       ; let final_binders = map (mkNamedTyConBinder Specified) good_tvs
-                            ++ tc_binders
+       ; let final_binders =  map (mkNamedTyConBinder Inferred) qkvs
+                           ++ map (mkNamedTyConBinder Specified) scoped_kvs
+                           ++ tc_binders
              tycon = mkTcTyCon name (ppr user_tyvars) final_binders res_kind
                                (mkTyVarNamePairs (scoped_kvs ++ tc_tvs))
                                flav
@@ -1634,23 +1667,16 @@ kcLHsQTyVars name flav cusk
        ; traceTc "kcLHsQTyVars: cusk" $
          vcat [ ppr name, ppr kv_ns, ppr hs_tvs, ppr dep_names
               , ppr tc_tvs, ppr (mkTyConKind final_binders res_kind)
-              , ppr qkvs, ppr meta_tvs, ppr good_tvs, ppr final_binders ]
+              , ppr qkvs, ppr final_binders ]
 
-       ; return (tycon, stuff) }
+       ; return tycon }
 
   | otherwise
-  = do { typeintype <- xoptM LangExt.TypeInType
-
-             -- if -XNoTypeInType and we know all the implicits are kind vars,
-             -- just give the kind *. This prevents test
-             -- dependent/should_fail/KindLevelsB from compiling, as it should
-       ; let default_kind
-               | typeintype = Nothing
-               | otherwise  = Just liftedTypeKind
-           -- Why newSigTyVar?  See Note [Kind generalisation and sigTvs]
-       ; (scoped_kvs, (tc_tvs, (res_kind, stuff)))
-           <- kcImplicitTKBndrs kv_ns default_kind $
-              kcLHsTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside
+  = do { (scoped_kvs, (tc_tvs, res_kind))
+           -- Why kcImplicitTKBndrs which uses newSigTyVar?
+           -- See Note [Kind generalisation and sigTvs]
+           <- kcImplicitTKBndrs kv_ns $
+              kcLHsQTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside
 
        ; let   -- NB: Don't add scoped_kvs to tyConTyVars, because they
                -- must remain lined up with the binders
@@ -1662,14 +1688,9 @@ kcLHsQTyVars name flav cusk
        ; traceTc "kcLHsQTyVars: not-cusk" $
          vcat [ ppr name, ppr kv_ns, ppr hs_tvs, ppr dep_names
               , ppr tc_tvs, ppr (mkTyConKind tc_binders res_kind) ]
-       ; return (tycon, stuff) }
+       ; return tycon }
   where
     open_fam = tcFlavourIsOpen flav
-    not_associated = case flav of
-      DataFamilyFlavour assoc     -> not assoc
-      OpenTypeFamilyFlavour assoc -> not assoc
-      _                           -> True
-
     skol_info = TyConSkol flav name
 
     mk_tc_binder :: LHsTyVarBndr GhcRn -> TyVar -> TyConBinder
@@ -1680,42 +1701,27 @@ kcLHsQTyVars name flav cusk
        | otherwise
        = mkAnonTyConBinder tv
 
-    report_non_cusk_tvs all_tvs
-      = do { all_tvs <- mapM zonkTyCoVarKind all_tvs
-           ; let (_, tidy_tvs)         = tidyOpenTyCoVars emptyTidyEnv all_tvs
-                 (meta_tvs, other_tvs) = partition isMetaTyVar tidy_tvs
-
-           ; addErr $
-             vcat [ text "You have written a *complete user-suppled kind signature*,"
-                  , hang (text "but the following variable" <> plural meta_tvs <+>
-                          isOrAre meta_tvs <+> text "undetermined:")
-                       2 (vcat (map pp_tv meta_tvs))
-                  , text "Perhaps add a kind signature."
-                  , hang (text "Inferred kinds of user-written variables:")
-                       2 (vcat (map pp_tv other_tvs)) ] }
-      where
-        pp_tv tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
 kcLHsQTyVars _ _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars"
 
-kcLHsTyVarBndrs :: Bool   -- True <=> bump the TcLevel when bringing vars into scope
-                -> Bool   -- True <=> Default un-annotated tyvar
-                          --          binders to kind *
-                -> SkolemInfo
-                -> [LHsTyVarBndr GhcRn]
-                -> TcM r
-                -> TcM ([TyVar], r)
+kcLHsQTyVarBndrs :: Bool   -- True <=> bump the TcLevel when bringing vars into scope
+                 -> Bool   -- True <=> Default un-annotated tyvar
+                           --          binders to kind *
+                 -> SkolemInfo
+                 -> [LHsTyVarBndr GhcRn]
+                 -> TcM r
+                 -> TcM ([TyVar], r)
 -- There may be dependency between the explicit "ty" vars.
 -- So, we have to handle them one at a time.
-kcLHsTyVarBndrs _ _ _ [] thing
+kcLHsQTyVarBndrs _ _ _ [] thing
   = do { stuff <- thing; return ([], stuff) }
 
-kcLHsTyVarBndrs cusk open_fam skol_info (L _ hs_tv : hs_tvs) thing
+kcLHsQTyVarBndrs cusk open_fam skol_info (L _ hs_tv : hs_tvs) thing
   = do { tv_pair@(tv, _) <- kc_hs_tv hs_tv
                -- NB: Bring all tvs into scope, even non-dependent ones,
                -- as they're needed in type synonyms, data constructors, etc.
 
        ; (tvs, stuff) <- bind_unless_scoped tv_pair $
-                         kcLHsTyVarBndrs cusk open_fam skol_info hs_tvs $
+                         kcLHsQTyVarBndrs cusk open_fam skol_info hs_tvs $
                          thing
 
        ; return ( tv : tvs, stuff ) }
@@ -1732,38 +1738,83 @@ kcLHsTyVarBndrs cusk open_fam skol_info (L _ hs_tv : hs_tvs) thing
          -- `dependent` testsuite directory.
 
     kc_hs_tv :: HsTyVarBndr GhcRn -> TcM (TcTyVar, Bool)
-    kc_hs_tv (UserTyVar _ lname@(L _ name))
-      = do { tv_pair@(tv, in_scope) <- tcHsTyVarName newSkolemTyVar Nothing name
-
-             -- Open type/data families default their variables to kind *.
-             -- But don't default in-scope class tyvars, of course
-           ; when (open_fam && not in_scope) $
-             discardResult $ unifyKind (Just (HsTyVar noExt NotPromoted lname))
-                                       liftedTypeKind (tyVarKind tv)
-
-           ; return tv_pair }
-
-    kc_hs_tv (KindedTyVar _ (L _ name) lhs_kind)
+      -- Special handling for the case where the binder is already in scope
+      -- See Note [Associated type tyvar names] in Class and
+      --     Note [TyVar binders for associated decls] in HsDecls
+    kc_hs_tv (UserTyVar _ (L _ name))
+      = do { mb_tv <- tcLookupLcl_maybe name
+           ; case mb_tv of  -- See Note [TyVar binders for associated decls]
+                Just (ATyVar _ tv) -> return (tv, True)
+                _ -> do { kind <- if open_fam
+                                  then return liftedTypeKind
+                                  else newMetaKindVar
+                                  -- Open type/data families default their variables
+                                  -- variables to kind *.  But don't default in-scope
+                                  -- class tyvars, of course
+                        ; tv <- newSkolemTyVar name kind
+                        ; return (tv, False) } }
+
+    kc_hs_tv (KindedTyVar _ lname@(L _ name) lhs_kind)
       = do { kind <- tcLHsKindSig (TyVarBndrKindCtxt name) lhs_kind
-           ; tcHsTyVarName newSkolemTyVar (Just kind) name }
+           ; mb_tv <- tcLookupLcl_maybe name
+           ; case mb_tv of
+               Just (ATyVar _ tv)
+                 -> do { discardResult $
+                           unifyKind (Just (HsTyVar noExt NotPromoted lname))
+                                     kind (tyVarKind tv)
+                       ; return (tv, True) }
+               _ -> do { tv <- newSkolemTyVar name kind
+                       ; return (tv, False) } }
 
     kc_hs_tv (XTyVarBndr{}) = panic "kc_hs_tv"
 
-tcImplicitTKBndrs :: SkolemInfo
-                  -> [Name]
-                  -> TcM a
-                  -> TcM ([TcTyVar], a)
-tcImplicitTKBndrs = tcImplicitTKBndrsX newSkolemTyVar Nothing
+{- Note [Kind-checking tyvar binders for associated types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When kind-checking the type-variable binders for associated
+   data/newtype decls
+   family decls
+we behave specially for type variables that are already in scope;
+that is, bound by the enclosing class decl.  This is done in
+kcLHsQTyVarBndrs:
+  * The use of tcImplicitQTKBndrs
+  * The tcLookupLocal_maybe code in kc_hs_tv
+
+See Note [Associated type tyvar names] in Class and
+    Note [TyVar binders for associated decls] in HsDecls
+
+We must do the same for family instance decls, where the in-scope
+variables may be bound by the enclosing class instance decl.
+Hence the use of tcImplicitQTKBndrs in tcFamTyPats.
+-}
+
 
--- | Like 'tcImplicitTKBndrs', but uses 'newSigTyVar' to create tyvars
-tcImplicitTKBndrsSig :: SkolemInfo
-                     -> [Name]
-                     -> TcM a
-                     -> TcM ([TcTyVar], a)
-tcImplicitTKBndrsSig = tcImplicitTKBndrsX newSigTyVar Nothing
+--------------------------------------
+-- Implicit binders
+--------------------------------------
 
-tcImplicitTKBndrsX :: (Name -> Kind -> TcM TcTyVar) -- new_tv function
-                   -> Maybe Kind           -- Just k <=> assign all names this kind
+-- | Bring implicitly quantified type/kind variables into scope during
+-- kind checking. Uses SigTvs, as per Note [Use SigTvs in kind-checking pass]
+-- in TcTyClsDecls.
+kcImplicitTKBndrs :: [Name]     -- of the vars
+                  -> TcM a
+                  -> TcM ([TcTyVar], a)  -- returns the tyvars created
+                                         -- these are *not* dependency ordered
+kcImplicitTKBndrs var_ns thing_inside
+  = do { tkvs <- mapM newFlexiKindedSigTyVar var_ns
+       ; result <- tcExtendTyVarEnv tkvs thing_inside
+       ; return (tkvs, result) }
+
+
+tcImplicitTKBndrs, tcImplicitTKBndrsSig, tcImplicitQTKBndrs
+  :: SkolemInfo
+  -> [Name]
+  -> TcM a
+  -> TcM ([TcTyVar], a)
+tcImplicitTKBndrs    = tcImplicitTKBndrsX newFlexiKindedSkolemTyVar
+tcImplicitTKBndrsSig = tcImplicitTKBndrsX newFlexiKindedSigTyVar
+tcImplicitQTKBndrs   = tcImplicitTKBndrsX newFlexiKindedQTyVar
+
+tcImplicitTKBndrsX :: (Name -> TcM TcTyVar) -- new_tv function
                    -> SkolemInfo
                    -> [Name]
                    -> TcM a
@@ -1777,7 +1828,7 @@ tcImplicitTKBndrsX :: (Name -> Kind -> TcM TcTyVar) -- new_tv function
 --
 -- * Returned TcTyVars have zonked kinds
 --   See Note [Keeping scoped variables in order: Implicit]
-tcImplicitTKBndrsX new_tv m_kind skol_info tv_names thing_inside
+tcImplicitTKBndrsX new_tv skol_info tv_names thing_inside
   | null tv_names -- Short cut for the common case where there
                   -- are no implicit type variables to bind
   = do { result <- solveLocalEqualities thing_inside
@@ -1787,42 +1838,72 @@ tcImplicitTKBndrsX new_tv m_kind skol_info tv_names thing_inside
   = do { (skol_tvs, result)
            <- solveLocalEqualities $
               checkTvConstraints skol_info Nothing $
-              do { tv_pairs <- mapM (tcHsTyVarName new_tv m_kind) tv_names
-                 ; let must_scope_tvs = [ tv | (tv, False) <- tv_pairs ]
-                 ; result <- tcExtendTyVarEnv must_scope_tvs $
-                             thing_inside
-                 ; return (map fst tv_pairs, result) }
-
+              do { tkvs <- mapM new_tv tv_names
+                 ; result <- tcExtendTyVarEnv tkvs thing_inside
+                 ; return (tkvs, result) }
 
        ; skol_tvs <- mapM zonkTcTyCoVarBndr skol_tvs
           -- use zonkTcTyCoVarBndr because a skol_tv might be a SigTv
 
+          -- do a stable topological sort, following
+          -- Note [Ordering of implicit variables] in HsTypes
        ; let final_tvs = toposortTyVars skol_tvs
        ; traceTc "tcImplicitTKBndrs" (ppr tv_names $$ ppr final_tvs)
        ; return (final_tvs, result) }
 
--- | Bring implicitly quantified type/kind variables into scope during
--- kind checking. Uses SigTvs, as per Note [Use SigTvs in kind-checking pass]
--- in TcTyClsDecls.
-kcImplicitTKBndrs :: [Name]     -- of the vars
-                  -> Maybe Kind -- Just k <=> use k as the kind for all vars
-                                -- Nothing <=> use a meta-tyvar
+newFlexiKindedQTyVar :: Name -> TcM TcTyVar
+-- Make a new skolem for an implicit binder in a type/class/type
+-- instance declaration, with a flexi-kind
+-- But check for in-scope-ness, and if so return that instead
+newFlexiKindedQTyVar name
+  = do { mb_tv <- tcLookupLcl_maybe name
+       ; case mb_tv of
+           Just (ATyVar _ tv) -> return tv
+           _ -> newFlexiKindedSkolemTyVar name }
+
+newFlexiKindedTyVar :: (Name -> Kind -> TcM TyVar) -> Name -> TcM TyVar
+newFlexiKindedTyVar new_tv name
+  = do { kind <- newMetaKindVar
+       ; new_tv name kind }
+
+newFlexiKindedSkolemTyVar :: Name -> TcM TyVar
+newFlexiKindedSkolemTyVar = newFlexiKindedTyVar newSkolemTyVar
+
+newFlexiKindedSigTyVar :: Name -> TcM TyVar
+newFlexiKindedSigTyVar = newFlexiKindedTyVar newSigTyVar
+
+--------------------------------------
+-- Explicit binders
+--------------------------------------
+
+-- | Used during the "kind-checking" pass in TcTyClsDecls only,
+-- and even then only for data-con declarations.
+-- See Note [Use SigTvs in kind-checking pass] in TcTyClsDecls
+kcExplicitTKBndrs :: [LHsTyVarBndr GhcRn]
                   -> TcM a
-                  -> TcM ([TcTyVar], a)  -- returns the tyvars created
-                                         -- these are *not* dependency ordered
-kcImplicitTKBndrs var_ns m_kind thing_inside
-  = do { tkvs_pairs <- mapM (tcHsTyVarName newSigTyVar m_kind) var_ns
-       ; let must_scope_tkvs = [ tkv | (tkv, False) <- tkvs_pairs ]
-       ; result <- tcExtendTyVarEnv must_scope_tkvs $
-                   thing_inside
-       ; return (map fst tkvs_pairs, result) }
+                  -> TcM a
+kcExplicitTKBndrs [] thing_inside = thing_inside
+kcExplicitTKBndrs (L _ hs_tv : hs_tvs) thing_inside
+  = do { tv <- tcHsTyVarBndr newSigTyVar hs_tv
+       ; tcExtendTyVarEnv [tv] $
+         kcExplicitTKBndrs hs_tvs thing_inside }
 
 tcExplicitTKBndrs :: SkolemInfo
                   -> [LHsTyVarBndr GhcRn]
                   -> TcM a
                   -> TcM ([TcTyVar], a)
--- See also Note [Associated type tyvar names] in Class
 tcExplicitTKBndrs skol_info hs_tvs thing_inside
+-- Used for the forall'd binders in type signatures of various kinds:
+--     - function signatures
+--     - data con signatures in GADT-style decls
+--     - pattern synonym signatures
+--     - expression type signatures
+--
+-- Specifically NOT used for the binders of a data type
+-- or type family decl. So the forall'd variables always /shadow/
+-- anything already in scope, and the complications of
+-- tcHsQTyVarName to not apply.
+--
 -- This function brings into scope a telescope of binders as written by
 -- the user. At first blush, it would then seem that we should bring
 -- them into scope one at a time, bumping the TcLevel each time.
@@ -1854,46 +1935,29 @@ tcExplicitTKBndrs skol_info hs_tvs thing_inside
     bind_tvbs [] = do { result <- thing_inside
                       ; return ([], result) }
     bind_tvbs (L _ tvb : tvbs)
-      = do { (tv, in_scope) <- tcHsTyVarBndr newSkolemTyVar tvb
-           ; (if in_scope then id else tcExtendTyVarEnv [tv]) $
-           do { (tvs, result) <- bind_tvbs tvbs
-              ; return (tv : tvs, result) }}
+      = do { tv <- tcHsTyVarBndr newSkolemTyVar tvb
+           ; tcExtendTyVarEnv [tv] $
+        do { (tvs, result) <- bind_tvbs tvbs
+           ; return (tv : tvs, result) }}
 
     doc = sep (map ppr hs_tvs)
 
--- | Used during the "kind-checking" pass in TcTyClsDecls only.
--- See Note [Use SigTvs in kind-checking pass] in TcTyClsDecls
-kcExplicitTKBndrs :: [LHsTyVarBndr GhcRn]
-                  -> TcM a
-                  -> TcM a
-kcExplicitTKBndrs [] thing_inside = thing_inside
-kcExplicitTKBndrs (L _ hs_tv : hs_tvs) thing_inside
-  = do { (tv, _) <- tcHsTyVarBndr newSigTyVar hs_tv
-       ; tcExtendTyVarEnv [tv] $
-         kcExplicitTKBndrs hs_tvs thing_inside }
-
+-----------------
 tcHsTyVarBndr :: (Name -> Kind -> TcM TyVar)
-              -> HsTyVarBndr GhcRn -> TcM (TcTyVar, Bool)
+              -> HsTyVarBndr GhcRn -> TcM TcTyVar
 -- Return a TcTyVar, built using the provided function
 -- Typically the Kind inside the HsTyVarBndr will be a tyvar
 -- with a mutable kind in it.
 --
--- These variables might be in scope already (with associated types, for example).
--- This function then checks that the kind annotation (if any) matches the
--- kind of the in-scope type variable.
---
 -- Returned TcTyVar has the same name; no cloning
---
--- See also Note [Associated type tyvar names] in Class
---
--- Returns True iff the tyvar was already in scope
 tcHsTyVarBndr new_tv (UserTyVar _ (L _ tv_nm))
-  = tcHsTyVarName new_tv Nothing tv_nm
+  = newFlexiKindedTyVar new_tv tv_nm
 tcHsTyVarBndr new_tv (KindedTyVar _ (L _ tv_nm) lhs_kind)
   = do { kind <- tcLHsKindSig (TyVarBndrKindCtxt tv_nm) lhs_kind
-       ; tcHsTyVarName new_tv (Just kind) tv_nm }
+       ; new_tv tv_nm kind }
 tcHsTyVarBndr _ (XTyVarBndr _) = panic "tcHsTyVarBndr"
 
+-----------------
 newWildTyVar :: Name -> TcM TcTyVar
 -- ^ New unification variable for a wildcard
 newWildTyVar _name
@@ -1905,31 +1969,6 @@ newWildTyVar _name
        ; traceTc "newWildTyVar" (ppr tyvar)
        ; return tyvar }
 
--- | Produce a tyvar of the given name (with the kind provided, or
--- otherwise a meta-var kind). If
--- the name is already in scope, return the scoped variable, checking
--- to make sure the known kind matches any kind provided. The
--- second return value says whether the variable is in scope (True)
--- or not (False). (Use this for associated types, for example.)
-tcHsTyVarName :: (Name -> Kind -> TcM TcTyVar) -- new_tv function
-              -> Maybe Kind  -- Just k <=> use k as the variable's kind
-                             -- Nothing <=> use a meta-tyvar
-              -> Name -> TcM (TcTyVar, Bool)
-tcHsTyVarName new_tv m_kind name
-  = do { mb_tv <- tcLookupLcl_maybe name
-       ; case mb_tv of
-           Just (ATyVar _ tv)
-             -> do { whenIsJust m_kind $ \ kind ->
-                     discardResult $
-                     unifyKind (Just (HsTyVar noExt NotPromoted (noLoc name)))
-                       kind (tyVarKind tv)
-                   ; return (tv, True) }
-           _ -> do { kind <- case m_kind of
-                               Just kind -> return kind
-                               Nothing   -> newMetaKindVar
-                   ; tv <- new_tv name kind
-                   ; return (tv, False) }}
-
 --------------------------
 -- Bringing tyvars into scope
 --------------------------
@@ -1953,7 +1992,7 @@ scopeTyVars2 :: SkolemInfo -> [(Name, TcTyVar)] -> TcM a -> TcM a
 scopeTyVars2 skol_info prs thing_inside
   = fmap snd $ -- discard the TcEvBinds, which will always be empty
     checkConstraints skol_info (map snd prs) [{- no EvVars -}] $
-    tcExtendTyVarEnv2 prs $
+    tcExtendNameTyVarEnv prs $
     thing_inside
 
 ------------------
@@ -2110,7 +2149,7 @@ kcTyClTyVars :: Name -> TcM a -> TcM a
 kcTyClTyVars tycon_name thing_inside
   -- See Note [Use SigTvs in kind-checking pass] in TcTyClsDecls
   = do { tycon <- kcLookupTcTyCon tycon_name
-       ; tcExtendTyVarEnv2 (tcTyConScopedTyVars tycon) $ thing_inside }
+       ; tcExtendNameTyVarEnv (tcTyConScopedTyVars tycon) $ thing_inside }
 
 tcTyClTyVars :: Name
              -> ([TyConBinder] -> Kind -> TcM a) -> TcM a
@@ -2707,8 +2746,10 @@ It does sort checking and desugaring at the same time, in one single pass.
 tcLHsKindSig :: UserTypeCtxt -> LHsKind GhcRn -> TcM Kind
 tcLHsKindSig ctxt hs_kind
 -- See  Note [Recipe for checking a signature] in TcHsType
+-- Result is zonked
   = do { kind <- solveLocalEqualities $
                  tc_lhs_kind kindLevelMode hs_kind
+       ; traceTc "tcLHsKindSig" (ppr hs_kind $$ ppr kind)
        ; kind <- zonkPromoteType kind
          -- This zonk is very important in the case of higher rank kinds
          -- E.g. Trac #13879    f :: forall (p :: forall z (y::z). <blah>).
@@ -2718,6 +2759,7 @@ tcLHsKindSig ctxt hs_kind
          --      else we may fail to substitute properly
 
        ; checkValidType ctxt kind
+       ; traceTc "tcLHsKindSig2" (ppr kind)
        ; return kind }
 
 tc_lhs_kind :: TcTyMode -> LHsKind GhcRn -> TcM Kind
@@ -2731,11 +2773,12 @@ promotionErr name err
                    2 (parens reason))
   where
     reason = case err of
+               ConstrainedDataConPE pred
+                              -> text "it has an unpromotable context"
+                                 <+> quotes (ppr pred)
                FamDataConPE   -> text "it comes from a data family instance"
                NoDataKindsTC  -> text "perhaps you intended to use DataKinds"
                NoDataKindsDC  -> text "perhaps you intended to use DataKinds"
-               NoTypeInTypeTC -> text "perhaps you intended to use TypeInType"
-               NoTypeInTypeDC -> text "perhaps you intended to use TypeInType"
                PatSynPE       -> text "pattern synonyms cannot be promoted"
                PatSynExPE     -> sep [ text "the existential variables of a pattern synonym"
                                      , text "signature do not scope over the pattern" ]
@@ -2786,19 +2829,16 @@ reportFloatingKvs tycon_name flav all_tvs bad_tvs
        ; bad_tvs <- mapM zonkTcTyVarToTyVar bad_tvs
        ; let (tidy_env, tidy_all_tvs) = tidyOpenTyCoVars emptyTidyEnv all_tvs
              tidy_bad_tvs             = map (tidyTyVarOcc tidy_env) bad_tvs
-       ; typeintype <- xoptM LangExt.TypeInType
-       ; mapM_ (report typeintype tidy_all_tvs) tidy_bad_tvs }
+       ; mapM_ (report tidy_all_tvs) tidy_bad_tvs }
   where
-    report typeintype tidy_all_tvs tidy_bad_tv
+    report tidy_all_tvs tidy_bad_tv
       = addErr $
         vcat [ text "Kind variable" <+> quotes (ppr tidy_bad_tv) <+>
                text "is implicitly bound in" <+> ppr flav
              , quotes (ppr tycon_name) <> comma <+>
                text "but does not appear as the kind of any"
              , text "of its type variables. Perhaps you meant"
-             , text "to bind it" <+> ppWhen (not typeintype)
-                                            (text "(with TypeInType)") <+>
-                                 text "explicitly somewhere?"
+             , text "to bind it explicitly somewhere?"
              , ppWhen (not (null tidy_all_tvs)) $
                  hang (text "Type variables with inferred kinds:")
                  2 (ppr_tv_bndrs tidy_all_tvs) ]