Improve error recovery in the typechecker
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 13 Mar 2019 11:15:20 +0000 (11:15 +0000)
committerMarge Bot <ben+marge-bot@smart-cactus.org>
Sat, 16 Mar 2019 12:08:25 +0000 (08:08 -0400)
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:
compiler/ghci/RtClosureInspect.hs
compiler/typecheck/TcBackpack.hs
compiler/typecheck/TcBinds.hs
compiler/typecheck/TcRnExports.hs
compiler/typecheck/TcRnMonad.hs
compiler/typecheck/TcSigs.hs
compiler/typecheck/TcSimplify.hs
compiler/typecheck/TcUnify.hs
testsuite/tests/dependent/should_fail/BadTelescope2.hs
testsuite/tests/dependent/should_fail/BadTelescope2.stderr
testsuite/tests/dependent/should_fail/BadTelescope5.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/BadTelescope5.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T15743c.stderr
testsuite/tests/dependent/should_fail/T16418.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T16418.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/all.T
testsuite/tests/patsyn/should_fail/T9161-1.hs
testsuite/tests/patsyn/should_fail/T9161-1.stderr
testsuite/tests/patsyn/should_fail/T9161-2.hs
testsuite/tests/patsyn/should_fail/T9161-2.stderr
testsuite/tests/typecheck/should_fail/tcfail212.stderr

index 436b756..c64ffa9 100644 (file)
@@ -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
index f361192..7fffcd1 100644 (file)
@@ -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
index b4803fc..9cdc939 100644 (file)
@@ -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
index f584a7f..e4009e6 100644 (file)
@@ -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
index 951cc7a..3997f2d 100644 (file)
@@ -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
index d2e4a62..5d8d92a 100644 (file)
@@ -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!
 -}
 
 {- *********************************************************************
index cd9d858..c0fc4e8 100644 (file)
@@ -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
index 29aff60..d8b1edf 100644 (file)
@@ -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
index e33fdf1..73f6967 100644 (file)
@@ -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
index a8c4b68..3637dec 100644 (file)
@@ -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 (file)
index 0000000..ce2368b
--- /dev/null
@@ -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 (file)
index 0000000..da79678
--- /dev/null
@@ -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
index 8e3ad50..4cb1c0c 100644 (file)
@@ -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 (file)
index 0000000..8097e3c
--- /dev/null
@@ -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 (file)
index 0000000..fa2263a
--- /dev/null
@@ -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 -> ()
index 1f75a85..1e6ab40 100644 (file)
@@ -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, [''])
index c14eb54..32a6f9d 100644 (file)
@@ -1,6 +1,8 @@
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE DataKinds #-}
 
+module Bug where
+
 pattern PATTERN = ()
 
 wrongLift :: PATTERN
index fff6efe..39faffd 100644 (file)
@@ -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
index 941d23e..ccdfa1f 100644 (file)
@@ -1,6 +1,8 @@
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE DataKinds, KindSignatures, PolyKinds #-}
 
+module Bug where
+
 pattern PATTERN = ()
 
 data Proxy (tag :: k) (a :: *)
index cc42931..71f7cbe 100644 (file)
@@ -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’
index ad5985e..011a377 100644 (file)
@@ -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)