Fix error recovery in solveEqualities

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.

3 files changed, 83 insertions, 28 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
 
diff --git a/compiler/GHC/Tc/Gen/Default.hs b/compiler/GHC/Tc/Gen/Default.hs
index d37f26df40..c8106858b9 100644
--- a/compiler/GHC/Tc/Gen/Default.hs
+++ b/compiler/GHC/Tc/Gen/Default.hs
@@ -12,6 +12,8 @@ import GHC.Prelude
 
 import GHC.Hs
 import GHC.Core.Class
+import GHC.Core.Type ( typeKind )
+import GHC.Types.Var( tyVarKind )
 import GHC.Tc.Utils.Monad
 import GHC.Tc.Utils.Env
 import GHC.Tc.Gen.HsType
@@ -82,13 +84,20 @@ tc_default_ty deflt_clss hs_ty
         ; return ty }
 
 check_instance :: Type -> Class -> TcM Bool
-  -- Check that ty is an instance of cls
-  -- We only care about whether it worked or not; return a boolean
+-- Check that ty is an instance of cls
+-- We only care about whether it worked or not; return a boolean
+-- This checks that  cls :: k -> Constraint
+-- with just one argument and no polymorphism; if we need to add
+-- polymorphism we can make it more complicated.  For now we are
+-- concerned with classes like
+--    Num      :: Type -> Constraint
+--    Foldable :: (Type->Type) -> Constraint
 check_instance ty cls
-  = do  { (_, success) <- discardErrs $
-                          askNoErrs $
-                          simplifyDefault [mkClassPred cls [ty]]
-        ; return success }
+  | [cls_tv] <- classTyVars cls
+  , tyVarKind cls_tv `tcEqType` typeKind ty
+  = simplifyDefault [mkClassPred cls [ty]]
+  | otherwise
+  = return False
 
 defaultDeclCtxt :: SDoc
 defaultDeclCtxt = text "When checking the types in a default declaration"
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index 991708111d..2d97b84e9d 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -218,7 +218,13 @@ simplifyAndEmitFlatConstraints wanted
        ; traceTc "emitFlatConstraints {" (ppr wanted)
        ; case floatKindEqualities wanted of
            Nothing -> do { traceTc "emitFlatConstraints } failing" (ppr wanted)
-                         ; emitConstraints wanted -- So they get reported!
+                         -- Emit the bad constraints, wrapped in an implication
+                         -- See Note [Wrapping failing kind equalities]
+                         ; tclvl  <- TcM.getTcLevel
+                         ; implic <- buildTvImplication UnkSkol [] tclvl wanted
+                                     -- UnkSkol: doesn't matter, because
+                                     -- we bind no skolem varaibles here
+                         ; emitImplication implic
                          ; failM }
            Just (simples, holes)
               -> do { _ <- promoteTyVarSet (tyCoVarsOfCts simples)
@@ -376,6 +382,40 @@ All this is done:
 
 See also #18062, #11506
 
+Note [Wrapping failing kind equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In simplifyAndEmitFlatConstraints, if we fail to get down to simple
+flat constraints we will
+* re-emit the constraints so that they are reported
+* fail in the monad
+But there is a Terrible Danger that, if -fdefer-type-errors is on, and
+we just re-emit an insoluble constraint like (* ~ (*->*)), that we'll
+report only a warning and proceed with compilation.  But if we ever fail
+in the monad it should be fatal; we should report an error and stop after
+the type checker.  If not, chaos results: #19142.
+
+Our solution is this:
+* Even with -fdefer-type-errors, inside an implication with no place for
+  value bindings (ic_binds = CoEvBindsVar), report failing equalities as
+  errors.  We have to do this anyway; see GHC.Tc.Errors
+  Note [Failing equalities with no evidence bindings].
+
+* Right here in simplifyAndEmitFlatConstraints, use buildTvImplication
+  to wrap the failing constraint in a degenerate implication (no
+  skolems, no theta, no bumped TcLevel), with ic_binds = CoEvBindsVar.
+  That way any failing equalities will lead to an error not a warning,
+  irrespective of -fdefer-type-errors.
+
+  This is a slight hack, because the implication doesn't have a bumped
+  TcLevel, but that doesn't matter.
+
+We re-emit the implication rather than reporting the errors right now,
+so that the error mesages are improved by other solving and defaulting.
+e.g. we prefer
+    Cannot match 'Type->Type' with 'Type'
+to  Cannot match 'Type->Type' with 'TYPE r0'
+
+
 Note [floatKindEqualities vs approximateWC]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 floatKindEqualities and approximateWC are strikingly similar to each
@@ -757,13 +797,12 @@ simplifyInteractive wanteds
 
 ------------------
 simplifyDefault :: ThetaType    -- Wanted; has no type variables in it
-                -> TcM ()       -- Succeeds if the constraint is soluble
+                -> TcM Bool     -- Return if the constraint is soluble
 simplifyDefault theta
   = do { traceTc "simplifyDefault" empty
        ; wanteds  <- newWanteds DefaultOrigin theta
        ; unsolved <- runTcSDeriveds (solveWantedsAndDrop (mkSimpleWC wanteds))
-       ; reportAllUnsolved unsolved
-       ; return () }
+       ; return (isEmptyWC unsolved) }
 
 ------------------
 tcCheckSatisfiability :: InertSet -> Bag EvVar -> TcM (Maybe InertSet)