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.

10 files changed, 139 insertions, 32 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)
diff --git a/docs/users_guide/exts/defer_type_errors.rst b/docs/users_guide/exts/defer_type_errors.rst
index 146fc01760..1c644c5eda 100644
--- a/docs/users_guide/exts/defer_type_errors.rst
+++ b/docs/users_guide/exts/defer_type_errors.rst
@@ -99,7 +99,7 @@ Limitations of deferred type errors
 The errors that can be deferred are:
 
 - Out of scope term variables
-- Equality constraints; e.g. `ord True` gives rise to an insoluble equality constraint `Char ~ Bool`, which can be deferred.
+- Equality constraints; e.g. ``ord True`` gives rise to an insoluble equality constraint ``Char ~ Bool``, which can be deferred.
 - Type-class and implicit-parameter constraints
 
 All other type errors are reported immediately, and cannot be deferred; for
@@ -107,15 +107,22 @@ example, an ill-kinded type signature, an instance declaration that is
 non-terminating or ill-formed, a type-family instance that does not
 obey the declared injectivity constraints, etc etc.
 
-In a few cases, even equality constraints cannot be deferred.  Specifically:
+In a few cases, equality constraints cannot be deferred.  Specifically:
 
-- Kind-equalities cannot be deferred, e.g. ::
+- Kind errors in a type or kind signature, partial type signatures, or pattern signature.
+  e.g. ::
 
     f :: Int Bool -> Char
 
   This type signature contains a kind error which cannot be deferred.
 
-- Type equalities under a forall cannot be deferred (c.f. `#14605
+- Type equalities under a forall (c.f. `#14605
   <https://gitlab.haskell.org/ghc/ghc/issues/14605>`_).
 
+- Kind errors in a visible type application. e.g. ::
 
+    reverse @Maybe xs
+
+- Kind errors in a ``default`` declaration.  e.g. ::
+
+    default( Double, Int Int )
diff --git a/testsuite/tests/ghci/scripts/T19158.script b/testsuite/tests/ghci/scripts/T19158.script
new file mode 100644
index 0000000000..81d392cf43
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T19158.script
@@ -0,0 +1,3 @@
+:set -fdefer-type-errors
+:set -XTypeApplications
+:t id @Maybe
diff --git a/testsuite/tests/ghci/scripts/T19158.stderr b/testsuite/tests/ghci/scripts/T19158.stderr
new file mode 100644
index 0000000000..9b15a102e8
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T19158.stderr
@@ -0,0 +1,6 @@
+
+<interactive>:1:5: error:
+    • Expecting one more argument to ‘Maybe’
+      Expected a type, but ‘Maybe’ has kind ‘* -> *’
+    • In the type ‘Maybe’
+      In the expression: id @Maybe
diff --git a/testsuite/tests/ghci/scripts/all.T b/testsuite/tests/ghci/scripts/all.T
index f5c1a4ca39..08a6c4ee6a 100755
--- a/testsuite/tests/ghci/scripts/all.T
+++ b/testsuite/tests/ghci/scripts/all.T
@@ -327,3 +327,5 @@ test('T18644', normal, ghci_script, ['T18644.script'])
 test('T18755', normal, ghci_script, ['T18755.script'])
 test('T18828', normal, ghci_script, ['T18828.script'])
 test('T19197', normal, ghci_script, ['T19197.script'])
+test('T19158', normal, ghci_script, ['T19158.script'])
+
diff --git a/testsuite/tests/typecheck/should_fail/T19142.hs b/testsuite/tests/typecheck/should_fail/T19142.hs
new file mode 100644
index 0000000000..6c49498efa
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19142.hs
@@ -0,0 +1,20 @@
+{-# OPTIONS_GHC -fdefer-type-errors #-}
+{-# LANGUAGE ExplicitForAll
+           , TypeApplications
+           , KindSignatures
+           , ScopedTypeVariables
+#-}
+
+module T19142 where
+
+-- Both these examples gave Lint errors
+-- NB: the -fdefer-type-errors at the top!!
+
+-- Example 1
+f (x :: Maybe Maybe) = x
+
+-- Example 2
+foo :: forall (f :: * -> *) . String
+foo = ""
+
+g x = foo @Int
diff --git a/testsuite/tests/typecheck/should_fail/T19142.stderr b/testsuite/tests/typecheck/should_fail/T19142.stderr
new file mode 100644
index 0000000000..fc94a4166f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19142.stderr
@@ -0,0 +1,13 @@
+
+T19142.hs:14:15: error:
+    • Expecting one more argument to ‘Maybe’
+      Expected a type, but ‘Maybe’ has kind ‘* -> *’
+    • In the first argument of ‘Maybe’, namely ‘Maybe’
+      In the type ‘Maybe Maybe’
+      In a pattern type signature: Maybe Maybe
+
+T19142.hs:20:12: error:
+    • Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’
+    • In the type ‘Int’
+      In the expression: foo @Int
+      In an equation for ‘g’: g x = foo @Int
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 76f99f81c6..e191a736aa 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -612,3 +612,4 @@ test('TyAppPat_ScopedTyVarConflict', normal, compile_fail, [''])
 test('TyAppPat_TooMany', normal, compile_fail, [''])
 test('T12178a', normal, compile_fail, [''])
 test('T18869', normal, compile_fail, [''])
+test('T19142', normal, compile_fail, [''])