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.

1 files changed, 43 insertions, 2 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