Drop support for kind constraints.wip/p547

This implements proposal 547 and closes ticket #22298.
See the proposal and ticket for motivation.

Compiler perf improves a bit

Metrics: compile_time/bytes allocated
-------------------------------------
  CoOpt_Singletons(normal)   -2.4% GOOD
            T12545(normal)   +1.0%
            T13035(normal)  -13.5% GOOD
            T18478(normal)   +0.9%
            T9872d(normal)   -2.2% GOOD

                 geo. mean   -0.2%
                 minimum    -13.5%
                 maximum     +1.0%

Metric Decrease:
    CoOpt_Singletons
    T13035
    T9872d

18 files changed, 114 insertions, 426 deletions

diff --git a/compiler/GHC/Core/DataCon.hs b/compiler/GHC/Core/DataCon.hs
index e3d6331195..1b9a4a1815 100644
--- a/compiler/GHC/Core/DataCon.hs
+++ b/compiler/GHC/Core/DataCon.hs
@@ -614,7 +614,7 @@ A DataCon has two different sets of type variables:
     (that is, they are TyVars/TyCoVars instead of ForAllTyBinders).
 
 Often (dcUnivTyVars ++ dcExTyCoVars) = dcUserTyVarBinders; but they may differ
-for three reasons, coming next:
+for two reasons, coming next:
 
 --- Reason (R1): Order of quantification in GADT syntax ---
 
@@ -703,55 +703,6 @@ Putting this all together, all variables used on the left-hand side of an
 equation in the dcEqSpec will be in dcUnivTyVars but *not* in
 dcUserTyVarBinders.
 
---- Reason (R3): Kind equalities may have been solved ---
-
-Consider now this case:
-
-  type family F a where
-    F Type = False
-    F _    = True
-  type T :: forall k. (F k ~ True) => k -> k -> Type
-  data T a b where
-    MkT :: T Maybe List
-
-The constraint F k ~ True tells us that T does not want to be indexed by, say,
-Int. Now let's consider the Core types involved:
-
-  axiom for F: axF[0] :: F Type ~ False
-               axF[1] :: forall a. F a ~ True   (a must be apart from Type)
-  tycon: T :: forall k. (F k ~ True) -> k -> k -> Type
-  wrapper: MkT :: T @(Type -> Type) @(Eq# (axF[1] (Type -> Type)) Maybe List
-  worker:  MkT :: forall k (c :: F k ~ True) (a :: k) (b :: k).
-                  (k ~# (Type -> Type), a ~# Maybe, b ~# List) =>
-                  T @k @c a b
-
-The key observation here is that the worker quantifies over c, while the wrapper
-does not. The worker *must* quantify over c, because c is a universal variable,
-and the result of the worker must be the type constructor applied to a sequence
-of plain type variables. But the wrapper certainly does not need to quantify over
-any evidence that F (Type -> Type) ~ True, as no variables are needed there.
-
-(Aside: the c here is a regular type variable, *not* a coercion variable. This
-is because F k ~ True is a *lifted* equality, not the unlifted ~#. This is why
-we see Eq# in the type of the wrapper: Eq# boxes the unlifted ~# to become a
-lifted ~. See also Note [The equality types story] in GHC.Builtin.Types.Prim about
-Eq# and Note [Constraints in kinds] in GHC.Core.TyCo.Rep about having this constraint
-in the first place.)
-
-In this case, we'll have these fields of the DataCon:
-
-  dcUserTyVarBinders = []    -- the wrapper quantifies over nothing
-  dcUnivTyVars = [k, c, a, b]
-  dcExTyCoVars = []  -- no existentials here, but a different constructor might have
-  dcEqSpec = [k ~# (Type -> Type), a ~# Maybe, b ~# List]
-
-Note that c is in the dcUserTyVars, but mentioned neither in the dcUserTyVarBinders nor
-in the dcEqSpec. We thus have Reason (R3): a variable might be missing from the
-dcUserTyVarBinders if its type's kind is Constraint.
-
-(At one point, we thought that the dcEqSpec would have to be non-empty. But that
-wouldn't account for silly cases like type T :: (True ~ True) => Type.)
-
 --- End of Reasons ---
 
 INVARIANT(dataConTyVars): the set of tyvars in dcUserTyVarBinders
@@ -1230,11 +1181,9 @@ mkDataCon name declared_infix prom_info
       -- fresh_names: make sure that the "anonymous" tyvars don't
       -- clash in name or unique with the universal/existential ones.
       -- Tiresome!  And unnecessary because these tyvars are never looked at
-    prom_theta_bndrs = [ mkInvisAnonTyConBinder (mkTyVar n t)
-     {- Invisible -}   | (n,t) <- fresh_names `zip` theta ]
     prom_arg_bndrs   = [ mkAnonTyConBinder (mkTyVar n t)
      {- Visible -}     | (n,t) <- dropList theta fresh_names `zip` map scaledThing orig_arg_tys ]
-    prom_bndrs       = prom_tv_bndrs ++ prom_theta_bndrs ++ prom_arg_bndrs
+    prom_bndrs       = prom_tv_bndrs ++ prom_arg_bndrs
     prom_res_kind    = orig_res_ty
     promoted         = mkPromotedDataCon con name prom_info prom_bndrs
                                          prom_res_kind roles rep_info
@@ -1861,20 +1810,15 @@ checkDataConTyVars dc@(MkData { dcUnivTyVars = univ_tvs
                               , dcExTyCoVars = ex_tvs
                               , dcEqSpec = eq_spec })
      -- use of sets here: (R1) from the Note
-  = mkUnVarSet depleted_worker_vars == mkUnVarSet depleted_wrapper_vars &&
+  = mkUnVarSet depleted_worker_vars == mkUnVarSet wrapper_vars &&
     all (not . is_eq_spec_var) wrapper_vars
   where
-    is_constraint_var v = typeTypeOrConstraint (tyVarKind v) == ConstraintLike
-      -- implements (R3) from the Note
-
     worker_vars = univ_tvs ++ ex_tvs
     eq_spec_tvs = mkUnVarSet (map eqSpecTyVar eq_spec)
     is_eq_spec_var = (`elemUnVarSet` eq_spec_tvs)  -- (R2) from the Note
-    depleted_worker_vars = filterOut (is_eq_spec_var <||> is_constraint_var)
-                                     worker_vars
+    depleted_worker_vars = filterOut is_eq_spec_var worker_vars
 
     wrapper_vars = dataConUserTyVars dc
-    depleted_wrapper_vars = filterOut is_constraint_var wrapper_vars
 
 dataConUserTyVarsNeedWrapper :: DataCon -> Bool
 -- Check whether the worker and wapper have the same type variables
diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs
index 4247e9f8dd..c90ff3b3c9 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs
+++ b/compiler/GHC/Core/TyCo/Rep.hs
@@ -325,113 +325,6 @@ Because the tyvar form above includes r in its result, we must
 be careful not to let any variables escape -- thus the last premise
 of the rule above.
 
-Note [Constraints in kinds]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Do we allow a type constructor to have a kind like
-   S :: Eq a => a -> Type
-
-No, we do not.  Doing so would mean would need a TyConApp like
-   S @k @(d :: Eq k) (ty :: k)
- and we have no way to build, or decompose, evidence like
- (d :: Eq k) at the type level.
-
-But we admit one exception: equality.  We /do/ allow, say,
-   MkT :: (a ~ b) => a -> b -> Type a b
-
-Why?  Because we can, without much difficulty.  Moreover
-we can promote a GADT data constructor (see TyCon
-Note [Promoted data constructors]), like
-  data GT a b where
-    MkGT : a -> a -> GT a a
-so programmers might reasonably expect to be able to
-promote MkT as well.
-
-How does this work?
-
-* In GHC.Tc.Validity.checkConstraintsOK we reject kinds that
-  have constraints other than (a~b) and (a~~b).
-
-* In Inst.tcInstInvisibleTyBinder we instantiate a call
-  of MkT by emitting
-     [W] co :: alpha ~# beta
-  and producing the elaborated term
-     MkT @alpha @beta (Eq# alpha beta co)
-  We don't generate a boxed "Wanted"; we generate only a
-  regular old /unboxed/ primitive-equality Wanted, and build
-  the box on the spot.
-
-* How can we get such a MkT?  By promoting a GADT-style data
-  constructor, written with an explicit equality constraint.
-     data T a b where
-       MkT :: (a~b) => a -> b -> T a b
-  See DataCon.mkPromotedDataCon
-  and Note [Promoted data constructors] in GHC.Core.TyCon
-
-* We support both homogeneous (~) and heterogeneous (~~)
-  equality.  (See Note [The equality types story]
-  in GHC.Builtin.Types.Prim for a primer on these equality types.)
-
-* How do we prevent a MkT having an illegal constraint like
-  Eq a?  We check for this at use-sites; see GHC.Tc.Gen.HsType.tcTyVar,
-  specifically dc_theta_illegal_constraint.
-
-* Notice that nothing special happens if
-    K :: (a ~# b) => blah
-  because (a ~# b) is not a predicate type, and is never
-  implicitly instantiated. (Mind you, it's not clear how you
-  could creates a type constructor with such a kind.) See
-  Note [Types for coercions, predicates, and evidence]
-
-* The existence of promoted MkT with an equality-constraint
-  argument is the (only) reason that the AnonTCB constructor
-  of TyConBndrVis carries an FunTyFlag.
-  For example, when we promote the data constructor
-     MkT :: forall a b. (a~b) => a -> b -> T a b
-  we get a PromotedDataCon with tyConBinders
-      Bndr (a :: Type)  (NamedTCB Inferred)
-      Bndr (b :: Type)  (NamedTCB Inferred)
-      Bndr (_ :: a ~ b) (AnonTCB FTF_C_T)
-      Bndr (_ :: a)     (AnonTCB FTF_T_T))
-      Bndr (_ :: b)     (AnonTCB FTF_T_T))
-
-* One might reasonably wonder who *unpacks* these boxes once they are
-  made. After all, there is no type-level `case` construct. The
-  surprising answer is that no one ever does. Instead, if a GADT
-  constructor is used on the left-hand side of a type family equation,
-  that occurrence forces GHC to unify the types in question. For
-  example:
-
-  data G a where
-    MkG :: G Bool
-
-  type family F (x :: G a) :: a where
-    F MkG = False
-
-  When checking the LHS `F MkG`, GHC sees the MkG constructor and then must
-  unify F's implicit parameter `a` with Bool. This succeeds, making the equation
-
-    F Bool (MkG @Bool <Bool>) = False
-
-  Note that we never need unpack the coercion. This is because type
-  family equations are *not* parametric in their kind variables. That
-  is, we could have just said
-
-  type family H (x :: G a) :: a where
-    H _ = False
-
-  The presence of False on the RHS also forces `a` to become Bool,
-  giving us
-
-    H Bool _ = False
-
-  The fact that any of this works stems from the lack of phase
-  separation between types and kinds (unlike the very present phase
-  separation between terms and types).
-
-  Once we have the ability to pattern-match on types below top-level,
-  this will no longer cut it, but it seems fine for now.
-
-
 Note [Arguments to type constructors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Because of kind polymorphism, in addition to type application we now
diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs
index f08d18ffc2..0311ba32bd 100644
--- a/compiler/GHC/Core/TyCon.hs
+++ b/compiler/GHC/Core/TyCon.hs
@@ -20,10 +20,10 @@ module GHC.Core.TyCon(
         PromDataConInfo(..), TyConFlavour(..),
 
         -- * TyConBinder
-        TyConBinder, TyConBndrVis(..), TyConPiTyBinder,
+        TyConBinder, TyConBndrVis(..),
         mkNamedTyConBinder, mkNamedTyConBinders,
         mkRequiredTyConBinder,
-        mkAnonTyConBinder, mkAnonTyConBinders, mkInvisAnonTyConBinder,
+        mkAnonTyConBinder, mkAnonTyConBinders,
         tyConBinderForAllTyFlag, tyConBndrVisForAllTyFlag, isNamedTyConBinder,
         isVisibleTyConBinder, isInvisibleTyConBinder, isVisibleTcbVis,
 
@@ -445,38 +445,29 @@ See #19367.
 
 ************************************************************************
 *                                                                      *
-                    TyConBinder, TyConPiTyBinder
+                    TyConBinder
 *                                                                      *
 ************************************************************************
 -}
 
 type TyConBinder     = VarBndr TyVar   TyConBndrVis
-type TyConPiTyBinder = VarBndr TyCoVar TyConBndrVis
-     -- Only PromotedDataCon has TyConPiTyBinders
-     -- See Note [Promoted GADT data constructors]
 
 data TyConBndrVis
-  = NamedTCB ForAllTyFlag
-  | AnonTCB  FunTyFlag
+  = NamedTCB ForAllTyFlag  -- ^ A named, forall-bound variable (invisible or not)
+  | AnonTCB                -- ^ an ordinary, visible type argument
 
 instance Outputable TyConBndrVis where
   ppr (NamedTCB flag) = ppr flag
-  ppr (AnonTCB af)    = ppr af
+  ppr AnonTCB         = text "AnonTCB"
 
 mkAnonTyConBinder :: TyVar -> TyConBinder
 -- Make a visible anonymous TyCon binder
 mkAnonTyConBinder tv = assert (isTyVar tv) $
-                       Bndr tv (AnonTCB visArgTypeLike)
+                       Bndr tv AnonTCB
 
 mkAnonTyConBinders :: [TyVar] -> [TyConBinder]
 mkAnonTyConBinders tvs = map mkAnonTyConBinder tvs
 
-mkInvisAnonTyConBinder :: TyVar -> TyConBinder
--- Make an /invisible/ anonymous TyCon binder
--- Not used much
-mkInvisAnonTyConBinder tv = assert (isTyVar tv) $
-                            Bndr tv (AnonTCB invisArgTypeLike)
-
 mkNamedTyConBinder :: ForAllTyFlag -> TyVar -> TyConBinder
 -- The odd argument order supports currying
 mkNamedTyConBinder vis tv = assert (isTyVar tv) $
@@ -499,10 +490,8 @@ tyConBinderForAllTyFlag :: TyConBinder -> ForAllTyFlag
 tyConBinderForAllTyFlag (Bndr _ vis) = tyConBndrVisForAllTyFlag vis
 
 tyConBndrVisForAllTyFlag :: TyConBndrVis -> ForAllTyFlag
-tyConBndrVisForAllTyFlag (NamedTCB vis)     = vis
-tyConBndrVisForAllTyFlag (AnonTCB af)    -- See Note [AnonTCB with constraint arg]
-  | isVisibleFunArg af = Required
-  | otherwise          = Inferred
+tyConBndrVisForAllTyFlag (NamedTCB vis) = vis
+tyConBndrVisForAllTyFlag AnonTCB        = Required
 
 isNamedTyConBinder :: TyConBinder -> Bool
 -- Identifies kind variables
@@ -517,7 +506,7 @@ isVisibleTyConBinder (Bndr _ tcb_vis) = isVisibleTcbVis tcb_vis
 
 isVisibleTcbVis :: TyConBndrVis -> Bool
 isVisibleTcbVis (NamedTCB vis) = isVisibleForAllTyFlag vis
-isVisibleTcbVis (AnonTCB af)   = isVisibleFunArg af
+isVisibleTcbVis AnonTCB        = True
 
 isInvisibleTyConBinder :: VarBndr tv TyConBndrVis -> Bool
 -- Works for IfaceTyConBinder too
@@ -530,7 +519,7 @@ mkTyConKind bndrs res_kind = foldr mk res_kind bndrs
   where
     mk :: TyConBinder -> Kind -> Kind
     mk (Bndr tv (NamedTCB vis)) k = mkForAllTy (Bndr tv vis) k
-    mk (Bndr tv (AnonTCB af))   k = mkNakedFunTy af (varType tv) k
+    mk (Bndr tv AnonTCB)        k = mkNakedFunTy FTF_T_T (varType tv) k
     -- mkNakedFunTy: see Note [Naked FunTy] in GHC.Builtin.Types
 
 -- | (mkTyConTy tc) returns (TyConApp tc [])
@@ -549,9 +538,7 @@ tyConInvisTVBinders tc_bndrs
    mk_binder (Bndr tv tc_vis) = mkTyVarBinder vis tv
       where
         vis = case tc_vis of
-                AnonTCB af    -- Note [AnonTCB with constraint arg]
-                  | isInvisibleFunArg af -> InferredSpec
-                  | otherwise            -> SpecifiedSpec
+                AnonTCB                  -> SpecifiedSpec
                 NamedTCB Required        -> SpecifiedSpec
                 NamedTCB (Invisible vis) -> vis
 
@@ -561,35 +548,7 @@ tyConVisibleTyVars tc
   = [ tv | Bndr tv vis <- tyConBinders tc
          , isVisibleTcbVis vis ]
 
-{- Note [AnonTCB with constraint arg]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-It's pretty rare to have an (AnonTCB af) binder with af=FTF_C_T or FTF_C_C.
-The only way it can occur is through equality constraints in kinds. These
-can arise in one of two ways:
-
-* In a PromotedDataCon whose kind has an equality constraint:
-
-    'MkT :: forall a b. (a~b) => blah
-
-  See Note [Constraints in kinds] in GHC.Core.TyCo.Rep, and
-  Note [Promoted data constructors] in this module.
-
-* In a data type whose kind has an equality constraint, as in the
-  following example from #12102:
-
-    data T :: forall a. (IsTypeLit a ~ 'True) => a -> Type
-
-When mapping an (AnonTCB FTF_C_x) to an ForAllTyFlag, in
-tyConBndrVisForAllTyFlag, we use "Inferred" to mean "the user cannot
-specify this arguments, even with visible type/kind application;
-instead the type checker must fill it in.
-
-We map (AnonTCB FTF_T_x) to Required, of course: the user must
-provide it. It would be utterly wrong to do this for constraint
-arguments, which is why AnonTCB must have the FunTyFlag in
-the first place.
-
-Note [Building TyVarBinders from TyConBinders]
+{- Note [Building TyVarBinders from TyConBinders]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We sometimes need to build the quantified type of a value from
 the TyConBinders of a type or class.  For that we need not
@@ -645,7 +604,7 @@ in GHC.Core.TyCo.Rep), so we change it to Specified when making MkT's PiTyBinder
 {- Note [The binders/kind/arity fields of a TyCon]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 All TyCons have this group of fields
-  tyConBinders   :: [TyConBinder/TyConPiTyBinder]
+  tyConBinders   :: [TyConBinder]
   tyConResKind   :: Kind
   tyConTyVars    :: [TyVar]   -- Cached = binderVars tyConBinders
                               --   NB: Currently (Aug 2018), TyCons that own this
@@ -656,7 +615,7 @@ All TyCons have this group of fields
 
 They fit together like so:
 
-* tyConBinders gives the telescope of type/coercion variables on the LHS of the
+* tyConBinders gives the telescope of type variables on the LHS of the
   type declaration.  For example:
 
     type App a (b :: k) = a b
@@ -673,7 +632,7 @@ They fit together like so:
 * See Note [VarBndrs, ForAllTyBinders, TyConBinders, and visibility] in GHC.Core.TyCo.Rep
   for what the visibility flag means.
 
-* Each TyConBinder tyConBinders has a TyVar (sometimes it is TyCoVar), and
+* Each TyConBinder in tyConBinders has a TyVar, and
   that TyVar may scope over some other part of the TyCon's definition. Eg
       type T a = a -> a
   we have
@@ -745,12 +704,12 @@ instance OutputableBndr tv => Outputable (VarBndr tv TyConBndrVis) where
   ppr (Bndr v bi) = ppr bi <+> parens (pprBndr LetBind v)
 
 instance Binary TyConBndrVis where
-  put_ bh (AnonTCB af)   = do { putByte bh 0; put_ bh af }
+  put_ bh AnonTCB        = do { putByte bh 0 }
   put_ bh (NamedTCB vis) = do { putByte bh 1; put_ bh vis }
 
   get bh = do { h <- getByte bh
               ; case h of
-                  0 -> do { af  <- get bh; return (AnonTCB af) }
+                  0 -> return AnonTCB
                   _ -> do { vis <- get bh; return (NamedTCB vis) } }
 
 
@@ -915,6 +874,9 @@ data TyConDetails =
     }
 
   -- | Represents promoted data constructor.
+  -- The kind of a promoted data constructor is the *wrapper* type of
+  -- the original data constructor. This type must not have constraints
+  -- (as checked in GHC.Tc.Gen.HsType.tcTyVar).
   | PromotedDataCon {          -- See Note [Promoted data constructors]
         dataCon       :: DataCon,   -- ^ Corresponding data constructor
         tcRepName     :: TyConRepName,
@@ -958,17 +920,6 @@ where
 tcTyConScopedTyVars are used only for MonoTcTyCons, not PolyTcTyCons.
 See Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon] in GHC.Tc.Utils.TcType.
 
-Note [Promoted GADT data constructors]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Any promoted GADT data constructor will have a type with equality
-constraints in its type; e.g.
-    K :: forall a b. (a ~# [b]) => a -> b -> T a
-
-So, when promoted to become a type constructor, the tyConBinders
-will include CoVars.  That is why we use [TyConPiTyBinder] for the
-tyconBinders field.  TyConPiTyBinder is a synonym for TyConBinder,
-but with the clue that the binder can be a CoVar not just a TyVar.
-
 Note [Representation-polymorphic TyCons]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 To check for representation-polymorphism directly in the typechecker,
@@ -1946,7 +1897,7 @@ mkFamilyTyCon name binders res_kind resVar flav parent inj
 -- as the data constructor itself; when we pretty-print
 -- the TyCon we add a quote; see the Outputable TyCon instance
 mkPromotedDataCon :: DataCon -> Name -> TyConRepName
-                  -> [TyConPiTyBinder] -> Kind -> [Role]
+                  -> [TyConBinder] -> Kind -> [Role]
                   -> PromDataConInfo -> TyCon
 mkPromotedDataCon con name rep_name binders res_kind roles rep_info
   = mkTyCon name binders res_kind roles $
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 76326b6c50..1ef00b0977 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -1732,7 +1732,7 @@ tyConBindersPiTyBinders :: [TyConBinder] -> [PiTyBinder]
 tyConBindersPiTyBinders = map to_tyb
   where
     to_tyb (Bndr tv (NamedTCB vis)) = Named (Bndr tv vis)
-    to_tyb (Bndr tv (AnonTCB af))   = Anon (tymult (varType tv)) af
+    to_tyb (Bndr tv AnonTCB)        = Anon (tymult (varType tv)) FTF_T_T
 
 -- | Make a dependent forall over an 'Inferred' variable
 mkTyCoInvForAllTy :: TyCoVar -> Type -> Type
@@ -1794,7 +1794,7 @@ mkTyConBindersPreferAnon vars inner_tkvs = assert (all isTyVar vars)
               = ( Bndr v (NamedTCB Required) : binders
                 , fvs `delVarSet` v `unionVarSet` kind_vars )
               | otherwise
-              = ( Bndr v (AnonTCB visArgTypeLike) : binders
+              = ( Bndr v AnonTCB : binders
                 , fvs `unionVarSet` kind_vars )
       where
         (binders, fvs) = go vs
@@ -2488,9 +2488,8 @@ Here are the key kinding rules for types
           -- in GHC.Builtin.Types.Prim
 
           torc is TYPE or CONSTRAINT
-          ty : body_torc rep
-          bndr_torc is Type or Constraint
-          ki : bndr_torc
+          ty : torc rep
+          ki : Type
           `a` is a type variable
           `a` is not free in rep
 (FORALL1) -----------------------
@@ -2508,10 +2507,6 @@ Here are the key kinding rules for types
 Note that:
 * (FORALL1) rejects (forall (a::Maybe). blah)
 
-* (FORALL1) accepts (forall (a :: t1~t2) blah), where the type variable
-  (not coercion variable!) 'a' has a kind (t1~t2) that in turn has kind
-  Constraint.  See Note [Constraints in kinds] in GHC.Core.TyCo.Rep.
-
 * (FORALL2) Surprise 1:
   See GHC.Core.TyCo.Rep Note [Unused coercion variable in ForAllTy]
 
@@ -2809,8 +2804,7 @@ tyConAppNeedsKindSig spec_inj_pos tc n_args
     injective_vars_of_binder :: TyConBinder -> FV
     injective_vars_of_binder (Bndr tv vis) =
       case vis of
-        AnonTCB af     | isVisibleFunArg af
-                       -> injectiveVarsOfType False -- conservative choice
+        AnonTCB        -> injectiveVarsOfType False -- conservative choice
                                               (varType tv)
         NamedTCB argf  | source_of_injectivity argf
                        -> unitFV tv `unionFV`
diff --git a/compiler/GHC/CoreToIface.hs b/compiler/GHC/CoreToIface.hs
index 4194939082..98595f0403 100644
--- a/compiler/GHC/CoreToIface.hs
+++ b/compiler/GHC/CoreToIface.hs
@@ -81,6 +81,7 @@ import GHC.Types.Cpr ( topCprSig )
 
 import GHC.Utils.Outputable
 import GHC.Utils.Panic
+import GHC.Utils.Panic.Plain
 import GHC.Utils.Misc
 
 import Data.Maybe ( isNothing, catMaybes )
@@ -353,12 +354,8 @@ toIfaceAppArgsX fr kind ty_args
         ts' = go (extendTCvSubst env tv t) res ts
 
     go env (FunTy { ft_af = af, ft_res = res }) (t:ts)
-      = IA_Arg (toIfaceTypeX fr t) argf (go env res ts)
-      where
-        argf | isVisibleFunArg af = Required
-             | otherwise          = Inferred
-             -- It's rare for a kind to have a constraint argument, but it
-             -- can happen. See Note [AnonTCB with constraint arg] in GHC.Core.TyCon.
+      = assert (isVisibleFunArg af)
+        IA_Arg (toIfaceTypeX fr t) Required (go env res ts)
 
     go env ty ts@(t1:ts1)
       | not (isEmptyTCvSubst env)
diff --git a/compiler/GHC/Iface/Type.hs b/compiler/GHC/Iface/Type.hs
index 3e41a25132..608a16af4b 100644
--- a/compiler/GHC/Iface/Type.hs
+++ b/compiler/GHC/Iface/Type.hs
@@ -205,7 +205,7 @@ mkIfaceTyConKind :: [IfaceTyConBinder] -> IfaceKind -> IfaceKind
 mkIfaceTyConKind bndrs res_kind = foldr mk res_kind bndrs
   where
     mk :: IfaceTyConBinder -> IfaceKind -> IfaceKind
-    mk (Bndr tv (AnonTCB af))   k = IfaceFunTy af many_ty (ifaceBndrType tv) k
+    mk (Bndr tv AnonTCB)        k = IfaceFunTy FTF_T_T many_ty (ifaceBndrType tv) k
     mk (Bndr tv (NamedTCB vis)) k = IfaceForAllTy (Bndr tv vis) k
 
 ifaceForAllSpecToBndrs :: [IfaceForAllSpecBndr] -> [IfaceForAllBndr]
@@ -892,12 +892,7 @@ pprIfaceTyConBinders suppress_sig = sep . map go
     go (Bndr (IfaceTvBndr bndr) vis) =
       -- See Note [Pretty-printing invisible arguments]
       case vis of
-        AnonTCB  af
-          | isVisibleFunArg af -> ppr_bndr (UseBndrParens True)
-          | otherwise          -> char '@' <> braces (ppr_bndr (UseBndrParens False))
-          -- The above case is rare. (See Note [AnonTCB with constraint arg]
-          --   in GHC.Core.TyCon.)
-          -- Should we print these differently?
+        AnonTCB            -> ppr_bndr (UseBndrParens True)
         NamedTCB Required  -> ppr_bndr (UseBndrParens True)
         NamedTCB Specified -> char '@' <> ppr_bndr (UseBndrParens True)
         NamedTCB Inferred  -> char '@' <> braces (ppr_bndr (UseBndrParens False))
diff --git a/compiler/GHC/Rename/HsType.hs b/compiler/GHC/Rename/HsType.hs
index aaaa249ba2..df53523597 100644
--- a/compiler/GHC/Rename/HsType.hs
+++ b/compiler/GHC/Rename/HsType.hs
@@ -13,7 +13,7 @@
 module GHC.Rename.HsType (
         -- Type related stuff
         rnHsType, rnLHsType, rnLHsTypes, rnContext, rnMaybeContext,
-        rnHsKind, rnLHsKind, rnLHsTypeArgs,
+        rnLHsKind, rnLHsTypeArgs,
         rnHsSigType, rnHsWcType, rnHsPatSigTypeBindingVars,
         HsPatSigTypeScoping(..), rnHsSigWcType, rnHsPatSigType,
         newTyVarNameRn,
@@ -468,35 +468,6 @@ rnImplicitTvBndrs ctx mb_assoc implicit_vs_with_dups thing_inside
 {-
 rnHsType is here because we call it from loadInstDecl, and I didn't
 want a gratuitous knot.
-
-Note [HsQualTy in kinds]
-~~~~~~~~~~~~~~~~~~~~~~
-I was wondering whether HsQualTy could occur only at TypeLevel.  But no,
-we can have a qualified type in a kind too. Here is an example:
-
-  type family F a where
-    F Bool = Nat
-    F Nat  = Type
-
-  type family G a where
-    G Type = Type -> Type
-    G ()   = Nat
-
-  data X :: forall k1 k2. (F k1 ~ G k2) => k1 -> k2 -> Type where
-    MkX :: X 'True '()
-
-See that k1 becomes Bool and k2 becomes (), so the equality is
-satisfied. If I write MkX :: X 'True 'False, compilation fails with a
-suitable message:
-
-  MkX :: X 'True '()
-    • Couldn't match kind ‘G Bool’ with ‘Nat’
-      Expected kind: G Bool
-        Actual kind: F Bool
-
-However: in a kind, the constraints in the HsQualTy must all be
-equalities; or at least, any kinds with a class constraint are
-uninhabited. See Note [Constraints in kinds] in GHC.Core.TyCo.Rep.
 -}
 
 data RnTyKiEnv
@@ -552,9 +523,6 @@ rnHsType ctxt ty = rnHsTyKi (mkTyKiEnv ctxt TypeLevel RnTypeBody) ty
 rnLHsKind  :: HsDocContext -> LHsKind GhcPs -> RnM (LHsKind GhcRn, FreeVars)
 rnLHsKind ctxt kind = rnLHsTyKi (mkTyKiEnv ctxt KindLevel RnTypeBody) kind
 
-rnHsKind  :: HsDocContext -> HsKind GhcPs -> RnM (HsKind GhcRn, FreeVars)
-rnHsKind ctxt kind = rnHsTyKi  (mkTyKiEnv ctxt KindLevel RnTypeBody) kind
-
 -- renaming a type only, not a kind
 rnLHsTypeArg :: HsDocContext -> LHsTypeArg GhcPs
                 -> RnM (LHsTypeArg GhcRn, FreeVars)
@@ -610,11 +578,11 @@ rnHsTyKi env ty@(HsForAllTy { hst_tele = tele, hst_body = tau })
                              , hst_tele = tele' , hst_body =  tau' }
                 , fvs) } }
 
-rnHsTyKi env ty@(HsQualTy { hst_ctxt = lctxt, hst_body = tau })
-  = do { data_kinds <- xoptM LangExt.DataKinds -- See Note [HsQualTy in kinds]
-       ; when (not data_kinds && isRnKindLevel env)
-              (addErr (dataKindsErr env ty))
-       ; (ctxt', fvs1) <- rnTyKiContext env lctxt
+rnHsTyKi env (HsQualTy { hst_ctxt = lctxt, hst_body = tau })
+  = do { -- no need to check type vs kind level here; this is
+         -- checked in the type checker. See
+         -- Note [No constraints in kinds] in GHC.Tc.Validity
+         (ctxt', fvs1) <- rnTyKiContext env lctxt
        ; (tau',  fvs2) <- rnLHsTyKi env tau
        ; return (HsQualTy { hst_xqual = noExtField, hst_ctxt = ctxt'
                           , hst_body =  tau' }
diff --git a/compiler/GHC/Rename/Module.hs b/compiler/GHC/Rename/Module.hs
index 97726a279c..fc6846e566 100644
--- a/compiler/GHC/Rename/Module.hs
+++ b/compiler/GHC/Rename/Module.hs
@@ -2064,14 +2064,7 @@ preceded by `type`, with the following restrictions:
 (R3) There are no strictness flags, because they don't make sense at
      the type level.
 
-(R4) The types of the constructors contain no constraints other than
-     equality constraints.  (This is the same restriction imposed
-     on constructors to be promoted with the DataKinds extension in
-     dc_theta_illegal_constraint called from GHC.Tc.Gen.HsType.tcTyVar,
-     but in that case the restriction is imposed if and when a data
-     constructor is used in a type, whereas here it is imposed at
-     the point of definition.  See also Note [Constraints in kinds]
-     in GHC.Core.TyCo.Rep.)
+(R4) The types of the constructors contain no constraints.
 
 (R5) There are no deriving clauses.
 
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index d13aa6b21d..00b37709bd 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -913,9 +913,10 @@ instance Diagnostic TcRnMessage where
                         2 (parens reason))
         where
           reason = case err of
-                     ConstrainedDataConPE pred
+                     ConstrainedDataConPE theta
                                     -> text "it has an unpromotable context"
-                                       <+> quotes (ppr pred)
+                                       <+> quotes (pprTheta theta)
+
                      FamDataConPE   -> text "it comes from a data family instance"
                      NoDataKindsDC  -> text "perhaps you intended to use DataKinds"
                      PatSynPE       -> text "pattern synonyms cannot be promoted"
@@ -3385,7 +3386,7 @@ pprHoleError ctxt (Hole { hole_ty, hole_occ}) (HoleError sort other_tvs hole_sko
           2 (text "standing for" <+> quotes pp_hole_type_with_kind)
       ConstraintHole ->
         hang (text "Found extra-constraints wildcard standing for")
-          2 (quotes $ pprType hole_ty)  -- always kind constraint
+          2 (quotes $ pprType hole_ty)  -- always kind Constraint
 
     hole_kind = typeKind hole_ty
 
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index 335e7c4965..f4d7d85ed1 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -3854,9 +3854,8 @@ data PromotionErr
   | FamDataConPE     -- Data constructor for a data family
                      -- See Note [AFamDataCon: not promoting data family constructors]
                      -- in GHC.Tc.Utils.Env.
-  | ConstrainedDataConPE PredType
-                     -- Data constructor with a non-equality context
-                     -- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep
+  | ConstrainedDataConPE ThetaType -- Data constructor with a context
+                                   -- See Note [No constraints in kinds] in GHC.Tc.Validity
   | PatSynPE         -- Pattern synonyms
                      -- See Note [Don't promote pattern synonyms] in GHC.Tc.Utils.Env
 
@@ -3866,28 +3865,27 @@ data PromotionErr
   | NoDataKindsDC    -- -XDataKinds not enabled (for a datacon)
 
 instance Outputable PromotionErr where
-  ppr ClassPE                     = text "ClassPE"
-  ppr TyConPE                     = text "TyConPE"
-  ppr PatSynPE                    = text "PatSynPE"
-  ppr FamDataConPE                = text "FamDataConPE"
-  ppr (ConstrainedDataConPE pred) = text "ConstrainedDataConPE"
-                                      <+> parens (ppr pred)
-  ppr RecDataConPE                = text "RecDataConPE"
-  ppr NoDataKindsDC               = text "NoDataKindsDC"
-  ppr TermVariablePE              = text "TermVariablePE"
+  ppr ClassPE              = text "ClassPE"
+  ppr TyConPE              = text "TyConPE"
+  ppr PatSynPE             = text "PatSynPE"
+  ppr FamDataConPE         = text "FamDataConPE"
+  ppr (ConstrainedDataConPE theta) = text "ConstrainedDataConPE" <+> parens (ppr theta)
+  ppr RecDataConPE         = text "RecDataConPE"
+  ppr NoDataKindsDC        = text "NoDataKindsDC"
+  ppr TermVariablePE       = text "TermVariablePE"
 
 pprPECategory :: PromotionErr -> SDoc
 pprPECategory = text . capitalise . peCategory
 
 peCategory :: PromotionErr -> String
-peCategory ClassPE                = "class"
-peCategory TyConPE                = "type constructor"
-peCategory PatSynPE               = "pattern synonym"
-peCategory FamDataConPE           = "data constructor"
+peCategory ClassPE              = "class"
+peCategory TyConPE              = "type constructor"
+peCategory PatSynPE             = "pattern synonym"
+peCategory FamDataConPE         = "data constructor"
 peCategory ConstrainedDataConPE{} = "data constructor"
-peCategory RecDataConPE           = "data constructor"
-peCategory NoDataKindsDC          = "data constructor"
-peCategory TermVariablePE         = "term variable"
+peCategory RecDataConPE         = "data constructor"
+peCategory NoDataKindsDC        = "data constructor"
+peCategory TermVariablePE       = "term variable"
 
 -- | Stores the information to be reported in a representation-polymorphism
 -- error message.
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 9d9f597db2..a0a2a51cee 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -137,7 +137,7 @@ import GHC.Data.Bag( unitBag )
 import Data.Function ( on )
 import Data.List.NonEmpty ( NonEmpty(..), nonEmpty )
 import qualified Data.List.NonEmpty as NE
-import Data.List ( find, mapAccumL )
+import Data.List ( mapAccumL )
 import Control.Monad
 import Data.Tuple( swap )
 
@@ -1613,8 +1613,7 @@ tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args
         case ki_binder of
 
         -- FunTy with PredTy on LHS, or ForAllTy with Inferred
-        Named (Bndr _ Inferred)          -> instantiate ki_binder inner_ki
-        Anon _ af | isInvisibleFunArg af -> instantiate ki_binder inner_ki
+        Named (Bndr kv Inferred)         -> instantiate kv inner_ki
 
         Named (Bndr _ Specified) ->  -- Visible kind application
           do { traceTc "tcInferTyApps (vis kind app)"
@@ -1644,9 +1643,9 @@ tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args
       ---------------- HsValArg: a normal argument (fun ty)
       (HsValArg arg : args, Just (ki_binder, inner_ki))
         -- next binder is invisible; need to instantiate it
-        | isInvisiblePiTyBinder ki_binder   -- FunTy with constraint on LHS;
-                                            -- or ForAllTy with Inferred or Specified
-         -> instantiate ki_binder inner_ki
+        | Named (Bndr kv flag) <- ki_binder
+        , isInvisibleForAllTyFlag flag   -- ForAllTy with Inferred or Specified
+         -> instantiate kv inner_ki
 
         -- "normal" case
         | otherwise
@@ -1984,23 +1983,16 @@ tcTyVar name         -- Could be a tyvar, a tycon, or a datacon
                        -- see #15245
                        promotionErr name FamDataConPE
                    ; let (_, _, _, theta, _, _) = dataConFullSig dc
-                   ; traceTc "tcTyVar" (ppr dc <+> ppr theta $$ ppr (dc_theta_illegal_constraint theta))
-                   ; case dc_theta_illegal_constraint theta of
-                       Just pred -> promotionErr name $
-                                    ConstrainedDataConPE pred
-                       Nothing   -> pure ()
+                   ; traceTc "tcTyVar" (ppr dc <+> ppr theta)
+                     -- promotionErr: Note [No constraints in kinds] in GHC.Tc.Validity
+                   ; unless (null theta) $
+                     promotionErr name (ConstrainedDataConPE theta)
                    ; let tc = promoteDataCon dc
                    ; return (mkTyConApp tc [], tyConKind tc) }
 
            APromotionErr err -> promotionErr name err
 
            _  -> wrongThingErr "type" thing name }
-  where
-    -- We cannot promote a data constructor with a context that contains
-    -- constraints other than equalities, so error if we find one.
-    -- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep
-    dc_theta_illegal_constraint :: ThetaType -> Maybe PredType
-    dc_theta_illegal_constraint = find (not . isEqPred)
 
 {-
 Note [Recursion through the kinds]
@@ -3715,9 +3707,10 @@ splitTyConKind skol_info in_scope avoid_occs kind
                     Nothing -> (reverse acc, substTy subst kind)
 
                     Just (Anon arg af, kind')
-                      -> go occs' uniqs' subst' (tcb : acc) kind'
+                      -> assert (af == FTF_T_T) $
+                         go occs' uniqs' subst' (tcb : acc) kind'
                       where
-                        tcb    = Bndr tv (AnonTCB af)
+                        tcb    = Bndr tv AnonTCB
                         arg'   = substTy subst (scaledThing arg)
                         name   = mkInternalName uniq occ loc
                         tv     = mkTcTyVar name arg' details
@@ -3858,7 +3851,8 @@ tcbVisibilities tc orig_args
     go fun_kind subst all_args@(arg : args)
       | Just (tcb, inner_kind) <- splitPiTy_maybe fun_kind
       = case tcb of
-          Anon _ af           -> AnonTCB af   : go inner_kind subst  args
+          Anon _ af           -> assert (af == FTF_T_T) $
+                                 AnonTCB      : go inner_kind subst  args
           Named (Bndr tv vis) -> NamedTCB vis : go inner_kind subst' args
                  where
                     subst' = extendTCvSubst subst tv arg
diff --git a/compiler/GHC/Tc/Solver/Rewrite.hs b/compiler/GHC/Tc/Solver/Rewrite.hs
index 252e2aba52..6892e9853f 100644
--- a/compiler/GHC/Tc/Solver/Rewrite.hs
+++ b/compiler/GHC/Tc/Solver/Rewrite.hs
@@ -1077,7 +1077,7 @@ ty_con_binders_ty_binders' = foldr go ([], False)
   where
     go (Bndr tv (NamedTCB vis)) (bndrs, _)
       = (Named (Bndr tv vis) : bndrs, True)
-    go (Bndr tv (AnonTCB af))   (bndrs, n)
-      = (Anon (tymult (tyVarKind tv)) af : bndrs, n)
+    go (Bndr tv AnonTCB)   (bndrs, n)
+      = (Anon (tymult (tyVarKind tv)) FTF_T_T : bndrs, n)
     {-# INLINE go #-}
 {-# INLINE ty_con_binders_ty_binders' #-}
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index c5f924cea8..32c64b6c7f 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -4069,8 +4069,7 @@ mkGADTVars tmpl_tvs dc_tvs subst
               tv_kind  = tyVarKind t_tv
               tv_kind' = substTy t_sub tv_kind
               t_tv'    = setTyVarKind t_tv tv_kind'
-              eqs' | isConstraintLikeKind (typeKind tv_kind') = eqs
-                   | otherwise = (t_tv', r_ty) : eqs
+              eqs'     = (t_tv', r_ty) : eqs
 
       | otherwise
       = pprPanic "mkGADTVars" (ppr tmpl_tvs $$ ppr subst)
diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs
index abbee42526..0b6b519028 100644
--- a/compiler/GHC/Tc/Utils/Instantiate.hs
+++ b/compiler/GHC/Tc/Utils/Instantiate.hs
@@ -43,7 +43,7 @@ import GHC.Prelude
 import GHC.Driver.Session
 import GHC.Driver.Env
 
-import GHC.Builtin.Types  ( heqDataCon, eqDataCon, integerTyConName )
+import GHC.Builtin.Types  ( heqDataCon, integerTyConName )
 import GHC.Builtin.Names
 
 import GHC.Hs
@@ -53,14 +53,12 @@ import GHC.Core.InstEnv
 import GHC.Core.Predicate
 import GHC.Core ( Expr(..), isOrphan ) -- For the Coercion constructor
 import GHC.Core.Type
-import GHC.Core.Multiplicity
-import GHC.Core.TyCo.Rep
 import GHC.Core.TyCo.Ppr ( debugPprType )
 import GHC.Core.Class( Class )
 import GHC.Core.DataCon
 
 import {-# SOURCE #-}   GHC.Tc.Gen.Expr( tcCheckPolyExpr, tcSyntaxOp )
-import {-# SOURCE #-}   GHC.Tc.Utils.Unify( unifyType, unifyKind )
+import {-# SOURCE #-}   GHC.Tc.Utils.Unify( unifyType )
 import GHC.Tc.Utils.Zonk
 import GHC.Tc.Utils.Monad
 import GHC.Tc.Types.Constraint
@@ -386,71 +384,21 @@ tcInstInvisibleTyBindersN n ty
 
     go n subst kind
       | n > 0
-      , Just (bndr, body) <- tcSplitPiTy_maybe kind
-      , isInvisiblePiTyBinder bndr
-      = do { (subst', arg) <- tcInstInvisibleTyBinder subst bndr
+      , Just (bndr, body) <- tcSplitForAllTyVarBinder_maybe kind
+      , isInvisibleForAllTyFlag (binderFlag bndr)
+      = do { (subst', arg) <- tcInstInvisibleTyBinder subst (binderVar bndr)
            ; (args, inner_ty) <- go (n-1) subst' body
            ; return (arg:args, inner_ty) }
       | otherwise
       = return ([], substTy subst kind)
 
-tcInstInvisibleTyBinder :: Subst -> PiTyVarBinder -> TcM (Subst, TcType)
+tcInstInvisibleTyBinder :: Subst -> TyVar -> TcM (Subst, TcType)
 -- Called only to instantiate kinds, in user-written type signatures
 
-tcInstInvisibleTyBinder subst (Named (Bndr tv _))
+tcInstInvisibleTyBinder subst tv
   = do { (subst', tv') <- newMetaTyVarX subst tv
        ; return (subst', mkTyVarTy tv') }
 
-tcInstInvisibleTyBinder subst (Anon ty af)
-  | Just (mk, k1, k2) <- get_eq_tys_maybe (substTy subst (scaledThing ty))
-    -- For kinds like (k1 ~ k2) => blah, we want to emit a unification
-    -- constraint for (k1 ~# k2) and return the argument (Eq# k1 k2)
-    -- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep
-    -- Equality is the *only* constraint currently handled in types.
-  = assert (isInvisibleFunArg af) $
-    do { co <- unifyKind Nothing k1 k2
-       ; return (subst, mk co) }
-
-  | otherwise  -- This should never happen
-               -- See GHC.Core.TyCo.Rep Note [Constraints in kinds]
-  = pprPanic "tcInvisibleTyBinder" (ppr ty)
-
--------------------------------
-get_eq_tys_maybe :: Type
-                 -> Maybe ( Coercion -> Type
-                             -- Given a coercion proving t1 ~# t2, produce the
-                             -- right instantiation for the PiTyVarBinder at hand
-                          , Type  -- t1
-                          , Type  -- t2
-                          )
--- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep
-get_eq_tys_maybe ty
-  -- Lifted heterogeneous equality (~~)
-  | Just (tc, [_, _, k1, k2]) <- splitTyConApp_maybe ty
-  , tc `hasKey` heqTyConKey
-  = Just (mkHEqBoxTy k1 k2, k1, k2)
-
-  -- Lifted homogeneous equality (~)
-  | Just (tc, [_, k1, k2]) <- splitTyConApp_maybe ty
-  , tc `hasKey` eqTyConKey
-  = Just (mkEqBoxTy k1 k2, k1, k2)
-
-  | otherwise
-  = Nothing
-
--- | This takes @a ~# b@ and returns @a ~~ b@.
-mkHEqBoxTy :: Type -> Type -> TcCoercion -> Type
-mkHEqBoxTy ty1 ty2 co
-  = mkTyConApp (promoteDataCon heqDataCon) [k1, k2, ty1, ty2, mkCoercionTy co]
-  where k1 = typeKind ty1
-        k2 = typeKind ty2
-
--- | This takes @a ~# b@ and returns @a ~ b@.
-mkEqBoxTy :: Type -> Type -> TcCoercion -> Type
-mkEqBoxTy ty1 ty2 co
-  = mkTyConApp (promoteDataCon eqDataCon) [k, ty1, ty2, mkCoercionTy co]
-  where k = typeKind ty1
-
 {- *********************************************************************
 *                                                                      *
         SkolemTvs (immutable)
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index 98b8e2ae76..28894d68ed 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -1342,7 +1342,7 @@ getDFunTyLitKey (CharTyLit n) = mkOccName Name.varName (show n)
 -- Always succeeds, even if it returns an empty list.
 tcSplitPiTys :: Type -> ([PiTyVarBinder], Type)
 tcSplitPiTys ty
-  = assert (all isTyBinder (fst sty) )   -- No CoVar binders here
+  = assert (all isTyBinder (fst sty))   -- No CoVar binders here
     sty
   where sty = splitPiTys ty
 
@@ -1365,7 +1365,7 @@ tcSplitForAllTyVarBinder_maybe _                = Nothing
 -- returning just the tyvars.
 tcSplitForAllTyVars :: Type -> ([TyVar], Type)
 tcSplitForAllTyVars ty
-  = assert (all isTyVar (fst sty) ) sty
+  = assert (all isTyVar (fst sty)) sty
   where sty = splitForAllTyCoVars ty
 
 -- | Like 'tcSplitForAllTyVars', but only splits 'ForAllTy's with 'Invisible'
diff --git a/compiler/GHC/Tc/Utils/Unify.hs-boot b/compiler/GHC/Tc/Utils/Unify.hs-boot
index 8afdbcd5ed..0d82ea613e 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs-boot
+++ b/compiler/GHC/Tc/Utils/Unify.hs-boot
@@ -12,6 +12,5 @@ import GHC.Tc.Types.Origin   ( CtOrigin, TypedThing )
 --   GHC.Tc.Utils.Unify and GHC.Tc.Utils.Instantiate
 
 unifyType :: Maybe TypedThing -> TcTauType -> TcTauType -> TcM TcCoercion
-unifyKind :: Maybe TypedThing -> TcTauType -> TcTauType -> TcM TcCoercion
 
 tcSubMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 5ac3377a33..949eb90d53 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -520,6 +520,8 @@ typeOrKindCtxt (DataKindCtxt {})          = OnlyKindCtxt
 typeOrKindCtxt (TySynKindCtxt {})         = OnlyKindCtxt
 typeOrKindCtxt (TyFamResKindCtxt {})      = OnlyKindCtxt
 
+-- These cases are also described in Note [No constraints in kinds], so any
+-- change here should be reflected in that note.
 typeOrKindCtxt (TySynCtxt {}) = BothTypeAndKindCtxt
   -- Type synonyms can have types and kinds on their RHSs
 typeOrKindCtxt (GhciCtxt {})  = BothTypeAndKindCtxt
@@ -543,7 +545,6 @@ typeLevelUserTypeCtxt ctxt = case typeOrKindCtxt ctxt of
 -- | Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the
 -- context for a kind of a type, where the arbitrary use of constraints is
 -- currently disallowed.
--- (See @Note [Constraints in kinds]@ in "GHC.Core.TyCo.Rep".)
 allConstraintsAllowed :: UserTypeCtxt -> Bool
 allConstraintsAllowed = typeLevelUserTypeCtxt
 
@@ -931,10 +932,9 @@ checkConstraintsOK :: ValidityEnv -> ThetaType -> Type -> TcM ()
 checkConstraintsOK ve theta ty
   | null theta                         = return ()
   | allConstraintsAllowed (ve_ctxt ve) = return ()
-  | otherwise
-  = -- We are in a kind, where we allow only equality predicates
-    -- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep, and #16263
-    checkTcM (all isEqPred theta) (env, TcRnConstraintInKind (tidyType env ty))
+  | otherwise -- We are unambiguously in a kind; see
+              -- Note [No constraints in kinds]
+  = failWithTcM (env, TcRnConstraintInKind (tidyType env ty))
   where env = ve_tidy_env ve
 
 checkVdqOK :: ValidityEnv -> [TyVarBinder] -> Type -> TcM ()
@@ -945,7 +945,25 @@ checkVdqOK ve tvbs ty = do
     no_vdq = all (isInvisibleForAllTyFlag . binderFlag) tvbs
     ValidityEnv{ve_tidy_env = env, ve_ctxt = ctxt} = ve
 
-{-
+{- Note [No constraints in kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+GHC does not allow constraints in kinds. Equality constraints
+in kinds were allowed from GHC 8.0, but this "feature" was removed
+as part of Proposal #547 (https://github.com/ghc-proposals/ghc-proposals/pull/547),
+which contains further context and motivation for the removal.
+
+The lack of constraints in kinds is enforced by checkConstraintsOK, which
+uses the UserTypeCtxt to determine if we are unambiguously checking a kind.
+There are two ambiguous contexts (constructor BothTypeAndKindCtxt of TypeOrKindCtxt)
+as written in typeOfKindCtxt:
+  - TySynCtxt: this is the RHS of a type synonym. We check the expansion of type
+    synonyms for constraints, so this is handled at the usage site of the synonym.
+  - GhciCtxt: This is the type in a :kind command. A constraint here does not cause
+    any trouble, because the type cannot be used to classify a type.
+
+Beyond these two cases, we also promote data constructors. We check for constraints
+in data constructor types in GHC.Tc.Gen.HsType.tcTyVar.
+
 Note [Liberal type synonyms]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
diff --git a/compiler/GHC/Types/Var.hs b/compiler/GHC/Types/Var.hs
index 69ba5b0d22..e95abc0855 100644
--- a/compiler/GHC/Types/Var.hs
+++ b/compiler/GHC/Types/Var.hs
@@ -681,10 +681,6 @@ Currently there are nine different uses of 'VarBndr':
 * TyCon.TyConBinder = VarBndr TyVar TyConBndrVis
   Binders of a TyCon; see TyCon in GHC.Core.TyCon
 
-* TyCon.TyConPiTyBinder = VarBndr TyCoVar TyConBndrVis
-  Binders of a PromotedDataCon
-  See Note [Promoted GADT data constructors] in GHC.Core.TyCon
-
 * IfaceType.IfaceForAllBndr     = VarBndr IfaceBndr ForAllTyFlag
 * IfaceType.IfaceForAllSpecBndr = VarBndr IfaceBndr Specificity
 * IfaceType.IfaceTyConBinder    = VarBndr IfaceBndr TyConBndrVis