Fix error recovery in solveEqualitieswip/T19142

As #19142 showed, with -fdefer-type-errors we were allowing
compilation to proceed despite a fatal kind error. This patch
fixes it, as described in the new note in GHC.Tc.Solver,
     Note [Wrapping failing kind equalities]

Also fixes #19158

Also when checking
   default( ty1, ty2, ... )

only consider a possible default (C ty2) if ty2 is kind-compatible
with C.  Previously we could form kind-incompatible constraints, with
who knows what kind of chaos resulting.  (Actually, no chaos results,
but that's only by accident.  It's plain wrong to form the constraint
(Num Either) for example.)  I just happened to notice
this during fixing #19142.

1 files changed, 25 insertions, 18 deletions

diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index 4f7c9dfea2..f6bb5f7d42 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -167,7 +167,6 @@ reportUnsolved wanted
 -- See Note [Deferring coercion errors to runtime]
 -- Used by solveEqualities for kind equalities
 --      (see Note [Fail fast on kind errors] in "GHC.Tc.Solver")
--- and for simplifyDefault.
 reportAllUnsolved :: WantedConstraints -> TcM ()
 reportAllUnsolved wanted
   = do { ev_binds <- newNoTcEvBinds
@@ -378,15 +377,30 @@ deferringAnyBindings (CEC { cec_defer_type_errors  = TypeError
                           , cec_out_of_scope_holes = HoleError }) = False
 deferringAnyBindings _                                            = True
 
--- | Transforms a 'ReportErrCtxt' into one that does not defer any bindings
--- at all.
-noDeferredBindings :: ReportErrCtxt -> ReportErrCtxt
-noDeferredBindings ctxt = ctxt { cec_defer_type_errors  = TypeError
-                               , cec_expr_holes         = HoleError
-                               , cec_out_of_scope_holes = HoleError }
-
-{- Note [Suppressing error messages]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+maybeSwitchOffDefer :: EvBindsVar -> ReportErrCtxt -> ReportErrCtxt
+-- Switch off defer-type-errors inside CoEvBindsVar
+-- See Note [Failing equalities with no evidence bindings]
+maybeSwitchOffDefer evb ctxt
+ | CoEvBindsVar{} <- evb
+ = ctxt { cec_defer_type_errors  = TypeError
+        , cec_expr_holes         = HoleError
+        , cec_out_of_scope_holes = HoleError }
+ | otherwise
+ = ctxt
+
+{- Note [Failing equalities with no evidence bindings]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If we go inside an implication that has no term evidence
+(e.g. unifying under a forall), we can't defer type errors.  You could
+imagine using the /enclosing/ bindings (in cec_binds), but that may
+not have enough stuff in scope for the bindings to be well typed.  So
+we just switch off deferred type errors altogether.  See #14605.
+
+This is done by maybeSwitchOffDefer.  It's also useful in one other
+place: see Note [Wrapping failing kind equalities] in GHC.Tc.Solver.
+
+Note [Suppressing error messages]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The cec_suppress flag says "don't report any errors".  Instead, just create
 evidence bindings (as usual).  It's used when more important errors have occurred.
 
@@ -445,15 +459,8 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs
     implic' = implic { ic_skols = tvs'
                      , ic_given = map (tidyEvVar env1) given
                      , ic_info  = info' }
-    ctxt1 | CoEvBindsVar{} <- evb    = noDeferredBindings ctxt
-          | otherwise                = ctxt
-          -- If we go inside an implication that has no term
-          -- evidence (e.g. unifying under a forall), we can't defer
-          -- type errors.  You could imagine using the /enclosing/
-          -- bindings (in cec_binds), but that may not have enough stuff
-          -- in scope for the bindings to be well typed.  So we just
-          -- switch off deferred type errors altogether.  See #14605.
 
+    ctxt1 = maybeSwitchOffDefer evb ctxt
     ctxt' = ctxt1 { cec_tidy     = env1
                   , cec_encl     = implic' : cec_encl ctxt