Simplify treatment of heterogeneous equalitywip/no-coholes

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, 55 insertions, 5 deletions

diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs
index 626b1bbc78..317ca00906 100644
--- a/compiler/GHC/Core/Coercion.hs
+++ b/compiler/GHC/Core/Coercion.hs
@@ -12,7 +12,8 @@
 module GHC.Core.Coercion (
         -- * Main data type
         Coercion, CoercionN, CoercionR, CoercionP, MCoercion(..), MCoercionR,
-        UnivCoProvenance, CoercionHole(..), coHoleCoVar, setCoHoleCoVar,
+        UnivCoProvenance, CoercionHole(..), BlockSubstFlag(..),
+        coHoleCoVar, setCoHoleCoVar,
         LeftOrRight(..),
         Var, CoVar, TyCoVar,
         Role(..), ltRole,
@@ -111,7 +112,9 @@ module GHC.Core.Coercion (
         -- * Other
         promoteCoercion, buildCoercion,
 
-        simplifyArgsWorker
+        simplifyArgsWorker,
+
+        badCoercionHole, badCoercionHoleCo
        ) where
 
 #include "HsVersions.h"
@@ -148,6 +151,7 @@ import UniqFM
 import Control.Monad (foldM, zipWithM)
 import Data.Function ( on )
 import Data.Char( isDigit )
+import qualified Data.Monoid as Monoid
 
 {-
 %************************************************************************
@@ -2904,3 +2908,40 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
                     ppr (take 10 orig_roles), -- often infinite!
                     ppr orig_tys])
            -}
+
+{-
+%************************************************************************
+%*                                                                      *
+       Coercion holes
+%*                                                                      *
+%************************************************************************
+-}
+
+bad_co_hole_ty :: Type -> Monoid.Any
+bad_co_hole_co :: Coercion -> Monoid.Any
+(bad_co_hole_ty, _, bad_co_hole_co, _)
+  = foldTyCo folder ()
+  where
+    folder = TyCoFolder { tcf_view  = const Nothing
+                        , tcf_tyvar = const2 (Monoid.Any False)
+                        , tcf_covar = const2 (Monoid.Any False)
+                        , tcf_hole  = const hole
+                        , tcf_tycobinder = const2
+                        }
+
+    const2 :: a -> b -> c -> a
+    const2 x _ _ = x
+
+    hole :: CoercionHole -> Monoid.Any
+    hole (CoercionHole { ch_blocker = YesBlockSubst }) = Monoid.Any True
+    hole _                                             = Monoid.Any False
+
+-- | Is there a blocking coercion hole in this type? See
+-- TcCanonical Note [Equalities with incompatible kinds]
+badCoercionHole :: Type -> Bool
+badCoercionHole = Monoid.getAny . bad_co_hole_ty
+
+-- | Is there a blocking coercion hole in this coercion? See
+-- TcCanonical Note [Equalities with incompatible kinds]
+badCoercionHoleCo :: Coercion -> Bool
+badCoercionHoleCo = Monoid.getAny . bad_co_hole_co
diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs
index 26c01ebcb8..c1ca32fc3c 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs
+++ b/compiler/GHC/Core/TyCo/Rep.hs
@@ -39,7 +39,7 @@ module GHC.Core.TyCo.Rep (
         -- * Coercions
         Coercion(..),
         UnivCoProvenance(..),
-        CoercionHole(..), coHoleCoVar, setCoHoleCoVar,
+        CoercionHole(..), BlockSubstFlag(..), coHoleCoVar, setCoHoleCoVar,
         CoercionN, CoercionR, CoercionP, KindCoercion,
         MCoercion(..), MCoercionR, MCoercionN,
 
@@ -1487,12 +1487,18 @@ instance Outputable UnivCoProvenance where
 
 -- | A coercion to be filled in by the type-checker. See Note [Coercion holes]
 data CoercionHole
-  = CoercionHole { ch_co_var :: CoVar
+  = CoercionHole { ch_co_var  :: CoVar
                        -- See Note [CoercionHoles and coercion free variables]
 
-                 , ch_ref    :: IORef (Maybe Coercion)
+                 , ch_blocker :: BlockSubstFlag  -- should this hole block substitution?
+                                                 -- See (2a) in TcCanonical
+                                                 -- Note [Equalities with incompatible kinds]
+                 , ch_ref     :: IORef (Maybe Coercion)
                  }
 
+data BlockSubstFlag = YesBlockSubst
+                    | NoBlockSubst
+
 coHoleCoVar :: CoercionHole -> CoVar
 coHoleCoVar = ch_co_var
 
@@ -1508,6 +1514,9 @@ instance Data.Data CoercionHole where
 instance Outputable CoercionHole where
   ppr (CoercionHole { ch_co_var = cv }) = braces (ppr cv)
 
+instance Outputable BlockSubstFlag where
+  ppr YesBlockSubst = text "YesBlockSubst"
+  ppr NoBlockSubst  = text "NoBlockSubst"
 
 {- Note [Phantom coercions]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~