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

9 files changed, 71 insertions, 114 deletions

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*