Add diagnostic codes

This MR adds diagnostic codes, assigning unique numeric codes to
error and warnings, e.g.

  error: [GHC-53633]
  Pattern match is redundant

This is achieved as follows:

  - a type family GhcDiagnosticCode that gives the diagnostic code
    for each diagnostic constructor,
  - a type family ConRecursInto that specifies whether to recur into
    an argument of the constructor to obtain a more fine-grained code
    (e.g. different error codes for different 'deriving' errors),
  - generics machinery to generate the value-level function assigning
    each diagnostic its error code; see Note [Diagnostic codes using generics]
    in GHC.Types.Error.Codes.

The upshot is that, to add a new diagnostic code, contributors only need
to modify the two type families mentioned above. All logic relating to
diagnostic codes is thus contained to the GHC.Types.Error.Codes module,
with no code duplication.

This MR also refactors error message datatypes a bit, ensuring we can
derive Generic for them, and cleans up the logic around constraint
solver reports by splitting up 'TcSolverReportInfo' into separate
datatypes (see #20772).

Fixes #21684

2 files changed, 569 insertions, 446 deletions

diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index 7d4e7e3948..ab338cf452 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE DataKinds #-}
 
 {-# OPTIONS_GHC -fno-warn-orphans #-} -- instance Diagnostic TcRnMessage
 
@@ -56,6 +57,7 @@ import GHC.Types.FieldLabel (flIsOverloaded)
 import GHC.Types.Hint (UntickedPromotedThing(..), pprUntickedConstructor, isBareSymbol)
 import GHC.Types.Hint.Ppr () -- Outputable GhcHint
 import GHC.Types.Basic
+import GHC.Types.Error.Codes ( constructorCode )
 import GHC.Types.Id
 import GHC.Types.Name
 import GHC.Types.Name.Reader ( GreName(..), pprNameProvenance
@@ -102,19 +104,18 @@ instance Diagnostic TcRnMessage where
       -> case msg_with_info of
            TcRnMessageDetailed err_info msg
              -> messageWithInfoDiagnosticMessage unit_state err_info (diagnosticMessage msg)
-    TcRnSolverReport msgs _ _
-      -> mkDecorated $
-           map pprSolverReportWithCtxt msgs
+    TcRnSolverReport msg _ _
+      -> mkSimpleDecorated $ pprSolverReportWithCtxt msg
     TcRnRedundantConstraints redundants (info, show_info)
       -> mkSimpleDecorated $
          text "Redundant constraint" <> plural redundants <> colon
            <+> pprEvVarTheta redundants
          $$ if show_info then text "In" <+> ppr info else empty
-    TcRnInaccessibleCode implic contras
+    TcRnInaccessibleCode implic contra
       -> mkSimpleDecorated $
          hang (text "Inaccessible code in")
            2 (ppr (ic_info implic))
-         $$ vcat (map pprSolverReportWithCtxt (NE.toList contras))
+         $$ pprSolverReportWithCtxt contra
     TcRnTypeDoesNotHaveFixedRuntimeRep ty prov (ErrInfo extra supplementary)
       -> mkDecorated [pprTypeDoesNotHaveFixedRuntimeRep ty prov, extra, supplementary]
     TcRnImplicitLift id_or_name ErrInfo{..}
@@ -906,7 +907,7 @@ instance Diagnostic TcRnMessage where
                      TyConPE        -> same_rec_group_msg
                      TermVariablePE -> text "term variables cannot be promoted"
           same_rec_group_msg = text "it is defined and used in the same recursive group"
-    TcRnMatchesHaveDiffNumArgs argsContext match1 bad_matches
+    TcRnMatchesHaveDiffNumArgs argsContext (MatchArgMatches match1 bad_matches)
       -> mkSimpleDecorated $
            (vcat [ pprArgsContext argsContext <+>
                    text "have different numbers of arguments"
@@ -1634,16 +1635,29 @@ instance Diagnostic TcRnMessage where
       -> noHints
     TcRnSpecialiseNotVisible name
       -> [SuggestSpecialiseVisibilityHints name]
-    TcRnNameByTemplateHaskellQuote{} -> noHints
-    TcRnIllegalBindingOfBuiltIn{} -> noHints
-    TcRnPragmaWarning{} -> noHints
-    TcRnIllegalHsigDefaultMethods{} -> noHints
-    TcRnBadGenericMethod{} -> noHints
-    TcRnWarningMinimalDefIncomplete{} -> noHints
-    TcRnDefaultMethodForPragmaLacksBinding{} -> noHints
-    TcRnIgnoreSpecialisePragmaOnDefMethod{} -> noHints
-    TcRnBadMethodErr{} -> noHints
-    TcRnNoExplicitAssocTypeOrDefaultDeclaration{} -> noHints
+    TcRnNameByTemplateHaskellQuote{}
+      -> noHints
+    TcRnIllegalBindingOfBuiltIn{}
+      -> noHints
+    TcRnPragmaWarning{}
+      -> noHints
+    TcRnIllegalHsigDefaultMethods{}
+      -> noHints
+    TcRnBadGenericMethod{}
+      -> noHints
+    TcRnWarningMinimalDefIncomplete{}
+      -> noHints
+    TcRnDefaultMethodForPragmaLacksBinding{}
+      -> noHints
+    TcRnIgnoreSpecialisePragmaOnDefMethod{}
+      -> noHints
+    TcRnBadMethodErr{}
+      -> noHints
+    TcRnNoExplicitAssocTypeOrDefaultDeclaration{}
+      -> noHints
+
+  diagnosticCode = constructorCode
+
 
 -- | Change [x] to "x", [x, y] to "x and y", [x, y, z] to "x, y, and z",
 -- and so on.  The `and` stands for any `conjunction`, which is passed in.
@@ -2059,11 +2073,6 @@ pprSolverReportWithCtxt (SolverReportWithCtxt { reportContext = ctxt, reportCont
 
 -- | Pretty-print a 'TcSolverReportMsg', with its enclosing 'SolverReportErrCtxt'.
 pprTcSolverReportMsg :: SolverReportErrCtxt -> TcSolverReportMsg -> SDoc
-pprTcSolverReportMsg ctxt (TcReportWithInfo msg (info :| infos)) =
-  vcat
-    ( pprTcSolverReportMsg ctxt msg
-    : pprTcSolverReportInfo ctxt info
-    : map (pprTcSolverReportInfo ctxt) infos )
 pprTcSolverReportMsg _ (BadTelescope telescope skols) =
   hang (text "These kind and type variables:" <+> ppr telescope $$
        text "are out of dependency order. Perhaps try this ordering:")
@@ -2074,143 +2083,22 @@ pprTcSolverReportMsg _ (UserTypeError ty) =
   pprUserTypeErrorTy ty
 pprTcSolverReportMsg ctxt (ReportHoleError hole err) =
   pprHoleError ctxt hole err
-pprTcSolverReportMsg _ (CannotUnifyWithPolytype item tv1 ty2) =
-  vcat [ (if isSkolemTyVar tv1
-          then text "Cannot equate type variable"
-          else text "Cannot instantiate unification variable")
-         <+> quotes (ppr tv1)
-       , hang (text "with a" <+> what <+> text "involving polytypes:") 2 (ppr ty2) ]
-  where
-    what = text $ levelString $
-           ctLocTypeOrKind_maybe (errorItemCtLoc item) `orElse` TypeLevel
-pprTcSolverReportMsg _
-  (Mismatch { mismatch_ea   = add_ea
-            , mismatch_item = item
-            , mismatch_ty1  = ty1
-            , mismatch_ty2  = ty2 })
-  = addArising (errorItemCtLoc item) msg
-  where
-    msg
-      | (isLiftedRuntimeRep ty1 && isUnliftedRuntimeRep ty2) ||
-        (isLiftedRuntimeRep ty2 && isUnliftedRuntimeRep ty1) ||
-        (isLiftedLevity ty1 && isUnliftedLevity ty2) ||
-        (isLiftedLevity ty2 && isUnliftedLevity ty1)
-      = text "Couldn't match a lifted type with an unlifted type"
-
-      | isAtomicTy ty1 || isAtomicTy ty2
-      = -- Print with quotes
-        sep [ text herald1 <+> quotes (ppr ty1)
-            , nest padding $
-              text herald2 <+> quotes (ppr ty2) ]
-
-      | otherwise
-      = -- Print with vertical layout
-        vcat [ text herald1 <> colon <+> ppr ty1
-             , nest padding $
-               text herald2 <> colon <+> ppr ty2 ]
-
-    herald1 = conc [ "Couldn't match"
-                   , if is_repr then "representation of" else ""
-                   , if add_ea then "expected"          else ""
-                   , what ]
-    herald2 = conc [ "with"
-                   , if is_repr then "that of"          else ""
-                   , if add_ea then ("actual " ++ what) else "" ]
-
-    padding = length herald1 - length herald2
-
-    is_repr = case errorItemEqRel item of { ReprEq -> True; NomEq -> False }
-
-    what = levelString (ctLocTypeOrKind_maybe (errorItemCtLoc item) `orElse` TypeLevel)
-
-    conc :: [String] -> String
-    conc = foldr1 add_space
-
-    add_space :: String -> String -> String
-    add_space s1 s2 | null s1   = s2
-                    | null s2   = s1
-                    | otherwise = s1 ++ (' ' : s2)
-pprTcSolverReportMsg _
-  (KindMismatch { kmismatch_what     = thing
-                , kmismatch_expected = exp
-                , kmismatch_actual   = act })
-  = hang (text "Expected" <+> kind_desc <> comma)
-      2 (text "but" <+> quotes (ppr thing) <+> text "has kind" <+>
-        quotes (ppr act))
-  where
-    kind_desc | tcIsConstraintKind exp = text "a constraint"
-              | Just arg <- kindRep_maybe exp  -- TYPE t0
-              , tcIsTyVarTy arg = sdocOption sdocPrintExplicitRuntimeReps $ \case
-                                   True  -> text "kind" <+> quotes (ppr exp)
-                                   False -> text "a type"
-              | otherwise       = text "kind" <+> quotes (ppr exp)
-
-
 pprTcSolverReportMsg ctxt
-  (TypeEqMismatch { teq_mismatch_ppr_explicit_kinds = ppr_explicit_kinds
-                  , teq_mismatch_item     = item
-                  , teq_mismatch_ty1      = ty1
-                  , teq_mismatch_ty2      = ty2
-                  , teq_mismatch_expected = exp
-                  , teq_mismatch_actual   = act
-                  , teq_mismatch_what     = mb_thing })
-  = addArising ct_loc $ pprWithExplicitKindsWhen ppr_explicit_kinds msg
-  where
-    msg
-      | isUnliftedTypeKind act, isLiftedTypeKind exp
-      = sep [ text "Expecting a lifted type, but"
-            , thing_msg mb_thing (text "an") (text "unlifted") ]
-      | isLiftedTypeKind act, isUnliftedTypeKind exp
-      = sep [ text "Expecting an unlifted type, but"
-            , thing_msg mb_thing (text "a") (text "lifted") ]
-      | tcIsLiftedTypeKind exp
-      = maybe_num_args_msg $$
-        sep [ text "Expected a type, but"
-            , case mb_thing of
-                Nothing    -> text "found something with kind"
-                Just thing -> quotes (ppr thing) <+> text "has kind"
-            , quotes (pprWithTYPE act) ]
-      | Just nargs_msg <- num_args_msg
-      , Right ea_msg <- mk_ea_msg ctxt (Just item) level orig
-      = nargs_msg $$ pprTcSolverReportMsg ctxt ea_msg
-      | -- pprTrace "check" (ppr ea_looks_same $$ ppr exp $$ ppr act $$ ppr ty1 $$ ppr ty2) $
-        ea_looks_same ty1 ty2 exp act
-      , Right ea_msg <- mk_ea_msg ctxt (Just item) level orig
-      = pprTcSolverReportMsg ctxt ea_msg
-      -- The mismatched types are /inside/ exp and act
-      | let mismatch_err = Mismatch False item ty1 ty2
-            errs = case mk_ea_msg ctxt Nothing level orig of
-              Left ea_info -> [ mkTcReportWithInfo mismatch_err ea_info ]
-              Right ea_err -> [ mismatch_err, ea_err ]
-      = vcat $ map (pprTcSolverReportMsg ctxt) errs
-
-    ct_loc = errorItemCtLoc item
-    orig   = errorItemOrigin item
-    level  = ctLocTypeOrKind_maybe ct_loc `orElse` TypeLevel
-
-    thing_msg (Just thing) _  levity = quotes (ppr thing) <+> text "is" <+> levity
-    thing_msg Nothing      an levity = text "got" <+> an <+> levity <+> text "type"
-
-    num_args_msg = case level of
-      KindLevel
-        | not (isMetaTyVarTy exp) && not (isMetaTyVarTy act)
-           -- if one is a meta-tyvar, then it's possible that the user
-           -- has asked for something impredicative, and we couldn't unify.
-           -- Don't bother with counting arguments.
-        -> let n_act = count_args act
-               n_exp = count_args exp in
-           case n_act - n_exp of
-             n | n > 0   -- we don't know how many args there are, so don't
-                         -- recommend removing args that aren't
-               , Just thing <- mb_thing
-               -> Just $ pprTcSolverReportMsg ctxt (ExpectingMoreArguments n thing)
-             _ -> Nothing
-
-      _ -> Nothing
-
-    maybe_num_args_msg = num_args_msg `orElse` empty
-
-    count_args ty = count isVisibleBinder $ fst $ splitPiTys ty
+  (CannotUnifyVariable
+    { mismatchMsg             = msg
+    , cannotUnifyReason       = reason })
+  =  pprMismatchMsg ctxt msg
+  $$ pprCannotUnifyVariableReason ctxt reason
+pprTcSolverReportMsg ctxt
+  (Mismatch
+     { mismatchMsg           = mismatch_msg
+     , mismatchTyVarInfo     = tv_info
+     , mismatchAmbiguityInfo = ambig_infos
+     , mismatchCoercibleInfo = coercible_info })
+  = hang (pprMismatchMsg ctxt mismatch_msg)
+     2 (vcat ( maybe empty (pprTyVarInfo ctxt) tv_info
+             : maybe empty pprCoercibleMsg coercible_info
+             : map pprAmbiguityInfo ambig_infos ))
 pprTcSolverReportMsg _ (FixedRuntimeRepError frr_origs) =
   vcat (map make_msg frr_origs)
   where
@@ -2287,28 +2175,6 @@ pprTcSolverReportMsg _ (FixedRuntimeRepError frr_origs) =
           = quotes (text "Levity")
           | otherwise
           = text "type"
-
-pprTcSolverReportMsg _ (SkolemEscape item implic esc_skols) =
-  let
-    esc_doc = sep [ text "because" <+> what <+> text "variable" <> plural esc_skols
-                <+> pprQuotedList esc_skols
-              , text "would escape" <+>
-                if isSingleton esc_skols then text "its scope"
-                                         else text "their scope" ]
-  in
-  vcat [ nest 2 $ esc_doc
-       , sep [ (if isSingleton esc_skols
-                then text "This (rigid, skolem)" <+>
-                     what <+> text "variable is"
-                else text "These (rigid, skolem)" <+>
-                     what <+> text "variables are")
-         <+> text "bound by"
-       , nest 2 $ ppr (ic_info implic)
-       , nest 2 $ text "at" <+>
-         ppr (getLclEnvLoc (ic_env implic)) ] ]
-  where
-    what = text $ levelString $
-           ctLocTypeOrKind_maybe (errorItemCtLoc item) `orElse` TypeLevel
 pprTcSolverReportMsg _ (UntouchableVariable tv implic)
   | Implic { ic_given = given, ic_info = skol_info } <- implic
   = sep [ quotes (ppr tv) <+> text "is untouchable"
@@ -2333,52 +2199,11 @@ pprTcSolverReportMsg ctxt (UnboundImplicitParams (item :| items)) =
      then addArising (errorItemCtLoc item) $
             sep [ text "Unbound implicit parameter" <> plural preds
                 , nest 2 (pprParendTheta preds) ]
-     else pprTcSolverReportMsg ctxt (CouldNotDeduce givens (item :| items) Nothing)
+     else pprMismatchMsg ctxt (CouldNotDeduce givens (item :| items) Nothing)
   where
     preds = map errorItemPred (item : items)
-pprTcSolverReportMsg ctxt (CouldNotDeduce useful_givens (item :| others) mb_extra)
-  = main_msg $$
-     case supplementary of
-      Left infos
-        -> vcat (map (pprTcSolverReportInfo ctxt) infos)
-      Right other_msg
-        -> pprTcSolverReportMsg ctxt other_msg
-  where
-    main_msg
-      | null useful_givens
-      = addArising ct_loc (no_instance_msg <+> missing)
-      | otherwise
-      = vcat (addArising ct_loc (no_deduce_msg <+> missing)
-              : pp_givens useful_givens)
-
-    supplementary = case mb_extra of
-      Nothing
-        -> Left []
-      Just (CND_Extra level ty1 ty2)
-        -> mk_supplementary_ea_msg ctxt level ty1 ty2 orig
-    ct_loc = errorItemCtLoc item
-    orig   = ctLocOrigin ct_loc
-    wanteds = map errorItemPred (item:others)
-
-    no_instance_msg =
-      case wanteds of
-        [wanted] | Just (tc, _) <- splitTyConApp_maybe wanted
-                 -- Don't say "no instance" for a constraint such as "c" for a type variable c.
-                 , isClassTyCon tc -> text "No instance for"
-        _ -> text "Could not solve:"
-
-    no_deduce_msg =
-      case wanteds of
-        [_wanted] -> text "Could not deduce"
-        _         -> text "Could not deduce:"
-
-    missing =
-      case wanteds of
-        [wanted] -> quotes (ppr wanted)
-        _        -> pprTheta wanteds
-
-pprTcSolverReportMsg ctxt (AmbiguityPreventsSolvingCt item ambigs) =
-  pprTcSolverReportInfo ctxt (Ambiguity True ambigs) <+>
+pprTcSolverReportMsg _ (AmbiguityPreventsSolvingCt item ambigs) =
+  pprAmbiguityInfo (Ambiguity True ambigs) <+>
   pprArising (errorItemCtLoc item) $$
   text "prevents the constraint" <+> quotes (pprParendType $ errorItemPred item)
   <+> text "from being solved."
@@ -2386,12 +2211,12 @@ pprTcSolverReportMsg ctxt@(CEC {cec_encl = implics})
   (CannotResolveInstance item unifiers candidates imp_errs suggs binds)
   =
     vcat
-      [ pprTcSolverReportMsg ctxt no_inst_msg
+      [ no_inst_msg
       , nest 2 extra_note
       , mb_patsyn_prov `orElse` empty
       , ppWhen (has_ambigs && not (null unifiers && null useful_givens))
         (vcat [ ppUnless lead_with_ambig $
-                  pprTcSolverReportInfo ctxt (Ambiguity False (ambig_kvs, ambig_tvs))
+                  pprAmbiguityInfo (Ambiguity False (ambig_kvs, ambig_tvs))
               , pprRelevantBindings binds
               , potential_msg ])
       , ppWhen (isNothing mb_patsyn_prov) $
@@ -2421,12 +2246,12 @@ pprTcSolverReportMsg ctxt@(CEC {cec_encl = implics})
                    && not (null unifiers)
                    && null useful_givens
 
-    no_inst_msg :: TcSolverReportMsg
+    no_inst_msg :: SDoc
     no_inst_msg
       | lead_with_ambig
-      = AmbiguityPreventsSolvingCt item (ambig_kvs, ambig_tvs)
+      = pprTcSolverReportMsg ctxt $ AmbiguityPreventsSolvingCt item (ambig_kvs, ambig_tvs)
       | otherwise
-      = CouldNotDeduce useful_givens (item :| []) Nothing
+      = pprMismatchMsg ctxt $ CouldNotDeduce useful_givens (item :| []) Nothing
 
     -- Report "potential instances" only when the constraint arises
     -- directly from the user's use of an overloaded function
@@ -2556,6 +2381,242 @@ pprTcSolverReportMsg _ (UnsafeOverlap item matches unsafe_overlapped) =
     pred        = errorItemPred item
     (clas, tys) = getClassPredTys pred
 
+pprCannotUnifyVariableReason :: SolverReportErrCtxt -> CannotUnifyVariableReason -> SDoc
+pprCannotUnifyVariableReason ctxt (CannotUnifyWithPolytype item tv1 ty2 mb_tv_info) =
+  vcat [ (if isSkolemTyVar tv1
+          then text "Cannot equate type variable"
+          else text "Cannot instantiate unification variable")
+         <+> quotes (ppr tv1)
+       , hang (text "with a" <+> what <+> text "involving polytypes:") 2 (ppr ty2)
+       , maybe empty (pprTyVarInfo ctxt) mb_tv_info ]
+  where
+    what = text $ levelString $
+           ctLocTypeOrKind_maybe (errorItemCtLoc item) `orElse` TypeLevel
+
+pprCannotUnifyVariableReason _ (SkolemEscape item implic esc_skols) =
+  let
+    esc_doc = sep [ text "because" <+> what <+> text "variable" <> plural esc_skols
+                <+> pprQuotedList esc_skols
+              , text "would escape" <+>
+                if isSingleton esc_skols then text "its scope"
+                                         else text "their scope" ]
+  in
+  vcat [ nest 2 $ esc_doc
+       , sep [ (if isSingleton esc_skols
+                then text "This (rigid, skolem)" <+>
+                     what <+> text "variable is"
+                else text "These (rigid, skolem)" <+>
+                     what <+> text "variables are")
+         <+> text "bound by"
+       , nest 2 $ ppr (ic_info implic)
+       , nest 2 $ text "at" <+>
+         ppr (getLclEnvLoc (ic_env implic)) ] ]
+  where
+    what = text $ levelString $
+           ctLocTypeOrKind_maybe (errorItemCtLoc item) `orElse` TypeLevel
+
+pprCannotUnifyVariableReason ctxt
+  (OccursCheck
+    { occursCheckInterestingTyVars = interesting_tvs
+    , occursCheckAmbiguityInfos    = ambig_infos })
+  = ppr_interesting_tyVars interesting_tvs
+  $$ vcat (map pprAmbiguityInfo ambig_infos)
+  where
+    ppr_interesting_tyVars [] = empty
+    ppr_interesting_tyVars (tv:tvs) =
+      hang (text "Type variable kinds:") 2 $
+      vcat (map (tyvar_binding . tidyTyCoVarOcc (cec_tidy ctxt))
+                (tv:tvs))
+    tyvar_binding tyvar = ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)
+pprCannotUnifyVariableReason ctxt (DifferentTyVars tv_info)
+  = pprTyVarInfo ctxt tv_info
+pprCannotUnifyVariableReason ctxt (RepresentationalEq tv_info mb_coercible_msg)
+  = pprTyVarInfo ctxt tv_info
+  $$ maybe empty pprCoercibleMsg mb_coercible_msg
+
+pprMismatchMsg :: SolverReportErrCtxt -> MismatchMsg -> SDoc
+pprMismatchMsg ctxt
+  (BasicMismatch { mismatch_ea   = ea
+                 , mismatch_item = item
+                 , mismatch_ty1  = ty1
+                 , mismatch_ty2  = ty2
+                 , mismatch_whenMatching = mb_match_txt
+                 , mismatch_mb_same_occ  = same_occ_info })
+  = addArising (errorItemCtLoc item) msg
+  $$ maybe empty (pprWhenMatching ctxt) mb_match_txt
+  $$ maybe empty pprSameOccInfo same_occ_info
+  where
+    msg
+      | (isLiftedRuntimeRep ty1 && isUnliftedRuntimeRep ty2) ||
+        (isLiftedRuntimeRep ty2 && isUnliftedRuntimeRep ty1) ||
+        (isLiftedLevity ty1 && isUnliftedLevity ty2) ||
+        (isLiftedLevity ty2 && isUnliftedLevity ty1)
+      = text "Couldn't match a lifted type with an unlifted type"
+
+      | isAtomicTy ty1 || isAtomicTy ty2
+      = -- Print with quotes
+        sep [ text herald1 <+> quotes (ppr ty1)
+            , nest padding $
+              text herald2 <+> quotes (ppr ty2) ]
+
+      | otherwise
+      = -- Print with vertical layout
+        vcat [ text herald1 <> colon <+> ppr ty1
+             , nest padding $
+               text herald2 <> colon <+> ppr ty2 ]
+
+    want_ea = case ea of { NoEA -> False; EA {} -> True }
+
+    herald1 = conc [ "Couldn't match"
+                   , if is_repr then "representation of" else ""
+                   , if want_ea then "expected"          else ""
+                   , what ]
+    herald2 = conc [ "with"
+                   , if is_repr then "that of"          else ""
+                   , if want_ea then ("actual " ++ what) else "" ]
+
+    padding = length herald1 - length herald2
+
+    is_repr = case errorItemEqRel item of { ReprEq -> True; NomEq -> False }
+
+    what = levelString (ctLocTypeOrKind_maybe (errorItemCtLoc item) `orElse` TypeLevel)
+
+    conc :: [String] -> String
+    conc = foldr1 add_space
+
+    add_space :: String -> String -> String
+    add_space s1 s2 | null s1   = s2
+                    | null s2   = s1
+                    | otherwise = s1 ++ (' ' : s2)
+pprMismatchMsg _
+  (KindMismatch { kmismatch_what     = thing
+                , kmismatch_expected = exp
+                , kmismatch_actual   = act })
+  = hang (text "Expected" <+> kind_desc <> comma)
+      2 (text "but" <+> quotes (ppr thing) <+> text "has kind" <+>
+        quotes (ppr act))
+  where
+    kind_desc | tcIsConstraintKind exp = text "a constraint"
+              | Just arg <- kindRep_maybe exp  -- TYPE t0
+              , tcIsTyVarTy arg = sdocOption sdocPrintExplicitRuntimeReps $ \case
+                                   True  -> text "kind" <+> quotes (ppr exp)
+                                   False -> text "a type"
+              | otherwise       = text "kind" <+> quotes (ppr exp)
+
+pprMismatchMsg ctxt
+  (TypeEqMismatch { teq_mismatch_ppr_explicit_kinds = ppr_explicit_kinds
+                  , teq_mismatch_item     = item
+                  , teq_mismatch_ty1      = ty1
+                  , teq_mismatch_ty2      = ty2
+                  , teq_mismatch_expected = exp
+                  , teq_mismatch_actual   = act
+                  , teq_mismatch_what     = mb_thing
+                  , teq_mb_same_occ       = mb_same_occ })
+  = (addArising ct_loc $ pprWithExplicitKindsWhen ppr_explicit_kinds msg)
+  $$ maybe empty pprSameOccInfo mb_same_occ
+  where
+    msg
+      | isUnliftedTypeKind act, isLiftedTypeKind exp
+      = sep [ text "Expecting a lifted type, but"
+            , thing_msg mb_thing (text "an") (text "unlifted") ]
+      | isLiftedTypeKind act, isUnliftedTypeKind exp
+      = sep [ text "Expecting an unlifted type, but"
+            , thing_msg mb_thing (text "a") (text "lifted") ]
+      | tcIsLiftedTypeKind exp
+      = maybe_num_args_msg $$
+        sep [ text "Expected a type, but"
+            , case mb_thing of
+                Nothing    -> text "found something with kind"
+                Just thing -> quotes (ppr thing) <+> text "has kind"
+            , quotes (pprWithTYPE act) ]
+      | Just nargs_msg <- num_args_msg
+      , Right ea_msg <- mk_ea_msg ctxt (Just item) level orig
+      = nargs_msg $$ pprMismatchMsg ctxt ea_msg
+      | -- pprTrace "check" (ppr ea_looks_same $$ ppr exp $$ ppr act $$ ppr ty1 $$ ppr ty2) $
+        ea_looks_same ty1 ty2 exp act
+      , Right ea_msg <- mk_ea_msg ctxt (Just item) level orig
+      = pprMismatchMsg ctxt ea_msg
+
+      | otherwise
+      =
+      -- The mismatched types are /inside/ exp and act
+        let mismatch_err = mkBasicMismatchMsg NoEA item ty1 ty2
+            errs = case mk_ea_msg ctxt Nothing level orig of
+              Left ea_info -> pprMismatchMsg ctxt mismatch_err : map (pprExpectedActualInfo ctxt) ea_info
+              Right ea_err -> [ pprMismatchMsg ctxt mismatch_err, pprMismatchMsg ctxt ea_err ]
+        in vcat errs
+
+    ct_loc = errorItemCtLoc item
+    orig   = errorItemOrigin item
+    level  = ctLocTypeOrKind_maybe ct_loc `orElse` TypeLevel
+
+    thing_msg (Just thing) _  levity = quotes (ppr thing) <+> text "is" <+> levity
+    thing_msg Nothing      an levity = text "got" <+> an <+> levity <+> text "type"
+
+    num_args_msg = case level of
+      KindLevel
+        | not (isMetaTyVarTy exp) && not (isMetaTyVarTy act)
+           -- if one is a meta-tyvar, then it's possible that the user
+           -- has asked for something impredicative, and we couldn't unify.
+           -- Don't bother with counting arguments.
+        -> let n_act = count_args act
+               n_exp = count_args exp in
+           case n_act - n_exp of
+             n | n > 0   -- we don't know how many args there are, so don't
+                         -- recommend removing args that aren't
+               , Just thing <- mb_thing
+               -> Just $ pprTcSolverReportMsg ctxt (ExpectingMoreArguments n thing)
+             _ -> Nothing
+
+      _ -> Nothing
+
+    maybe_num_args_msg = num_args_msg `orElse` empty
+
+    count_args ty = count isVisibleBinder $ fst $ splitPiTys ty
+
+pprMismatchMsg ctxt (CouldNotDeduce useful_givens (item :| others) mb_extra)
+  = main_msg $$
+     case supplementary of
+      Left infos
+        -> vcat (map (pprExpectedActualInfo ctxt) infos)
+      Right other_msg
+        -> pprMismatchMsg ctxt other_msg
+  where
+    main_msg
+      | null useful_givens
+      = addArising ct_loc (no_instance_msg <+> missing)
+      | otherwise
+      = vcat (addArising ct_loc (no_deduce_msg <+> missing)
+              : pp_givens useful_givens)
+
+    supplementary = case mb_extra of
+      Nothing
+        -> Left []
+      Just (CND_Extra level ty1 ty2)
+        -> mk_supplementary_ea_msg ctxt level ty1 ty2 orig
+    ct_loc = errorItemCtLoc item
+    orig   = ctLocOrigin ct_loc
+    wanteds = map errorItemPred (item:others)
+
+    no_instance_msg =
+      case wanteds of
+        [wanted] | Just (tc, _) <- splitTyConApp_maybe wanted
+                 -- Don't say "no instance" for a constraint such as "c" for a type variable c.
+                 , isClassTyCon tc -> text "No instance for"
+        _ -> text "Could not solve:"
+
+    no_deduce_msg =
+      case wanteds of
+        [_wanted] -> text "Could not deduce"
+        _         -> text "Could not deduce:"
+
+    missing =
+      case wanteds of
+        [wanted] -> quotes (ppr wanted)
+        _        -> pprTheta wanteds
+
+
+
 {- *********************************************************************
 *                                                                      *
                  Displaying potential instances
@@ -2746,50 +2807,17 @@ we want to give it a bit of structure.  Here's the plan
 
 {- *********************************************************************
 *                                                                      *
-                    Outputting TcSolverReportInfo
+             Outputting additional solver report information
 *                                                                      *
 **********************************************************************-}
 
 -- | Pretty-print an informational message, to accompany a 'TcSolverReportMsg'.
-pprTcSolverReportInfo :: SolverReportErrCtxt -> TcSolverReportInfo -> SDoc
-pprTcSolverReportInfo _ (Ambiguity prepend_msg (ambig_kvs, ambig_tvs)) = msg
-  where
-
-    msg |  any isRuntimeUnkSkol ambig_kvs  -- See Note [Runtime skolems]
-        || any isRuntimeUnkSkol ambig_tvs
-        = vcat [ text "Cannot resolve unknown runtime type"
-                 <> plural ambig_tvs <+> pprQuotedList ambig_tvs
-               , text "Use :print or :force to determine these types"]
-
-        | not (null ambig_tvs)
-        = pp_ambig (text "type") ambig_tvs
-
-        | otherwise
-        = pp_ambig (text "kind") ambig_kvs
-
-    pp_ambig what tkvs
-      | prepend_msg -- "Ambiguous type variable 't0'"
-      = text "Ambiguous" <+> what <+> text "variable"
-        <> plural tkvs <+> pprQuotedList tkvs
-
-      | otherwise -- "The type variable 't0' is ambiguous"
-      = text "The" <+> what <+> text "variable" <> plural tkvs
-        <+> pprQuotedList tkvs <+> isOrAre tkvs <+> text "ambiguous"
-pprTcSolverReportInfo ctxt (TyVarInfo tv ) =
-  case tcTyVarDetails tv of
-    SkolemTv sk_info _ _   -> pprSkols ctxt [(getSkolemInfo sk_info, [tv])]
-    RuntimeUnk {} -> quotes (ppr tv) <+> text "is an interactive-debugger skolem"
-    MetaTv {}     -> empty
-pprTcSolverReportInfo _ (NonInjectiveTyFam tc) =
-  text "NB:" <+> quotes (ppr tc)
-  <+> text "is a non-injective type family"
-pprTcSolverReportInfo _ (ReportCoercibleMsg msg) =
-  pprCoercibleMsg msg
-pprTcSolverReportInfo _ (ExpectedActual { ea_expected = exp, ea_actual = act }) =
+pprExpectedActualInfo :: SolverReportErrCtxt -> ExpectedActualInfo -> SDoc
+pprExpectedActualInfo _ (ExpectedActual { ea_expected = exp, ea_actual = act }) =
   vcat
     [ text "Expected:" <+> ppr exp
     , text "  Actual:" <+> ppr act ]
-pprTcSolverReportInfo _
+pprExpectedActualInfo _
   (ExpectedActualAfterTySynExpansion
     { ea_expanded_expected = exp
     , ea_expanded_actual   = act } )
@@ -2797,7 +2825,23 @@ pprTcSolverReportInfo _
       [ text "Type synonyms expanded:"
       , text "Expected type:" <+> ppr exp
       , text "  Actual type:" <+> ppr act ]
-pprTcSolverReportInfo ctxt (WhenMatching cty1 cty2 sub_o mb_sub_t_or_k) =
+
+pprCoercibleMsg :: CoercibleMsg -> SDoc
+pprCoercibleMsg (UnknownRoles ty) =
+  hang (text "NB: We cannot know what roles the parameters to" <+>
+          quotes (ppr ty) <+> text "have;")
+       2 (text "we must assume that the role is nominal")
+pprCoercibleMsg (TyConIsAbstract tc) =
+  hsep [ text "NB: The type constructor"
+       , quotes (pprSourceTyCon tc)
+       , text "is abstract" ]
+pprCoercibleMsg (OutOfScopeNewtypeConstructor tc dc) =
+  hang (text "The data constructor" <+> quotes (ppr $ dataConName dc))
+    2 (sep [ text "of newtype" <+> quotes (pprSourceTyCon tc)
+           , text "is not in scope" ])
+
+pprWhenMatching :: SolverReportErrCtxt -> WhenMatching -> SDoc
+pprWhenMatching ctxt (WhenMatching cty1 cty2 sub_o mb_sub_t_or_k) =
   sdocOption sdocPrintExplicitCoercions $ \printExplicitCoercions ->
     if printExplicitCoercions
        || not (cty1 `pickyEqType` cty2)
@@ -2813,9 +2857,48 @@ pprTcSolverReportInfo ctxt (WhenMatching cty1 cty2 sub_o mb_sub_t_or_k) =
     sub_whats  = text (levelString sub_t_or_k) <> char 's'
     supplementary =
       case mk_supplementary_ea_msg ctxt sub_t_or_k cty1 cty2 sub_o of
-        Left infos -> vcat $ map (pprTcSolverReportInfo ctxt) infos
-        Right msg  -> pprTcSolverReportMsg ctxt msg
-pprTcSolverReportInfo _ (SameOcc same_pkg n1 n2) =
+        Left infos -> vcat $ map (pprExpectedActualInfo ctxt) infos
+        Right msg  -> pprMismatchMsg ctxt msg
+
+pprTyVarInfo :: SolverReportErrCtxt -> TyVarInfo -> SDoc
+pprTyVarInfo ctxt (TyVarInfo { thisTyVar = tv1, otherTy = mb_tv2 }) =
+  mk_msg tv1 $$ case mb_tv2 of { Nothing -> empty; Just tv2 -> mk_msg tv2 }
+  where
+    mk_msg tv = case tcTyVarDetails tv of
+      SkolemTv sk_info _ _ -> pprSkols ctxt [(getSkolemInfo sk_info, [tv])]
+      RuntimeUnk {} -> quotes (ppr tv) <+> text "is an interactive-debugger skolem"
+      MetaTv {}     -> empty
+
+pprAmbiguityInfo :: AmbiguityInfo -> SDoc
+pprAmbiguityInfo (Ambiguity prepend_msg (ambig_kvs, ambig_tvs)) = msg
+  where
+
+    msg |  any isRuntimeUnkSkol ambig_kvs  -- See Note [Runtime skolems]
+        || any isRuntimeUnkSkol ambig_tvs
+        = vcat [ text "Cannot resolve unknown runtime type"
+                 <> plural ambig_tvs <+> pprQuotedList ambig_tvs
+               , text "Use :print or :force to determine these types"]
+
+        | not (null ambig_tvs)
+        = pp_ambig (text "type") ambig_tvs
+
+        | otherwise
+        = pp_ambig (text "kind") ambig_kvs
+
+    pp_ambig what tkvs
+      | prepend_msg -- "Ambiguous type variable 't0'"
+      = text "Ambiguous" <+> what <+> text "variable"
+        <> plural tkvs <+> pprQuotedList tkvs
+
+      | otherwise -- "The type variable 't0' is ambiguous"
+      = text "The" <+> what <+> text "variable" <> plural tkvs
+        <+> pprQuotedList tkvs <+> isOrAre tkvs <+> text "ambiguous"
+pprAmbiguityInfo (NonInjectiveTyFam tc) =
+  text "NB:" <+> quotes (ppr tc)
+  <+> text "is a non-injective type family"
+
+pprSameOccInfo :: SameOccInfo -> SDoc
+pprSameOccInfo (SameOcc same_pkg n1 n2) =
   text "NB:" <+> (ppr_from same_pkg n1 $$ ppr_from same_pkg n2)
   where
     ppr_from same_pkg nm
@@ -2831,26 +2914,6 @@ pprTcSolverReportInfo _ (SameOcc same_pkg n1 n2) =
         pkg = moduleUnit mod
         mod = nameModule nm
         loc = nameSrcSpan nm
-pprTcSolverReportInfo ctxt (OccursCheckInterestingTyVars (tv :| tvs)) =
-  hang (text "Type variable kinds:") 2 $
-    vcat (map (tyvar_binding . tidyTyCoVarOcc (cec_tidy ctxt))
-              (tv:tvs))
-  where
-    tyvar_binding tyvar = ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)
-
-pprCoercibleMsg :: CoercibleMsg -> SDoc
-pprCoercibleMsg (UnknownRoles ty) =
-  hang (text "NB: We cannot know what roles the parameters to" <+>
-          quotes (ppr ty) <+> text "have;")
-       2 (text "we must assume that the role is nominal")
-pprCoercibleMsg (TyConIsAbstract tc) =
-  hsep [ text "NB: The type constructor"
-       , quotes (pprSourceTyCon tc)
-       , text "is abstract" ]
-pprCoercibleMsg (OutOfScopeNewtypeConstructor tc dc) =
-  hang (text "The data constructor" <+> quotes (ppr $ dataConName dc))
-    2 (sep [ text "of newtype" <+> quotes (pprSourceTyCon tc)
-           , text "is not in scope" ])
 
 {- *********************************************************************
 *                                                                      *
@@ -3229,7 +3292,7 @@ skolsSpan skol_tvs = foldr1 combineSrcSpans (map getSrcSpan skol_tvs)
 **********************************************************************-}
 
 mk_supplementary_ea_msg :: SolverReportErrCtxt -> TypeOrKind
-                        -> Type -> Type -> CtOrigin -> Either [TcSolverReportInfo] TcSolverReportMsg
+                        -> Type -> Type -> CtOrigin -> Either [ExpectedActualInfo] MismatchMsg
 mk_supplementary_ea_msg ctxt level ty1 ty2 orig
   | TypeEqOrigin { uo_expected = exp, uo_actual = act } <- orig
   , not (ea_looks_same ty1 ty2 exp act)
@@ -3252,7 +3315,7 @@ ea_looks_same ty1 ty2 exp act
       -- (TYPE 'LiftedRep) and Type both print the same way.
 
 mk_ea_msg :: SolverReportErrCtxt -> Maybe ErrorItem -> TypeOrKind
-          -> CtOrigin -> Either [TcSolverReportInfo] TcSolverReportMsg
+          -> CtOrigin -> Either [ExpectedActualInfo] MismatchMsg
 -- Constructs a "Couldn't match" message
 -- The (Maybe ErrorItem) says whether this is the main top-level message (Just)
 --     or a supplementary message (Nothing)
@@ -3264,16 +3327,9 @@ mk_ea_msg ctxt at_top level
                          , kmismatch_expected = exp
                          , kmismatch_actual   = act }
   | Just item <- at_top
-  , let mismatch =
-          Mismatch
-            { mismatch_ea   = True
-            , mismatch_item = item
-            , mismatch_ty1  = exp
-            , mismatch_ty2  = act }
-  = Right $
-    if expanded_syns
-    then mkTcReportWithInfo mismatch [ea_expanded]
-    else mismatch
+  , let  ea = EA $ if expanded_syns then Just ea_expanded else Nothing
+         mismatch = mkBasicMismatchMsg ea item exp act
+  = Right mismatch
   | otherwise
   = Left $
     if expanded_syns
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index 34fba52546..a6125e7dfc 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -1,8 +1,11 @@
+{-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
 
 module GHC.Tc.Errors.Types (
   -- * Main types
     TcRnMessage(..)
+  , mkTcRnUnknownMessage
   , TcRnMessageDetailed(..)
   , ErrInfo(..)
   , FixedRuntimeRepProvenance(..)
@@ -48,9 +51,16 @@ module GHC.Tc.Errors.Types (
   , SolverReportWithCtxt(..)
   , SolverReportErrCtxt(..)
   , getUserGivens, discardProvCtxtGivens
-  , TcSolverReportMsg(..), TcSolverReportInfo(..)
+  , TcSolverReportMsg(..)
+  , CannotUnifyVariableReason(..)
+  , MismatchMsg(..)
+  , MismatchEA(..)
+  , mkPlainMismatchMsg, mkBasicMismatchMsg
+  , WhenMatching(..)
+  , ExpectedActualInfo(..)
+  , TyVarInfo(..), SameOccInfo(..)
+  , AmbiguityInfo(..)
   , CND_Extra(..)
-  , mkTcReportWithInfo
   , FitsMbSuppressed(..)
   , ValidHoleFits(..), noValidHoleFits
   , HoleFitDispConfig(..)
@@ -64,7 +74,7 @@ module GHC.Tc.Errors.Types (
   , UnsupportedCallConvention(..)
   , ExpectedBackends
   , ArgOrResult(..)
-  , MatchArgsContext(..)
+  , MatchArgsContext(..), MatchArgBadMatches(..)
   ) where
 
 import GHC.Prelude
@@ -111,10 +121,11 @@ import GHC.Data.FastString (FastString)
 import Language.Haskell.Syntax.Basic (FieldLabelString(..))
 
 import qualified Data.List.NonEmpty as NE
-import           Data.Typeable hiding (TyCon)
-import qualified Data.Semigroup as Semigroup
+import           Data.Typeable (Typeable)
 import GHC.Unit.Module.Warnings (WarningTxt)
 
+import GHC.Generics ( Generic )
+
 {-
 Note [Migrating TcM Messages]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -167,13 +178,17 @@ data TcRnMessageDetailed
   = TcRnMessageDetailed !ErrInfo
                         -- ^ Extra info associated with the message
                         !TcRnMessage
+  deriving Generic
+
+mkTcRnUnknownMessage :: (Diagnostic a, Typeable a) => a -> TcRnMessage
+mkTcRnUnknownMessage diag = TcRnUnknownMessage (UnknownDiagnostic diag)
 
 -- | An error which might arise during typechecking/renaming.
 data TcRnMessage where
   {-| Simply wraps a generic 'Diagnostic' message @a@. It can be used by plugins
       to provide custom diagnostic messages originated during typechecking/renaming.
   -}
-  TcRnUnknownMessage :: (Diagnostic a, Typeable a) => a -> TcRnMessage
+  TcRnUnknownMessage :: UnknownDiagnostic -> TcRnMessage
 
   {-| TcRnMessageWithInfo is a constructor which is used when extra information is needed
       to be provided in order to qualify a diagnostic and where it was originated (and why).
@@ -193,7 +208,7 @@ data TcRnMessage where
       See the documentation of the 'TcSolverReportMsg' datatype for an overview
       of the different errors.
   -}
-  TcRnSolverReport :: [SolverReportWithCtxt]
+  TcRnSolverReport :: SolverReportWithCtxt
                    -> DiagnosticReason
                    -> [GhcHint]
                    -> TcRnMessage
@@ -234,8 +249,8 @@ data TcRnMessage where
 
     Test cases: T7293, T7294, T15558, T17646, T18572, T18610, tcfail167.
   -}
-  TcRnInaccessibleCode :: Implication -- ^ The implication containing a contradiction.
-                       -> NE.NonEmpty SolverReportWithCtxt -- ^ The contradiction(s).
+  TcRnInaccessibleCode :: Implication          -- ^ The implication containing a contradiction.
+                       -> SolverReportWithCtxt -- ^ The contradiction.
                        -> TcRnMessage
 
   {-| A type which was expected to have a fixed runtime representation
@@ -263,7 +278,7 @@ data TcRnMessage where
 
      Test cases: th/T17804
   -}
-  TcRnImplicitLift :: Outputable var => var -> !ErrInfo -> TcRnMessage
+  TcRnImplicitLift :: Name -> !ErrInfo -> TcRnMessage
   {-| TcRnUnusedPatternBinds is a warning (controlled with -Wunused-pattern-binds)
       that occurs if a pattern binding binds no variables at all, unless it is a
       lone wild-card pattern, or a banged pattern.
@@ -1744,7 +1759,7 @@ data TcRnMessage where
 
     Test cases: ffi/should_fail/T20116
   -}
-  TcRnForeignImportPrimExtNotSet :: ForeignImport p -> TcRnMessage
+  TcRnForeignImportPrimExtNotSet :: ForeignImport GhcRn -> TcRnMessage
 
   {- TcRnForeignImportPrimSafeAnn is an error declaring that the safe/unsafe
      annotation should not be used with @prim@ foreign imports.
@@ -1754,7 +1769,7 @@ data TcRnMessage where
 
     Test cases: None
   -}
-  TcRnForeignImportPrimSafeAnn :: ForeignImport p -> TcRnMessage
+  TcRnForeignImportPrimSafeAnn :: ForeignImport GhcRn -> TcRnMessage
 
   {- TcRnForeignFunctionImportAsValue is an error explaining that foreign @value@
      imports cannot have function types.
@@ -1764,7 +1779,7 @@ data TcRnMessage where
 
     Test cases: ffi/should_fail/capi_value_function
   -}
-  TcRnForeignFunctionImportAsValue :: ForeignImport p -> TcRnMessage
+  TcRnForeignFunctionImportAsValue :: ForeignImport GhcRn -> TcRnMessage
 
   {- TcRnFunPtrImportWithoutAmpersand is a warning controlled by @-Wdodgy-foreign-imports@
      that informs the user of a possible missing @&@ in the declaration of a
@@ -1775,7 +1790,7 @@ data TcRnMessage where
 
     Test cases: ffi/should_compile/T1357
   -}
-  TcRnFunPtrImportWithoutAmpersand :: ForeignImport p -> TcRnMessage
+  TcRnFunPtrImportWithoutAmpersand :: ForeignImport GhcRn -> TcRnMessage
 
   {- TcRnIllegalForeignDeclBackend is an error occurring when a foreign import declaration
      is not compatible with the code generation backend being used.
@@ -1785,7 +1800,7 @@ data TcRnMessage where
     Test cases: None
   -}
   TcRnIllegalForeignDeclBackend
-    :: Either (ForeignExport p) (ForeignImport p)
+    :: Either (ForeignExport GhcRn) (ForeignImport GhcRn)
     -> Backend
     -> ExpectedBackends
     -> TcRnMessage
@@ -1799,7 +1814,9 @@ data TcRnMessage where
 
     Test cases: None
   -}
-  TcRnUnsupportedCallConv :: Either (ForeignExport p) (ForeignImport p) -> UnsupportedCallConvention -> TcRnMessage
+  TcRnUnsupportedCallConv :: Either (ForeignExport GhcRn) (ForeignImport GhcRn)
+                          -> UnsupportedCallConvention
+                          -> TcRnMessage
 
   {- TcRnIllegalForeignType is an error for when a type appears in a foreign
      function signature that is not compatible with the FFI.
@@ -2055,8 +2072,7 @@ data TcRnMessage where
   -}
   TcRnMatchesHaveDiffNumArgs
     :: !MatchArgsContext
-    -> !(LocatedA (Match GhcRn body))
-    -> !(NE.NonEmpty (LocatedA (Match GhcRn body))) -- ^ bad matches
+    -> !MatchArgBadMatches
     -> TcRnMessage
 
   {- TcRnCannotBindScopedTyVarInPatSig is an error stating that scoped type
@@ -2272,6 +2288,8 @@ data TcRnMessage where
             :: Name
             -> TcRnMessage
 
+  deriving Generic
+
 -- | Specifies which back ends can handle a requested foreign import or export
 type ExpectedBackends = [Backend]
 -- | Specifies which calling convention is unsupported on the current platform
@@ -2492,6 +2510,7 @@ data DeriveInstanceErrReason
   -- | We couldn't derive an instance either because the type was not an
   -- enum type or because it did have more than one constructor.
   | DerivErrEnumOrProduct !DeriveInstanceErrReason !DeriveInstanceErrReason
+  deriving Generic
 
 data DeriveInstanceBadConstructor
   =
@@ -2643,9 +2662,9 @@ See 'GHC.Tc.Errors.Types.SolverReport' and 'GHC.Tc.Errors.mkErrorReport'.
 -- See Note [Error report] for details.
 data SolverReport
   = SolverReport
-  { sr_important_msgs :: [SolverReportWithCtxt]
-  , sr_supplementary  :: [SolverReportSupplementary]
-  , sr_hints          :: [GhcHint]
+  { sr_important_msg :: SolverReportWithCtxt
+  , sr_supplementary :: [SolverReportSupplementary]
+  , sr_hints         :: [GhcHint]
   }
 
 -- | Additional information to print in a 'SolverReport', after the
@@ -2668,14 +2687,7 @@ data SolverReportWithCtxt =
     , reportContent :: TcSolverReportMsg
       -- ^ The content of the message to report.
     }
-
-instance Semigroup SolverReport where
-    SolverReport main1 supp1 hints1 <> SolverReport main2 supp2 hints2
-      = SolverReport (main1 ++ main2) (supp1 ++ supp2) (hints1 ++ hints2)
-
-instance Monoid SolverReport where
-    mempty = SolverReport [] [] []
-    mappend = (Semigroup.<>)
+  deriving Generic
 
 -- | Context needed when reporting a 'TcSolverReportMsg', such as
 -- the enclosing implication constraints or whether we are deferring type errors.
@@ -2820,15 +2832,6 @@ discardProvCtxtGivens orig givens  -- See Note [discardProvCtxtGivens]
 -- This is usually, some sort of unsolved constraint error,
 -- but we try to be specific about the precise problem we encountered.
 data TcSolverReportMsg
-  -- NB: this datatype is only a first step in refactoring GHC.Tc.Errors
-  -- to use the diagnostic infrastructure (TcRnMessage etc).
-  -- If you see possible improvements, please go right ahead!
-
-  -- | Wrap a message with additional information.
-  --
-  -- Prefer using the 'mkTcReportWithInfo' smart constructor
-  = TcReportWithInfo TcSolverReportMsg (NE.NonEmpty TcSolverReportInfo)
-
   -- | Quantified variables appear out of dependency order.
   --
   -- Example:
@@ -2836,7 +2839,7 @@ data TcSolverReportMsg
   --   forall (a :: k) k. ...
   --
   -- Test cases: BadTelescope2, T16418, T16247, T16726, T18451.
-  | BadTelescope TyVarBndrs [TyCoVar]
+  = BadTelescope TyVarBndrs [TyCoVar]
 
   -- | We came across a custom type error and we have decided to report it.
   --
@@ -2855,69 +2858,31 @@ data TcSolverReportMsg
   -- See 'HoleError'.
   | ReportHoleError Hole HoleError
 
-  -- | A type equality between a type variable and a polytype.
-  --
-  -- Test cases: T12427a, T2846b, T10194, ...
-  | CannotUnifyWithPolytype ErrorItem TyVar Type
-
-  -- | Couldn't unify two types or kinds.
-  --
-  --  Example:
-  --
-  --    3 + 3# -- can't match a lifted type with an unlifted type
+  -- | Trying to unify an untouchable variable, e.g. a variable from an outer scope.
   --
-  --  Test cases: T1396, T8263, ...
-  | Mismatch
-      { mismatch_ea   :: Bool        -- ^ Should this be phrased in terms of expected vs actual?
-      , mismatch_item :: ErrorItem   -- ^ The constraint in which the mismatch originated.
-      , mismatch_ty1  :: Type        -- ^ First type (the expected type if if mismatch_ea is True)
-      , mismatch_ty2  :: Type        -- ^ Second type (the actual type if mismatch_ea is True)
-      }
+  -- Test case: Simple14
+  | UntouchableVariable
+    { untouchableTyVar :: TyVar
+    , untouchableTyVarImplication :: Implication
+    }
 
-  -- | A type has an unexpected kind.
-  --
-  -- Test cases: T2994, T7609, ...
-  | KindMismatch
-      { kmismatch_what     :: TypedThing -- ^ What thing is 'kmismatch_actual' the kind of?
-      , kmismatch_expected :: Type
-      , kmismatch_actual   :: Type
-      }
-    -- TODO: combine 'Mismatch' and 'KindMismatch' messages.
+  -- | Cannot unify a variable, because of a type mismatch.
+  | CannotUnifyVariable
+    { mismatchMsg             :: MismatchMsg
+    , cannotUnifyReason       :: CannotUnifyVariableReason }
 
-  -- | A mismatch between two types, which arose from a type equality.
-  --
-  -- Test cases: T1470, tcfail212.
-  | TypeEqMismatch
-      { teq_mismatch_ppr_explicit_kinds :: Bool
-      , teq_mismatch_item     :: ErrorItem
-      , teq_mismatch_ty1      :: Type
-      , teq_mismatch_ty2      :: Type
-      , teq_mismatch_expected :: Type -- ^ The overall expected type
-      , teq_mismatch_actual   :: Type -- ^ The overall actual type
-      , teq_mismatch_what     :: Maybe TypedThing -- ^ What thing is 'teq_mismatch_actual' the kind of?
-      }
-    -- TODO: combine 'Mismatch' and 'TypeEqMismatch' messages.
+  -- | A mismatch between two types.
+  | Mismatch
+     { mismatchMsg           :: MismatchMsg
+     , mismatchTyVarInfo     :: Maybe TyVarInfo
+     , mismatchAmbiguityInfo :: [AmbiguityInfo]
+     , mismatchCoercibleInfo :: Maybe CoercibleMsg }
 
    -- | A violation of the representation-polymorphism invariants.
    --
    -- See 'FixedRuntimeRepErrorInfo' and 'FixedRuntimeRepContext' for more information.
   | FixedRuntimeRepError [FixedRuntimeRepErrorInfo]
 
-  -- | A skolem type variable escapes its scope.
-  --
-  -- Example:
-  --
-  --   data Ex where { MkEx :: a -> MkEx }
-  --   foo (MkEx x) = x
-  --
-  -- Test cases: TypeSkolEscape, T11142.
-  | SkolemEscape ErrorItem Implication [TyVar]
-
-  -- | Trying to unify an untouchable variable, e.g. a variable from an outer scope.
-  --
-  -- Test case: Simple14
-  | UntouchableVariable TyVar Implication
-
   -- | An equality between two types is blocked on a kind equality
   -- beteen their kinds.
   --
@@ -2944,21 +2909,6 @@ data TcSolverReportMsg
   | UnboundImplicitParams
       (NE.NonEmpty ErrorItem)
 
-  -- | Couldn't solve some Wanted constraints using the Givens.
-  -- This is the most commonly used constructor, used for generic
-  -- @"No instance for ..."@ and @"Could not deduce ... from"@ messages.
-  | CouldNotDeduce
-     { cnd_user_givens :: [Implication]
-        -- | The Wanted constraints we couldn't solve.
-        --
-        -- N.B.: the 'ErrorItem' at the head of the list has been tidied,
-        -- perhaps not the others.
-     , cnd_wanted      :: NE.NonEmpty ErrorItem
-
-       -- | Some additional info consumed by 'mk_supplementary_ea_msg'.
-     , cnd_extra       :: Maybe CND_Extra
-     }
-
   -- | A constraint couldn't be solved because it contains
   -- ambiguous type variables.
   --
@@ -3008,17 +2958,148 @@ data TcSolverReportMsg
     , unsafeOverlap_matches :: [ClsInst]
     , unsafeOverlapped      :: [ClsInst] }
 
+  deriving Generic
+
+data MismatchMsg
+  =  -- | Couldn't unify two types or kinds.
+  --
+  --  Example:
+  --
+  --    3 + 3# -- can't match a lifted type with an unlifted type
+  --
+  --  Test cases: T1396, T8263, ...
+    BasicMismatch -- SLD TODO rename this
+      { mismatch_ea           :: MismatchEA  -- ^ Should this be phrased in terms of expected vs actual?
+      , mismatch_item         :: ErrorItem   -- ^ The constraint in which the mismatch originated.
+      , mismatch_ty1          :: Type        -- ^ First type (the expected type if if mismatch_ea is True)
+      , mismatch_ty2          :: Type        -- ^ Second type (the actual type if mismatch_ea is True)
+      , mismatch_whenMatching :: Maybe WhenMatching
+      , mismatch_mb_same_occ  :: Maybe SameOccInfo
+      }
+
+  -- | A type has an unexpected kind.
+  --
+  -- Test cases: T2994, T7609, ...
+  | KindMismatch
+      { kmismatch_what     :: TypedThing -- ^ What thing is 'kmismatch_actual' the kind of?
+      , kmismatch_expected :: Type
+      , kmismatch_actual   :: Type
+      }
+    -- TODO: combine with 'BasicMismatch'.
+
+  -- | A mismatch between two types, which arose from a type equality.
+  --
+  -- Test cases: T1470, tcfail212.
+  | TypeEqMismatch
+      { teq_mismatch_ppr_explicit_kinds :: Bool
+      , teq_mismatch_item     :: ErrorItem
+      , teq_mismatch_ty1      :: Type
+      , teq_mismatch_ty2      :: Type
+      , teq_mismatch_expected :: Type -- ^ The overall expected type
+      , teq_mismatch_actual   :: Type -- ^ The overall actual type
+      , teq_mismatch_what     :: Maybe TypedThing -- ^ What thing is 'teq_mismatch_actual' the kind of?
+      , teq_mb_same_occ       :: Maybe SameOccInfo
+      }
+    -- TODO: combine with 'BasicMismatch'.
+
+  -- | Couldn't solve some Wanted constraints using the Givens.
+  -- Used for messages such as @"No instance for ..."@ and
+  -- @"Could not deduce ... from"@.
+  | CouldNotDeduce
+     { cnd_user_givens :: [Implication]
+        -- | The Wanted constraints we couldn't solve.
+        --
+        -- N.B.: the 'ErrorItem' at the head of the list has been tidied,
+        -- perhaps not the others.
+     , cnd_wanted      :: NE.NonEmpty ErrorItem
+
+       -- | Some additional info consumed by 'mk_supplementary_ea_msg'.
+     , cnd_extra       :: Maybe CND_Extra
+     }
+  deriving Generic
+
+mkBasicMismatchMsg :: MismatchEA -> ErrorItem -> Type -> Type -> MismatchMsg
+mkBasicMismatchMsg ea item ty1 ty2
+  = BasicMismatch
+      { mismatch_ea           = ea
+      , mismatch_item         = item
+      , mismatch_ty1          = ty1
+      , mismatch_ty2          = ty2
+      , mismatch_whenMatching = Nothing
+      , mismatch_mb_same_occ  = Nothing
+      }
+
+-- | Whether to use expected/actual in a type mismatch message.
+data MismatchEA
+  -- | Don't use expected/actual.
+  = NoEA
+  -- | Use expected/actual.
+  | EA
+  { mismatch_mbEA :: Maybe ExpectedActualInfo
+    -- ^ Whether to also mention type synonym expansion.
+  }
+
+data CannotUnifyVariableReason
+  =  -- | A type equality between a type variable and a polytype.
+    --
+    -- Test cases: T12427a, T2846b, T10194, ...
+    CannotUnifyWithPolytype ErrorItem TyVar Type (Maybe TyVarInfo)
+
+  -- | An occurs check.
+  | OccursCheck
+    { occursCheckInterestingTyVars :: [TyVar]
+    , occursCheckAmbiguityInfos    :: [AmbiguityInfo] }
+
+  -- | A skolem type variable escapes its scope.
+  --
+  -- Example:
+  --
+  --   data Ex where { MkEx :: a -> MkEx }
+  --   foo (MkEx x) = x
+  --
+  -- Test cases: TypeSkolEscape, T11142.
+  | SkolemEscape ErrorItem Implication [TyVar]
+
+  -- | Can't unify the type variable with the other type
+  -- due to the kind of type variable it is.
+  --
+  -- For example, trying to unify a 'SkolemTv' with the
+  -- type Int, or with a 'TyVarTv'.
+  | DifferentTyVars TyVarInfo
+  | RepresentationalEq TyVarInfo (Maybe CoercibleMsg)
+  deriving Generic
+
+mkPlainMismatchMsg :: MismatchMsg -> TcSolverReportMsg
+mkPlainMismatchMsg msg
+  = Mismatch
+     { mismatchMsg           = msg
+     , mismatchTyVarInfo     = Nothing
+     , mismatchAmbiguityInfo = []
+     , mismatchCoercibleInfo = Nothing }
+
 -- | Additional information to be given in a 'CouldNotDeduce' message,
 -- which is then passed on to 'mk_supplementary_ea_msg'.
 data CND_Extra = CND_Extra TypeOrKind Type Type
 
--- | Additional information that can be appended to an existing 'TcSolverReportMsg'.
-data TcSolverReportInfo
-  -- NB: this datatype is only a first step in refactoring GHC.Tc.Errors
-  -- to use the diagnostic infrastructure (TcRnMessage etc).
-  -- It would be better for these constructors to not be so closely tied
-  -- to the constructors of 'TcSolverReportMsg'.
-  -- If you see possible improvements, please go right ahead!
+-- | A cue to print out information about type variables,
+-- e.g. where they were bound, when there is a mismatch @tv1 ~ ty2@.
+data TyVarInfo =
+  TyVarInfo { thisTyVar :: TyVar
+            , thisTyVarIsUntouchable :: Maybe Implication
+            , otherTy   :: Maybe TyVar }
+
+-- | Add some information to disambiguate errors in which
+-- two 'Names' would otherwise appear to be identical.
+--
+-- See Note [Disambiguating (X ~ X) errors].
+data SameOccInfo
+  = SameOcc
+    { sameOcc_same_pkg :: Bool -- ^ Whether the two 'Name's also came from the same package.
+    , sameOcc_lhs :: Name
+    , sameOcc_rhs :: Name }
+
+-- | Add some information about ambiguity
+data AmbiguityInfo
 
   -- | Some type variables remained ambiguous: print them to the user.
   = Ambiguity
@@ -3028,38 +3109,24 @@ data TcSolverReportInfo
                                                 -- Guaranteed to not both be empty.
     }
 
-  -- | Specify some information about a type variable,
-  -- e.g. its 'SkolemInfo'.
-  | TyVarInfo TyVar
-
   -- | Remind the user that a particular type family is not injective.
   | NonInjectiveTyFam TyCon
 
-  -- | Explain why we couldn't coerce between two types. See 'CoercibleMsg'.
-  | ReportCoercibleMsg CoercibleMsg
-
+-- | Expected/actual information.
+data ExpectedActualInfo
   -- | Display the expected and actual types.
-  | ExpectedActual
+  = ExpectedActual
      { ea_expected, ea_actual :: Type }
 
   -- | Display the expected and actual types, after expanding type synonyms.
   | ExpectedActualAfterTySynExpansion
      { ea_expanded_expected, ea_expanded_actual :: Type }
 
-  -- | Explain how a kind equality originated.
-  | WhenMatching TcType TcType CtOrigin (Maybe TypeOrKind)
+-- | Explain how a kind equality originated.
+data WhenMatching
 
-  -- | Add some information to disambiguate errors in which
-  -- two 'Names' would otherwise appear to be identical.
-  --
-  -- See Note [Disambiguating (X ~ X) errors].
-  | SameOcc
-    { sameOcc_same_pkg :: Bool -- ^ Whether the two 'Name's also came from the same package.
-    , sameOcc_lhs :: Name
-    , sameOcc_rhs :: Name }
-
-  -- | Report some type variables that might be participating in an occurs-check failure.
-  | OccursCheckInterestingTyVars (NE.NonEmpty TyVar)
+  = WhenMatching TcType TcType CtOrigin (Maybe TypeOrKind)
+  deriving Generic
 
 -- | Some form of @"not in scope"@ error. See also the 'OutOfScopeHole'
 -- constructor of 'HoleError'.
@@ -3099,6 +3166,7 @@ data NotInScopeError
   -- or, a class doesn't have an associated type with this name,
   -- or, a record doesn't have a record field with this name.
   | UnknownSubordinate SDoc
+  deriving Generic
 
 -- | Create a @"not in scope"@ error message for the given 'RdrName'.
 mkTcRnNotInScope :: RdrName -> NotInScopeError -> TcRnMessage
@@ -3175,15 +3243,6 @@ data PotentialInstances
   , unifiers :: [ClsInst]
   }
 
--- | Append additional information to a `TcSolverReportMsg`.
-mkTcReportWithInfo :: TcSolverReportMsg -> [TcSolverReportInfo] -> TcSolverReportMsg
-mkTcReportWithInfo msg []
-  = msg
-mkTcReportWithInfo (TcReportWithInfo msg (prev NE.:| prevs)) infos
-  = TcReportWithInfo msg (prev NE.:| prevs ++ infos)
-mkTcReportWithInfo msg (info : infos)
-  = TcReportWithInfo msg (info NE.:| infos)
-
 -- | A collection of valid hole fits or refinement fits,
 -- in which some fits might have been suppressed.
 data FitsMbSuppressed
@@ -3323,3 +3382,11 @@ data MatchArgsContext
       !Name -- ^ Name of the function
   | PatternArgs
       !(HsMatchContext GhcTc) -- ^ Pattern match specifics
+
+-- | The information necessary to report mismatched
+-- numbers of arguments in a match group.
+data MatchArgBadMatches where
+  MatchArgMatches
+    ::  { matchArgFirstMatch :: LocatedA (Match GhcRn body)
+        , matchArgBadMatches :: NE.NonEmpty (LocatedA (Match GhcRn body)) }
+    -> MatchArgBadMatches