Simplify treatment of heterogeneous equality

Previously, if we had a [W] (a :: k1) ~ (rhs :: k2), we would
spit out a [D] k1 ~ k2 and part the W as irreducible, hoping for
a unification. But we needn't do this. Instead, we now spit out
a [W] co :: k2 ~ k1 and then use co to cast the rhs of the original
Wanted. This means that we retain the connection between the
spat-out constraint and the original.

The problem with this new approach is that we cannot use the
casted equality for substitution; it's too like wanteds-rewriting-
wanteds. So, we forbid CTyEqCans that mention coercion holes.

All the details are in Note [Equalities with incompatible kinds]
in TcCanonical.

There are a few knock-on effects, documented where they occur.

While debugging an error in this patch, Simon and I ran into
infelicities in how patterns and matches are printed; we made
small improvements.

This patch includes mitigations for #17828, which causes spurious
pattern-match warnings. When #17828 is fixed, these lines should
be removed.

2 files changed, 37 insertions, 37 deletions

diff --git a/compiler/GHC/Hs/Expr.hs b/compiler/GHC/Hs/Expr.hs
index 551401be6c..2e05270065 100644
--- a/compiler/GHC/Hs/Expr.hs
+++ b/compiler/GHC/Hs/Expr.hs
@@ -1089,10 +1089,9 @@ ppr_expr (XExpr x) = case ghcPass @p of
   GhcPs -> ppr x
   GhcRn -> ppr x
   GhcTc -> case x of
-    HsWrap co_fn e ->  pprHsWrapper co_fn (\parens -> if parens then pprExpr e
+    HsWrap co_fn e -> pprHsWrapper co_fn (\parens -> if parens then pprExpr e
                                                       else pprExpr e)
 
-
 ppr_infix_expr :: forall p. (OutputableBndrId p) => HsExpr (GhcPass p) -> Maybe SDoc
 ppr_infix_expr (HsVar _ (L _ v))    = Just (pprInfixOcc v)
 ppr_infix_expr (HsConLikeOut _ c)   = Just (pprInfixOcc (conLikeName c))
@@ -1118,7 +1117,7 @@ ppr_apps fun args = hang (ppr_expr fun) 2 (fsep (map pp args))
     -- pp (Right (LHsWcTypeX (HsWC { hswc_body = L _ arg })))
     --   = char '@' <> pprHsType arg
     pp (Right arg)
-      = char '@' <> ppr arg
+      = text "@" <> ppr arg
 
 pprExternalSrcLoc :: (StringLiteral,(Int,Int),(Int,Int)) -> SDoc
 pprExternalSrcLoc (StringLiteral _ src,(n1,n2),(n3,n4))
@@ -1712,41 +1711,39 @@ pprPatBind pat (grhss)
 
 pprMatch :: (OutputableBndrId idR, Outputable body)
          => Match (GhcPass idR) body -> SDoc
-pprMatch match
+pprMatch (Match { m_pats = pats, m_ctxt = ctxt, m_grhss = grhss })
   = sep [ sep (herald : map (nest 2 . pprParendLPat appPrec) other_pats)
-        , nest 2 (pprGRHSs ctxt (m_grhss match)) ]
+        , nest 2 (pprGRHSs ctxt grhss) ]
   where
-    ctxt = m_ctxt match
     (herald, other_pats)
         = case ctxt of
             FunRhs {mc_fun=L _ fun, mc_fixity=fixity, mc_strictness=strictness}
-                | strictness == SrcStrict -> ASSERT(null $ m_pats match)
-                                             (char '!'<>pprPrefixOcc fun, m_pats match)
-                        -- a strict variable binding
-                | fixity == Prefix -> (pprPrefixOcc fun, m_pats match)
-                        -- f x y z = e
-                        -- Not pprBndr; the AbsBinds will
-                        -- have printed the signature
-
-                | null pats2 -> (pp_infix, [])
-                        -- x &&& y = e
-
-                | otherwise -> (parens pp_infix, pats2)
-                        -- (x &&& y) z = e
-                where
-                  pp_infix = pprParendLPat opPrec pat1
-                         <+> pprInfixOcc fun
-                         <+> pprParendLPat opPrec pat2
-
-            LambdaExpr -> (char '\\', m_pats match)
-
-            _  -> if null (m_pats match)
-                     then (empty, [])
-                     else ASSERT2( null pats1, ppr ctxt $$ ppr pat1 $$ ppr pats1 )
-                          (ppr pat1, [])        -- No parens around the single pat
-
-    (pat1:pats1) = m_pats match
-    (pat2:pats2) = pats1
+                | SrcStrict <- strictness
+                -> ASSERT(null pats)     -- A strict variable binding
+                   (char '!'<>pprPrefixOcc fun, pats)
+
+                | Prefix <- fixity
+                -> (pprPrefixOcc fun, pats) -- f x y z = e
+                                            -- Not pprBndr; the AbsBinds will
+                                            -- have printed the signature
+                | otherwise
+                -> case pats of
+                     (p1:p2:rest)
+                        | null rest -> (pp_infix, [])           -- x &&& y = e
+                        | otherwise -> (parens pp_infix, rest)  -- (x &&& y) z = e
+                        where
+                          pp_infix = pprParendLPat opPrec p1
+                                     <+> pprInfixOcc fun
+                                     <+> pprParendLPat opPrec p2
+                     _ -> pprPanic "pprMatch" (ppr ctxt $$ ppr pats)
+
+            LambdaExpr -> (char '\\', pats)
+
+            _ -> case pats of
+                   []    -> (empty, [])
+                   [pat] -> (ppr pat, [])  -- No parens around the single pat in a case
+                   _     -> pprPanic "pprMatch" (ppr ctxt $$ ppr pats)
+pprMatch (XMatch nec) = noExtCon nec
 
 pprGRHSs :: (OutputableBndrId idR, Outputable body)
          => HsMatchContext passL -> GRHSs (GhcPass idR) body -> SDoc
diff --git a/compiler/GHC/Hs/Pat.hs b/compiler/GHC/Hs/Pat.hs
index c427d977ed..1bddfa2c71 100644
--- a/compiler/GHC/Hs/Pat.hs
+++ b/compiler/GHC/Hs/Pat.hs
@@ -1,3 +1,4 @@
+
 {-
 (c) The University of Glasgow 2006
 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
@@ -58,6 +59,7 @@ import TcEvidence
 import BasicTypes
 -- others:
 import GHC.Core.Ppr ( {- instance OutputableBndr TyVar -} )
+import GHC.Driver.Session ( gopt, GeneralFlag(Opt_PrintTypecheckerElaboration) )
 import TysWiredIn
 import Var
 import RdrName ( RdrName )
@@ -526,10 +528,11 @@ pprPat (NPat _ l (Just _) _)    = char '-' <> ppr l
 pprPat (NPlusKPat _ n k _ _ _)  = hcat [ppr n, char '+', ppr k]
 pprPat (SplicePat _ splice)     = pprSplice splice
 pprPat (CoPat _ co pat _)       = pprIfTc @p $
-                                  pprHsWrapper co $ \parens
-                                              -> if parens
-                                                 then pprParendPat appPrec pat
-                                                 else pprPat pat
+                                  sdocWithDynFlags $ \ dflags ->
+                                  if gopt Opt_PrintTypecheckerElaboration dflags
+                                  then hang (text "CoPat" <+> parens (ppr co))
+                                          2 (pprParendPat appPrec pat)
+                                  else pprPat pat
 pprPat (SigPat _ pat ty)        = ppr pat <+> dcolon <+> ppr_ty
   where ppr_ty = case ghcPass @p of
                    GhcPs -> ppr ty