Unify result type earlier to improve error messageswip/T19364

Ticket #19364 helpfully points out that we do not currently take
advantage of pushing the result type of an application into the
arguments.  This makes error messages notably less good.

The fix is rather easy: move the result-type unification step earlier.
It's even a bit more efficient; in the the checking case we now
do one less zonk.

See Note [Unify with expected type before typechecking arguments]
in GHC.Tc.Gen.App

This change generally improves error messages, but it made one worse:
typecheck/should_fail/T16204c. That led me to the realisation that
a good error can be replaced by a less-good one, which provoked
me to change GHC.Tc.Solver.Interact.inertsCanDischarge.  It's
explained in the new Note [Combining equalities]

One other refactoring: I discovered that KindEqOrigin didn't need a
Maybe in its type -- a nice simplification.

8 files changed, 230 insertions, 141 deletions

diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index 0e687040e0..82dbd65848 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -1901,7 +1901,7 @@ tk_eq_msg ctxt ct ty1 ty2 orig@(TypeEqOrigin { uo_actual = act
     count_args ty = count isVisibleBinder $ fst $ splitPiTys ty
 
 tk_eq_msg ctxt ct ty1 ty2
-          (KindEqOrigin cty1 mb_cty2 sub_o mb_sub_t_or_k)
+          (KindEqOrigin cty1 cty2 sub_o mb_sub_t_or_k)
   = vcat [ headline_eq_msg False ct ty1 ty2
          , supplementary_msg ]
   where
@@ -1911,17 +1911,15 @@ tk_eq_msg ctxt ct ty1 ty2
 
     supplementary_msg
       = sdocOption sdocPrintExplicitCoercions $ \printExplicitCoercions ->
-        case mb_cty2 of
-          Just cty2
-            |  printExplicitCoercions
-            || not (cty1 `pickyEqType` cty2)
-            -> vcat [ hang (text "When matching" <+> sub_whats)
-                         2 (vcat [ ppr cty1 <+> dcolon <+>
+        if printExplicitCoercions
+           || not (cty1 `pickyEqType` cty2)
+          then vcat [ hang (text "When matching" <+> sub_whats)
+                          2 (vcat [ ppr cty1 <+> dcolon <+>
                                    ppr (tcTypeKind cty1)
                                  , ppr cty2 <+> dcolon <+>
                                    ppr (tcTypeKind cty2) ])
                     , mk_supplementary_ea_msg ctxt sub_t_or_k cty1 cty2 sub_o ]
-          _ -> text "When matching the kind of" <+> quotes (ppr cty1)
+          else text "When matching the kind of" <+> quotes (ppr cty1)
 
 tk_eq_msg _ _ _ _ _ = panic "typeeq_mismatch_msg"
 
@@ -2873,8 +2871,7 @@ relevantBindings want_filtering ctxt ct
              -- For *kind* errors, report the relevant bindings of the
              -- enclosing *type* equality, because that's more useful for the programmer
        ; let extra_tvs = case tidy_orig of
-                             KindEqOrigin t1 m_t2 _ _ -> tyCoVarsOfTypes $
-                                                         t1 : maybeToList m_t2
+                             KindEqOrigin t1 t2 _ _ -> tyCoVarsOfTypes [t1,t2]
                              _                        -> emptyVarSet
              ct_fvs = tyCoVarsOfCt ct `unionVarSet` extra_tvs
 
diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs
index 29dc16ab07..cc1411ba90 100644
--- a/compiler/GHC/Tc/Gen/App.hs
+++ b/compiler/GHC/Tc/Gen/App.hs
@@ -244,9 +244,13 @@ tcApp works like this:
    when in checking mode.  This is the shaded part of APP-Downarrow
    in Fig 5.
 
-5. Use tcValArgs to typecheck the value arguments
+5. Use unifyResultType to match up the result type of the call
+   with that expected by the context.  See Note [Unify with
+   expected type before typechecking arguments]
 
-6. After a gruesome special case for tagToEnum, rebuild the result.
+6. Use tcValArgs to typecheck the value arguments
+
+7. After a gruesome special case for tagToEnum, rebuild the result.
 
 
 Some cases that /won't/ work:
@@ -274,6 +278,34 @@ particular Ids:
   the renamer (Note [Handling overloaded and rebindable constructs] in
   GHC.Rename.Expr), and we want them to be instantiated impredicatively
   so that (f `op`), say, will work OK even if `f` is higher rank.
+
+Note [Unify with expected type before typechecking arguments]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this (#19364)
+  data Pair a b = Pair a b
+  baz :: MkPair Int Bool
+  baz = MkPair "yes" "no"
+
+We instantiate MkPair with `alpha`, `beta`, and push its argument
+types (`alpha` and `beta`) into the arguments ("yes" and "no").
+But if we first unify the result type (Pair alpha beta) with the expected
+type (Pair Int Bool) we will push the much more informative types
+`Int` and `Bool` into the arguments.   This makes a difference:
+
+Unify result type /after/ typechecking the args
+    • Couldn't match type ‘[Char]’ with ‘Bool’
+      Expected type: Pair Foo Bar
+        Actual type: Pair [Char] [Char]
+    • In the expression: Pair "yes" "no"
+
+Unify result type /before/ typechecking the args
+    • Couldn't match type ‘[Char]’ with ‘Bool’
+      Expected: Foo
+        Actual: String
+    • In the first argument of ‘Pair’, namely ‘"yes"’
+
+The latter is much better. That is why we call unifyExpectedType
+before tcValArgs.
 -}
 
 tcApp :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
@@ -288,7 +320,26 @@ tcApp rn_expr exp_res_ty
        ; (delta, inst_args, app_res_rho) <- tcInstFun do_ql True fun fun_sigma rn_args
 
        -- Quick look at result
-       ; quickLookResultType do_ql delta app_res_rho exp_res_ty
+       ; app_res_rho <- if do_ql
+                        then quickLookResultType delta app_res_rho exp_res_ty
+                        else return app_res_rho
+
+       -- Unify with expected type from the context
+       -- See Note [Unify with expected type before typechecking arguments]
+       --
+       -- perhaps_add_res_ty_ctxt: Inside an expansion, the addFunResCtxt stuff is
+       --    more confusing than helpful because the function at the head isn't in
+       --    the source program; it was added by the renamer.  See
+       --    Note [Handling overloaded and rebindable constructs] in GHC.Rename.Expr
+       ; let  perhaps_add_res_ty_ctxt thing_inside
+                 | insideExpansion fun_ctxt
+                 = thing_inside
+                 | otherwise
+                 = addFunResCtxt rn_fun rn_args app_res_rho exp_res_ty $
+                   thing_inside
+
+       ; res_co <- perhaps_add_res_ty_ctxt $
+                   unifyExpectedType rn_expr app_res_rho exp_res_ty
 
        ; whenDOptM Opt_D_dump_tc_trace $
          do { inst_args <- mapM zonkArg inst_args  -- Only when tracing
@@ -304,35 +355,13 @@ tcApp rn_expr exp_res_ty
        -- Typecheck the value arguments
        ; tc_args <- tcValArgs do_ql inst_args
 
-       -- Zonk the result type, to ensure that we substitute out
-       -- any filled-in instantiation variable before calling tcWrapResultMono
-       -- In the Check case, this isn't really necessary, because tcWrapResultMono
-       -- just drops to tcUnify; but in the Infer case a filled-in instantiation
-       -- variable might perhaps escape into the constraint generator. The safe
-       -- thing to do is to any instantaition variables away.
-       -- See Note [Instantiation variables are short lived]
-       ; app_res_rho <- zonkQuickLook do_ql app_res_rho
-
-       -- Special case for tagToEnum#
-       ; if isTagToEnum rn_fun
-         then tcTagToEnum rn_expr tc_fun fun_ctxt tc_args app_res_rho exp_res_ty
-         else
-
-    do { -- Reconstruct
-       ; let tc_expr = rebuildHsApps tc_fun fun_ctxt tc_args
-
-             -- Set a context for the helpful
-             --    "Probably cause: f applied to too many args"
-             -- But not in generated code, where we don't want
-             -- to mention internal (rebindable syntax) function names
-             set_res_ctxt thing_inside
-                | insideExpansion tc_args
-                = thing_inside
-                | otherwise
-                = addFunResCtxt tc_fun tc_args app_res_rho exp_res_ty thing_inside
+       -- Reconstruct, with special case for tagToEnum#
+       ; tc_expr <- if isTagToEnum rn_fun
+                    then tcTagToEnum tc_fun fun_ctxt tc_args app_res_rho
+                    else return (rebuildHsApps tc_fun fun_ctxt tc_args)
 
        -- Wrap the result
-       ; set_res_ctxt $ tcWrapResultMono rn_expr tc_expr app_res_rho exp_res_ty } }
+       ; return (mkHsWrapCo res_co tc_expr) }
 
 --------------------
 wantQuickLook :: HsExpr GhcRn -> TcM Bool
@@ -869,18 +898,28 @@ skipQuickLook :: Delta -> LHsExpr GhcRn -> TcM (Delta, EValArg 'TcpInst)
 skipQuickLook delta larg = return (delta, ValArg larg)
 
 ----------------
-quickLookResultType :: Bool -> Delta -> TcRhoType -> ExpRhoType -> TcM ()
+quickLookResultType :: Delta -> TcRhoType -> ExpRhoType -> TcM TcRhoType
 -- This function implements the shaded bit of rule APP-Downarrow in
 -- Fig 5 of the QL paper: "A quick look at impredicativity" (ICFP'20).
-
-quickLookResultType do_ql delta app_res_rho exp_res_ty
-  | do_ql
-  , not (isEmptyVarSet delta)  -- Optimisation only
-  , Just exp_rho <- checkingExpType_maybe exp_res_ty
-                               -- In checking mode only
-  = qlUnify delta app_res_rho exp_rho
-  | otherwise
-  = return ()
+-- It returns its second argument, but with any variables in Delta
+-- substituted out, so no variables in Delta escape
+
+quickLookResultType delta app_res_rho (Check exp_rho)
+  = -- In checking mode only, do qlUnify with the expected result type
+    do { unless (isEmptyVarSet delta)  $ -- Optimisation only
+         qlUnify delta app_res_rho exp_rho
+       ; return app_res_rho }
+
+quickLookResultType _ app_res_rho (Infer {})
+  = zonkTcType app_res_rho
+    -- Zonk the result type, to ensure that we substitute out any
+    -- filled-in instantiation variable before calling
+    -- unifyExpectedType. In the Check case, this isn't necessary,
+    -- because unifyExpectedType just drops to tcUnify; but in the
+    -- Infer case a filled-in instantiation variable (filled in by
+    -- tcInstFun) might perhaps escape into the constraint
+    -- generator. The safe thing to do is to zonk any instantiation
+    -- variables away.  See Note [Instantiation variables are short lived]
 
 ---------------------
 qlUnify :: Delta -> TcType -> TcType -> TcM ()
@@ -1080,8 +1119,7 @@ findNoQuantVars fun_ty args
 {- Note [tagToEnum#]
 ~~~~~~~~~~~~~~~~~~~~
 Nasty check to ensure that tagToEnum# is applied to a type that is an
-enumeration TyCon.  Unification may refine the type later, but this
-check won't see that, alas.  It's crude, because it relies on our
+enumeration TyCon.  It's crude, because it relies on our
 knowing *now* that the type is ok, which in turn relies on the
 eager-unification part of the type checker pushing enough information
 here.  In theory the Right Thing to do is to have a new form of
@@ -1109,54 +1147,48 @@ isTagToEnum :: HsExpr GhcRn -> Bool
 isTagToEnum (HsVar _ (L _ fun_id)) = fun_id `hasKey` tagToEnumKey
 isTagToEnum _ = False
 
-tcTagToEnum :: HsExpr GhcRn
-            -> HsExpr GhcTc -> AppCtxt -> [HsExprArg 'TcpTc]
-            -> TcRhoType -> ExpRhoType
+tcTagToEnum :: HsExpr GhcTc -> AppCtxt -> [HsExprArg 'TcpTc]
+            -> TcRhoType
             -> TcM (HsExpr GhcTc)
 -- tagToEnum# :: forall a. Int# -> a
 -- See Note [tagToEnum#]   Urgh!
-tcTagToEnum expr fun fun_ctxt args app_res_ty res_ty
-  | null val_args
-  = failWithTc (text "tagToEnum# must appear applied to one argument")
-
-  | otherwise
-  = do { res_ty <- readExpType res_ty
-       ; ty'    <- zonkTcType res_ty
+tcTagToEnum tc_fun fun_ctxt tc_args res_ty
+  | [val_arg] <- dropWhile (not . isHsValArg) tc_args
+  = do { res_ty <- zonkTcType res_ty
 
        -- Check that the type is algebraic
-       ; case tcSplitTyConApp_maybe ty' of {
-           Nothing -> do { addErrTc (mk_error ty' doc1)
+       ; case tcSplitTyConApp_maybe res_ty of {
+           Nothing -> do { addErrTc (mk_error res_ty doc1)
                          ; vanilla_result } ;
            Just (tc, tc_args) ->
 
     do { -- Look through any type family
        ; fam_envs <- tcGetFamInstEnvs
        ; case tcLookupDataFamInst_maybe fam_envs tc tc_args of {
-           Nothing -> do { check_enumeration ty' tc
+           Nothing -> do { check_enumeration res_ty tc
                          ; vanilla_result } ;
            Just (rep_tc, rep_args, coi) ->
 
     do { -- coi :: tc tc_args ~R rep_tc rep_args
-         check_enumeration ty' rep_tc
+         check_enumeration res_ty rep_tc
        ; let rep_ty  = mkTyConApp rep_tc rep_args
-             fun'    = mkHsWrap (WpTyApp rep_ty) fun
-             expr'   = rebuildHsApps fun' fun_ctxt val_args
+             tc_fun' = mkHsWrap (WpTyApp rep_ty) tc_fun
+             tc_expr = rebuildHsApps tc_fun' fun_ctxt [val_arg]
              df_wrap = mkWpCastR (mkTcSymCo coi)
-       ; return (mkHsWrap df_wrap expr') }}}}}
+       ; return (mkHsWrap df_wrap tc_expr) }}}}}
 
-  where
-    val_args = dropWhile (not . isHsValArg) args
+  | otherwise
+  = failWithTc (text "tagToEnum# must appear applied to one value argument")
 
-    vanilla_result
-      = do { let expr' = rebuildHsApps fun fun_ctxt args
-           ; tcWrapResultMono expr expr' app_res_ty res_ty }
+  where
+    vanilla_result = return (rebuildHsApps tc_fun fun_ctxt tc_args)
 
     check_enumeration ty' tc
       | isEnumerationTyCon tc = return ()
       | otherwise             = addErrTc (mk_error ty' doc2)
 
     doc1 = vcat [ text "Specify the type by giving a type signature"
-                , text "e.g. (tagToEnum# x) :: Bool" ]
+               , text "e.g. (tagToEnum# x) :: Bool" ]
     doc2 = text "Result type must be an enumeration type"
 
     mk_error :: TcType -> SDoc -> SDoc
@@ -1174,5 +1206,3 @@ tcTagToEnum expr fun fun_ctxt args app_res_ty res_ty
 
 tcExprPrag :: HsPragE GhcRn -> HsPragE GhcTc
 tcExprPrag (HsPragSCC x1 src ann) = HsPragSCC x1 src ann
-
-
diff --git a/compiler/GHC/Tc/Gen/Head.hs b/compiler/GHC/Tc/Gen/Head.hs
index faf5e0f2f2..5b57f397ce 100644
--- a/compiler/GHC/Tc/Gen/Head.hs
+++ b/compiler/GHC/Tc/Gen/Head.hs
@@ -16,9 +16,10 @@
 -}
 
 module GHC.Tc.Gen.Head
-       ( HsExprArg(..), EValArg(..), TcPass(..), AppCtxt(..), appCtxtLoc
+       ( HsExprArg(..), EValArg(..), TcPass(..)
+       , AppCtxt(..), appCtxtLoc, insideExpansion
        , splitHsApps, rebuildHsApps
-       , addArgWrap, isHsValArg, insideExpansion
+       , addArgWrap, isHsValArg
        , countLeadingValArgs, isVisibleArg, pprHsExprArgTc
 
        , tcInferAppHead, tcInferAppHead_maybe
@@ -204,6 +205,10 @@ appCtxtLoc :: AppCtxt -> SrcSpan
 appCtxtLoc (VAExpansion _ l) = l
 appCtxtLoc (VACall _ _ l)    = l
 
+insideExpansion :: AppCtxt -> Bool
+insideExpansion (VAExpansion {}) = True
+insideExpansion (VACall {})      = False
+
 instance Outputable AppCtxt where
   ppr (VAExpansion e _) = text "VAExpansion" <+> ppr e
   ppr (VACall f n _)    = text "VACall" <+> int n <+> ppr f
@@ -317,12 +322,6 @@ isVisibleArg (EValArg {})  = True
 isVisibleArg (ETypeArg {}) = True
 isVisibleArg _             = False
 
-insideExpansion :: [HsExprArg p] -> Bool
-insideExpansion args = any is_expansion args
-  where
-    is_expansion (EWrap (EExpand {})) = True
-    is_expansion _                    = False
-
 instance OutputableBndrId (XPass p) => Outputable (HsExprArg p) where
   ppr (EValArg { eva_arg = arg })      = text "EValArg" <+> ppr arg
   ppr (EPrag _ p)                      = text "EPrag" <+> ppr p
@@ -850,9 +849,10 @@ tcCheckId :: Name -> ExpRhoType -> TcM (HsExpr GhcTc)
 tcCheckId name res_ty
   = do { (expr, actual_res_ty) <- tcInferId name
        ; traceTc "tcCheckId" (vcat [ppr name, ppr actual_res_ty, ppr res_ty])
-       ; addFunResCtxt expr [] actual_res_ty res_ty $
-         tcWrapResultO (OccurrenceOf name) (HsVar noExtField (noLoc name)) expr
-                                           actual_res_ty res_ty }
+       ; addFunResCtxt rn_fun [] actual_res_ty res_ty $
+         tcWrapResultO (OccurrenceOf name) rn_fun expr actual_res_ty res_ty }
+  where
+    rn_fun = HsVar noExtField (noLoc name)
 
 ------------------------
 tcInferId :: Name -> TcM (HsExpr GhcTc, TcSigmaType)
@@ -1157,13 +1157,15 @@ naughtiness in both branches.  c.f. TcTyClsBindings.mkAuxBinds.
 *                                                                      *
 ********************************************************************* -}
 
-addFunResCtxt :: HsExpr GhcTc -> [HsExprArg 'TcpTc]
+addFunResCtxt :: HsExpr GhcRn -> [HsExprArg 'TcpRn]
               -> TcType -> ExpRhoType
               -> TcM a -> TcM a
 -- When we have a mis-match in the return type of a function
 -- try to give a helpful message about too many/few arguments
-addFunResCtxt fun args fun_res_ty env_ty
-  = addLandmarkErrCtxtM (\env -> (env, ) <$> mk_msg)
+-- But not in generated code, where we don't want
+-- to mention internal (rebindable syntax) function names
+addFunResCtxt fun args fun_res_ty env_ty thing_inside
+  = addLandmarkErrCtxtM (\env -> (env, ) <$> mk_msg) thing_inside
       -- NB: use a landmark error context, so that an empty context
       -- doesn't suppress some more useful context
   where
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index b8df1fbae6..8474ca7007 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -465,11 +465,12 @@ both. (They probably started as [WD] and got split; this is relatively
 rare and it doesn't seem worth trying to put them back together again.)
 -}
 
-solveOneFromTheOther :: CtEvidence  -- Inert
-                     -> CtEvidence  -- WorkItem
+solveOneFromTheOther :: CtEvidence  -- Inert    (Dict or Irred)
+                     -> CtEvidence  -- WorkItem (same predicate as inert)
                      -> TcS InteractResult
 -- Precondition:
 -- * inert and work item represent evidence for the /same/ predicate
+-- * Both are CDictCan or CIrredCan
 --
 -- We can always solve one from the other: even if both are wanted,
 -- although we don't rewrite wanteds with wanteds, we can combine
@@ -499,8 +500,8 @@ solveOneFromTheOther ev_i ev_w
        -- Inert is Given or Wanted
   = case ev_i of
       CtWanted { ctev_nosh = WOnly }
-          | WDeriv <- nosh_w -> return KeepWork
-      _                      -> return KeepInert
+          | WDeriv <- nosh_w           -> return KeepWork
+      _                                -> return KeepInert
       -- Consider work  item [WD] C ty1 ty2
       --          inert item [W]  C ty1 ty2
       -- Then we must keep the work item.  But if the
@@ -511,7 +512,7 @@ solveOneFromTheOther ev_i ev_w
   -- From here on the work-item is Given
 
   | CtWanted { ctev_loc = loc_i } <- ev_i
-  , prohibitedSuperClassSolve (ctEvLoc ev_w) loc_i
+  , prohibitedSuperClassSolve loc_w loc_i
   = do { traceTcS "prohibitedClassSolve2" (ppr ev_i $$ ppr ev_w)
        ; return KeepInert }      -- Just discard the un-usable Given
                                  -- This never actually happens because
@@ -1439,49 +1440,107 @@ solving.
 **********************************************************************
 -}
 
-inertsCanDischarge :: InertCans -> CanEqLHS -> TcType -> CtFlavourRole
+{- Note [Combining equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have
+   Inert:     g1 :: a ~ t
+   Work item: g2 :: a ~ t
+
+Then we can simply solve g2 from g1, thus g2 := g1.  Easy!
+But it's not so simple:
+
+* If t is a type variable, the equalties might be oriented differently:
+      e.g. (g1 :: a~b) and (g2 :: b~a)
+  So we look both ways round.  Hence the SwapFlag result to
+  inertsCanDischarge.
+
+* We can only do g2 := g1 if g1 can discharge g2; that depends on
+  (a) the role and (b) the flavour.  E.g. a representational equality
+  cannot discharge a nominal one; a Wanted cannot discharge a Given.
+  The predicate is eqCanDischargeFR.
+
+* If the inert is [W] and the work-item is [WD] we don't want to
+  forget the [D] part; hence the Bool result of inertsCanDischarge.
+
+* Visibility. Suppose  S :: forall k. k -> Type, and consider unifying
+      S @Type (a::Type)  ~   S @(Type->Type) (b::Type->Type)
+  From the first argument we get (Type ~ Type->Type); from the second
+  argument we get (a ~ b) which in turn gives (Type ~ Type->Type).
+  See typecheck/should_fail/T16204c.
+
+  That first argument is invisible in the source program (aside from
+  visible type application), so we'd much prefer to get the error from
+  the second. We track visiblity in the uo_visible field of a TypeEqOrigin.
+  We use this to prioritise visible errors (see GHC.Tc.Errors.tryReporters,
+  the partition on isVisibleOrigin).
+
+  So when combining two otherwise-identical equalites, we want to
+  keep the visible one, and discharge the invisible one.  Hence the
+  call to strictly_more_visible.
+-}
+
+inertsCanDischarge :: InertCans -> Ct
                    -> Maybe ( CtEvidence  -- The evidence for the inert
                             , SwapFlag    -- Whether we need mkSymCo
                             , Bool)       -- True <=> keep a [D] version
                                           --          of the [WD] constraint
-inertsCanDischarge inerts lhs rhs fr
+inertsCanDischarge inerts (CEqCan { cc_lhs = lhs_w, cc_rhs = rhs_w
+                                  , cc_ev = ev_w, cc_eq_rel = eq_rel })
   | (ev_i : _) <- [ ev_i | CEqCan { cc_ev = ev_i, cc_rhs = rhs_i
                                   , cc_eq_rel = eq_rel }
-                             <- findEq inerts lhs
-                         , (ctEvFlavour ev_i, eq_rel) `eqCanDischargeFR` fr
-                         , rhs_i `tcEqType` rhs ]
+                             <- findEq inerts lhs_w
+                         , rhs_i `tcEqType` rhs_w
+                         , inert_beats_wanted ev_i eq_rel ]
   =  -- Inert:     a ~ ty
      -- Work item: a ~ ty
     Just (ev_i, NotSwapped, keep_deriv ev_i)
 
-  | Just rhs_lhs <- canEqLHS_maybe rhs
+  | Just rhs_lhs <- canEqLHS_maybe rhs_w
   , (ev_i : _) <- [ ev_i | CEqCan { cc_ev = ev_i, cc_rhs = rhs_i
                                   , cc_eq_rel = eq_rel }
                              <- findEq inerts rhs_lhs
-                         , (ctEvFlavour ev_i, eq_rel) `eqCanDischargeFR` fr
-                         , rhs_i `tcEqType` canEqLHSType lhs ]
+                         , rhs_i `tcEqType` canEqLHSType lhs_w
+                         , inert_beats_wanted ev_i eq_rel ]
   =  -- Inert:     a ~ b
      -- Work item: b ~ a
      Just (ev_i, IsSwapped, keep_deriv ev_i)
 
-  | otherwise
-  = Nothing
-
   where
+    loc_w  = ctEvLoc ev_w
+    flav_w = ctEvFlavour ev_w
+    fr_w   = (flav_w, eq_rel)
+
+    inert_beats_wanted ev_i eq_rel
+      = -- eqCanDischargeFR:    see second bullet of Note [Combining equalities]
+        -- strictly_more_visible: see last bullet of Note [Combining equalities]
+        fr_i`eqCanDischargeFR` fr_w
+        && not ((loc_w `strictly_more_visible` ctEvLoc ev_i)
+                 && (fr_w `eqCanDischargeFR` fr_i))
+      where
+        fr_i = (ctEvFlavour ev_i, eq_rel)
+
+    -- See Note [Combining equalities], third bullet
     keep_deriv ev_i
       | Wanted WOnly  <- ctEvFlavour ev_i  -- inert is [W]
-      , (Wanted WDeriv, _) <- fr           -- work item is [WD]
+      , Wanted WDeriv <- flav_w            -- work item is [WD]
       = True   -- Keep a derived version of the work item
       | otherwise
       = False  -- Work item is fully discharged
 
+    -- See Note [Combining equalities], final bullet
+    strictly_more_visible loc1 loc2
+       = not (isVisibleOrigin (ctLocOrigin loc2)) &&
+         isVisibleOrigin (ctLocOrigin loc1)
+
+inertsCanDischarge _ _ = Nothing
+
+
 interactEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
 interactEq inerts workItem@(CEqCan { cc_lhs = lhs
-                                         , cc_rhs = rhs
-                                         , cc_ev = ev
-                                         , cc_eq_rel = eq_rel })
-  | Just (ev_i, swapped, keep_deriv)
-       <- inertsCanDischarge inerts lhs rhs (ctEvFlavour ev, eq_rel)
+                                   , cc_rhs = rhs
+                                   , cc_ev = ev
+                                   , cc_eq_rel = eq_rel })
+  | Just (ev_i, swapped, keep_deriv) <- inertsCanDischarge inerts workItem
   = do { setEvBindIfWanted ev $
          evCoercion (maybeTcSymCo swapped $
                      tcDowngradeRole (eqRelRole eq_rel)
diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index 3862d842b0..29344b17d7 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -1559,10 +1559,9 @@ instance Outputable TcEvDest where
 
 instance Outputable CtEvidence where
   ppr ev = ppr (ctEvFlavour ev)
-           <+> pp_ev
-           <+> braces (ppr (ctl_depth (ctEvLoc ev))) <> dcolon
-                  -- Show the sub-goal depth too
-           <+> ppr (ctEvPred ev)
+           <+> pp_ev <+> braces (ppr (ctl_depth (ctEvLoc ev)))
+                         -- Show the sub-goal depth too
+               <> dcolon <+> ppr (ctEvPred ev)
     where
       pp_ev = case ev of
              CtGiven { ctev_evar = v } -> ppr v
@@ -1860,7 +1859,7 @@ data CtLoc = CtLoc { ctl_origin :: CtOrigin
 mkKindLoc :: TcType -> TcType   -- original *types* being compared
           -> CtLoc -> CtLoc
 mkKindLoc s1 s2 loc = setCtLocOrigin (toKindLoc loc)
-                        (KindEqOrigin s1 (Just s2) (ctLocOrigin loc)
+                        (KindEqOrigin s1 s2 (ctLocOrigin loc)
                                       (ctLocTypeOrKind_maybe loc))
 
 -- | Take a CtLoc and moves it to the kind level
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index b0d970bb37..648bf5ce12 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -361,7 +361,7 @@ data CtOrigin
                  }
 
   | KindEqOrigin
-      TcType (Maybe TcType)     -- A kind equality arising from unifying these two types
+      TcType TcType             -- A kind equality arising from unifying these two types
       CtOrigin                  -- originally arising from this
       (Maybe TypeOrKind)        -- the level of the eq this arises from
 
@@ -559,16 +559,15 @@ pprCtOrigin (FunDepOrigin2 pred1 orig1 pred2 loc2)
                , hang (text "instance" <+> quotes (ppr pred2))
                     2 (text "at" <+> ppr loc2) ])
 
-pprCtOrigin (KindEqOrigin t1 (Just t2) _ _)
-  = hang (ctoHerald <+> text "a kind equality arising from")
-       2 (sep [ppr t1, char '~', ppr t2])
-
 pprCtOrigin AssocFamPatOrigin
   = text "when matching a family LHS with its class instance head"
 
-pprCtOrigin (KindEqOrigin t1 Nothing _ _)
-  = hang (ctoHerald <+> text "a kind equality when matching")
-       2 (ppr t1)
+pprCtOrigin (TypeEqOrigin { uo_actual = t1, uo_expected =  t2, uo_visible = vis })
+  = text "a type equality" <> brackets (ppr vis) <+> sep [ppr t1, char '~', ppr t2]
+
+pprCtOrigin (KindEqOrigin t1 t2 _ _)
+  = hang (ctoHerald <+> text "a kind equality arising from")
+       2 (sep [ppr t1, char '~', ppr t2])
 
 pprCtOrigin (DerivOriginDC dc n _)
   = hang (ctoHerald <+> text "the" <+> speakNth n
@@ -641,7 +640,6 @@ pprCtO DefaultOrigin         = text "a 'default' declaration"
 pprCtO DoOrigin              = text "a do statement"
 pprCtO MCompOrigin           = text "a statement in a monad comprehension"
 pprCtO ProcOrigin            = text "a proc expression"
-pprCtO (TypeEqOrigin t1 t2 _ _)= text "a type equality" <+> sep [ppr t1, char '~', ppr t2]
 pprCtO AnnOrigin             = text "an annotation"
 pprCtO (ExprHoleOrigin occ)  = text "a use of" <+> quotes (ppr occ)
 pprCtO (TypeHoleOrigin occ)  = text "a use of wildcard" <+> quotes (ppr occ)
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index ed9ee9cc44..1e82be0f0e 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -137,7 +137,6 @@ import GHC.Types.Basic ( TypeOrKind(..) )
 
 import Control.Monad
 import GHC.Data.Maybe
-import Control.Arrow    ( second )
 import qualified Data.Semigroup as Semi
 
 {-
@@ -2516,13 +2515,11 @@ zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual   = act
        ; (env2, exp') <- zonkTidyTcType env1 exp
        ; 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
-                             Just ty2 -> second Just <$> zonkTidyTcType env1 ty2
-                             Nothing  -> return (env1, Nothing)
-       ; (env3, orig')  <- zonkTidyOrigin env2 orig
-       ; return (env3, KindEqOrigin ty1' m_ty2' orig' t_or_k) }
+zonkTidyOrigin env (KindEqOrigin ty1 ty2 orig t_or_k)
+  = do { (env1, ty1')  <- zonkTidyTcType env  ty1
+       ; (env2, ty2')  <- zonkTidyTcType env1 ty2
+       ; (env3, orig') <- zonkTidyOrigin env2 orig
+       ; return (env3, KindEqOrigin ty1' ty2' orig' t_or_k) }
 zonkTidyOrigin env (FunDepOrigin1 p1 o1 l1 p2 o2 l2)
   = do { (env1, p1') <- zonkTidyTcType env  p1
        ; (env2, p2') <- zonkTidyTcType env1 p2
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index 121ebfbe7e..eee4e1844c 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -22,7 +22,7 @@ module GHC.Tc.Utils.Unify (
   buildImplicationFor, buildTvImplication, emitResidualTvConstraint,
 
   -- Various unifications
-  unifyType, unifyKind,
+  unifyType, unifyKind, unifyExpectedType,
   uType, promoteTcType,
   swapOverTyVars, canSolveByUnification,
 
@@ -543,11 +543,18 @@ tcWrapResultMono :: HsExpr GhcRn -> HsExpr GhcTc
 -- It means we don't need to pass in a CtOrigin
 tcWrapResultMono rn_expr expr act_ty res_ty
   = ASSERT2( isRhoTy act_ty, ppr act_ty $$ ppr rn_expr )
-    do { co <- case res_ty of
-                  Infer inf_res -> fillInferResult act_ty inf_res
-                  Check exp_ty  -> unifyType (Just (ppr rn_expr)) act_ty exp_ty
+    do { co <- unifyExpectedType rn_expr act_ty res_ty
        ; return (mkHsWrapCo co expr) }
 
+unifyExpectedType :: HsExpr GhcRn
+                  -> TcRhoType   -- Actual -- a rho-type not a sigma-type
+                  -> ExpRhoType  -- Expected
+                  -> TcM TcCoercionN
+unifyExpectedType rn_expr act_ty exp_ty
+  = case exp_ty of
+      Infer inf_res -> fillInferResult act_ty inf_res
+      Check exp_ty  -> unifyType (Just (ppr rn_expr)) act_ty exp_ty
+
 ------------------------
 tcSubTypePat :: CtOrigin -> UserTypeCtxt
             -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
@@ -1249,7 +1256,7 @@ uType t_or_k origin orig_ty1 orig_ty2
       = do { let ty1 = coercionType co1
                  ty2 = coercionType co2
            ; kco <- uType KindLevel
-                          (KindEqOrigin orig_ty1 (Just orig_ty2) origin
+                          (KindEqOrigin orig_ty1 orig_ty2 origin
                                         (Just t_or_k))
                           ty1 ty2
            ; return $ mkProofIrrelCo Nominal kco co1 co2 }
@@ -1463,7 +1470,7 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
             ; defer }
 
     ty1 = mkTyVarTy tv1
-    kind_origin = KindEqOrigin ty1 (Just ty2) origin (Just t_or_k)
+    kind_origin = KindEqOrigin ty1 ty2 origin (Just t_or_k)
 
     defer = unSwap swapped (uType_defer t_or_k origin) ty1 ty2