Fix #13819 by refactoring TypeEqOrigin.uo_thing

The uo_thing field of TypeEqOrigin is used to track the
"thing" (either term or type) that has the type (kind) stored
in the TypeEqOrigin fields. Previously, this was sometimes a
proper Core Type, which needed zonking and tidying. Now, it
is only HsSyn: much simpler, and the error messages now use
the user-written syntax.

But this aspect of uo_thing didn't cause #13819; it was the
sibling field uo_arity that did. uo_arity stored the number
of arguments of uo_thing, useful when reporting something
like "should have written 2 fewer arguments". We wouldn't want
to say that if the thing didn't have two arguments. However,
in practice, GHC was getting this wrong, and this message
didn't seem all that helpful. Furthermore, the calculation
of the number of arguments is what caused #13819 to fall over.
This patch just removes uo_arity. In my opinion, the change
to error messages is a nudge in the right direction.

Test case: typecheck/should_fail/T13819

17 files changed, 169 insertions, 213 deletions

diff --git a/compiler/ghci/RtClosureInspect.hs b/compiler/ghci/RtClosureInspect.hs
index 785513b3b6..263aeba7e9 100644
--- a/compiler/ghci/RtClosureInspect.hs
+++ b/compiler/ghci/RtClosureInspect.hs
@@ -637,7 +637,7 @@ addConstraint actual expected = do
       discardResult $
       captureConstraints $
       do { (ty1, ty2) <- congruenceNewtypes actual expected
-         ; unifyType noThing ty1 ty2 }
+         ; unifyType Nothing ty1 ty2 }
      -- TOMDO: what about the coercion?
      -- we should consider family instances
 
@@ -1186,7 +1186,7 @@ congruenceNewtypes lhs rhs = go lhs rhs >>= \rhs' -> return (lhs,rhs')
                (_, vars) <- instTyVars (tyConTyVars new_tycon)
                let ty' = mkTyConApp new_tycon (mkTyVarTys vars)
                    rep_ty = unwrapType ty'
-               _ <- liftTcM (unifyType noThing ty rep_ty)
+               _ <- liftTcM (unifyType Nothing ty rep_ty)
         -- assumes that reptype doesn't ^^^^ touch tyconApp args
                return ty'
 
diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs
index 20c3d5cbb9..9c59c0c451 100644
--- a/compiler/typecheck/Inst.hs
+++ b/compiler/typecheck/Inst.hs
@@ -33,7 +33,7 @@ module Inst (
 #include "HsVersions.h"
 
 import {-# SOURCE #-}   TcExpr( tcPolyExpr, tcSyntaxOp )
-import {-# SOURCE #-}   TcUnify( unifyType, unifyKind, noThing )
+import {-# SOURCE #-}   TcUnify( unifyType, unifyKind )
 
 import BasicTypes ( IntegralLit(..), SourceText(..) )
 import FastString
@@ -324,13 +324,13 @@ instCallConstraints orig preds
   where
     go pred
      | Just (Nominal, ty1, ty2) <- getEqPredTys_maybe pred -- Try short-cut #1
-     = do  { co <- unifyType noThing ty1 ty2
+     = do  { co <- unifyType Nothing ty1 ty2
            ; return (EvCoercion co) }
 
        -- Try short-cut #2
      | Just (tc, args@[_, _, ty1, ty2]) <- splitTyConApp_maybe pred
      , tc `hasKey` heqTyConKey
-     = do { co <- unifyType noThing ty1 ty2
+     = do { co <- unifyType Nothing ty1 ty2
           ; return (EvDFunApp (dataConWrapId heqDataCon) args [EvCoercion co]) }
 
      | otherwise
@@ -409,7 +409,7 @@ tcInstBinder _ subst (Anon ty)
                                    , uo_expected = k2
                                    , uo_thing    = Nothing }
        ; co <- case role of
-                 Nominal          -> unifyKind noThing k1 k2
+                 Nominal          -> unifyKind Nothing k1 k2
                  Representational -> emitWantedEq origin KindLevel role k1 k2
                  Phantom          -> pprPanic "tcInstBinder Phantom" (ppr ty)
        ; arg' <- mk co k1 k2
diff --git a/compiler/typecheck/TcArrows.hs b/compiler/typecheck/TcArrows.hs
index b72b9b193c..d74794922d 100644
--- a/compiler/typecheck/TcArrows.hs
+++ b/compiler/typecheck/TcArrows.hs
@@ -275,7 +275,7 @@ tc_cmd env
 --              Do notation
 
 tc_cmd env (HsCmdDo (L l stmts) _) (cmd_stk, res_ty)
-  = do  { co <- unifyType noThing unitTy cmd_stk  -- Expecting empty argument stack
+  = do  { co <- unifyType Nothing unitTy cmd_stk  -- Expecting empty argument stack
         ; stmts' <- tcStmts ArrowExpr (tcArrDoStmt env) stmts res_ty
         ; return (mkHsCmdWrap (mkWpCastN co) (HsCmdDo (L l stmts') res_ty)) }
 
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index ea107a86da..3c6a1b7fe3 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -1684,7 +1684,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2
   = do { let main_msg = addArising (ctOrigin ct) $
                         vcat [ hang (text "Kind mismatch: cannot unify" <+>
                                      parens (ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)) <+>
-                                     text "with")
+                                     text "with:")
                                   2 (sep [ppr ty2, dcolon, ppr k2])
                              , text "Their kinds differ." ]
              cast_msg
@@ -1999,7 +1999,7 @@ mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
         -> empty
 
     thing_msg = case maybe_thing of
-                  Just thing -> \_ -> quotes (ppr thing) <+> text "is"
+                  Just thing -> \_ -> quotes thing <+> text "is"
                   Nothing    -> \vowel -> text "got a" <>
                                           if vowel then char 'n' else empty
     msg2 = sep [ text "Expecting a lifted type, but"
@@ -2009,12 +2009,12 @@ mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
     msg4 = maybe_num_args_msg $$
            sep [ text "Expected a type, but"
                , maybe (text "found something with kind")
-                       (\thing -> quotes (ppr thing) <+> text "has kind")
+                       (\thing -> quotes thing <+> text "has kind")
                        maybe_thing
                , quotes (ppr act) ]
 
     msg5 th = hang (text "Expected" <+> kind_desc <> comma)
-                 2 (text "but" <+> quotes (ppr th) <+> text "has kind" <+>
+                 2 (text "but" <+> quotes th <+> text "has kind" <+>
                     quotes (ppr act))
       where
         kind_desc | isConstraintKind exp = text "a constraint"
@@ -2026,17 +2026,13 @@ mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
         -> let n_act = count_args act
                n_exp = count_args exp in
            case n_act - n_exp of
-             n | n /= 0
+             n | n > 0   -- we don't know how many args there are, so don't
+                         -- recommend removing args that aren't
                , Just thing <- maybe_thing
-               , case errorThingNumArgs_maybe thing of
-                   Nothing           -> n > 0
-                   Just num_act_args -> num_act_args >= -n
-                     -- don't report to strip off args that aren't there
                -> Just $ text "Expecting" <+> speakN (abs n) <+>
-                         more_or_fewer <+> quotes (ppr thing)
+                         more <+> quotes thing
                where
-                 more_or_fewer
-                  | n < 0     = text "fewer arguments to"
+                 more
                   | n == 1    = text "more argument to"
                   | otherwise = text "more arguments to"  -- n > 1
              _ -> Nothing
diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs
index 0e1e8662bf..1896c6843f 100644
--- a/compiler/typecheck/TcExpr.hs
+++ b/compiler/typecheck/TcExpr.hs
@@ -166,8 +166,8 @@ NB: The res_ty is always deeply skolemised.
 -}
 
 tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTcId)
-tcExpr (HsVar (L _ name)) res_ty = tcCheckId name res_ty
-tcExpr (HsUnboundVar uv)  res_ty = tcUnboundId uv res_ty
+tcExpr (HsVar (L _ name))   res_ty = tcCheckId name res_ty
+tcExpr e@(HsUnboundVar uv)  res_ty = tcUnboundId e uv res_ty
 
 tcExpr e@(HsApp {})     res_ty = tcApp1 e res_ty
 tcExpr e@(HsAppType {}) res_ty = tcApp1 e res_ty
@@ -370,7 +370,7 @@ tcExpr expr@(OpApp arg1 op fix arg2) res_ty
        ; let doc   = text "The first argument of ($) takes"
              orig1 = lexprCtOrigin arg1
        ; (wrap_arg1, [arg2_sigma], op_res_ty) <-
-           matchActualFunTys doc orig1 (Just arg1) 1 arg1_ty
+           matchActualFunTys doc orig1 (Just (unLoc arg1)) 1 arg1_ty
 
          -- We have (arg1 $ arg2)
          -- So: arg1_ty = arg2_ty -> op_res_ty
@@ -385,7 +385,7 @@ tcExpr expr@(OpApp arg1 op fix arg2) res_ty
        --
        -- The *result* type can have any kind (Trac #8739),
        -- so we don't need to check anything for that
-       ; _ <- unifyKind (Just arg2_sigma) (typeKind arg2_sigma) liftedTypeKind
+       ; _ <- unifyKind (Just (HsCoreTy arg2_sigma)) (typeKind arg2_sigma) liftedTypeKind
            -- ignore the evidence. arg2_sigma must have type * or #,
            -- because we know arg2_sigma -> or_res_ty is well-kinded
            -- (because otherwise matchActualFunTys would fail)
@@ -434,7 +434,7 @@ tcExpr expr@(OpApp arg1 op fix arg2) res_ty
 tcExpr expr@(SectionR op arg2) res_ty
   = do { (op', op_ty) <- tcInferFun op
        ; (wrap_fun, [arg1_ty, arg2_ty], op_res_ty)
-                  <- matchActualFunTys (mk_op_msg op) fn_orig (Just op) 2 op_ty
+                  <- matchActualFunTys (mk_op_msg op) fn_orig (Just (unLoc op)) 2 op_ty
        ; wrap_res <- tcSubTypeHR SectionOrigin (Just expr)
                                  (mkFunTy arg1_ty op_res_ty) res_ty
        ; arg2' <- tcArg op arg2 arg2_ty 2
@@ -453,7 +453,7 @@ tcExpr expr@(SectionL arg1 op) res_ty
                          | otherwise                            = 2
 
        ; (wrap_fn, (arg1_ty:arg_tys), op_res_ty)
-           <- matchActualFunTys (mk_op_msg op) fn_orig (Just op)
+           <- matchActualFunTys (mk_op_msg op) fn_orig (Just (unLoc op))
                                 n_reqd_args op_ty
        ; wrap_res <- tcSubTypeHR SectionOrigin (Just expr)
                                  (mkFunTys arg_tys op_res_ty) res_ty
@@ -938,7 +938,7 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty
 
         ; wrap_res <- tcSubTypeHR (exprCtOrigin expr)
                                   (Just expr) rec_res_ty res_ty
-        ; co_scrut <- unifyType (Just record_expr) record_rho scrut_ty
+        ; co_scrut <- unifyType (Just (unLoc record_expr)) record_rho scrut_ty
                 -- NB: normal unification is OK here (as opposed to subsumption),
                 -- because for this to work out, both record_rho and scrut_ty have
                 -- to be normal datatypes -- no contravariant stuff can go on
@@ -974,8 +974,8 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty
                     , rupd_cons = relevant_cons, rupd_in_tys = scrut_inst_tys
                     , rupd_out_tys = result_inst_tys, rupd_wrap = req_wrap } }
 
-tcExpr (HsRecFld f) res_ty
-    = tcCheckRecSelId f res_ty
+tcExpr e@(HsRecFld f) res_ty
+    = tcCheckRecSelId e f res_ty
 
 {-
 ************************************************************************
@@ -1037,10 +1037,10 @@ tcExpr (HsSpliceE (HsSpliced mod_finalizers (HsSplicedExpr expr)))
        tcExpr expr res_ty
 tcExpr (HsSpliceE splice)        res_ty
   = tcSpliceExpr splice res_ty
-tcExpr (HsBracket brack)         res_ty
-  = tcTypedBracket   brack res_ty
-tcExpr (HsRnBracketOut brack ps) res_ty
-  = tcUntypedBracket brack ps res_ty
+tcExpr e@(HsBracket brack)         res_ty
+  = tcTypedBracket e brack res_ty
+tcExpr e@(HsRnBracketOut brack ps) res_ty
+  = tcUntypedBracket e brack ps res_ty
 
 {-
 ************************************************************************
@@ -1194,7 +1194,7 @@ tcApp m_herald orig_fun orig_args res_ty
                 -- up to call that function
            ; wrap_res <- addFunResCtxt True (unLoc fun) actual_res_ty res_ty $
                          tcSubTypeDS_NC_O orig GenSigCtxt
-                           (Just $ foldl mk_hs_app fun args)
+                           (Just $ unLoc $ foldl mk_hs_app fun args)
                            actual_res_ty res_ty
 
            ; return (wrap_res, mkLHsWrap wrap_fun fun1, args1) }
@@ -1290,7 +1290,7 @@ tcArgs fun orig_fun_ty fun_orig orig_args herald
 
     go acc_args n fun_ty (Left arg : args)
       = do { (wrap, [arg_ty], res_ty)
-               <- matchActualFunTysPart herald fun_orig (Just fun) 1 fun_ty
+               <- matchActualFunTysPart herald fun_orig (Just (unLoc fun)) 1 fun_ty
                                         acc_args orig_arity
                -- wrap :: fun_ty "->" arg_ty -> res_ty
            ; arg' <- tcArg fun arg arg_ty n
@@ -1449,7 +1449,7 @@ tcSynArgA :: CtOrigin
             -- and a wrapper to be applied to the overall expression
 tcSynArgA orig sigma_ty arg_shapes res_shape thing_inside
   = do { (match_wrapper, arg_tys, res_ty)
-           <- matchActualFunTys herald orig noThing (length arg_shapes) sigma_ty
+           <- matchActualFunTys herald orig Nothing (length arg_shapes) sigma_ty
               -- match_wrapper :: sigma_ty "->" (arg_tys -> res_ty)
        ; ((result, res_wrapper), arg_wrappers)
            <- tc_syn_args_e arg_tys arg_shapes $ \ arg_results ->
@@ -1623,18 +1623,18 @@ tcCheckId name res_ty
   = do { (expr, actual_res_ty) <- tcInferId name
        ; traceTc "tcCheckId" (vcat [ppr name, ppr actual_res_ty, ppr res_ty])
        ; addFunResCtxt False (HsVar (noLoc name)) actual_res_ty res_ty $
-         tcWrapResultO (OccurrenceOf name)  expr actual_res_ty res_ty }
+         tcWrapResultO (OccurrenceOf name) (HsVar (noLoc name)) expr actual_res_ty res_ty }
 
-tcCheckRecSelId :: AmbiguousFieldOcc GhcRn -> ExpRhoType -> TcM (HsExpr GhcTcId)
-tcCheckRecSelId f@(Unambiguous (L _ lbl) _) res_ty
+tcCheckRecSelId :: HsExpr GhcRn -> AmbiguousFieldOcc GhcRn -> ExpRhoType -> TcM (HsExpr GhcTcId)
+tcCheckRecSelId rn_expr f@(Unambiguous (L _ lbl) _) res_ty
   = do { (expr, actual_res_ty) <- tcInferRecSelId f
        ; addFunResCtxt False (HsRecFld f) actual_res_ty res_ty $
-         tcWrapResultO (OccurrenceOfRecSel lbl) expr actual_res_ty res_ty }
-tcCheckRecSelId (Ambiguous lbl _) res_ty
+         tcWrapResultO (OccurrenceOfRecSel lbl) rn_expr expr actual_res_ty res_ty }
+tcCheckRecSelId rn_expr (Ambiguous lbl _) res_ty
   = case tcSplitFunTy_maybe =<< checkingExpType_maybe res_ty of
       Nothing       -> ambiguousSelector lbl
       Just (arg, _) -> do { sel_name <- disambiguateSelector lbl arg
-                          ; tcCheckRecSelId (Unambiguous lbl sel_name) res_ty }
+                          ; tcCheckRecSelId rn_expr (Unambiguous lbl sel_name) res_ty }
 
 ------------------------
 tcInferRecSelId :: AmbiguousFieldOcc GhcRn -> TcM (HsExpr GhcTcId, TcRhoType)
@@ -1724,7 +1724,7 @@ tc_infer_id lbl id_name
       | otherwise                  = return ()
 
 
-tcUnboundId :: UnboundVar -> ExpRhoType -> TcM (HsExpr GhcTcId)
+tcUnboundId :: HsExpr GhcRn -> UnboundVar -> ExpRhoType -> TcM (HsExpr GhcTcId)
 -- Typecheck an occurrence of an unbound Id
 --
 -- Some of these started life as a true expression hole "_".
@@ -1733,7 +1733,7 @@ tcUnboundId :: UnboundVar -> ExpRhoType -> TcM (HsExpr GhcTcId)
 -- We turn all of them into HsVar, since HsUnboundVar can't contain an
 -- Id; and indeed the evidence for the CHoleCan does bind it, so it's
 -- not unbound any more!
-tcUnboundId unbound res_ty
+tcUnboundId rn_expr unbound res_ty
  = do { ty <- newOpenFlexiTyVarTy  -- Allow Int# etc (Trac #12531)
       ; let occ = unboundVarOcc unbound
       ; name <- newSysName occ
@@ -1745,7 +1745,7 @@ tcUnboundId unbound res_ty
                                               , ctev_loc  = loc}
                            , cc_hole = ExprHole unbound }
       ; emitInsoluble can
-      ; tcWrapResultO (UnboundOccurrenceOf occ) (HsVar (noLoc ev)) ty res_ty }
+      ; tcWrapResultO (UnboundOccurrenceOf occ) rn_expr (HsVar (noLoc ev)) ty res_ty }
 
 
 {-
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 045a0a1983..bca9cc3b13 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -270,11 +270,12 @@ tcHsClsInstType user_ctxt hs_inst_ty
 -- Used for 'VECTORISE [SCALAR] instance' declarations
 tcHsVectInst :: LHsSigType GhcRn -> TcM (Class, [Type])
 tcHsVectInst ty
-  | Just (L _ cls_name, tys) <- hsTyGetAppHead_maybe (hsSigType ty)
+  | let hs_cls_ty = hsSigType ty
+  , Just (L _ cls_name, tys) <- hsTyGetAppHead_maybe hs_cls_ty
     -- Ignoring the binders looks pretty dodgy to me
   = do { (cls, cls_kind) <- tcClass cls_name
        ; (applied_class, _res_kind)
-           <- tcInferApps typeLevelMode cls_name (mkClassPred cls []) cls_kind tys
+           <- tcInferApps typeLevelMode hs_cls_ty (mkClassPred cls []) cls_kind tys
        ; case tcSplitTyConApp_maybe applied_class of
            Just (_tc, args) -> ASSERT( _tc == classTyCon cls )
                                return (cls, args)
@@ -470,11 +471,11 @@ tc_infer_hs_type mode (HsAppTy ty1 ty2)
        ; fun_kind' <- zonkTcType fun_kind
        ; tcInferApps mode fun_ty fun_ty' fun_kind' arg_tys }
 tc_infer_hs_type mode (HsParTy t)     = tc_infer_lhs_type mode t
-tc_infer_hs_type mode (HsOpTy lhs (L _ op) rhs)
+tc_infer_hs_type mode (HsOpTy lhs (L loc_op op) rhs)
   | not (op `hasKey` funTyConKey)
   = do { (op', op_kind) <- tcTyVar mode op
        ; op_kind' <- zonkTcType op_kind
-       ; tcInferApps mode op op' op_kind' [lhs, rhs] }
+       ; tcInferApps mode (noLoc $ HsTyVar NotPromoted (L loc_op op)) op' op_kind' [lhs, rhs] }
 tc_infer_hs_type mode (HsKindSig ty sig)
   = do { sig' <- tc_lhs_kind (kindLevel mode) sig
        ; ty' <- tc_lhs_type mode ty sig'
@@ -510,11 +511,11 @@ tc_fun_type mode ty1 ty2 exp_kind = case mode_level mode of
        ; res_k <- newOpenTypeKind
        ; ty1' <- tc_lhs_type mode ty1 arg_k
        ; ty2' <- tc_lhs_type mode ty2 res_k
-       ; checkExpectedKind (mkFunTy ty1' ty2') liftedTypeKind exp_kind }
+       ; checkExpectedKind (HsFunTy ty1 ty2) (mkFunTy ty1' ty2') liftedTypeKind exp_kind }
   KindLevel ->  -- no representation polymorphism in kinds. yet.
     do { ty1' <- tc_lhs_type mode ty1 liftedTypeKind
        ; ty2' <- tc_lhs_type mode ty2 liftedTypeKind
-       ; checkExpectedKind (mkFunTy ty1' ty2') liftedTypeKind exp_kind }
+       ; checkExpectedKind (HsFunTy ty1 ty2) (mkFunTy ty1' ty2') liftedTypeKind exp_kind }
 
 ------------------------------------------
 -- See also Note [Bidirectional type checking]
@@ -579,30 +580,30 @@ tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind
                 else do { ek <- newOpenTypeKind
                                 -- The body kind (result of the function)
                                 -- can be * or #, hence newOpenTypeKind
-                        ; ty <- tc_lhs_type mode ty ek
-                        ; checkExpectedKind ty liftedTypeKind exp_kind }
+                        ; ty' <- tc_lhs_type mode ty ek
+                        ; checkExpectedKind (unLoc ty) ty' liftedTypeKind exp_kind }
 
        ; return (mkPhiTy ctxt' ty') }
 
 --------- Lists, arrays, and tuples
-tc_hs_type mode (HsListTy elt_ty) exp_kind
+tc_hs_type mode rn_ty@(HsListTy elt_ty) exp_kind
   = do { tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
        ; checkWiredInTyCon listTyCon
-       ; checkExpectedKind (mkListTy tau_ty) liftedTypeKind exp_kind }
+       ; checkExpectedKind rn_ty (mkListTy tau_ty) liftedTypeKind exp_kind }
 
-tc_hs_type mode (HsPArrTy elt_ty) exp_kind
+tc_hs_type mode rn_ty@(HsPArrTy elt_ty) exp_kind
   = do { MASSERT( isTypeLevel (mode_level mode) )
        ; tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
        ; checkWiredInTyCon parrTyCon
-       ; checkExpectedKind (mkPArrTy tau_ty) liftedTypeKind exp_kind }
+       ; checkExpectedKind rn_ty (mkPArrTy tau_ty) liftedTypeKind exp_kind }
 
 -- See Note [Distinguishing tuple kinds] in HsTypes
 -- See Note [Inferring tuple kinds]
-tc_hs_type mode (HsTupleTy HsBoxedOrConstraintTuple hs_tys) exp_kind
+tc_hs_type mode rn_ty@(HsTupleTy HsBoxedOrConstraintTuple hs_tys) exp_kind
      -- (NB: not zonking before looking at exp_k, to avoid left-right bias)
   | Just tup_sort <- tupKindSort_maybe exp_kind
   = traceTc "tc_hs_type tuple" (ppr hs_tys) >>
-    tc_tuple mode tup_sort hs_tys exp_kind
+    tc_tuple rn_ty mode tup_sort hs_tys exp_kind
   | otherwise
   = do { traceTc "tc_hs_type tuple 2" (ppr hs_tys)
        ; (tys, kinds) <- mapAndUnzipM (tc_infer_lhs_type mode) hs_tys
@@ -620,14 +621,14 @@ tc_hs_type mode (HsTupleTy HsBoxedOrConstraintTuple hs_tys) exp_kind
          -- In the [] case, it's not clear what the kind is, so guess *
 
        ; tys' <- sequence [ setSrcSpan loc $
-                            checkExpectedKind ty kind arg_kind
-                          | ((L loc _),ty,kind) <- zip3 hs_tys tys kinds ]
+                            checkExpectedKind hs_ty ty kind arg_kind
+                          | ((L loc hs_ty),ty,kind) <- zip3 hs_tys tys kinds ]
 
-       ; finish_tuple tup_sort tys' (map (const arg_kind) tys') exp_kind }
+       ; finish_tuple rn_ty tup_sort tys' (map (const arg_kind) tys') exp_kind }
 
 
-tc_hs_type mode (HsTupleTy hs_tup_sort tys) exp_kind
-  = tc_tuple mode tup_sort tys exp_kind
+tc_hs_type mode rn_ty@(HsTupleTy hs_tup_sort tys) exp_kind
+  = tc_tuple rn_ty mode tup_sort tys exp_kind
   where
     tup_sort = case hs_tup_sort of  -- Fourth case dealt with above
                   HsUnboxedTuple    -> UnboxedTuple
@@ -635,28 +636,29 @@ tc_hs_type mode (HsTupleTy hs_tup_sort tys) exp_kind
                   HsConstraintTuple -> ConstraintTuple
                   _                 -> panic "tc_hs_type HsTupleTy"
 
-tc_hs_type mode (HsSumTy hs_tys) exp_kind
+tc_hs_type mode rn_ty@(HsSumTy hs_tys) exp_kind
   = do { let arity = length hs_tys
        ; arg_kinds <- mapM (\_ -> newOpenTypeKind) hs_tys
        ; tau_tys   <- zipWithM (tc_lhs_type mode) hs_tys arg_kinds
        ; let arg_reps = map (getRuntimeRepFromKind "tc_hs_type HsSumTy") arg_kinds
              arg_tys  = arg_reps ++ tau_tys
-       ; checkExpectedKind (mkTyConApp (sumTyCon arity) arg_tys)
+       ; checkExpectedKind rn_ty
+                           (mkTyConApp (sumTyCon arity) arg_tys)
                            (unboxedSumKind arg_reps)
                            exp_kind
        }
 
 --------- Promoted lists and tuples
-tc_hs_type mode (HsExplicitListTy _ _k tys) exp_kind
+tc_hs_type mode rn_ty@(HsExplicitListTy _ _k tys) exp_kind
   = do { tks <- mapM (tc_infer_lhs_type mode) tys
-       ; (taus', kind) <- unifyKinds tks
+       ; (taus', kind) <- unifyKinds tys tks
        ; let ty = (foldr (mk_cons kind) (mk_nil kind) taus')
-       ; checkExpectedKind ty (mkListTy kind) exp_kind }
+       ; checkExpectedKind rn_ty ty (mkListTy kind) exp_kind }
   where
     mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
     mk_nil  k     = mkTyConApp (promoteDataCon nilDataCon) [k]
 
-tc_hs_type mode (HsExplicitTupleTy _ tys) exp_kind
+tc_hs_type mode rn_ty@(HsExplicitTupleTy _ tys) exp_kind
   -- using newMetaKindVar means that we force instantiations of any polykinded
   -- types. At first, I just used tc_infer_lhs_type, but that led to #11255.
   = do { ks   <- replicateM arity newMetaKindVar
@@ -664,35 +666,35 @@ tc_hs_type mode (HsExplicitTupleTy _ tys) exp_kind
        ; let kind_con   = tupleTyCon           Boxed arity
              ty_con     = promotedTupleDataCon Boxed arity
              tup_k      = mkTyConApp kind_con ks
-       ; checkExpectedKind (mkTyConApp ty_con (ks ++ taus)) tup_k exp_kind }
+       ; checkExpectedKind rn_ty (mkTyConApp ty_con (ks ++ taus)) tup_k exp_kind }
   where
     arity = length tys
 
 --------- Constraint types
-tc_hs_type mode (HsIParamTy (L _ n) ty) exp_kind
+tc_hs_type mode rn_ty@(HsIParamTy (L _ n) ty) exp_kind
   = do { MASSERT( isTypeLevel (mode_level mode) )
        ; ty' <- tc_lhs_type mode ty liftedTypeKind
        ; let n' = mkStrLitTy $ hsIPNameFS n
        ; ipClass <- tcLookupClass ipClassName
-       ; checkExpectedKind (mkClassPred ipClass [n',ty'])
+       ; checkExpectedKind rn_ty (mkClassPred ipClass [n',ty'])
            constraintKind exp_kind }
 
-tc_hs_type mode (HsEqTy ty1 ty2) exp_kind
+tc_hs_type mode rn_ty@(HsEqTy ty1 ty2) exp_kind
   = do { (ty1', kind1) <- tc_infer_lhs_type mode ty1
        ; (ty2', kind2) <- tc_infer_lhs_type mode ty2
-       ; ty2'' <- checkExpectedKind ty2' kind2 kind1
+       ; ty2'' <- checkExpectedKind (unLoc ty2) ty2' kind2 kind1
        ; eq_tc <- tcLookupTyCon eqTyConName
        ; let ty' = mkNakedTyConApp eq_tc [kind1, ty1', ty2'']
-       ; checkExpectedKind ty' constraintKind exp_kind }
+       ; checkExpectedKind rn_ty ty' constraintKind exp_kind }
 
 --------- Literals
-tc_hs_type _ (HsTyLit (HsNumTy _ n)) exp_kind
+tc_hs_type _ rn_ty@(HsTyLit (HsNumTy _ n)) exp_kind
   = do { checkWiredInTyCon typeNatKindCon
-       ; checkExpectedKind (mkNumLitTy n) typeNatKind exp_kind }
+       ; checkExpectedKind rn_ty (mkNumLitTy n) typeNatKind exp_kind }
 
-tc_hs_type _ (HsTyLit (HsStrTy _ s)) exp_kind
+tc_hs_type _ rn_ty@(HsTyLit (HsStrTy _ s)) exp_kind
   = do { checkWiredInTyCon typeSymbolKindCon
-       ; checkExpectedKind (mkStrLitTy s) typeSymbolKind exp_kind }
+       ; checkExpectedKind rn_ty (mkStrLitTy s) typeSymbolKind exp_kind }
 
 --------- Potentially kind-polymorphic types: call the "up" checker
 -- See Note [Future-proofing the type checker]
@@ -723,7 +725,7 @@ tcWildCardOcc wc_info exp_kind
 tc_infer_hs_type_ek :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
 tc_infer_hs_type_ek mode ty ek
   = do { (ty', k) <- tc_infer_hs_type mode ty
-       ; checkExpectedKind ty' k ek }
+       ; checkExpectedKind ty ty' k ek }
 
 ---------------------------
 tupKindSort_maybe :: TcKind -> Maybe TupleSort
@@ -734,23 +736,24 @@ tupKindSort_maybe k
   | isLiftedTypeKind k = Just BoxedTuple
   | otherwise          = Nothing
 
-tc_tuple :: TcTyMode -> TupleSort -> [LHsType GhcRn] -> TcKind -> TcM TcType
-tc_tuple mode tup_sort tys exp_kind
+tc_tuple :: HsType GhcRn -> TcTyMode -> TupleSort -> [LHsType GhcRn] -> TcKind -> TcM TcType
+tc_tuple rn_ty mode tup_sort tys exp_kind
   = do { arg_kinds <- case tup_sort of
            BoxedTuple      -> return (nOfThem arity liftedTypeKind)
            UnboxedTuple    -> mapM (\_ -> newOpenTypeKind) tys
            ConstraintTuple -> return (nOfThem arity constraintKind)
        ; tau_tys <- zipWithM (tc_lhs_type mode) tys arg_kinds
-       ; finish_tuple tup_sort tau_tys arg_kinds exp_kind }
+       ; finish_tuple rn_ty tup_sort tau_tys arg_kinds exp_kind }
   where
     arity   = length tys
 
-finish_tuple :: TupleSort
+finish_tuple :: HsType GhcRn
+             -> TupleSort
              -> [TcType]    -- ^ argument types
              -> [TcKind]    -- ^ of these kinds
              -> TcKind      -- ^ expected kind of the whole tuple
              -> TcM TcType
-finish_tuple tup_sort tau_tys tau_kinds exp_kind
+finish_tuple rn_ty tup_sort tau_tys tau_kinds exp_kind
   = do { traceTc "finish_tuple" (ppr res_kind $$ ppr tau_kinds $$ ppr exp_kind)
        ; let arg_tys  = case tup_sort of
                    -- See also Note [Unboxed tuple RuntimeRep vars] in TyCon
@@ -766,7 +769,7 @@ finish_tuple tup_sort tau_tys tau_kinds exp_kind
                                ; checkWiredInTyCon tc
                                ; return tc }
            UnboxedTuple  -> return (tupleTyCon Unboxed arity)
-       ; checkExpectedKind (mkTyConApp tycon arg_tys) res_kind exp_kind }
+       ; checkExpectedKind rn_ty (mkTyConApp tycon arg_tys) res_kind exp_kind }
   where
     arity = length tau_tys
     tau_reps = map (getRuntimeRepFromKind "finish_tuple") tau_kinds
@@ -857,35 +860,37 @@ tc_infer_args mode orig_ty binders mb_kind_info orig_args n0
 -- necessary. If you wish to apply a type to a list of HsTypes, this is
 -- your function.
 -- Used for type-checking types only.
-tcInferApps :: Outputable fun
-            => TcTyMode
-            -> fun                  -- ^ Function (for printing only)
+tcInferApps :: TcTyMode
+            -> LHsType GhcRn        -- ^ Function (for printing only)
             -> TcType               -- ^ Function (could be knot-tied)
             -> TcKind               -- ^ Function kind (zonked)
             -> [LHsType GhcRn]      -- ^ Args
             -> TcM (TcType, TcKind) -- ^ (f args, result kind)
-tcInferApps mode orig_ty ty ki args = go ty ki args 1
+tcInferApps mode orig_ty ty ki args = go [] ty ki args 1
   where
-    go fun fun_kind []   _ = return (fun, fun_kind)
-    go fun fun_kind args n
+    go _acc_args fun fun_kind []   _ = return (fun, fun_kind)
+    go acc_args fun fun_kind args n
       | let (binders, res_kind) = splitPiTys fun_kind
       , not (null binders)
       = do { (subst, leftover_binders, args', leftover_args, n')
                 <- tc_infer_args mode orig_ty binders Nothing args n
            ; let fun_kind' = substTyUnchecked subst $
                              mkPiTys leftover_binders res_kind
-           ; go (mkNakedAppTys fun args') fun_kind' leftover_args n' }
+           ; go (reverse (dropTail (length leftover_args) args) ++ acc_args)
+                (mkNakedAppTys fun args') fun_kind' leftover_args n' }
 
-    go fun fun_kind all_args@(arg:args) n
-      = do { (co, arg_k, res_k) <- matchExpectedFunKind (length all_args)
-                                                        fun fun_kind
+    go acc_args fun fun_kind (arg:args) n
+      = do { (co, arg_k, res_k) <- matchExpectedFunKind (mkHsAppTys orig_ty (reverse acc_args))
+                                                        fun_kind
            ; arg' <- addErrCtxt (funAppCtxt orig_ty arg n) $
                      tc_lhs_type mode arg arg_k
-           ; go (mkNakedAppTy (fun `mkNakedCastTy` co) arg')
+           ; go (arg : acc_args)
+                (mkNakedAppTy (fun `mkNakedCastTy` co) arg')
                 res_k args (n+1) }
 
 --------------------------
-checkExpectedKind :: TcType               -- the type whose kind we're checking
+checkExpectedKind :: HsType GhcRn         -- HsType whose kind we're checking
+                  -> TcType               -- the type whose kind we're checking
                   -> TcKind               -- the known kind of that type, k
                   -> TcKind               -- the expected kind, exp_kind
                   -> TcM TcType    -- a possibly-inst'ed, casted type :: exp_kind
@@ -893,12 +898,11 @@ checkExpectedKind :: TcType               -- the type whose kind we're checking
 --      (checkExpectedKind ty act_kind exp_kind)
 -- checks that the actual kind act_kind is compatible
 --      with the expected kind exp_kind
-checkExpectedKind ty act_kind exp_kind
+checkExpectedKind hs_ty ty act_kind exp_kind
  = do { (ty', act_kind') <- instantiate ty act_kind exp_kind
       ; let origin = TypeEqOrigin { uo_actual   = act_kind'
                                   , uo_expected = exp_kind
-                                  , uo_thing    = Just $ mkTypeErrorThing ty'
-                                  }
+                                  , uo_thing    = Just (ppr hs_ty) }
       ; co_k <- uType origin KindLevel act_kind' exp_kind
       ; traceTc "checkExpectedKind" (vcat [ ppr act_kind
                                           , ppr exp_kind
@@ -941,6 +945,7 @@ instantiateTyN n ty ki
                                         , ppr ki' ])
        ; return (mkNakedAppTys ty inst_args, ki') }
 
+
 ---------------------------
 tcHsContext :: LHsContext GhcRn -> TcM [PredType]
 tcHsContext = tc_hs_context typeLevelMode
@@ -1418,13 +1423,13 @@ kcHsTyVarBndrs name flav cusk all_kind_vars
       = tcExtendTyVarEnv [tv] thing_inside
 
     kc_hs_tv :: HsTyVarBndr GhcRn -> TcM (TcTyVar, Bool)
-    kc_hs_tv (UserTyVar (L _ name))
+    kc_hs_tv (UserTyVar lname@(L _ name))
       = do { tv_pair@(tv, scoped) <- tcHsTyVarName Nothing name
 
               -- Open type/data families default their variables to kind *.
            ; when (open_fam && not scoped) $ -- (don't default class tyvars)
-             discardResult $ unifyKind (Just (mkTyVarTy tv)) liftedTypeKind
-                                                             (tyVarKind tv)
+             discardResult $ unifyKind (Just (HsTyVar NotPromoted lname)) liftedTypeKind
+                                       (tyVarKind tv)
 
            ; return tv_pair }
 
@@ -1578,7 +1583,7 @@ tcHsTyVarName m_kind name
            Just (ATyVar _ tv)
              -> do { whenIsJust m_kind $ \ kind ->
                      discardResult $
-                     unifyKind (Just (mkTyVarTy tv)) kind (tyVarKind tv)
+                     unifyKind (Just (HsTyVar NotPromoted (noLoc name))) kind (tyVarKind tv)
                    ; return (tv, True) }
            _ -> do { kind <- case m_kind of
                                Just kind -> return kind
@@ -2050,11 +2055,11 @@ in-scope variables that it should not unify with, but it's fiddly.
 
 -}
 
-unifyKinds :: [(TcType, TcKind)] -> TcM ([TcType], TcKind)
-unifyKinds act_kinds
+unifyKinds :: [LHsType GhcRn] -> [(TcType, TcKind)] -> TcM ([TcType], TcKind)
+unifyKinds rn_tys act_kinds
   = do { kind <- newMetaKindVar
-       ; let check (ty, act_kind) = checkExpectedKind ty act_kind kind
-       ; tys' <- mapM check act_kinds
+       ; let check rn_ty (ty, act_kind) = checkExpectedKind (unLoc rn_ty) ty act_kind kind
+       ; tys' <- zipWithM check rn_tys act_kinds
        ; return (tys', kind) }
 
 {-
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 0a1de443b3..19b0381d2d 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -66,7 +66,6 @@ module TcMType (
   --------------------------------
   -- Zonking and tidying
   zonkTidyTcType, zonkTidyOrigin,
-  mkTypeErrorThing, mkTypeErrorThingArgs,
   tidyEvVar, tidyCt, tidySkolemInfo,
   skolemiseRuntimeUnk,
   zonkTcTyVar, zonkTcTyVars, zonkTcTyVarToTyVar,
@@ -1526,32 +1525,17 @@ zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType)
 zonkTidyTcType env ty = do { ty' <- zonkTcType ty
                            ; return (tidyOpenType env ty') }
 
--- | Make an 'ErrorThing' storing a type.
-mkTypeErrorThing :: TcType -> ErrorThing
-mkTypeErrorThing ty = ErrorThing ty (Just $ length $ snd $ repSplitAppTys ty)
-                                 zonkTidyTcType
-   -- NB: Use *rep*splitAppTys, else we get #11313
-
--- | Make an 'ErrorThing' storing a type, with some extra args known about
-mkTypeErrorThingArgs :: TcType -> Int -> ErrorThing
-mkTypeErrorThingArgs ty num_args
-  = ErrorThing ty (Just $ (length $ snd $ repSplitAppTys ty) + num_args)
-               zonkTidyTcType
-
 zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
 zonkTidyOrigin env (GivenOrigin skol_info)
   = do { skol_info1 <- zonkSkolemInfo skol_info
        ; let skol_info2 = tidySkolemInfo env skol_info1
        ; return (env, GivenOrigin skol_info2) }
 zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual   = act
-                                      , uo_expected = exp
-                                      , uo_thing    = m_thing })
+                                      , uo_expected = exp })
   = do { (env1, act') <- zonkTidyTcType env  act
        ; (env2, exp') <- zonkTidyTcType env1 exp
-       ; (env3, m_thing') <- zonkTidyErrorThing env2 m_thing
-       ; return ( env3, orig { uo_actual   = act'
-                             , uo_expected = exp'
-                             , uo_thing    = m_thing' }) }
+       ; return ( env2, orig { uo_actual   = act'
+                             , uo_expected = exp' }) }
 zonkTidyOrigin env (KindEqOrigin ty1 m_ty2 orig t_or_k)
   = do { (env1, ty1')   <- zonkTidyTcType env  ty1
        ; (env2, m_ty2') <- case m_ty2 of
@@ -1570,14 +1554,6 @@ zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2)
        ; return (env3, FunDepOrigin2 p1' o1' p2' l2) }
 zonkTidyOrigin env orig = return (env, orig)
 
-zonkTidyErrorThing :: TidyEnv -> Maybe ErrorThing
-                   -> TcM (TidyEnv, Maybe ErrorThing)
-zonkTidyErrorThing env (Just (ErrorThing thing n_args zonker))
-  = do { (env', thing') <- zonker env thing
-       ; return (env', Just $ ErrorThing thing' n_args zonker) }
-zonkTidyErrorThing env Nothing
-  = return (env, Nothing)
-
 ----------------
 tidyCt :: TidyEnv -> Ct -> Ct
 -- Used only in error reporting
diff --git a/compiler/typecheck/TcPat.hs b/compiler/typecheck/TcPat.hs
index 0d0e16a346..18b148d8b6 100644
--- a/compiler/typecheck/TcPat.hs
+++ b/compiler/typecheck/TcPat.hs
@@ -348,7 +348,7 @@ tc_pat penv (LazyPat pat) pat_ty thing_inside
 
         -- Check that the expected pattern type is itself lifted
         ; pat_ty <- readExpType pat_ty
-        ; _ <- unifyType noThing (typeKind pat_ty) liftedTypeKind
+        ; _ <- unifyType Nothing (typeKind pat_ty) liftedTypeKind
 
         ; return (LazyPat pat', res) }
 
@@ -382,7 +382,7 @@ tc_pat penv (ViewPat expr pat _) overall_pat_ty thing_inside
         ; let expr_orig = lexprCtOrigin expr
               herald    = text "A view pattern expression expects"
         ; (expr_wrap1, [inf_arg_ty], inf_res_ty)
-            <- matchActualFunTys herald expr_orig (Just expr) 1 expr'_inferred
+            <- matchActualFunTys herald expr_orig (Just (unLoc expr)) 1 expr'_inferred
             -- expr_wrap1 :: expr'_inferred "->" (inf_arg_ty -> inf_res_ty)
 
          -- check that overall pattern is more polymorphic than arg type
@@ -896,7 +896,7 @@ matchExpectedConTy (PE { pe_orig = orig }) data_tc exp_pat_ty
                                              ppr exp_pat_ty,
                                              ppr pat_ty,
                                              ppr pat_rho, ppr wrap])
-       ; co1 <- unifyType noThing (mkTyConApp fam_tc (substTys subst fam_args)) pat_rho
+       ; co1 <- unifyType Nothing (mkTyConApp fam_tc (substTys subst fam_args)) pat_rho
              -- co1 : T (ty1,ty2) ~N pat_rho
              -- could use tcSubType here... but it's the wrong way round
              -- for actual vs. expected in error messages.
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 2a04bf2a1c..a95079e597 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -97,7 +97,6 @@ module TcRnTypes(
         ctLocDepth, bumpCtLocDepth,
         setCtLocOrigin, setCtLocEnv, setCtLocSpan,
         CtOrigin(..), exprCtOrigin, lexprCtOrigin, matchesCtOrigin, grhssCtOrigin,
-        ErrorThing(..), mkErrorThing, errorThingNumArgs_maybe,
         TypeOrKind(..), isTypeLevel, isKindLevel,
         pprCtOrigin, pprCtLoc,
         pushErrCtxt, pushErrCtxtSameOrigin,
@@ -3160,7 +3159,7 @@ data CtOrigin
 
   | TypeEqOrigin { uo_actual   :: TcType
                  , uo_expected :: TcType
-                 , uo_thing    :: Maybe ErrorThing
+                 , uo_thing    :: Maybe SDoc
                                   -- ^ The thing that has type "actual"
                  }
 
@@ -3237,13 +3236,6 @@ data CtOrigin
         -- Skolem variable arose when we were testing if an instance
         -- is solvable or not.
 
--- | A thing that can be stored for error message generation only.
--- It is stored with a function to zonk and tidy the thing.
-data ErrorThing
-  = forall a. Outputable a => ErrorThing a
-                                         (Maybe Arity)  -- # of args, if known
-                                         (TidyEnv -> a -> TcM (TidyEnv, a))
-
 -- | Flag to see whether we're type-checking terms or kind-checking types
 data TypeOrKind = TypeLevel | KindLevel
   deriving Eq
@@ -3260,20 +3252,9 @@ isKindLevel :: TypeOrKind -> Bool
 isKindLevel TypeLevel = False
 isKindLevel KindLevel = True
 
--- | Make an 'ErrorThing' that doesn't need tidying or zonking
-mkErrorThing :: Outputable a => a -> ErrorThing
-mkErrorThing thing = ErrorThing thing Nothing (\env x -> return (env, x))
-
--- | Retrieve the # of arguments in the error thing, if known
-errorThingNumArgs_maybe :: ErrorThing -> Maybe Arity
-errorThingNumArgs_maybe (ErrorThing _ args _) = args
-
 instance Outputable CtOrigin where
   ppr = pprCtOrigin
 
-instance Outputable ErrorThing where
-  ppr (ErrorThing thing _ _) = ppr thing
-
 ctoHerald :: SDoc
 ctoHerald = text "arising from"
 
diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs
index c898fd96bd..3ff93b6bfa 100644
--- a/compiler/typecheck/TcSigs.hs
+++ b/compiler/typecheck/TcSigs.hs
@@ -32,7 +32,7 @@ import TcRnMonad
 import TcType
 import TcMType
 import TcValidity ( checkValidType )
-import TcUnify( tcSkolemise, unifyType, noThing )
+import TcUnify( tcSkolemise, unifyType )
 import Inst( topInstantiate )
 import TcEnv( tcLookupId )
 import TcEvidence( HsWrapper, (<.>) )
@@ -722,7 +722,7 @@ tcSpecWrapper ctxt poly_ty spec_ty
   = do { (sk_wrap, inst_wrap)
                <- tcSkolemise ctxt spec_ty $ \ _ spec_tau ->
                   do { (inst_wrap, tau) <- topInstantiate orig poly_ty
-                     ; _ <- unifyType noThing spec_tau tau
+                     ; _ <- unifyType Nothing spec_tau tau
                             -- Deliberately ignore the evidence
                             -- See Note [Handling SPECIALISE pragmas],
                             --   wrinkle (2)
diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs
index 6d687b6bcd..824227a60c 100644
--- a/compiler/typecheck/TcSplice.hs
+++ b/compiler/typecheck/TcSplice.hs
@@ -135,8 +135,8 @@ import GHC.Exts         ( unsafeCoerce# )
 ************************************************************************
 -}
 
-tcTypedBracket   :: HsBracket GhcRn -> ExpRhoType -> TcM (HsExpr GhcTcId)
-tcUntypedBracket :: HsBracket GhcRn -> [PendingRnSplice] -> ExpRhoType
+tcTypedBracket   :: HsExpr GhcRn -> HsBracket GhcRn -> ExpRhoType -> TcM (HsExpr GhcTcId)
+tcUntypedBracket :: HsExpr GhcRn -> HsBracket GhcRn -> [PendingRnSplice] -> ExpRhoType
                  -> TcM (HsExpr GhcTcId)
 tcSpliceExpr     :: HsSplice GhcRn  -> ExpRhoType -> TcM (HsExpr GhcTcId)
         -- None of these functions add constraints to the LIE
@@ -157,7 +157,7 @@ runAnnotation     :: CoreAnnTarget -> LHsExpr GhcRn -> TcM Annotation
 
 -- See Note [How brackets and nested splices are handled]
 -- tcTypedBracket :: HsBracket Name -> TcRhoType -> TcM (HsExpr TcId)
-tcTypedBracket brack@(TExpBr expr) res_ty
+tcTypedBracket rn_expr brack@(TExpBr expr) res_ty
   = addErrCtxt (quotationCtxtDoc brack) $
     do { cur_stage <- getStage
        ; ps_ref <- newMutVar []
@@ -176,20 +176,21 @@ tcTypedBracket brack@(TExpBr expr) res_ty
        ; ps' <- readMutVar ps_ref
        ; texpco <- tcLookupId unsafeTExpCoerceName
        ; tcWrapResultO (Shouldn'tHappenOrigin "TExpBr")
+                       rn_expr
                        (unLoc (mkHsApp (nlHsTyApp texpco [expr_ty])
                                               (noLoc (HsTcBracketOut brack ps'))))
                        meta_ty res_ty }
-tcTypedBracket other_brack _
+tcTypedBracket _ other_brack _
   = pprPanic "tcTypedBracket" (ppr other_brack)
 
 -- tcUntypedBracket :: HsBracket Name -> [PendingRnSplice] -> ExpRhoType -> TcM (HsExpr TcId)
-tcUntypedBracket brack ps res_ty
+tcUntypedBracket rn_expr brack ps res_ty
   = do { traceTc "tc_bracket untyped" (ppr brack $$ ppr ps)
        ; ps' <- mapM tcPendingSplice ps
        ; meta_ty <- tcBrackTy brack
        ; traceTc "tc_bracket done untyped" (ppr meta_ty)
        ; tcWrapResultO (Shouldn'tHappenOrigin "untyped bracket")
-                       (HsTcBracketOut brack ps') meta_ty res_ty }
+                       rn_expr (HsTcBracketOut brack ps') meta_ty res_ty }
 
 ---------------
 tcBrackTy :: HsBracket GhcRn -> TcM TcType
diff --git a/compiler/typecheck/TcSplice.hs-boot b/compiler/typecheck/TcSplice.hs-boot
index 2aa51c8bcd..03b2c31315 100644
--- a/compiler/typecheck/TcSplice.hs-boot
+++ b/compiler/typecheck/TcSplice.hs-boot
@@ -17,11 +17,13 @@ tcSpliceExpr :: HsSplice GhcRn
              -> ExpRhoType
              -> TcM (HsExpr GhcTcId)
 
-tcUntypedBracket :: HsBracket GhcRn
+tcUntypedBracket :: HsExpr GhcRn
+                 -> HsBracket GhcRn
                  -> [PendingRnSplice]
                  -> ExpRhoType
                  -> TcM (HsExpr GhcTcId)
-tcTypedBracket :: HsBracket GhcRn
+tcTypedBracket :: HsExpr GhcRn
+               -> HsBracket GhcRn
                -> ExpRhoType
                -> TcM (HsExpr GhcTcId)
 
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 3f53946031..6addbf2c38 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -1203,7 +1203,7 @@ kcDataDefn fam_name (HsIB { hsib_body = pats })
             Just k  -> do { k' <- tcLHsKindSig k
                           ; unifyKind (Just hs_ty_pats) res_k k' } }
   where
-    hs_ty_pats = mkHsAppTys (noLoc $ HsTyVar NotPromoted (noLoc fam_name)) pats
+    hs_ty_pats = unLoc $ mkHsAppTys (noLoc $ HsTyVar NotPromoted (noLoc fam_name)) pats
 
 {-
 Kind check type patterns and kind annotate the embedded type variables.
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index c937a9f3fa..9d5391028e 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -66,6 +66,7 @@ module TcType (
   tcRepSplitTyConApp_maybe, tcRepSplitTyConApp_maybe',
   tcTyConAppTyCon, tcTyConAppTyCon_maybe, tcTyConAppArgs,
   tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcRepSplitAppTy_maybe,
+  tcRepGetNumAppTys,
   tcGetCastedTyVar_maybe, tcGetTyVar_maybe, tcGetTyVar, nextRole,
   tcSplitSigmaTy, tcSplitNestedSigmaTys, tcDeepSplitSigmaTy_maybe,
 
@@ -1569,6 +1570,12 @@ tcSplitAppTys ty
                    Just (ty', arg) -> go ty' (arg:args)
                    Nothing         -> (ty,args)
 
+-- | Returns the number of arguments in the given type, without
+-- looking through synonyms. This is used only for error reporting.
+-- We don't look through synonyms because of #11313.
+tcRepGetNumAppTys :: Type -> Arity
+tcRepGetNumAppTys = length . snd . repSplitAppTys
+
 -----------------------
 -- | If the type is a tyvar, possibly under a cast, returns it, along
 -- with the coercion. Thus, the co is :: kind tv ~N kind type
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index 94296474b1..e09b5bfe6b 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -16,7 +16,7 @@ module TcUnify (
   checkConstraints, buildImplicationFor,
 
   -- Various unifications
-  unifyType, unifyTheta, unifyKind, noThing,
+  unifyType, unifyTheta, unifyKind,
   uType, promoteTcType,
   swapOverTyVars, canSolveByUnification,
 
@@ -201,10 +201,9 @@ matchExpectedFunTys herald arity orig_ty thing_inside
 
 -- Like 'matchExpectedFunTys', but used when you have an "actual" type,
 -- for example in function application
-matchActualFunTys :: Outputable a
-                  => SDoc   -- See Note [Herald for matchExpectedFunTys]
+matchActualFunTys :: SDoc   -- See Note [Herald for matchExpectedFunTys]
                   -> CtOrigin
-                  -> Maybe a   -- the thing with type TcSigmaType
+                  -> Maybe (HsExpr GhcRn)   -- the thing with type TcSigmaType
                   -> Arity
                   -> TcSigmaType
                   -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
@@ -215,10 +214,9 @@ matchActualFunTys herald ct_orig mb_thing arity ty
 
 -- | Variant of 'matchActualFunTys' that works when supplied only part
 -- (that is, to the right of some arrows) of the full function type
-matchActualFunTysPart :: Outputable a
-                      => SDoc -- See Note [Herald for matchExpectedFunTys]
+matchActualFunTysPart :: SDoc -- See Note [Herald for matchExpectedFunTys]
                       -> CtOrigin
-                      -> Maybe a  -- the thing with type TcSigmaType
+                      -> Maybe (HsExpr GhcRn)  -- the thing with type TcSigmaType
                       -> Arity
                       -> TcSigmaType
                       -> [TcSigmaType] -- reversed args. See (*) below.
@@ -400,7 +398,7 @@ matchExpectedTyConApp tc orig_ty
            ; traceTc "matchExpectedTyConApp" (ppr tc $$ ppr (tyConTyVars tc) $$ ppr arg_tvs)
            ; let args = mkTyVarTys arg_tvs
                  tc_template = mkTyConApp tc args
-           ; co <- unifyType noThing tc_template orig_ty
+           ; co <- unifyType Nothing tc_template orig_ty
            ; return (co, args) }
 
 ----------------------
@@ -432,7 +430,7 @@ matchExpectedAppTy orig_ty
     defer
       = do { ty1 <- newFlexiTyVarTy kind1
            ; ty2 <- newFlexiTyVarTy kind2
-           ; co <- unifyType noThing (mkAppTy ty1 ty2) orig_ty
+           ; co <- unifyType Nothing (mkAppTy ty1 ty2) orig_ty
            ; return (co, (ty1, ty2)) }
 
     orig_kind = typeKind orig_ty
@@ -531,9 +529,8 @@ skolemising the type.
 
 -- | Call this variant when you are in a higher-rank situation and
 -- you know the right-hand type is deeply skolemised.
-tcSubTypeHR :: Outputable a
-            => CtOrigin    -- ^ of the actual type
-            -> Maybe a     -- ^ If present, it has type ty_actual
+tcSubTypeHR :: CtOrigin               -- ^ of the actual type
+            -> Maybe (HsExpr GhcRn)   -- ^ If present, it has type ty_actual
             -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
 tcSubTypeHR orig = tcSubTypeDS_NC_O orig GenSigCtxt
 
@@ -566,7 +563,7 @@ tcSubTypeO orig ctxt ty_actual ty_expected
                                        , pprUserTypeCtxt ctxt
                                        , ppr ty_actual
                                        , ppr ty_expected ])
-       ; tcSubTypeDS_NC_O orig ctxt noThing ty_actual ty_expected }
+       ; tcSubTypeDS_NC_O orig ctxt Nothing ty_actual ty_expected }
 
 addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a
 addSubTypeCtxt ty_actual ty_expected thing_inside
@@ -613,12 +610,11 @@ tcSubTypeDS :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> ExpRhoType -> TcM HsWr
 tcSubTypeDS orig ctxt ty_actual ty_expected
   = addSubTypeCtxt ty_actual ty_expected $
     do { traceTc "tcSubTypeDS_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
-       ; tcSubTypeDS_NC_O orig ctxt noThing ty_actual ty_expected }
+       ; tcSubTypeDS_NC_O orig ctxt Nothing ty_actual ty_expected }
 
-tcSubTypeDS_NC_O :: Outputable a
-                 => CtOrigin   -- origin used for instantiation only
+tcSubTypeDS_NC_O :: CtOrigin   -- origin used for instantiation only
                  -> UserTypeCtxt
-                 -> Maybe a
+                 -> Maybe (HsExpr GhcRn)
                  -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
 -- Just like tcSubType, but with the additional precondition that
 -- ty_expected is deeply skolemised
@@ -628,7 +624,7 @@ tcSubTypeDS_NC_O inst_orig ctxt m_thing ty_actual ty_expected
       Check ty      -> tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty
          where
            eq_orig = TypeEqOrigin { uo_actual = ty_actual, uo_expected = ty
-                                  , uo_thing = mkErrorThing <$> m_thing }
+                                  , uo_thing  = ppr <$> m_thing }
 
 ---------------
 tc_sub_tc_type :: CtOrigin   -- used when calling uType
@@ -801,17 +797,17 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
 -- expressions
 tcWrapResult :: HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType
              -> TcM (HsExpr GhcTcId)
-tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr)
+tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr) rn_expr
 
 -- | Sometimes we don't have a @HsExpr Name@ to hand, and this is more
 -- convenient.
-tcWrapResultO :: CtOrigin -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType
+tcWrapResultO :: CtOrigin -> HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType
                -> TcM (HsExpr GhcTcId)
-tcWrapResultO orig expr actual_ty res_ty
+tcWrapResultO orig rn_expr expr actual_ty res_ty
   = do { traceTc "tcWrapResult" (vcat [ text "Actual:  " <+> ppr actual_ty
                                       , text "Expected:" <+> ppr res_ty ])
        ; cow <- tcSubTypeDS_NC_O orig GenSigCtxt
-                                 (Just expr) actual_ty res_ty
+                                 (Just rn_expr) actual_ty res_ty
        ; return (mkHsWrap cow expr) }
 
 -----------------------------------
@@ -1184,7 +1180,7 @@ The exported functions are all defined as versions of some
 non-exported generic functions.
 -}
 
-unifyType :: Outputable a => Maybe a   -- ^ If present, has type 'ty1'
+unifyType :: Maybe (HsExpr GhcRn)   -- ^ If present, has type 'ty1'
           -> TcTauType -> TcTauType -> TcM TcCoercionN
 -- Actual and expected types
 -- Returns a coercion : ty1 ~ ty2
@@ -1192,24 +1188,18 @@ unifyType thing ty1 ty2 = traceTc "utype" (ppr ty1 $$ ppr ty2 $$ ppr thing) >>
                           uType origin TypeLevel ty1 ty2
   where
     origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2
-                          , uo_thing  = mkErrorThing <$> thing }
+                          , uo_thing  = ppr <$> thing }
 
--- | Use this instead of 'Nothing' when calling 'unifyType' without
--- a good "thing" (where the "thing" has the "actual" type passed in)
--- This has an 'Outputable' instance, avoiding amgiguity problems.
-noThing :: Maybe (HsExpr GhcRn)
-noThing = Nothing
-
-unifyKind :: Outputable a => Maybe a -> TcKind -> TcKind -> TcM CoercionN
+unifyKind :: Maybe (HsType GhcRn) -> TcKind -> TcKind -> TcM CoercionN
 unifyKind thing ty1 ty2 = traceTc "ukind" (ppr ty1 $$ ppr ty2 $$ ppr thing) >>
                           uType origin KindLevel ty1 ty2
   where origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2
-                              , uo_thing  = mkErrorThing <$> thing }
+                              , uo_thing  = ppr <$> thing }
 
 ---------------
 unifyPred :: PredType -> PredType -> TcM TcCoercionN
 -- Actual and expected types
-unifyPred = unifyType noThing
+unifyPred = unifyType Nothing
 
 ---------------
 unifyTheta :: TcThetaType -> TcThetaType -> TcM [TcCoercionN]
@@ -1779,12 +1769,12 @@ we return a made-up TcTyVarDetails, but I think it works smoothly.
 -}
 
 -- | Breaks apart a function kind into its pieces.
-matchExpectedFunKind :: Arity           -- ^ # of args remaining, only for errors
-                     -> TcType          -- ^ type, only for errors
+matchExpectedFunKind :: Outputable fun
+                     => fun             -- ^ type, only for errors
                      -> TcKind          -- ^ function kind
                      -> TcM (Coercion, TcKind, TcKind)
                                   -- ^ co :: old_kind ~ arg -> res
-matchExpectedFunKind num_args_remaining ty = go
+matchExpectedFunKind hs_ty = go
   where
     go k | Just k' <- tcView k = go k'
 
@@ -1802,10 +1792,9 @@ matchExpectedFunKind num_args_remaining ty = go
       = do { arg_kind <- newMetaKindVar
            ; res_kind <- newMetaKindVar
            ; let new_fun = mkFunTy arg_kind res_kind
-                 thing   = mkTypeErrorThingArgs ty num_args_remaining
                  origin  = TypeEqOrigin { uo_actual   = k
                                         , uo_expected = new_fun
-                                        , uo_thing    = Just thing
+                                        , uo_thing    = Just (ppr hs_ty)
                                         }
            ; co <- uType origin KindLevel k new_fun
            ; return (co, arg_kind, res_kind) }
diff --git a/compiler/typecheck/TcUnify.hs-boot b/compiler/typecheck/TcUnify.hs-boot
index 9af4c27775..5335c15db7 100644
--- a/compiler/typecheck/TcUnify.hs-boot
+++ b/compiler/typecheck/TcUnify.hs-boot
@@ -2,13 +2,12 @@ module TcUnify where
 import TcType      ( TcTauType )
 import TcRnTypes   ( TcM )
 import TcEvidence  ( TcCoercion )
-import Outputable  ( Outputable )
 import HsExpr      ( HsExpr )
+import HsTypes     ( HsType )
 import HsExtension ( GhcRn )
 
 -- This boot file exists only to tie the knot between
 --              TcUnify and Inst
 
-unifyType :: Outputable a => Maybe a -> TcTauType -> TcTauType -> TcM TcCoercion
-unifyKind :: Outputable a => Maybe a -> TcTauType -> TcTauType -> TcM TcCoercion
-noThing   :: Maybe (HsExpr GhcRn)
+unifyType :: Maybe (HsExpr GhcRn) -> TcTauType -> TcTauType -> TcM TcCoercion
+unifyKind :: Maybe (HsType GhcRn) -> TcTauType -> TcTauType -> TcM TcCoercion
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index c53fcc8e22..16d3963764 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -789,7 +789,7 @@ splitAppTys ty = split ty ty []
     split orig_ty _                     args  = (orig_ty, args)
 
 -- | Like 'splitAppTys', but doesn't look through type synonyms
-repSplitAppTys :: Type -> (Type, [Type])
+repSplitAppTys :: HasDebugCallStack => Type -> (Type, [Type])
 repSplitAppTys ty = split ty []
   where
     split (AppTy ty arg) args = split ty (arg:args)