Convert diagnostics in GHC.Tc.Validity to proper TcRnMessage.

- Add 19 new messages. Update test outputs accordingly.

- Pretty print suggest-extensions hints: remove space before
interspersed commas.

- Refactor Rank's MonoType constructors. Each MonoType constructor
should represent a specific case. With the Doc suggestion belonging
to the TcRnMessage diagnostics instead.

- Move Rank from Validity to its own `GHC.Tc.Types.Rank` module.

- Remove the outdated `check_irred_pred` check.

- Remove the outdated duplication check in `check_valid_theta`, which
was subsumed by `redundant-constraints`.

- Add missing test cases for quantified-constraints/T16474 & th/T12387a.

6 files changed, 535 insertions, 229 deletions

diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index 90be5526b9..c07a3a7057 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -9,10 +9,13 @@ module GHC.Tc.Errors.Ppr (
 
 import GHC.Prelude
 
-import GHC.Core.TyCo.Ppr (pprWithTYPE)
+import GHC.Core.Class (Class(..))
+import GHC.Core.TyCo.Ppr (pprKind, pprParendType, pprType, pprWithTYPE)
 import GHC.Core.Type
 import GHC.Data.Bag
 import GHC.Tc.Errors.Types
+import GHC.Tc.Types.Rank (Rank(..))
+import GHC.Tc.Utils.TcType (tcSplitForAllTyVars)
 import GHC.Types.Error
 import GHC.Types.Name (pprPrefixName)
 import GHC.Types.Name.Reader (pprNameProvenance)
@@ -169,6 +172,79 @@ instance Diagnostic TcRnMessage where
       -> mkSimpleDecorated $
            hang (text "Overloaded signature conflicts with monomorphism restriction")
               2 (ppr sig)
+    TcRnTupleConstraintInst _
+      -> mkSimpleDecorated $ text "You can't specify an instance for a tuple constraint"
+    TcRnAbstractClassInst clas
+      -> mkSimpleDecorated $
+           text "Cannot define instance for abstract class" <+>
+           quotes (ppr (className clas))
+    TcRnNoClassInstHead tau
+      -> mkSimpleDecorated $
+           hang (text "Instance head is not headed by a class:") 2 (pprType tau)
+    TcRnUserTypeError ty
+      -> mkSimpleDecorated (pprUserTypeErrorTy ty)
+    TcRnConstraintInKind ty
+      -> mkSimpleDecorated $
+           text "Illegal constraint in a kind:" <+> pprType ty
+    TcRnUnboxedTupleTypeFuncArg ty
+      -> mkSimpleDecorated $
+           sep [ text "Illegal unboxed tuple type as function argument:"
+               , pprType ty ]
+    TcRnLinearFuncInKind ty
+      -> mkSimpleDecorated $
+           text "Illegal linear function in a kind:" <+> pprType ty
+    TcRnForAllEscapeError ty kind
+      -> mkSimpleDecorated $ vcat
+           [ hang (text "Quantified type's kind mentions quantified type variable")
+                2 (text "type:" <+> quotes (ppr ty))
+           , hang (text "where the body of the forall has this kind:")
+                2 (quotes (pprKind kind)) ]
+    TcRnVDQInTermType ty
+      -> mkSimpleDecorated $ vcat
+           [ hang (text "Illegal visible, dependent quantification" <+>
+                   text "in the type of a term:")
+                2 (pprType ty)
+           , text "(GHC does not yet support this)" ]
+    TcRnIllegalEqualConstraints ty
+      -> mkSimpleDecorated $
+           text "Illegal equational constraint" <+> pprType ty
+    TcRnBadQuantPredHead ty
+      -> mkSimpleDecorated $
+           hang (text "Quantified predicate must have a class or type variable head:")
+              2 (pprType ty)
+    TcRnIllegalTupleConstraint ty
+      -> mkSimpleDecorated $
+           text "Illegal tuple constraint:" <+> pprType ty
+    TcRnNonTypeVarArgInConstraint ty
+      -> mkSimpleDecorated $
+           hang (text "Non type-variable argument")
+              2 (text "in the constraint:" <+> pprType ty)
+    TcRnIllegalImplicitParam ty
+      -> mkSimpleDecorated $
+           text "Illegal implicit parameter" <+> quotes (pprType ty)
+    TcRnIllegalConstraintSynonymOfKind kind
+      -> mkSimpleDecorated $
+           text "Illegal constraint synonym of kind:" <+> quotes (pprKind kind)
+    TcRnIllegalClassInst tcf
+      -> mkSimpleDecorated $
+           vcat [ text "Illegal instance for a" <+> ppr tcf
+                , text "A class instance must be for a class" ]
+    TcRnOversaturatedVisibleKindArg ty
+      -> mkSimpleDecorated $
+           text "Illegal oversaturated visible kind argument:" <+>
+           quotes (char '@' <> pprParendType ty)
+    TcRnBadAssociatedType clas tc
+      -> mkSimpleDecorated $
+           hsep [ text "Class", quotes (ppr clas)
+                , text "does not have an associated type", quotes (ppr tc) ]
+    TcRnForAllRankErr rank ty
+      -> let herald = case tcSplitForAllTyVars ty of
+               ([], _) -> text "Illegal qualified type:"
+               _       -> text "Illegal polymorphic type:"
+             extra = case rank of
+               MonoTypeConstraint -> text "A constraint must be a monotype"
+               _                  -> empty
+         in mkSimpleDecorated $ vcat [hang herald 2 (pprType ty), extra]
 
   diagnosticReason = \case
     TcRnUnknownMessage m
@@ -248,6 +324,44 @@ instance Diagnostic TcRnMessage where
       -> WarningWithFlag Opt_WarnMissingLocalSignatures
     TcRnOverloadedSig{}
       -> ErrorWithoutFlag
+    TcRnTupleConstraintInst{}
+      -> ErrorWithoutFlag
+    TcRnAbstractClassInst{}
+      -> ErrorWithoutFlag
+    TcRnNoClassInstHead{}
+      -> ErrorWithoutFlag
+    TcRnUserTypeError{}
+      -> ErrorWithoutFlag
+    TcRnConstraintInKind{}
+      -> ErrorWithoutFlag
+    TcRnUnboxedTupleTypeFuncArg{}
+      -> ErrorWithoutFlag
+    TcRnLinearFuncInKind{}
+      -> ErrorWithoutFlag
+    TcRnForAllEscapeError{}
+      -> ErrorWithoutFlag
+    TcRnVDQInTermType{}
+      -> ErrorWithoutFlag
+    TcRnIllegalEqualConstraints{}
+      -> ErrorWithoutFlag
+    TcRnBadQuantPredHead{}
+      -> ErrorWithoutFlag
+    TcRnIllegalTupleConstraint{}
+      -> ErrorWithoutFlag
+    TcRnNonTypeVarArgInConstraint{}
+      -> ErrorWithoutFlag
+    TcRnIllegalImplicitParam{}
+      -> ErrorWithoutFlag
+    TcRnIllegalConstraintSynonymOfKind{}
+      -> ErrorWithoutFlag
+    TcRnIllegalClassInst{}
+      -> ErrorWithoutFlag
+    TcRnOversaturatedVisibleKindArg{}
+      -> ErrorWithoutFlag
+    TcRnBadAssociatedType{}
+      -> ErrorWithoutFlag
+    TcRnForAllRankErr{}
+      -> ErrorWithoutFlag
 
   diagnosticHints = \case
     TcRnUnknownMessage m
@@ -327,6 +441,50 @@ instance Diagnostic TcRnMessage where
       -> noHints
     TcRnOverloadedSig{}
       -> noHints
+    TcRnTupleConstraintInst{}
+      -> noHints
+    TcRnAbstractClassInst{}
+      -> noHints
+    TcRnNoClassInstHead{}
+      -> noHints
+    TcRnUserTypeError{}
+      -> noHints
+    TcRnConstraintInKind{}
+      -> noHints
+    TcRnUnboxedTupleTypeFuncArg{}
+      -> [suggestExtension LangExt.UnboxedTuples]
+    TcRnLinearFuncInKind{}
+      -> noHints
+    TcRnForAllEscapeError{}
+      -> noHints
+    TcRnVDQInTermType{}
+      -> noHints
+    TcRnIllegalEqualConstraints{}
+      -> [suggestAnyExtension [LangExt.GADTs, LangExt.TypeFamilies]]
+    TcRnBadQuantPredHead{}
+      -> noHints
+    TcRnIllegalTupleConstraint{}
+      -> [suggestExtension LangExt.ConstraintKinds]
+    TcRnNonTypeVarArgInConstraint{}
+      -> [suggestExtension LangExt.FlexibleContexts]
+    TcRnIllegalImplicitParam{}
+      -> noHints
+    TcRnIllegalConstraintSynonymOfKind{}
+      -> [suggestExtension LangExt.ConstraintKinds]
+    TcRnIllegalClassInst{}
+      -> noHints
+    TcRnOversaturatedVisibleKindArg{}
+      -> noHints
+    TcRnBadAssociatedType{}
+      -> noHints
+    TcRnForAllRankErr rank _
+      -> case rank of
+           LimitedRank{}      -> [suggestExtension LangExt.RankNTypes]
+           MonoTypeRankZero   -> [suggestExtension LangExt.RankNTypes]
+           MonoTypeTyConArg   -> [suggestExtension LangExt.ImpredicativeTypes]
+           MonoTypeSynArg     -> [suggestExtension LangExt.LiberalTypeSynonyms]
+           MonoTypeConstraint -> [suggestExtension LangExt.QuantifiedConstraints]
+           _                  -> noHints
 
 messageWithInfoDiagnosticMessage :: UnitState
                                  -> ErrInfo
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index 82a908cf5a..827dc4a4da 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -14,13 +14,16 @@ import GHC.Prelude
 import GHC.Hs
 import {-# SOURCE #-} GHC.Tc.Types (TcIdSigInfo)
 import GHC.Tc.Types.Constraint
+import GHC.Tc.Types.Rank (Rank)
 import GHC.Types.Error
 import GHC.Types.Name (Name, OccName)
 import GHC.Types.Name.Reader
 import GHC.Types.SrcLoc
 import GHC.Unit.Types (Module)
 import GHC.Utils.Outputable
-import GHC.Core.Type (Type, Var)
+import GHC.Core.Class (Class)
+import GHC.Core.Type (Kind, Type, Var)
+import GHC.Core.TyCon (TyConFlavour)
 import GHC.Unit.State (UnitState)
 import GHC.Types.Basic
 
@@ -62,7 +65,6 @@ existence of these two types, which for now remain a "necessary evil".
 
 -}
 
-
 -- The majority of TcRn messages come with extra context about the error,
 -- and this newtype captures it. See Note [Migrating TcM messages].
 data ErrInfo = ErrInfo {
@@ -509,6 +511,297 @@ data TcRnMessage where
   -}
   TcRnOverloadedSig :: TcIdSigInfo -> TcRnMessage
 
+  {-| TcRnTupleConstraintInst is an error that occurs whenever an instance
+      for a tuple constraint is specified.
+
+      Examples(s):
+        class C m a
+        class D m a
+        f :: (forall a. Eq a => (C m a, D m a)) => m a
+        f = undefined
+
+      Test cases: quantified-constraints/T15334
+  -}
+  TcRnTupleConstraintInst :: !Class -> TcRnMessage
+
+  {-| TcRnAbstractClassInst is an error that occurs whenever an instance
+      of an abstract class is specified.
+
+      Examples(s):
+        -- A.hs-boot
+        module A where
+        class C a
+
+        -- B.hs
+        module B where
+        import {-# SOURCE #-} A
+        instance C Int where
+
+        -- A.hs
+        module A where
+        import B
+        class C a where
+          f :: a
+
+        -- Main.hs
+        import A
+        main = print (f :: Int)
+
+      Test cases: typecheck/should_fail/T13068
+  -}
+  TcRnAbstractClassInst :: !Class -> TcRnMessage
+
+  {-| TcRnNoClassInstHead is an error that occurs whenever an instance
+      head is not headed by a class.
+
+      Examples(s):
+        instance c
+
+      Test cases: typecheck/rename/T5513
+                  typecheck/rename/T16385
+  -}
+  TcRnNoClassInstHead :: !Type -> TcRnMessage
+
+  {-| TcRnUserTypeError is an error that occurs due to a user's custom type error,
+      which can be triggered by adding a `TypeError` constraint in a type signature
+      or typeclass instance.
+
+      Examples(s):
+        f :: TypeError (Text "This is a type error")
+        f = undefined
+
+      Test cases: typecheck/should_fail/CustomTypeErrors02
+                  typecheck/should_fail/CustomTypeErrors03
+  -}
+  TcRnUserTypeError :: !Type -> TcRnMessage
+
+  {-| TcRnConstraintInKind is an error that occurs whenever a constraint is specified
+      in a kind.
+
+      Examples(s):
+        data Q :: Eq a => Type where {}
+
+      Test cases: dependent/should_fail/T13895
+                  polykinds/T16263
+                  saks/should_fail/saks_fail004
+                  typecheck/should_fail/T16059a
+                  typecheck/should_fail/T18714
+  -}
+  TcRnConstraintInKind :: !Type -> TcRnMessage
+
+  {-| TcRnUnboxedTupleTypeFuncArg is an error that occurs whenever an unboxed tuple type
+      is specified as a function argument.
+
+      Examples(s):
+        -- T15073.hs
+        import T15073a
+        newtype Foo a = MkFoo a
+          deriving P
+
+        -- T15073a.hs
+        class P a where
+          p :: a -> (# a #)
+
+      Test cases: deriving/should_fail/T15073.hs
+                  deriving/should_fail/T15073a.hs
+                  typecheck/should_fail/T16059d
+  -}
+  TcRnUnboxedTupleTypeFuncArg :: !Type -> TcRnMessage
+
+  {-| TcRnLinearFuncInKind is an error that occurs whenever a linear function is
+      specified in a kind.
+
+      Examples(s):
+        data A :: * %1 -> *
+
+      Test cases: linear/should_fail/LinearKind
+                  linear/should_fail/LinearKind2
+                  linear/should_fail/LinearKind3
+  -}
+  TcRnLinearFuncInKind :: !Type -> TcRnMessage
+
+  {-| TcRnForAllEscapeError is an error that occurs whenever a quantified type's kind
+      mentions quantified type variable.
+
+      Examples(s):
+        type T :: TYPE (BoxedRep l)
+        data T = MkT
+
+      Test cases: unlifted-datatypes/should_fail/UnlDataNullaryPoly
+  -}
+  TcRnForAllEscapeError :: !Type -> !Kind -> TcRnMessage
+
+  {-| TcRnVDQInTermType is an error that occurs whenever a visible dependent quantification
+      is specified in the type of a term.
+
+      Examples(s):
+        a = (undefined :: forall k -> k -> Type) @Int
+
+      Test cases: dependent/should_fail/T15859
+                  dependent/should_fail/T16326_Fail1
+                  dependent/should_fail/T16326_Fail2
+                  dependent/should_fail/T16326_Fail3
+                  dependent/should_fail/T16326_Fail4
+                  dependent/should_fail/T16326_Fail5
+                  dependent/should_fail/T16326_Fail6
+                  dependent/should_fail/T16326_Fail7
+                  dependent/should_fail/T16326_Fail8
+                  dependent/should_fail/T16326_Fail9
+                  dependent/should_fail/T16326_Fail10
+                  dependent/should_fail/T16326_Fail11
+                  dependent/should_fail/T16326_Fail12
+                  dependent/should_fail/T17687
+                  dependent/should_fail/T18271
+  -}
+  TcRnVDQInTermType :: !Type -> TcRnMessage
+
+  {-| TcRnIllegalEqualConstraints is an error that occurs whenever an illegal equational
+      constraint is specified.
+
+      Examples(s):
+        blah :: (forall a. a b ~ a c) => b -> c
+        blah = undefined
+
+      Test cases: typecheck/should_fail/T17563
+  -}
+  TcRnIllegalEqualConstraints :: !Type -> TcRnMessage
+
+  {-| TcRnBadQuantPredHead is an error that occurs whenever a quantified predicate
+      lacks a class or type variable head.
+
+      Examples(s):
+        class (forall a. A t a => A t [a]) => B t where
+          type A t a :: Constraint
+
+      Test cases: quantified-constraints/T16474
+  -}
+  TcRnBadQuantPredHead :: !Type -> TcRnMessage
+
+  {-| TcRnIllegalTupleConstraint is an error that occurs whenever an illegal tuple
+      constraint is specified.
+
+      Examples(s):
+        g :: ((Show a, Num a), Eq a) => a -> a
+        g = undefined
+
+      Test cases: typecheck/should_fail/tcfail209a
+  -}
+  TcRnIllegalTupleConstraint :: !Type -> TcRnMessage
+
+  {-| TcRnNonTypeVarArgInConstraint is an error that occurs whenever a non type-variable
+      argument is specified in a constraint.
+
+      Examples(s):
+        data T
+        instance Eq Int => Eq T
+
+      Test cases: ghci/scripts/T13202
+                  ghci/scripts/T13202a
+                  polykinds/T12055a
+                  typecheck/should_fail/T10351
+                  typecheck/should_fail/T19187
+                  typecheck/should_fail/T6022
+                  typecheck/should_fail/T8883
+  -}
+  TcRnNonTypeVarArgInConstraint :: !Type -> TcRnMessage
+
+  {-| TcRnIllegalImplicitParam is an error that occurs whenever an illegal implicit
+      parameter is specified.
+
+      Examples(s):
+        type Bla = ?x::Int
+        data T = T
+        instance Bla => Eq T
+
+      Test cases: polykinds/T11466
+                  typecheck/should_fail/T8912
+                  typecheck/should_fail/tcfail041
+                  typecheck/should_fail/tcfail211
+                  typecheck/should_fail/tcrun045
+  -}
+  TcRnIllegalImplicitParam :: !Type -> TcRnMessage
+
+  {-| TcRnIllegalConstraintSynonymOfKind is an error that occurs whenever an illegal constraint
+      synonym of kind is specified.
+
+      Examples(s):
+        type Showish = Show
+        f :: (Showish a) => a -> a
+        f = undefined
+
+      Test cases: typecheck/should_fail/tcfail209
+  -}
+  TcRnIllegalConstraintSynonymOfKind :: !Type -> TcRnMessage
+
+  {-| TcRnIllegalClassInst is an error that occurs whenever a class instance is specified
+      for a non-class.
+
+      Examples(s):
+        type C1 a = (Show (a -> Bool))
+        instance C1 Int where
+
+      Test cases: polykinds/T13267
+  -}
+  TcRnIllegalClassInst :: !TyConFlavour -> TcRnMessage
+
+  {-| TcRnOversaturatedVisibleKindArg is an error that occurs whenever an illegal oversaturated
+      visible kind argument is specified.
+
+      Examples(s):
+        type family
+          F2 :: forall (a :: Type). Type where
+          F2 @a = Maybe a
+
+      Test cases: typecheck/should_fail/T15793
+                  typecheck/should_fail/T16255
+  -}
+  TcRnOversaturatedVisibleKindArg :: !Type -> TcRnMessage
+
+  {-| TcRnBadAssociatedType is an error that occurs whenever a class doesn't have an
+      associated type.
+
+      Examples(s):
+        $(do d <- instanceD (cxt []) (conT ''Eq `appT` conT ''Foo)
+                    [tySynInstD $ tySynEqn Nothing (conT ''Rep `appT` conT ''Foo) (conT ''Maybe)]
+             return [d])
+        ======>
+        instance Eq Foo where
+          type Rep Foo = Maybe
+
+      Test cases: th/T12387a
+  -}
+  TcRnBadAssociatedType :: {-Class-} !Name -> {-TyCon-} !Name -> TcRnMessage
+
+  {-| TcRnForAllRankErr is an error that occurs whenever an illegal ranked type
+      is specified.
+
+      Examples(s):
+        foo :: (a,b) -> (a~b => t) -> (a,b)
+        foo p x = p
+
+      Test cases:
+        - ghci/should_run/T15806
+        - indexed-types/should_fail/SimpleFail15
+        - typecheck/should_fail/T11355
+        - typecheck/should_fail/T12083a
+        - typecheck/should_fail/T12083b
+        - typecheck/should_fail/T16059c
+        - typecheck/should_fail/T16059e
+        - typecheck/should_fail/T17213
+        - typecheck/should_fail/T18939_Fail
+        - typecheck/should_fail/T2538
+        - typecheck/should_fail/T5957
+        - typecheck/should_fail/T7019
+        - typecheck/should_fail/T7019a
+        - typecheck/should_fail/T7809
+        - typecheck/should_fail/T9196
+        - typecheck/should_fail/tcfail127
+        - typecheck/should_fail/tcfail184
+        - typecheck/should_fail/tcfail196
+        - typecheck/should_fail/tcfail197
+  -}
+  TcRnForAllRankErr :: !Rank -> !Type -> TcRnMessage
+
 -- | Which parts of a record field are affected by a particular error or warning.
 data RecordFieldPart
   = RecordFieldConstructor !Name
@@ -537,4 +830,3 @@ data LevityCheckProvenance
   | LevityCheckInFunUse !(LHsExpr GhcTc)
   | LevityCheckInValidDataCon
   | LevityCheckInValidClass
-
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index 07422604c8..52ef132aa3 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -2501,7 +2501,7 @@ tcClassATs :: Name                    -- The class name (not knot-tied)
            -> TcM [ClassATItem]
 tcClassATs class_name cls ats at_defs
   = do {  -- Complain about associated type defaults for non associated-types
-         sequence_ [ failWithTc (badATErr class_name n)
+         sequence_ [ failWithTc (TcRnBadAssociatedType class_name n)
                    | n <- map at_def_tycon at_defs
                    , not (n `elemNameSet` at_names) ]
        ; mapM tc_at ats }
diff --git a/compiler/GHC/Tc/Types/Rank.hs b/compiler/GHC/Tc/Types/Rank.hs
new file mode 100644
index 0000000000..b38c6e8722
--- /dev/null
+++ b/compiler/GHC/Tc/Types/Rank.hs
@@ -0,0 +1,40 @@
+module GHC.Tc.Types.Rank (Rank(..))  where
+
+import GHC.Base (Bool)
+import GHC.Utils.Outputable (Outputable, (<+>), parens, ppr, text)
+
+{-
+Note [Higher rank types]
+~~~~~~~~~~~~~~~~~~~~~~~~
+Technically
+            Int -> forall a. a->a
+is still a rank-1 type, but it's not Haskell 98 (#5957).  So the
+validity checker allow a forall after an arrow only if we allow it
+before -- that is, with Rank2Types or RankNTypes
+-}
+
+data Rank = ArbitraryRank -- Any rank ok
+
+          | LimitedRank   -- Note [Higher rank types]
+                 Bool     -- Forall ok at top
+                 Rank     -- Use for function arguments
+
+          -- Monotypes that could be a polytype through an extension
+          | MonoTypeRankZero   -- RankNTypes
+          | MonoTypeTyConArg   -- ImpredicativeTypes
+          | MonoTypeSynArg     -- LiberalTypeSynonyms
+          | MonoTypeConstraint -- QuantifiedConstraints
+          --
+
+          | MustBeMonoType  -- Monotype regardless of flags
+
+instance Outputable Rank where
+  ppr ArbitraryRank      = text "ArbitraryRank"
+  ppr (LimitedRank top_forall_ok r)
+                         = text "LimitedRank" <+> ppr top_forall_ok
+                                              <+> parens (ppr r)
+  ppr MonoTypeRankZero   = text "MonoTypeRankZero"
+  ppr MonoTypeTyConArg   = text "MonoTypeTyConArg"
+  ppr MonoTypeSynArg     = text "MonoTypeSynArg"
+  ppr MonoTypeConstraint = text "MonoTypeConstraint"
+  ppr MustBeMonoType     = text "MustBeMonoType"
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 9ba071bc78..9e0f070056 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -9,13 +9,13 @@
 -}
 
 module GHC.Tc.Validity (
-  Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
+  Rank(..), UserTypeCtxt(..), checkValidType, checkValidMonoType,
   checkValidTheta,
   checkValidInstance, checkValidInstHead, validDerivPred,
   checkTySynRhs,
   checkValidCoAxiom, checkValidCoAxBranch,
   checkValidTyFamEqn, checkValidAssocTyFamDeflt, checkConsistentFamInst,
-  badATErr, arityErr,
+  arityErr,
   checkTyConTelescope,
   allDistinctTyVars
   ) where
@@ -42,6 +42,7 @@ import GHC.Core.Class
 import GHC.Core.TyCon
 import GHC.Core.Predicate
 import GHC.Tc.Types.Origin
+import GHC.Tc.Types.Rank
 import GHC.Tc.Errors.Types
 
 -- others:
@@ -70,7 +71,6 @@ import GHC.Builtin.Uniques  ( mkAlphaTyVarUnique )
 import qualified GHC.LanguageExtensions as LangExt
 
 import Control.Monad
-import Data.Bifunctor
 import Data.Foldable
 import Data.Function
 import Data.List        ( (\\), nub )
@@ -274,9 +274,7 @@ checkUserTypeError ctxt ty
   fail_with :: Type -> TcM ()
   fail_with msg = do { env0 <- tcInitTidyEnv
                      ; let (env1, tidy_msg) = tidyOpenType env0 msg
-                     ; failWithTcM (env1
-                                   , TcRnUnknownMessage $
-                                       mkPlainError noHints (pprUserTypeErrorTy tidy_msg))
+                     ; failWithTcM (env1, TcRnUserTypeError tidy_msg)
                      }
 
 
@@ -355,10 +353,9 @@ checkValidType ctxt ty
                         | otherwise  = r
 
              rank1 = gen_rank r1
-             rank0 = gen_rank r0
+             rank0 = gen_rank MonoTypeRankZero
 
-             r0 = rankZeroMonoType
-             r1 = LimitedRank True r0
+             r1 = LimitedRank True MonoTypeRankZero
 
              rank
                = case ctxt of
@@ -371,7 +368,7 @@ checkValidType ctxt ty
                  KindSigCtxt    -> rank1
                  StandaloneKindSigCtxt{} -> rank1
                  TypeAppCtxt | impred_flag -> ArbitraryRank
-                             | otherwise   -> tyConArgMonoType
+                             | otherwise   -> MonoTypeTyConArg
                     -- Normally, ImpredicativeTypes is handled in check_arg_type,
                     -- but visible type applications don't go through there.
                     -- So we do this check here.
@@ -434,48 +431,15 @@ checkTySynRhs ctxt ty
                     (do { dflags <- getDynFlags
                         ; expand <- initialExpandMode
                         ; check_pred_ty emptyTidyEnv dflags ctxt expand ty })
-         else addErrTcM (constraintSynErr emptyTidyEnv actual_kind) }
+         else addErrTcM ( emptyTidyEnv
+                        , TcRnIllegalConstraintSynonymOfKind (tidyKind emptyTidyEnv actual_kind)
+                        ) }
 
   | otherwise
   = return ()
   where
     actual_kind = tcTypeKind ty
 
-{-
-Note [Higher rank types]
-~~~~~~~~~~~~~~~~~~~~~~~~
-Technically
-            Int -> forall a. a->a
-is still a rank-1 type, but it's not Haskell 98 (#5957).  So the
-validity checker allow a forall after an arrow only if we allow it
-before -- that is, with Rank2Types or RankNTypes
--}
-
-data Rank = ArbitraryRank         -- Any rank ok
-
-          | LimitedRank   -- Note [Higher rank types]
-                 Bool     -- Forall ok at top
-                 Rank     -- Use for function arguments
-
-          | MonoType SDoc   -- Monotype, with a suggestion of how it could be a polytype
-
-          | MustBeMonoType  -- Monotype regardless of flags
-
-instance Outputable Rank where
-  ppr ArbitraryRank  = text "ArbitraryRank"
-  ppr (LimitedRank top_forall_ok r)
-                     = text "LimitedRank" <+> ppr top_forall_ok
-                                          <+> parens (ppr r)
-  ppr (MonoType msg) = text "MonoType" <+> parens msg
-  ppr MustBeMonoType = text "MustBeMonoType"
-
-rankZeroMonoType, tyConArgMonoType, synArgMonoType, constraintMonoType :: Rank
-rankZeroMonoType   = MonoType (text "Perhaps you intended to use RankNTypes")
-tyConArgMonoType   = MonoType (text "Perhaps you intended to use ImpredicativeTypes")
-synArgMonoType     = MonoType (text "Perhaps you intended to use LiberalTypeSynonyms")
-constraintMonoType = MonoType (vcat [ text "A constraint must be a monotype"
-                                    , text "Perhaps you intended to use QuantifiedConstraints" ])
-
 funArgResRank :: Rank -> (Rank, Rank)             -- Function argument and result
 funArgResRank (LimitedRank _ arg_rank) = (arg_rank, LimitedRank (forAllAllowed arg_rank) arg_rank)
 funArgResRank other_rank               = (other_rank, other_rank)
@@ -743,7 +707,7 @@ check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
                           , ve_rank = rank, ve_expand = expand }) ty
   | not (null tvbs && null theta)
   = do  { traceTc "check_type" (ppr ty $$ ppr rank)
-        ; checkTcM (forAllAllowed rank) (forAllTyErr env rank ty)
+        ; checkTcM (forAllAllowed rank) (env, TcRnForAllRankErr rank (tidyType env ty))
                 -- Reject e.g. (Maybe (?x::Int => Int)),
                 -- with a decent error message
 
@@ -753,7 +717,7 @@ check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
 
         ; checkTcM (all (isInvisibleArgFlag . binderArgFlag) tvbs
                          || vdqAllowed ctxt)
-                   (illegalVDQTyErr env ty)
+                   (env, TcRnVDQInTermType (tidyType env ty))
                 -- Reject visible, dependent quantification in the type of a
                 -- term (e.g., `f :: forall a -> a -> Maybe a`)
 
@@ -774,7 +738,7 @@ check_type (ve@ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
                           , ve_rank = rank })
            ty@(FunTy _ mult arg_ty res_ty)
   = do  { failIfTcM (not (linearityAllowed ctxt) && not (isManyDataConTy mult))
-                     (linearFunKindErr env ty)
+                     (env, TcRnLinearFuncInKind (tidyType env ty))
         ; check_type (ve{ve_rank = arg_rank}) arg_ty
         ; check_type (ve{ve_rank = res_rank}) res_ty }
   where
@@ -874,10 +838,10 @@ field to False.
 check_ubx_tuple :: ValidityEnv -> KindOrType -> [KindOrType] -> TcM ()
 check_ubx_tuple (ve@ValidityEnv{ve_tidy_env = env}) ty tys
   = do  { ub_tuples_allowed <- xoptM LangExt.UnboxedTuples
-        ; checkTcM ub_tuples_allowed (ubxArgTyErr env ty)
+        ; checkTcM ub_tuples_allowed (env, TcRnUnboxedTupleTypeFuncArg (tidyType env ty))
 
         ; impred <- xoptM LangExt.ImpredicativeTypes
-        ; let rank' = if impred then ArbitraryRank else tyConArgMonoType
+        ; let rank' = if impred then ArbitraryRank else MonoTypeTyConArg
                 -- c.f. check_arg_type
                 -- However, args are allowed to be unlifted, or
                 -- more unboxed tuples, so can't use check_arg_ty
@@ -912,10 +876,10 @@ check_arg_type type_syn (ve@ValidityEnv{ve_ctxt = ctxt, ve_rank = rank}) ty
         ; let rank' = case rank of          -- Predictive => must be monotype
                         -- Rank-n arguments to type synonyms are OK, provided
                         -- that LiberalTypeSynonyms is enabled.
-                        _ | type_syn       -> synArgMonoType
+                        _ | type_syn       -> MonoTypeSynArg
                         MustBeMonoType     -> MustBeMonoType  -- Monotype, regardless
                         _other | impred    -> ArbitraryRank
-                               | otherwise -> tyConArgMonoType
+                               | otherwise -> MonoTypeTyConArg
                         -- Make sure that MustBeMonoType is propagated,
                         -- so that we don't suggest -XImpredicativeTypes in
                         --    (Ord (forall a.a)) => a -> a
@@ -933,20 +897,6 @@ check_arg_type type_syn (ve@ValidityEnv{ve_ctxt = ctxt, ve_rank = rank}) ty
         ; check_type (ve{ve_ctxt = ctxt', ve_rank = rank'}) ty }
 
 ----------------------------------------
-forAllTyErr :: TidyEnv -> Rank -> Type -> (TidyEnv, TcRnMessage)
-forAllTyErr env rank ty
-   = ( env
-     , TcRnUnknownMessage $ mkPlainError noHints $
-       vcat [ hang herald 2 (ppr_tidy env ty)
-            , suggestion ] )
-  where
-    (tvs, _rho) = tcSplitForAllTyVars ty
-    herald | null tvs  = text "Illegal qualified type:"
-           | otherwise = text "Illegal polymorphic type:"
-    suggestion = case rank of
-                   LimitedRank {} -> text "Perhaps you intended to use RankNTypes"
-                   MonoType d     -> d
-                   _              -> Outputable.empty -- Polytype is always illegal
 
 -- | Reject type variables that would escape their escape through a kind.
 -- See @Note [Type variables escaping through kinds]@.
@@ -967,15 +917,10 @@ checkEscapingKind env tvbs theta tau =
 forAllEscapeErr :: TidyEnv -> [TyVarBinder] -> ThetaType -> Type -> Kind
                 -> (TidyEnv, TcRnMessage)
 forAllEscapeErr env tvbs theta tau tau_kind
-  = ( env
-    , TcRnUnknownMessage $ mkPlainError noHints $
-      vcat [ hang (text "Quantified type's kind mentions quantified type variable")
-                2 (text "type:" <+> quotes (ppr (mkSigmaTy tvbs theta tau)))
-                -- NB: Don't tidy this type since the tvbs were already tidied
-                -- previously, and re-tidying them will make the names of type
-                -- variables different from tau_kind.
-           , hang (text "where the body of the forall has this kind:")
-                2 (quotes (ppr_tidy env tau_kind)) ] )
+  -- NB: Don't tidy the sigma type since the tvbs were already tidied
+  -- previously, and re-tidying them will make the names of type
+  -- variables different from tau_kind.
+  = (env, TcRnForAllEscapeError (mkSigmaTy tvbs theta tau) (tidyKind env tau_kind))
 
 {-
 Note [Type variables escaping through kinds]
@@ -996,14 +941,6 @@ its binding site! This is not desirable, so we establish a validity check
 kinds in this way.
 -}
 
-ubxArgTyErr :: TidyEnv -> Type -> (TidyEnv, TcRnMessage)
-ubxArgTyErr env ty
-  = ( env
-    , TcRnUnknownMessage $ mkPlainError noHints $
-      vcat [ sep [ text "Illegal unboxed tuple type as function argument:"
-                 , ppr_tidy env ty ]
-                 , text "Perhaps you intended to use UnboxedTuples" ] )
-
 checkConstraintsOK :: ValidityEnv -> ThetaType -> Type -> TcM ()
 checkConstraintsOK ve theta ty
   | null theta                         = return ()
@@ -1011,28 +948,8 @@ checkConstraintsOK ve theta ty
   | 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) $
-    constraintTyErr (ve_tidy_env ve) ty
-
-constraintTyErr :: TidyEnv -> Type -> (TidyEnv, TcRnMessage)
-constraintTyErr env ty
-  = (env
-    , TcRnUnknownMessage $ mkPlainError noHints $
-        text "Illegal constraint in a kind:" <+> ppr_tidy env ty)
-
--- | Reject a use of visible, dependent quantification in the type of a term.
-illegalVDQTyErr :: TidyEnv -> Type -> (TidyEnv, TcRnMessage)
-illegalVDQTyErr env ty =
-  (env, TcRnUnknownMessage $ mkPlainError noHints $ vcat
-  [ hang (text "Illegal visible, dependent quantification" <+>
-          text "in the type of a term:")
-       2 (ppr_tidy env ty)
-  , text "(GHC does not yet support this)" ] )
-
--- | Reject uses of linear function arrows in kinds.
-linearFunKindErr :: TidyEnv -> Type -> (TidyEnv, TcRnMessage)
-linearFunKindErr env ty =
-  (env, TcRnUnknownMessage $ mkPlainError noHints $ text "Illegal linear function in a kind:" <+> ppr_tidy env ty)
+    checkTcM (all isEqPred theta) (env, TcRnConstraintInKind (tidyType env ty))
+  where env = ve_tidy_env ve
 
 {-
 Note [Liberal type synonyms]
@@ -1123,15 +1040,8 @@ check_valid_theta _ _ _ []
   = return ()
 check_valid_theta env ctxt expand theta
   = do { dflags <- getDynFlags
-       ; let dia m = TcRnUnknownMessage $
-               mkPlainDiagnostic (WarningWithFlag Opt_WarnDuplicateConstraints) noHints m
-       ; diagnosticTcM (notNull dups) (second dia (dupPredWarn env dups))
        ; traceTc "check_valid_theta" (ppr theta)
        ; mapM_ (check_pred_ty env dflags ctxt expand) theta }
-  where
-    (_,dups) = removeDups nonDetCmpType theta
-    -- It's OK to use nonDetCmpType because dups only appears in the
-    -- warning
 
 -------------------------
 {- Note [Validity checking for constraints]
@@ -1169,7 +1079,7 @@ check_pred_ty env dflags ctxt expand pred
     rank | xopt LangExt.QuantifiedConstraints dflags
          = ArbitraryRank
          | otherwise
-         = constraintMonoType
+         = MonoTypeConstraint
 
     ve :: ValidityEnv
     ve = ValidityEnv{ ve_tidy_env = env
@@ -1203,7 +1113,7 @@ check_pred_help under_syn env dflags ctxt pred
               -- in Note [Lift equality constraints when quantifying] in GHC.Tc.Utils.TcType
 
       ForAllPred _ theta head -> check_quant_pred env dflags ctxt pred theta head
-      IrredPred {}            -> check_irred_pred under_syn env dflags pred
+      _                       -> return ()
 
 check_eq_pred :: TidyEnv -> DynFlags -> PredType -> TcM ()
 check_eq_pred env dflags pred
@@ -1211,7 +1121,7 @@ check_eq_pred env dflags pred
             -- families are permitted
     checkTcM (xopt LangExt.TypeFamilies dflags
               || xopt LangExt.GADTs dflags)
-             (eqPredTyErr env pred)
+             (env, TcRnIllegalEqualConstraints (tidyType env pred))
 
 check_quant_pred :: TidyEnv -> DynFlags -> UserTypeCtxt
                  -> PredType -> ThetaType -> PredType -> TcM ()
@@ -1229,7 +1139,7 @@ check_quant_pred env dflags ctxt pred theta head_pred
                                -- in check_pred_ty
             IrredPred {}      | hasTyVarHead head_pred
                               -> return ()
-            _                 -> failWithTcM (badQuantHeadErr env pred)
+            _                 -> failWithTcM (env, TcRnBadQuantPredHead (tidyType env pred))
 
          -- Check for termination
        ; unless (xopt LangExt.UndecidableInstances dflags) $
@@ -1240,23 +1150,11 @@ check_tuple_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> [
 check_tuple_pred under_syn env dflags ctxt pred ts
   = do { -- See Note [ConstraintKinds in predicates]
          checkTcM (under_syn || xopt LangExt.ConstraintKinds dflags)
-                  (predTupleErr env pred)
+                  (env, TcRnIllegalTupleConstraint (tidyType env pred))
        ; mapM_ (check_pred_help under_syn env dflags ctxt) ts }
     -- This case will not normally be executed because without
     -- -XConstraintKinds tuple types are only kind-checked as *
 
-check_irred_pred :: Bool -> TidyEnv -> DynFlags -> PredType -> TcM ()
-check_irred_pred under_syn env dflags pred
-    -- The predicate looks like (X t1 t2) or (x t1 t2) :: Constraint
-    -- where X is a type function
-  =      -- If it looks like (x t1 t2), require ConstraintKinds
-         --   see Note [ConstraintKinds in predicates]
-         -- But (X t1 t2) is always ok because we just require ConstraintKinds
-         -- at the definition site (#9838)
-    failIfTcM (not under_syn && not (xopt LangExt.ConstraintKinds dflags)
-                            && hasTyVarHead pred)
-              (predIrredErr env pred)
-
 {- Note [ConstraintKinds in predicates]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Don't check for -XConstraintKinds under a type synonym, because that
@@ -1278,12 +1176,12 @@ check_class_pred env dflags ctxt pred cls tys
 
   | isIPClass cls
   = do { check_arity
-       ; checkTcM (okIPCtxt ctxt) (badIPPred env pred) }
+       ; checkTcM (okIPCtxt ctxt) (env, TcRnIllegalImplicitParam (tidyType env pred)) }
 
   | otherwise     -- Includes Coercible
   = do { check_arity
        ; checkSimplifiableClassConstraint env dflags ctxt cls tys
-       ; checkTcM arg_tys_ok (predTyVarErr env pred) }
+       ; checkTcM arg_tys_ok (env, TcRnNonTypeVarArgInConstraint (tidyType env pred)) }
   where
     check_arity = checkTc (tys `lengthIs` classArity cls)
                           (tyConArityErr (classTyCon cls) tys)
@@ -1428,58 +1326,6 @@ checkThetaCtxt ctxt theta env
            , vcat [ text "In the context:" <+> pprTheta (tidyTypes env theta)
                   , text "While checking" <+> pprUserTypeCtxt ctxt ] )
 
-eqPredTyErr, predTupleErr, predIrredErr,
-   badQuantHeadErr :: TidyEnv -> PredType -> (TidyEnv, TcRnMessage)
-badQuantHeadErr env pred
-  = ( env
-    , TcRnUnknownMessage $ mkPlainError noHints $
-      hang (text "Quantified predicate must have a class or type variable head:")
-         2 (ppr_tidy env pred) )
-eqPredTyErr  env pred
-  = ( env
-    , TcRnUnknownMessage $ mkPlainError noHints $
-      text "Illegal equational constraint" <+> ppr_tidy env pred $$
-      parens (text "Use GADTs or TypeFamilies to permit this") )
-predTupleErr env pred
-  = ( env
-    , TcRnUnknownMessage $ mkPlainError noHints $
-      hang (text "Illegal tuple constraint:" <+> ppr_tidy env pred)
-         2 (parens constraintKindsMsg) )
-predIrredErr env pred
-  = ( env
-    , TcRnUnknownMessage $ mkPlainError noHints $
-      hang (text "Illegal constraint:" <+> ppr_tidy env pred)
-         2 (parens constraintKindsMsg) )
-
-predTyVarErr :: TidyEnv -> PredType -> (TidyEnv, TcRnMessage)
-predTyVarErr env pred
-  = (env
-    , TcRnUnknownMessage $ mkPlainError noHints $
-      vcat [ hang (text "Non type-variable argument")
-                2 (text "in the constraint:" <+> ppr_tidy env pred)
-           , parens (text "Use FlexibleContexts to permit this") ])
-
-badIPPred :: TidyEnv -> PredType -> (TidyEnv, TcRnMessage)
-badIPPred env pred
-  = ( env
-    , TcRnUnknownMessage $ mkPlainError noHints $
-      text "Illegal implicit parameter" <+> quotes (ppr_tidy env pred) )
-
-constraintSynErr :: TidyEnv -> Type -> (TidyEnv, TcRnMessage)
-constraintSynErr env kind
-  = ( env
-    , TcRnUnknownMessage $ mkPlainError noHints $
-      hang (text "Illegal constraint synonym of kind:" <+> quotes (ppr_tidy env kind))
-         2 (parens constraintKindsMsg) )
-
-dupPredWarn :: TidyEnv -> [NE.NonEmpty PredType] -> (TidyEnv, SDoc)
-dupPredWarn env dups
-  = ( env
-    , text "Duplicate constraint" <> plural primaryDups <> text ":"
-      <+> pprWithCommas (ppr_tidy env) primaryDups )
-  where
-    primaryDups = map NE.head dups
-
 tyConArityErr :: TyCon -> [TcType] -> TcRnMessage
 -- For type-constructor arity errors, be careful to report
 -- the number of /visible/ arguments required and supplied,
@@ -1566,7 +1412,7 @@ check_special_inst_head dflags is_boot is_sig ctxt clas cls_args
   -- If not in an hs-boot file, abstract classes cannot have instances
   | isAbstractClass clas
   , not is_boot
-  = failWithTc abstract_class_msg
+  = failWithTc (TcRnAbstractClassInst clas)
 
   -- For Typeable, don't complain about instances for
   -- standalone deriving; they are no-ops, and we warn about
@@ -1603,7 +1449,7 @@ check_special_inst_head dflags is_boot is_sig ctxt clas cls_args
   = checkHasFieldInst clas cls_args
 
   | isCTupleClass clas
-  = failWithTc tuple_class_msg
+  = failWithTc (TcRnTupleConstraintInst clas)
 
   -- Check language restrictions on the args to the class
   | check_h98_arg_shape
@@ -1658,10 +1504,6 @@ check_special_inst_head dflags is_boot is_sig ctxt clas cls_args
     rejected_class_msg :: TcRnMessage
     rejected_class_msg = TcRnUnknownMessage $ mkPlainError noHints $ rejected_class_doc
 
-    tuple_class_msg    :: TcRnMessage
-    tuple_class_msg    = TcRnUnknownMessage $ mkPlainError noHints $
-      text "You can't specify an instance for a tuple constraint"
-
     rejected_class_doc :: SDoc
     rejected_class_doc =
       text "Class" <+> quotes (ppr clas_nm)
@@ -1671,11 +1513,6 @@ check_special_inst_head dflags is_boot is_sig ctxt clas cls_args
     gen_inst_err = TcRnUnknownMessage $ mkPlainError noHints $
       rejected_class_doc $$ nest 2 (text "(in Safe Haskell)")
 
-    abstract_class_msg :: TcRnMessage
-    abstract_class_msg = TcRnUnknownMessage $ mkPlainError noHints $
-      text "Cannot define instance for abstract class"
-                         <+> quotes (ppr clas_nm)
-
     mb_ty_args_msg
       | not (xopt LangExt.TypeSynonymInstances dflags)
       , not (all tcInstHeadTyNotSynonym ty_args)
@@ -1899,16 +1736,10 @@ synonyms, by matching on TyConApp directly.
 checkValidInstance :: UserTypeCtxt -> LHsSigType GhcRn -> Type -> TcM ()
 checkValidInstance ctxt hs_type ty
   | not is_tc_app
-  = failWithTc (TcRnUnknownMessage $ mkPlainError noHints $
-      hang (text "Instance head is not headed by a class:") 2 ( ppr tau))
+  = failWithTc (TcRnNoClassInstHead tau)
 
   | isNothing mb_cls
-  = failWithTc (TcRnUnknownMessage $ mkPlainError noHints $
-      vcat [ text "Illegal instance for a" <+> ppr (tyConFlavour tc)
-                     , text "A class instance must be for a class" ])
-
-  | not arity_ok
-  = failWithTc (TcRnUnknownMessage $ mkPlainError noHints $ text "Arity mis-match in instance head")
+  = failWithTc (TcRnIllegalClassInst (tyConFlavour tc))
 
   | otherwise
   = do  { setSrcSpanA head_loc $
@@ -1950,7 +1781,6 @@ checkValidInstance ctxt hs_type ty
     TyConApp tc inst_tys = tau   -- See Note [Instances and constraint synonyms]
     mb_cls               = tyConClass_maybe tc
     Just clas            = mb_cls
-    arity_ok             = inst_tys `lengthIs` classArity clas
 
         -- The location of the "head" of the instance
     head_loc = getLoc (getLHsInstDeclHead hs_type)
@@ -2042,9 +1872,8 @@ noMoreMsg tvs what inst_head
    occurs = if isSingleton tvs1 then text "occurs"
                                else text "occur"
 
-undecidableMsg, constraintKindsMsg :: SDoc
-undecidableMsg     = text "Use UndecidableInstances to permit this"
-constraintKindsMsg = text "Use ConstraintKinds to permit this"
+undecidableMsg :: SDoc
+undecidableMsg = text "Use UndecidableInstances to permit this"
 
 {- Note [Type families in instance contexts]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2169,9 +1998,7 @@ checkValidTyFamEqn fam_tc qvs typats rhs
            case drop (tyConArity fam_tc) typats of
              [] -> pure ()
              spec_arg:_ ->
-               addErr $ TcRnUnknownMessage $ mkPlainError noHints $
-                 text "Illegal oversaturated visible kind argument:"
-                    <+> quotes (char '@' <> pprParendType spec_arg)
+               addErr (TcRnOversaturatedVisibleKindArg spec_arg)
 
          -- The argument patterns, and RHS, are all boxed tau types
          -- E.g  Reject type family F (a :: k1) :: k2
@@ -2387,13 +2214,6 @@ nestedMsg what
   = sep [ text "Illegal nested" <+> what
         , parens undecidableMsg ]
 
-badATErr :: Name -> Name -> TcRnMessage
-badATErr clas op
-  = TcRnUnknownMessage $ mkPlainError noHints $
-    hsep [text "Class", quotes (ppr clas),
-          text "does not have an associated type", quotes (ppr op)]
-
-
 -------------------------
 checkConsistentFamInst :: AssocInstInfo
                        -> TyCon     -- ^ Family tycon
@@ -2418,7 +2238,7 @@ checkConsistentFamInst (InClsInst { ai_class = clas
        -- See [Mismatched class methods and associated type families]
        -- in TcInstDecls.
        ; checkTc (Just (classTyCon clas) == tyConAssoc_maybe fam_tc)
-                 (badATErr (className clas) (tyConName fam_tc))
+                 (TcRnBadAssociatedType (className clas) (tyConName fam_tc))
 
        ; check_match arg_triples
        }
@@ -3028,10 +2848,6 @@ isTerminatingClass cls
     || cls `hasKey` typeableClassKey
     || cls `hasKey` coercibleTyConKey
 
--- | Tidy before printing a type
-ppr_tidy :: TidyEnv -> Type -> SDoc
-ppr_tidy env ty = pprType (tidyType env ty)
-
 allDistinctTyVars :: TyVarSet -> [KindOrType] -> Bool
 -- (allDistinctTyVars tvs tys) returns True if tys are
 -- a) all tyvars
diff --git a/compiler/GHC/Types/Hint/Ppr.hs b/compiler/GHC/Types/Hint/Ppr.hs
index ab3478d4c4..eb68ff0c33 100644
--- a/compiler/GHC/Types/Hint/Ppr.hs
+++ b/compiler/GHC/Types/Hint/Ppr.hs
@@ -29,10 +29,10 @@ instance Outputable GhcHint where
             (text "Perhaps you intended to use" <+> ppr ext) $$ extraUserInfo
           SuggestAnyExtension extraUserInfo exts ->
             let header = text "Enable any of the following extensions:"
-            in  header <+> hsep (intersperse (char ',') (map ppr exts)) $$ extraUserInfo
+            in  header <+> hcat (intersperse (text ", ") (map ppr exts)) $$ extraUserInfo
           SuggestExtensions extraUserInfo exts ->
             let header = text "Enable all of the following extensions:"
-            in  header <+> hsep (intersperse (char ',') (map ppr exts)) $$ extraUserInfo
+            in  header <+> hcat (intersperse (text ", ") (map ppr exts)) $$ extraUserInfo
     SuggestMissingDo
       -> text "Possibly caused by a missing 'do'?"
     SuggestLetInDo