Improve error recovery in the typechecker

Issue #16418 showed that we were carrying on too eagerly after a bogus
type signature was identified (a bad telescope in fact), leading to a
subsequent crash.

This led me in to a maze of twisty little passages in the typechecker's
error recovery, and I ended up doing some refactoring in TcRnMonad.
Some specfifics

* TcRnMonad.try_m is now called attemptM.

* I switched the order of the result pair in tryTc,
  to make it consistent with other similar functions.

* The actual exception used in the Tc monad is irrelevant so,
  to avoid polluting type signatures, I made tcTryM, a simple
  wrapper around tryM, and used it.

The more important changes are in

* TcSimplify.captureTopConstraints, where we should have been calling
  simplifyTop rather than reportUnsolved, so that levity defaulting
  takes place properly.

* TcUnify.emitResidualTvConstraint, where we need to set the correct
  status for a new implication constraint.  (Previously we ended up
  with an Insoluble constraint wrapped in an Unsolved implication,
  which meant that insolubleWC gave the wrong answer.

21 files changed, 327 insertions, 214 deletions

diff --git a/compiler/ghci/RtClosureInspect.hs b/compiler/ghci/RtClosureInspect.hs
index 436b756af6..c64ffa9ec3 100644
--- a/compiler/ghci/RtClosureInspect.hs
+++ b/compiler/ghci/RtClosureInspect.hs
@@ -765,7 +765,7 @@ cvObtainTerm hsc_env max_depth force old_ty hval = runTR hsc_env $ do
                         then parens (text "already monomorphic: " <> ppr my_ty)
                         else Ppr.empty)
         Right dcname <- liftIO $ constrClosToName hsc_env clos
-        (_,mb_dc)    <- tryTc (tcLookupDataCon dcname)
+        (mb_dc, _)   <- tryTc (tcLookupDataCon dcname)
         case mb_dc of
           Nothing -> do -- This can happen for private constructors compiled -O0
                         -- where the .hi descriptor does not export them
@@ -981,7 +981,7 @@ cvReconstructType hsc_env max_depth old_ty hval = runTR_maybe hsc_env $ do
       ConstrClosure{ptrArgs=pArgs} -> do
         Right dcname <- liftIO $ constrClosToName hsc_env clos
         traceTR (text "Constr1" <+> ppr dcname)
-        (_,mb_dc) <- tryTc (tcLookupDataCon dcname)
+        (mb_dc, _) <- tryTc (tcLookupDataCon dcname)
         case mb_dc of
           Nothing-> do
             forM pArgs $ \x -> do
diff --git a/compiler/typecheck/TcBackpack.hs b/compiler/typecheck/TcBackpack.hs
index f3611921ea..7fffcd1d18 100644
--- a/compiler/typecheck/TcBackpack.hs
+++ b/compiler/typecheck/TcBackpack.hs
@@ -582,7 +582,7 @@ mergeSignatures
                         -- signatures that are merged in, we will discover this
                         -- when we run exports_from_avail on the final merged
                         -- export list.
-                        (msgs, mb_r) <- tryTc $ do
+                        (mb_r, msgs) <- tryTc $ do
                             -- Suppose that we have written in a signature:
                             --  signature A ( module A ) where {- empty -}
                             -- If I am also inheriting a signature from a
diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs
index b4803fc043..9cdc939310 100644
--- a/compiler/typecheck/TcBinds.hs
+++ b/compiler/typecheck/TcBinds.hs
@@ -392,14 +392,13 @@ tcValBinds :: TopLevelFlag
            -> TcM ([(RecFlag, LHsBinds GhcTcId)], thing)
 
 tcValBinds top_lvl binds sigs thing_inside
-  = do  { let patsyns = getPatSynBinds binds
-
-            -- Typecheck the signature
+  = do  {   -- Typecheck the signatures
+            -- It's easier to do so now, once for all the SCCs together
+            -- because a single signature  f,g :: <type>
+            -- might relate to more than one SCC
         ; (poly_ids, sig_fn) <- tcAddPatSynPlaceholders patsyns $
                                 tcTySigs sigs
 
-        ; let prag_fn = mkPragEnv sigs (foldr (unionBags . snd) emptyBag binds)
-
                 -- Extend the envt right away with all the Ids
                 -- declared with complete type signatures
                 -- Do not extend the TcBinderStack; instead
@@ -413,6 +412,9 @@ tcValBinds top_lvl binds sigs thing_inside
                    ; let extra_binds = [ (NonRecursive, builder) | builder <- patsyn_builders ]
                    ; return (extra_binds, thing) }
             ; return (binds' ++ extra_binds', thing) }}
+  where
+    patsyns = getPatSynBinds binds
+    prag_fn = mkPragEnv sigs (foldr (unionBags . snd) emptyBag binds)
 
 ------------------------
 tcBindGroups :: TopLevelFlag -> TcSigFun -> TcPragEnv
diff --git a/compiler/typecheck/TcRnExports.hs b/compiler/typecheck/TcRnExports.hs
index f584a7fceb..e4009e6040 100644
--- a/compiler/typecheck/TcRnExports.hs
+++ b/compiler/typecheck/TcRnExports.hs
@@ -140,10 +140,10 @@ accumExports :: (ExportAccum -> x -> TcRn (Maybe (ExportAccum, y)))
              -> TcRn [y]
 accumExports f = fmap (catMaybes . snd) . mapAccumLM f' emptyExportAccum
   where f' acc x = do
-          m <- try_m (f acc x)
+          m <- attemptM (f acc x)
           pure $ case m of
-            Right (Just (acc', y)) -> (acc', Just y)
-            _                      -> (acc, Nothing)
+            Just (Just (acc', y)) -> (acc', Just y)
+            _                     -> (acc, Nothing)
 
 type ExportOccMap = OccEnv (Name, IE GhcPs)
         -- Tracks what a particular exported OccName
@@ -192,7 +192,7 @@ tcRnExports explicit_mod exports
         ; let do_it = exports_from_avail real_exports rdr_env imports this_mod
         ; (rn_exports, final_avails)
             <- if hsc_src == HsigFile
-                then do (msgs, mb_r) <- tryTc do_it
+                then do (mb_r, msgs) <- tryTc do_it
                         case mb_r of
                             Just r  -> return r
                             Nothing -> addMessages msgs >> failM
diff --git a/compiler/typecheck/TcRnMonad.hs b/compiler/typecheck/TcRnMonad.hs
index 951cc7a5a6..3997f2dc82 100644
--- a/compiler/typecheck/TcRnMonad.hs
+++ b/compiler/typecheck/TcRnMonad.hs
@@ -71,7 +71,7 @@ module TcRnMonad(
   -- * Shared error message stuff: renamer and typechecker
   mkLongErrAt, mkErrDocAt, addLongErrAt, reportErrors, reportError,
   reportWarning, recoverM, mapAndRecoverM, mapAndReportM, foldAndRecoverM,
-  try_m, tryTc,
+  attemptM, tryTc,
   askNoErrs, discardErrs, tryTcDiscardingErrs,
   checkNoErrs, whenNoErrs,
   ifErrsM, failIfErrsM,
@@ -986,130 +986,8 @@ reportWarning reason err
        ; (warns, errs) <- readTcRef errs_var
        ; writeTcRef errs_var (warns `snocBag` warn, errs) }
 
-try_m :: TcRn r -> TcRn (Either IOEnvFailure r)
--- Does tryM, with a debug-trace on failure
--- If we do recover from an exception, /insoluble/ constraints
--- (only) in 'thing' are are propagated
-try_m thing
-  = do { (mb_r, lie) <- tryCaptureConstraints thing
-       ; emitConstraints lie
-
-       -- Debug trace
-       ; case mb_r of
-            Left exn -> traceTc "tryTc/recoverM recovering from" $
-                        (text (showException exn) $$ ppr lie)
-            Right {} -> return ()
-
-       ; return mb_r }
-
------------------------
-recoverM :: TcRn r      -- Recovery action; do this if the main one fails
-         -> TcRn r      -- Main action: do this first;
-                        --  if it generates errors, propagate them all
-         -> TcRn r
--- Errors in 'thing' are retained
--- If we do recover from an exception, /insoluble/ constraints
--- (only) in 'thing' are are propagated
-recoverM recover thing
-  = do { mb_res <- try_m thing ;
-         case mb_res of
-           Left _    -> recover
-           Right res -> return res }
-
-
------------------------
-
--- | Drop elements of the input that fail, so the result
--- list can be shorter than the argument list
-mapAndRecoverM :: (a -> TcRn b) -> [a] -> TcRn [b]
-mapAndRecoverM f = mapMaybeM (fmap rightToMaybe . try_m . f)
-
--- | The accumulator is not updated if the action fails
-foldAndRecoverM :: (b -> a -> TcRn b) -> b -> [a] -> TcRn b
-foldAndRecoverM _ acc []     = return acc
-foldAndRecoverM f acc (x:xs) =
-                          do { mb_r <- try_m (f acc x)
-                             ; case mb_r of
-                                Left _  -> foldAndRecoverM f acc xs
-                                Right acc' -> foldAndRecoverM f acc' xs  }
-
--- | Succeeds if applying the argument to all members of the lists succeeds,
---   but nevertheless runs it on all arguments, to collect all errors.
-mapAndReportM :: (a -> TcRn b) -> [a] -> TcRn [b]
-mapAndReportM f xs = checkNoErrs (mapAndRecoverM f xs)
-
------------------------
-tryTc :: TcRn a -> TcRn (Messages, Maybe a)
--- (tryTc m) executes m, and returns
---      Just r,  if m succeeds (returning r)
---      Nothing, if m fails
--- It also returns all the errors and warnings accumulated by m
--- It always succeeds (never raises an exception)
-tryTc thing_inside
- = do { errs_var <- newTcRef emptyMessages ;
-
-        res  <- try_m $  -- Be sure to catch exceptions, so that
-                         -- we guaranteed to read the messages out
-                         -- of that brand-new errs_var!
-                setErrsVar errs_var $
-                thing_inside ;
-
-        msgs <- readTcRef errs_var ;
-
-        return (msgs, case res of
-                        Left _    -> Nothing
-                        Right val -> Just val)
-        -- The exception is always the IOEnv built-in
-        -- in exception; see IOEnv.failM
-   }
-
------------------------
-discardErrs :: TcRn a -> TcRn a
--- (discardErrs m) runs m,
---   discarding all error messages and warnings generated by m
--- If m fails, discardErrs fails, and vice versa
-discardErrs m
- = do { errs_var <- newTcRef emptyMessages
-      ; setErrsVar errs_var m }
-
------------------------
-tryTcDiscardingErrs :: TcM r -> TcM r -> TcM r
--- (tryTcDiscardingErrs recover main) tries 'main';
---      if 'main' succeeds with no error messages, it's the answer
---      otherwise discard everything from 'main', including errors,
---          and try 'recover' instead.
-tryTcDiscardingErrs recover main
-  = do  { (msgs, mb_res) <- tryTc main
-        ; dflags <- getDynFlags
-        ; case mb_res of
-            Just res | not (errorsFound dflags msgs)
-              -> -- 'main' succeeed with no error messages
-                 do { addMessages msgs  -- msgs might still have warnings
-                    ; return res }
-
-            _ -> -- 'main' failed, or produced an error message
-                 recover     -- Discard all errors and warnings entirely
-        }
 
 -----------------------
--- (askNoErrs m) runs m
--- If m fails,
---    then (askNoErrs m) fails
--- If m succeeds with result r,
---    then (askNoErrs m) succeeds with result (r, b),
---         where b is True iff m generated no errors
--- Regardless of success or failure,
---   propagate any errors/warnings generated by m
-askNoErrs :: TcRn a -> TcRn (a, Bool)
-askNoErrs m
-  = do { (msgs, mb_res) <- tryTc m
-       ; addMessages msgs  -- Always propagate errors
-       ; case mb_res of
-           Nothing  -> failM
-           Just res -> do { dflags <- getDynFlags
-                          ; let errs_found = errorsFound dflags msgs
-                          ; return (res, not errs_found) } }
------------------------
 checkNoErrs :: TcM r -> TcM r
 -- (checkNoErrs m) succeeds iff m succeeds and generates no errors
 -- If m fails then (checkNoErrsTc m) fails.
@@ -1212,6 +1090,224 @@ setCtLocM (CtLoc { ctl_env = lcl }) thing_inside
                            , tcl_ctxt  = tcl_ctxt lcl })
               thing_inside
 
+
+{- *********************************************************************
+*                                                                      *
+             Error recovery and exceptions
+*                                                                      *
+********************************************************************* -}
+
+tcTryM :: TcRn r -> TcRn (Maybe r)
+-- The most basic function: catch the exception
+--   Nothing => an exception happened
+--   Just r  => no exception, result R
+-- Errors and constraints are propagated in both cases
+-- Never throws an exception
+tcTryM thing_inside
+  = do { either_res <- tryM thing_inside
+       ; return (case either_res of
+                    Left _  -> Nothing
+                    Right r -> Just r) }
+         -- In the Left case the exception is always the IOEnv
+         -- built-in in exception; see IOEnv.failM
+
+-----------------------
+capture_constraints :: TcM r -> TcM (r, WantedConstraints)
+-- capture_constraints simply captures and returns the
+--                     constraints generated by thing_inside
+-- Precondition: thing_inside must not throw an exception!
+-- Reason for precondition: an exception would blow past the place
+-- where we read the lie_var, and we'd lose the constraints altogether
+capture_constraints thing_inside
+  = do { lie_var <- newTcRef emptyWC
+       ; res <- updLclEnv (\ env -> env { tcl_lie = lie_var }) $
+                thing_inside
+       ; lie <- readTcRef lie_var
+       ; return (res, lie) }
+
+capture_messages :: TcM r -> TcM (r, Messages)
+-- capture_messages simply captures and returns the
+--                  errors arnd warnings generated by thing_inside
+-- Precondition: thing_inside must not throw an exception!
+-- Reason for precondition: an exception would blow past the place
+-- where we read the msg_var, and we'd lose the constraints altogether
+capture_messages thing_inside
+  = do { msg_var <- newTcRef emptyMessages
+       ; res     <- setErrsVar msg_var thing_inside
+       ; msgs    <- readTcRef msg_var
+       ; return (res, msgs) }
+
+-----------------------
+-- (askNoErrs m) runs m
+-- If m fails,
+--    then (askNoErrs m) fails, propagating only
+--         insoluble constraints
+--
+-- If m succeeds with result r,
+--    then (askNoErrs m) succeeds with result (r, b),
+--         where b is True iff m generated no errors
+--
+-- Regardless of success or failure,
+--   propagate any errors/warnings generated by m
+askNoErrs :: TcRn a -> TcRn (a, Bool)
+askNoErrs thing_inside
+  = do { ((mb_res, lie), msgs) <- capture_messages    $
+                                  capture_constraints $
+                                  tcTryM thing_inside
+       ; addMessages msgs
+
+       ; case mb_res of
+           Nothing  -> do { emitConstraints (insolublesOnly lie)
+                          ; failM }
+
+           Just res -> do { emitConstraints lie
+                          ; dflags <- getDynFlags
+                          ; let errs_found = errorsFound dflags msgs
+                                          || insolubleWC lie
+                          ; return (res, not errs_found) } }
+
+-----------------------
+tryCaptureConstraints :: TcM a -> TcM (Maybe a, WantedConstraints)
+-- (tryCaptureConstraints_maybe m) runs m,
+--   and returns the type constraints it generates
+-- It never throws an exception; instead if thing_inside fails,
+--   it returns Nothing and the /insoluble/ constraints
+-- Error messages are propagated
+tryCaptureConstraints thing_inside
+  = do { (mb_res, lie) <- capture_constraints $
+                          tcTryM thing_inside
+
+       -- See Note [Constraints and errors]
+       ; let lie_to_keep = case mb_res of
+                             Nothing -> insolublesOnly lie
+                             Just {} -> lie
+
+       ; return (mb_res, lie_to_keep) }
+
+captureConstraints :: TcM a -> TcM (a, WantedConstraints)
+-- (captureConstraints m) runs m, and returns the type constraints it generates
+-- If thing_inside fails (throwing an exception),
+--   then (captureConstraints thing_inside) fails too
+--   propagating the insoluble constraints only
+-- Error messages are propagated in either case
+captureConstraints thing_inside
+  = do { (mb_res, lie) <- tryCaptureConstraints thing_inside
+
+            -- See Note [Constraints and errors]
+            -- If the thing_inside threw an exception, emit the insoluble
+            -- constraints only (returned by tryCaptureConstraints)
+            -- so that they are not lost
+       ; case mb_res of
+           Nothing  -> do { emitConstraints lie; failM }
+           Just res -> return (res, lie) }
+
+-----------------------
+attemptM :: TcRn r -> TcRn (Maybe r)
+-- (attemptM thing_inside) runs thing_inside
+-- If thing_inside succeeds, returning r,
+--   we return (Just r), and propagate all constraints and errors
+-- If thing_inside fail, throwing an exception,
+--   we return Nothing, propagating insoluble constraints,
+--                      and all errors
+-- attemptM never throws an exception
+attemptM thing_inside
+  = do { (mb_r, lie) <- tryCaptureConstraints thing_inside
+       ; emitConstraints lie
+
+       -- Debug trace
+       ; when (isNothing mb_r) $
+         traceTc "attemptM recovering with insoluble constraints" $
+                 (ppr lie)
+
+       ; return mb_r }
+
+-----------------------
+recoverM :: TcRn r      -- Recovery action; do this if the main one fails
+         -> TcRn r      -- Main action: do this first;
+                        --  if it generates errors, propagate them all
+         -> TcRn r
+-- (recoverM recover thing_inside) runs thing_inside
+-- If thing_inside fails, propagate its errors and insoluble constraints
+--                        and run 'recover'
+-- If thing_inside succeeds, propagate all its errors and constraints
+--
+-- Can fail, if 'recover' fails
+recoverM recover thing
+  = do { mb_res <- attemptM thing ;
+         case mb_res of
+           Nothing  -> recover
+           Just res -> return res }
+
+-----------------------
+
+-- | Drop elements of the input that fail, so the result
+-- list can be shorter than the argument list
+mapAndRecoverM :: (a -> TcRn b) -> [a] -> TcRn [b]
+mapAndRecoverM f xs
+  = do { mb_rs <- mapM (attemptM . f) xs
+       ; return [r | Just r <- mb_rs] }
+
+-- | Apply the function to all elements on the input list
+-- If all succeed, return the list of results
+-- Othewise fail, propagating all errors
+mapAndReportM :: (a -> TcRn b) -> [a] -> TcRn [b]
+mapAndReportM f xs
+  = do { mb_rs <- mapM (attemptM . f) xs
+       ; when (any isNothing mb_rs) failM
+       ; return [r | Just r <- mb_rs] }
+
+-- | The accumulator is not updated if the action fails
+foldAndRecoverM :: (b -> a -> TcRn b) -> b -> [a] -> TcRn b
+foldAndRecoverM _ acc []     = return acc
+foldAndRecoverM f acc (x:xs) =
+                          do { mb_r <- attemptM (f acc x)
+                             ; case mb_r of
+                                Nothing   -> foldAndRecoverM f acc xs
+                                Just acc' -> foldAndRecoverM f acc' xs  }
+
+-----------------------
+tryTc :: TcRn a -> TcRn (Maybe a, Messages)
+-- (tryTc m) executes m, and returns
+--      Just r,  if m succeeds (returning r)
+--      Nothing, if m fails
+-- It also returns all the errors and warnings accumulated by m
+-- It always succeeds (never raises an exception)
+tryTc thing_inside
+ = capture_messages (attemptM thing_inside)
+
+-----------------------
+discardErrs :: TcRn a -> TcRn a
+-- (discardErrs m) runs m,
+--   discarding all error messages and warnings generated by m
+-- If m fails, discardErrs fails, and vice versa
+discardErrs m
+ = do { errs_var <- newTcRef emptyMessages
+      ; setErrsVar errs_var m }
+
+-----------------------
+tryTcDiscardingErrs :: TcM r -> TcM r -> TcM r
+-- (tryTcDiscardingErrs recover thing_inside) tries 'thing_inside';
+--      if 'main' succeeds with no error messages, it's the answer
+--      otherwise discard everything from 'main', including errors,
+--          and try 'recover' instead.
+tryTcDiscardingErrs recover thing_inside
+  = do { ((mb_res, lie), msgs) <- capture_messages    $
+                                  capture_constraints $
+                                  tcTryM thing_inside
+        ; dflags <- getDynFlags
+        ; case mb_res of
+            Just res | not (errorsFound dflags msgs)
+                     , not (insolubleWC lie)
+              -> -- 'main' succeeed with no errors
+                 do { addMessages msgs  -- msgs might still have warnings
+                    ; emitConstraints lie
+                    ; return res }
+
+            _ -> -- 'main' failed, or produced an error message
+                 recover     -- Discard all errors and warnings
+                             -- and unsolved constraints entirely
+        }
+
 {-
 ************************************************************************
 *                                                                      *
@@ -1527,38 +1623,6 @@ emitInsolubles cts
 discardConstraints :: TcM a -> TcM a
 discardConstraints thing_inside = fst <$> captureConstraints thing_inside
 
-tryCaptureConstraints :: TcM a -> TcM (Either IOEnvFailure a, WantedConstraints)
--- (captureConstraints_maybe m) runs m,
--- and returns the type constraints it generates
--- It never throws an exception; instead if thing_inside fails,
---   it returns Left exn and the /insoluble/ constraints
-tryCaptureConstraints thing_inside
-  = do { lie_var <- newTcRef emptyWC
-       ; mb_res <- tryM $
-                   updLclEnv (\ env -> env { tcl_lie = lie_var }) $
-                   thing_inside
-       ; lie <- readTcRef lie_var
-
-       -- See Note [Constraints and errors]
-       ; let lie_to_keep = case mb_res of
-                             Left {}  -> insolublesOnly lie
-                             Right {} -> lie
-
-       ; return (mb_res, lie_to_keep) }
-
-captureConstraints :: TcM a -> TcM (a, WantedConstraints)
--- (captureConstraints m) runs m, and returns the type constraints it generates
-captureConstraints thing_inside
-  = do { (mb_res, lie) <- tryCaptureConstraints thing_inside
-
-            -- See Note [Constraints and errors]
-            -- If the thing_inside threw an exception, emit the insoluble
-            -- constraints only (returned by tryCaptureConstraints)
-            -- so that they are not lost
-       ; case mb_res of
-           Left _    -> do { emitConstraints lie; failM }
-           Right res -> return (res, lie) }
-
 -- | The name says it all. The returned TcLevel is the *inner* TcLevel.
 pushLevelAndCaptureConstraints :: TcM a -> TcM (TcLevel, WantedConstraints, a)
 pushLevelAndCaptureConstraints thing_inside
@@ -1662,7 +1726,7 @@ un-filled-in, and will emit a misleading error message.
 
 The underlying problem is that an exception interrupts the constraint
 gathering process. Bottom line: if we have an exception, it's best
-simply to discard any gathered constraints.  Hence in 'try_m' we
+simply to discard any gathered constraints.  Hence in 'attemptM' we
 capture the constraints in a fresh variable, and only emit them into
 the surrounding context if we exit normally.  If an exception is
 raised, simply discard the collected constraints... we have a hard
diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs
index d2e4a62546..5d8d92af80 100644
--- a/compiler/typecheck/TcSigs.hs
+++ b/compiler/typecheck/TcSigs.hs
@@ -168,14 +168,19 @@ completeSigPolyId_maybe sig
 
 tcTySigs :: [LSig GhcRn] -> TcM ([TcId], TcSigFun)
 tcTySigs hs_sigs
-  = checkNoErrs $   -- See Note [Fail eagerly on bad signatures]
-    do { ty_sigs_s <- mapAndRecoverM tcTySig hs_sigs
-       ; let ty_sigs  = concat ty_sigs_s
+  = checkNoErrs $
+    do { -- Fail if any of the signatures is duff
+         -- Hence mapAndReportM
+         -- See Note [Fail eagerly on bad signatures]
+         ty_sigs_s <- mapAndReportM tcTySig hs_sigs
+
+       ; let ty_sigs = concat ty_sigs_s
              poly_ids = mapMaybe completeSigPolyId_maybe ty_sigs
                         -- The returned [TcId] are the ones for which we have
                         -- a complete type signature.
                         -- See Note [Complete and partial type signatures]
              env = mkNameEnv [(tcSigInfoName sig, sig) | sig <- ty_sigs]
+
        ; return (poly_ids, lookupNameEnv env) }
 
 tcTySig :: LSig GhcRn -> TcM [TcSigInfo]
@@ -308,9 +313,15 @@ If a type signature is wrong, fail immediately:
    the code against the signature will give a very similar error
    to the ambiguity error.
 
-ToDo: this means we fall over if any type sig
-is wrong (eg at the top level of the module),
-which is over-conservative
+ToDo: this means we fall over if any top-level type signature in the
+module is wrong, because we typecheck all the signatures together
+(see TcBinds.tcValBinds).  Moreover, because of top-level
+captureTopConstraints, only insoluble constraints will be reported.
+We typecheck all signatures at the same time because a signature
+like   f,g :: blah   might have f and g from different SCCs.
+
+So it's a bit awkward to get better error recovery, and no one
+has complained!
 -}
 
 {- *********************************************************************
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index cd9d8585f5..c0fc4e860a 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -107,10 +107,12 @@ captureTopConstraints thing_inside
        -- constraints, report the latter before propagating the exception
        -- Otherwise they will be lost altogether
        ; case mb_res of
-           Right res -> return (res, lie `andWC` stWC)
-           Left {}   -> do { _ <- reportUnsolved lie; failM } }
-                -- This call to reportUnsolved is the reason
+           Just res -> return (res, lie `andWC` stWC)
+           Nothing  -> do { _ <- simplifyTop lie; failM } }
+                -- This call to simplifyTop is the reason
                 -- this function is here instead of TcRnMonad
+                -- We call simplifyTop so that it does defaulting
+                -- (esp of runtime-reps) before reporting errors
 
 simplifyTopImplic :: Bag Implication -> TcM ()
 simplifyTopImplic implics
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index 29aff60921..d8b1edf492 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -1179,8 +1179,15 @@ emitResidualTvConstraint skol_info m_telescope skol_tvs tclvl wanted
   | otherwise
   = do { ev_binds <- newNoTcEvBinds
        ; implic   <- newImplication
+       ; let status | insolubleWC wanted = IC_Insoluble
+                    | otherwise          = IC_Unsolved
+             -- If the inner constraints are insoluble,
+             -- we should mark the outer one similarly,
+             -- so that insolubleWC works on the outer one
+
        ; emitImplication $
-         implic { ic_tclvl     = tclvl
+         implic { ic_status    = status
+                , ic_tclvl     = tclvl
                 , ic_skols     = skol_tvs
                 , ic_no_eqs    = True
                 , ic_telescope = m_telescope
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope2.hs b/testsuite/tests/dependent/should_fail/BadTelescope2.hs
index e33fdf110e..73f69676e7 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope2.hs
+++ b/testsuite/tests/dependent/should_fail/BadTelescope2.hs
@@ -3,12 +3,9 @@
 module BadTelescope2 where
 
 import Data.Kind
-import Data.Proxy
 
 data SameKind :: k -> k -> *
 
 foo :: forall a k (b :: k). SameKind a b
 foo = undefined
 
-bar :: forall a k (b :: k) (c :: Proxy b) (d :: Proxy a). Proxy c -> SameKind b d
-bar = undefined
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope2.stderr b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
index a8c4b689ae..3637dece24 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
+++ b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
@@ -1,13 +1,6 @@
 
-BadTelescope2.hs:10:8: error:
+BadTelescope2.hs:9:8: error:
     • These kind and type variables: a k (b :: k)
       are out of dependency order. Perhaps try this ordering:
         k (a :: k) (b :: k)
     • In the type signature: foo :: forall a k (b :: k). SameKind a b
-
-BadTelescope2.hs:13:81: error:
-    • Expected kind ‘k’, but ‘d’ has kind ‘Proxy a’
-    • In the second argument of ‘SameKind’, namely ‘d’
-      In the type signature:
-        bar :: forall a k (b :: k) (c :: Proxy b) (d :: Proxy a).
-               Proxy c -> SameKind b d
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope5.hs b/testsuite/tests/dependent/should_fail/BadTelescope5.hs
new file mode 100644
index 0000000000..ce2368bbbe
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/BadTelescope5.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE DataKinds, PolyKinds, ExplicitForAll #-}
+
+module BadTelescope5 where
+
+import Data.Kind
+import Data.Proxy
+
+data SameKind :: k -> k -> *
+
+bar :: forall a k (b :: k) (c :: Proxy b) (d :: Proxy a). Proxy c -> SameKind b d
+bar = undefined
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope5.stderr b/testsuite/tests/dependent/should_fail/BadTelescope5.stderr
new file mode 100644
index 0000000000..da79678d5b
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/BadTelescope5.stderr
@@ -0,0 +1,7 @@
+
+BadTelescope5.hs:10:81: error:
+    • Expected kind ‘k’, but ‘d’ has kind ‘Proxy a’
+    • In the second argument of ‘SameKind’, namely ‘d’
+      In the type signature:
+        bar :: forall a k (b :: k) (c :: Proxy b) (d :: Proxy a).
+               Proxy c -> SameKind b d
diff --git a/testsuite/tests/dependent/should_fail/T15743c.stderr b/testsuite/tests/dependent/should_fail/T15743c.stderr
index 8e3ad5077f..4cb1c0c959 100644
--- a/testsuite/tests/dependent/should_fail/T15743c.stderr
+++ b/testsuite/tests/dependent/should_fail/T15743c.stderr
@@ -13,3 +13,18 @@ T15743c.hs:10:1: error:
         (b :: Proxy d)
         (x :: SimilarKind a b)
     • In the data type declaration for ‘T’
+
+T15743c.hs:11:1: error:
+    • The kind of ‘T2’ is ill-scoped
+        Inferred kind: T2 :: forall (d :: k).
+                             forall k (c :: k) (a :: Proxy c) (b :: Proxy d) ->
+                             SimilarKind a b -> *
+      NB: Specified variables (namely: (d :: k)) always come first
+      Perhaps try this order instead:
+        k
+        (d :: k)
+        (c :: k)
+        (a :: Proxy c)
+        (b :: Proxy d)
+        (x :: SimilarKind a b)
+    • In the data type declaration for ‘T2’
diff --git a/testsuite/tests/dependent/should_fail/T16418.hs b/testsuite/tests/dependent/should_fail/T16418.hs
new file mode 100644
index 0000000000..8097e3cbf3
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16418.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+module T16418 where
+
+import Data.Kind
+
+data SameKind :: forall k. k -> k -> Type
+
+f :: forall a k (b :: k). SameKind a b -> ()
+f = g
+  where
+    g :: SameKind a b -> ()
+    g _ = ()
diff --git a/testsuite/tests/dependent/should_fail/T16418.stderr b/testsuite/tests/dependent/should_fail/T16418.stderr
new file mode 100644
index 0000000000..fa2263abd3
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16418.stderr
@@ -0,0 +1,7 @@
+
+T16418.hs:9:6: error:
+    • These kind and type variables: a k (b :: k)
+      are out of dependency order. Perhaps try this ordering:
+        k (a :: k) (b :: k)
+    • In the type signature:
+        f :: forall a k (b :: k). SameKind a b -> ()
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 1f75a85716..1e6ab40b09 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -4,9 +4,10 @@ test('TypeSkolEscape', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
 test('BadTelescope', normal, compile_fail, [''])
 test('BadTelescope2', normal, compile_fail, [''])
 test('BadTelescope3', normal, compile_fail, [''])
+test('BadTelescope4', normal, compile_fail, [''])
+test('BadTelescope5', normal, compile_fail, [''])
 test('PromotedClass', normal, compile_fail, [''])
 test('SelfDep', normal, compile_fail, [''])
-test('BadTelescope4', normal, compile_fail, [''])
 test('RenamingStar', normal, compile_fail, [''])
 test('T11407', normal, compile_fail, [''])
 test('T11334b', normal, compile_fail, [''])
@@ -55,3 +56,4 @@ test('T16326_Fail12', normal, compile_fail, [''])
 test('T16391b', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
 test('T16344', normal, compile_fail, [''])
 test('T16344a', normal, compile_fail, [''])
+test('T16418', normal, compile_fail, [''])
diff --git a/testsuite/tests/patsyn/should_fail/T9161-1.hs b/testsuite/tests/patsyn/should_fail/T9161-1.hs
index c14eb542cc..32a6f9d6aa 100644
--- a/testsuite/tests/patsyn/should_fail/T9161-1.hs
+++ b/testsuite/tests/patsyn/should_fail/T9161-1.hs
@@ -1,6 +1,8 @@
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE DataKinds #-}
 
+module Bug where
+
 pattern PATTERN = ()
 
 wrongLift :: PATTERN
diff --git a/testsuite/tests/patsyn/should_fail/T9161-1.stderr b/testsuite/tests/patsyn/should_fail/T9161-1.stderr
index fff6efe286..39faffdaa8 100644
--- a/testsuite/tests/patsyn/should_fail/T9161-1.stderr
+++ b/testsuite/tests/patsyn/should_fail/T9161-1.stderr
@@ -1,5 +1,5 @@
 
-T9161-1.hs:6:14: error:
+T9161-1.hs:8:14: error:
     • Pattern synonym ‘PATTERN’ cannot be used here
         (pattern synonyms cannot be promoted)
     • In the type signature: wrongLift :: PATTERN
diff --git a/testsuite/tests/patsyn/should_fail/T9161-2.hs b/testsuite/tests/patsyn/should_fail/T9161-2.hs
index 941d23e35f..ccdfa1ff05 100644
--- a/testsuite/tests/patsyn/should_fail/T9161-2.hs
+++ b/testsuite/tests/patsyn/should_fail/T9161-2.hs
@@ -1,6 +1,8 @@
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE DataKinds, KindSignatures, PolyKinds #-}
 
+module Bug where
+
 pattern PATTERN = ()
 
 data Proxy (tag :: k) (a :: *)
diff --git a/testsuite/tests/patsyn/should_fail/T9161-2.stderr b/testsuite/tests/patsyn/should_fail/T9161-2.stderr
index cc429313aa..71f7cbe257 100644
--- a/testsuite/tests/patsyn/should_fail/T9161-2.stderr
+++ b/testsuite/tests/patsyn/should_fail/T9161-2.stderr
@@ -1,5 +1,5 @@
 
-T9161-2.hs:8:20: error:
+T9161-2.hs:10:20: error:
     • Pattern synonym ‘PATTERN’ cannot be used here
         (pattern synonyms cannot be promoted)
     • In the first argument of ‘Proxy’, namely ‘PATTERN’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail212.stderr b/testsuite/tests/typecheck/should_fail/tcfail212.stderr
index ad5985e63a..011a3772ef 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail212.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail212.stderr
@@ -16,25 +16,3 @@ tcfail212.hs:13:7: error:
 tcfail212.hs:13:13: error:
     • Expecting a lifted type, but ‘Int#’ is unlifted
     • In the type signature: g :: (Int#, Int#)
-
-tcfail212.hs:14:6: error:
-    • Couldn't match a lifted type with an unlifted type
-      When matching types
-        a :: *
-        Int# :: TYPE 'IntRep
-    • In the expression: 1#
-      In the expression: (1#, 2#)
-      In an equation for ‘g’: g = (1#, 2#)
-    • Relevant bindings include
-        g :: (a, b) (bound at tcfail212.hs:14:1)
-
-tcfail212.hs:14:10: error:
-    • Couldn't match a lifted type with an unlifted type
-      When matching types
-        b :: *
-        Int# :: TYPE 'IntRep
-    • In the expression: 2#
-      In the expression: (1#, 2#)
-      In an equation for ‘g’: g = (1#, 2#)
-    • Relevant bindings include
-        g :: (a, b) (bound at tcfail212.hs:14:1)