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.

1 files changed, 7 insertions, 4 deletions

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