-- | This module implements utilities for implementing generic error
-- recovery strategies in the elaborator /around/ noncooperative
-- functions (like the conversion checker). Using these functions should
-- be thought of as a fallback strategy wherever the type theory
-- prevents us from doing better; wherever possible, a domain-specific
-- solution to reconstructing a partial program where we can do more
-- checking is preferred.
--
-- In summary, the generic error recovery strategies work by catching
-- (through 'handleRecoverableError') whatever t'TypeError's are marked
-- "recoverable", which at the moment are those thrown in an environment
-- where 'envHardErrors' is 'False' (which is the default).
-- Non-recoverable errors bubble through these handlers as-is, and note
-- that the handler is not on the stack in its own recovery
-- continuation.
--
-- Some (dynamic) contexts require that thrown errors are /not/ deferred
-- through a generic strategy, even though such a handler would be
-- present on the stack when the error is thrown. For example, while we
-- /can/ ignore a conversion-checking error if the stack looks like
--
-- @
--   checkRHS ⟩ checkExpr ⟩ ... ⟩ conversionError
-- @
--
-- we should /not/ ignore the error if the stack instead looks like
--
-- @
--   solveConstraints ⟩ findInstance ⟩ checkExpr ⟩ ... ⟩ conversionError
-- @
--
-- because (in this case) the actual result of @findInstance@ depends on
-- the @checkExpr@ throwing an error but, if generic recovery is
-- allowed, @checkExpr@ would instead succeed (producing a metavariable)
-- with a warning. These contexts should be marked with a function like
-- 'withHardErrors'.

module Mikan.TypeChecking.Errors.Deferred
  -- * Errors as control flow
  ( handleRecoverableError
  , withHardErrors
  , withFencedErrors
  , withBatchedErrors
  , DeferredError
  , errClosure, errLoc, errState

  -- * Layered error handling
  -- $twoStep
  , suspendErrors
  , hardTypeError
  , softTypeError

  -- * Canned recovery strategies
  , deferredErrorTerm

  , sequenceErrors
  , sequenceErrors_
  )
  where

import Control.Monad.Error.Class
import Control.DeepSeq
import Control.Lens

import Data.Set qualified as Set
import Data.Foldable
import Data.Maybe
import Data.Char

import GHC.Generics (Generic)

import Mikan.Syntax.Position
import Mikan.Syntax.Internal
import Mikan.Syntax.Common

import Mikan.TypeChecking.Monad.Diagnostic
import Mikan.TypeChecking.Monad.MetaVars
import Mikan.TypeChecking.Monad.Debug
import Mikan.TypeChecking.Monad.Trace (MonadTrace, setCurrentRange)
import Mikan.TypeChecking.Monad.Base

import {-# SOURCE #-} Mikan.TypeChecking.MetaVars
import Mikan.TypeChecking.Warnings
import Mikan.TypeChecking.Reduce
import Mikan.TypeChecking.Pretty

import Mikan.Utils.Impossible
import Mikan.Utils.CallStack
import Mikan.Utils.Singleton
import Mikan.Utils.Monad
import Mikan.Utils.List
import Mikan.Utils.Set1 qualified as Set1

-- | A v'TypeError' that has been thrown as a 'TCErr'.
data DeferredError = DeferredError
  { DeferredError -> CallStack
_errLoc     :: !CallStack
  , DeferredError -> TCState
_errState   :: !TCState
  , DeferredError -> Closure SomeDiagnostic
_errClosure :: !(Closure SomeDiagnostic)
  }
  deriving (Int -> DeferredError -> ShowS
[DeferredError] -> ShowS
DeferredError -> String
(Int -> DeferredError -> ShowS)
-> (DeferredError -> String)
-> ([DeferredError] -> ShowS)
-> Show DeferredError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DeferredError -> ShowS
showsPrec :: Int -> DeferredError -> ShowS
$cshow :: DeferredError -> String
show :: DeferredError -> String
$cshowList :: [DeferredError] -> ShowS
showList :: [DeferredError] -> ShowS
Show, (forall x. DeferredError -> Rep DeferredError x)
-> (forall x. Rep DeferredError x -> DeferredError)
-> Generic DeferredError
forall x. Rep DeferredError x -> DeferredError
forall x. DeferredError -> Rep DeferredError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DeferredError -> Rep DeferredError x
from :: forall x. DeferredError -> Rep DeferredError x
$cto :: forall x. Rep DeferredError x -> DeferredError
to :: forall x. Rep DeferredError x -> DeferredError
Generic)

-- | The original location where the deferred error was thrown; see
-- 'tcErrLocation'.
errLoc :: Lens' DeferredError CallStack
errLoc :: Lens' DeferredError CallStack
errLoc CallStack -> f CallStack
f DeferredError
s = CallStack -> f CallStack
f (DeferredError -> CallStack
_errLoc DeferredError
s) f CallStack -> (CallStack -> DeferredError) -> f DeferredError
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \CallStack
loc -> DeferredError
s { _errLoc = loc }

-- | The 'TCSTate' where the deferred error was thrown; see
-- 'tcErrState'.
errState :: Lens' DeferredError TCState
errState :: Lens' DeferredError TCState
errState TCState -> f TCState
f DeferredError
s = TCState -> f TCState
f (DeferredError -> TCState
_errState DeferredError
s) f TCState -> (TCState -> DeferredError) -> f DeferredError
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \TCState
loc -> DeferredError
s { _errState = loc }

-- | The actual diagnostic behind a deferred error, in its lexical
-- context; see 'tcErrClosErr'.
errClosure :: Lens' DeferredError (Closure SomeDiagnostic)
errClosure :: Lens' DeferredError (Closure SomeDiagnostic)
errClosure Closure SomeDiagnostic -> f (Closure SomeDiagnostic)
f DeferredError
s = Closure SomeDiagnostic -> f (Closure SomeDiagnostic)
f (DeferredError -> Closure SomeDiagnostic
_errClosure DeferredError
s) f (Closure SomeDiagnostic)
-> (Closure SomeDiagnostic -> DeferredError) -> f DeferredError
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Closure SomeDiagnostic
loc -> DeferredError
s { _errClosure = loc }

instance LensTCEnv DeferredError where
  lensTCEnv :: Lens' DeferredError TCEnv
lensTCEnv = (Closure SomeDiagnostic -> f (Closure SomeDiagnostic))
-> DeferredError -> f DeferredError
Lens' DeferredError (Closure SomeDiagnostic)
errClosure ((Closure SomeDiagnostic -> f (Closure SomeDiagnostic))
 -> DeferredError -> f DeferredError)
-> ((TCEnv -> f TCEnv)
    -> Closure SomeDiagnostic -> f (Closure SomeDiagnostic))
-> (TCEnv -> f TCEnv)
-> DeferredError
-> f DeferredError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TCEnv -> f TCEnv)
-> Closure SomeDiagnostic -> f (Closure SomeDiagnostic)
forall a. LensTCEnv a => Lens' a TCEnv
Lens' (Closure SomeDiagnostic) TCEnv
lensTCEnv

instance NFData DeferredError

instance PrettyTCM DeferredError where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => DeferredError -> m Doc
prettyTCM (DeferredError CallStack
_ TCState
st Closure SomeDiagnostic
cl) = (TCState -> TCState) -> m Doc -> m Doc
forall a. (TCState -> TCState) -> m a -> m a
forall (m :: * -> *) a.
ReadTCState m =>
(TCState -> TCState) -> m a -> m a
withTCState (TCState -> TCState -> TCState
forall a b. a -> b -> a
const TCState
st) (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ Closure SomeDiagnostic -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *).
MonadPretty m =>
Closure SomeDiagnostic -> m Doc
prettyTCM Closure SomeDiagnostic
cl
    , Maybe (Closure Call) -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *).
MonadPretty m =>
Maybe (Closure Call) -> m Doc
prettyTCM (Closure SomeDiagnostic -> TCEnv
forall a. Closure a -> TCEnv
clEnv Closure SomeDiagnostic
cl TCEnv
-> Getting (Maybe (Closure Call)) TCEnv (Maybe (Closure Call))
-> Maybe (Closure Call)
forall s a. s -> Getting a s a -> a
^. Getting (Maybe (Closure Call)) TCEnv (Maybe (Closure Call))
Lens' TCEnv (Maybe (Closure Call))
eCall)
    ]

instance Diagnostic DeferredError where
  diagnosticReason :: DeferredError -> DiagnosticReason
diagnosticReason DeferredError
_ = DiagnosticReason
DiagError
  diagnosticString :: DeferredError -> String
diagnosticString (DeferredError CallStack
_ TCState
_ Closure{clValue :: forall a. Closure a -> a
clValue = SomeDiagnostic
v}) = SomeDiagnostic -> String
forall a. Diagnostic a => a -> String
diagnosticString SomeDiagnostic
v

instance HasRange DeferredError where
  getRange :: DeferredError -> Range
getRange DeferredError
err = DeferredError
err DeferredError -> Getting Range DeferredError Range -> Range
forall s a. s -> Getting a s a -> a
^. (TCEnv -> Const Range TCEnv)
-> DeferredError -> Const Range DeferredError
forall a. LensTCEnv a => Lens' a TCEnv
Lens' DeferredError TCEnv
lensTCEnv ((TCEnv -> Const Range TCEnv)
 -> DeferredError -> Const Range DeferredError)
-> ((Range -> Const Range Range) -> TCEnv -> Const Range TCEnv)
-> Getting Range DeferredError Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Range -> Const Range Range) -> TCEnv -> Const Range TCEnv
Lens' TCEnv Range
eRange

-- | Add the warnings corresponding to a 'DeferredError' to the TC
-- state.
warnDeferredError :: DeferredError -> TCM ()
warnDeferredError :: DeferredError -> TCM ()
warnDeferredError DeferredError
err =
  case SomeDiagnostic -> Maybe TypeError
forall a. Diagnostic a => SomeDiagnostic -> Maybe a
fromSomeDiagnostic (DeferredError
err DeferredError
-> Getting SomeDiagnostic DeferredError SomeDiagnostic
-> SomeDiagnostic
forall s a. s -> Getting a s a -> a
^. (Closure SomeDiagnostic
 -> Const SomeDiagnostic (Closure SomeDiagnostic))
-> DeferredError -> Const SomeDiagnostic DeferredError
Lens' DeferredError (Closure SomeDiagnostic)
errClosure ((Closure SomeDiagnostic
  -> Const SomeDiagnostic (Closure SomeDiagnostic))
 -> DeferredError -> Const SomeDiagnostic DeferredError)
-> ((SomeDiagnostic -> Const SomeDiagnostic SomeDiagnostic)
    -> Closure SomeDiagnostic
    -> Const SomeDiagnostic (Closure SomeDiagnostic))
-> Getting SomeDiagnostic DeferredError SomeDiagnostic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Closure SomeDiagnostic -> SomeDiagnostic)
-> (SomeDiagnostic -> Const SomeDiagnostic SomeDiagnostic)
-> Closure SomeDiagnostic
-> Const SomeDiagnostic (Closure SomeDiagnostic)
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to Closure SomeDiagnostic -> SomeDiagnostic
forall a. Closure a -> a
clValue) of
    -- if the deferred error was already a bag of warnings, we can just
    -- unpack that into the TC state.
    Just (NonFatalErrors Set1 TCWarning
ws) -> ASetter' TCState (Set TCWarning)
-> (Set TCWarning -> Set TCWarning) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
modifyingTC ASetter' TCState (Set TCWarning)
Lens' TCState (Set TCWarning)
stTCWarnings ((Set TCWarning -> Set TCWarning) -> TCM ())
-> (Set TCWarning -> Set TCWarning) -> TCM ()
forall a b. (a -> b) -> a -> b
$
      Set TCWarning -> Set TCWarning -> Set TCWarning
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set1 TCWarning -> Set TCWarning
forall a. NESet a -> Set a
Set1.toSet Set1 TCWarning
ws)

    -- drop the call from the environment when adding the warning, to
    -- prevent warning' from printing it in a duplicated environment.
    --
    -- the call in the error closure refers to the checkpoints as they
    -- exist in the error's saved TC state, not in the current TC state.
    -- this is handled by the PrettyTCM DeferredError instance.
    Maybe TypeError
_ -> Lens' TCEnv (Maybe (Closure Call))
-> (Maybe (Closure Call) -> Maybe (Closure Call))
-> TCM ()
-> TCM ()
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC (Maybe (Closure Call) -> f (Maybe (Closure Call)))
-> TCEnv -> f TCEnv
Lens' TCEnv (Maybe (Closure Call))
eCall (Maybe (Closure Call)
-> Maybe (Closure Call) -> Maybe (Closure Call)
forall a b. a -> b -> a
const Maybe (Closure Call)
forall a. Maybe a
Nothing) do
      CallStack -> List1 (Ranged DeferredError) -> TCM ()
forall (m :: * -> *) e.
(MonadWarning m, Diagnostic e) =>
CallStack -> List1 (Ranged e) -> m ()
warnings' (DeferredError
err DeferredError
-> Getting CallStack DeferredError CallStack -> CallStack
forall s a. s -> Getting a s a -> a
^. Getting CallStack DeferredError CallStack
Lens' DeferredError CallStack
errLoc) (List1 (Ranged DeferredError) -> TCM ())
-> List1 (Ranged DeferredError) -> TCM ()
forall a b. (a -> b) -> a -> b
$ Ranged DeferredError -> List1 (Ranged DeferredError)
forall el coll. Singleton el coll => el -> coll
singleton (Ranged DeferredError -> List1 (Ranged DeferredError))
-> Ranged DeferredError -> List1 (Ranged DeferredError)
forall a b. (a -> b) -> a -> b
$ DeferredError -> Ranged DeferredError
forall a. HasRange a => a -> Ranged a
itsRange DeferredError
err

-- | Handle any /recoverable/ errors thrown by the continuation with the
-- given function.
--
-- The dynamic behaviour of this function can be thought of as obeying
-- the equations
--
-- @
--   'handleRecoverableError' h ('softTypeError' e) = h e
--   'handleRecoverableError' h ('hardTypeError' e) = 'hardTypeError' e
-- @
handleRecoverableError
  :: MonadError TCErr m
  => (DeferredError -> m a)
  -> m a
  -> m a
handleRecoverableError :: forall (m :: * -> *) a.
MonadError TCErr m =>
(DeferredError -> m a) -> m a -> m a
handleRecoverableError DeferredError -> m a
recover m a
cont = m a
cont m a -> (TCErr -> m a) -> m a
forall a. m a -> (TCErr -> m a) -> m a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
  TypeError CallStack
loc TCState
st Closure SomeDiagnostic
cl
    | Bool -> Bool
not (Closure SomeDiagnostic -> TCEnv
forall a. Closure a -> TCEnv
clEnv Closure SomeDiagnostic
cl TCEnv -> Getting Bool TCEnv Bool -> Bool
forall s a. s -> Getting a s a -> a
^. Getting Bool TCEnv Bool
Lens' TCEnv Bool
eHardErrors) -> DeferredError -> m a
recover (DeferredError -> m a) -> DeferredError -> m a
forall a b. (a -> b) -> a -> b
$ CallStack -> TCState -> Closure SomeDiagnostic -> DeferredError
DeferredError CallStack
loc TCState
st Closure SomeDiagnostic
cl
  TCErr
err -> TCErr -> m a
forall a. TCErr -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
{-# INLINE handleRecoverableError #-}

-- | Run a type-checking computation marking all of its thrown type
-- errors unrecoverable. This can be used to skip
-- 'handleRecoverableError' handlers that appear below 'withHardErrors'
-- in the call stack.
--
-- Letting @E[_]@ stand for an arbitrary evaluation context built from
-- the functions in this module, the dynamic behaviour of this function
-- can be thought of as obeying the equation
--
-- @
--   'withHardErrors' E[ 'typeError' err ] = 'hardTypeError' err
-- @
--
-- In particular, any 'handleRecoverableError's installed during
-- execution of the continuation are skipped:
--
-- @
--   'withHardErrors' ('handleRecoverableError' _ ('typeError' e)) = 'hardTypeError' e
-- @
withHardErrors :: MonadTCEnv m => m a -> m a
withHardErrors :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
withHardErrors = Lens' TCEnv Bool -> (Bool -> Bool) -> m a -> m a
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eHardErrors (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True)
{-# INLINE withHardErrors #-}

debugErrs :: MonadDebug m => String -> m a -> m a
debugErrs :: forall (m :: * -> *) a. MonadDebug m => String -> m a -> m a
debugErrs String
s m a
k = String -> Int -> String -> m a -> m a
forall a. String -> Int -> String -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> String -> m a -> m a
verboseBracket String
"tc.term.recover" Int
60 String
s do
  String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.term.recover" Int
60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"hardErrors =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Bool -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Bool -> TCMT IO Doc) -> TCMT IO Bool -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Lens' TCEnv Bool -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eHardErrors)
  m a
k

-- | Run a type-checking computation under 'withHardErrors', but mark
-- any escaping errors with the ambient recovery flag.
--
-- Letting @E[_]@ stand for an arbitrary evaluation context built from
-- the functions in this module, the dynamic behaviour of this function
-- can be thought of as obeying the equations
--
-- @
--   'withFencedErrors' E[ 'softTypeError' err ] = 'typeError' err
--   'withFencedErrors' E[ 'hardTypeError' err ] = 'typeError' err
-- @
--
-- In particular, if 'withFencedErrors' is placed in a context where
-- errors are recoverable, any /unrecoverable/ errors thrown by the
-- continuation will be made /recoverable/ when re-thrown by
-- 'withFencedErrors' (if the context does not otherwise demand errors
-- are made unrecoverable).
withFencedErrors :: (MonadTCEnv m, MonadError TCErr m, MonadDebug m) => m a -> m a
withFencedErrors :: forall (m :: * -> *) a.
(MonadTCEnv m, MonadError TCErr m, MonadDebug m) =>
m a -> m a
withFencedErrors m a
cont = String -> m a -> m a
forall (m :: * -> *) a. MonadDebug m => String -> m a -> m a
debugErrs String
"withFencedErrors" do
  !hardErrors <- Lens' TCEnv Bool -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eHardErrors
  withHardErrors cont `catchError` \case
    TypeError CallStack
loc TCState
st Closure SomeDiagnostic
cl -> TCErr -> m a
forall a. TCErr -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCErr -> m a) -> TCErr -> m a
forall a b. (a -> b) -> a -> b
$ CallStack -> TCState -> Closure SomeDiagnostic -> TCErr
TypeError CallStack
loc TCState
st
      (Closure SomeDiagnostic -> TCErr)
-> Closure SomeDiagnostic -> TCErr
forall a b. (a -> b) -> a -> b
$! Closure SomeDiagnostic
cl Closure SomeDiagnostic
-> (Closure SomeDiagnostic -> Closure SomeDiagnostic)
-> Closure SomeDiagnostic
forall a b. a -> (a -> b) -> b
& (TCEnv -> Identity TCEnv)
-> Closure SomeDiagnostic -> Identity (Closure SomeDiagnostic)
forall a. LensTCEnv a => Lens' a TCEnv
Lens' (Closure SomeDiagnostic) TCEnv
lensTCEnv ((TCEnv -> Identity TCEnv)
 -> Closure SomeDiagnostic -> Identity (Closure SomeDiagnostic))
-> ((Bool -> Identity Bool) -> TCEnv -> Identity TCEnv)
-> (Bool -> Identity Bool)
-> Closure SomeDiagnostic
-> Identity (Closure SomeDiagnostic)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> Identity Bool) -> TCEnv -> Identity TCEnv
Lens' TCEnv Bool
eHardErrors ((Bool -> Identity Bool)
 -> Closure SomeDiagnostic -> Identity (Closure SomeDiagnostic))
-> Bool -> Closure SomeDiagnostic -> Closure SomeDiagnostic
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Bool
hardErrors
    TCErr
err -> TCErr -> m a
forall a. TCErr -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
{-# SPECIALIZE withFencedErrors :: TCM a -> TCM a #-}

-- | Group any errors deferred during execution of the continuation into
-- a single 'NonFatalErrors', raised with the ambient error recovery
-- flag.
--
-- This includes any errors deferred by a generic strategy within the
-- continuation.
withBatchedErrors
  :: (MonadTrace m, MonadTCState m, MonadError TCErr m, MonadDebug m)
  => m a
  -> m a
withBatchedErrors :: forall (m :: * -> *) a.
(MonadTrace m, MonadTCState m, MonadError TCErr m, MonadDebug m) =>
m a -> m a
withBatchedErrors m a
cont = String -> m a -> m a
forall (m :: * -> *) a. MonadDebug m => String -> m a -> m a
debugErrs String
"withBatchedErrors" do
  (res, warns) <- m a -> m (a, Set TCWarning)
forall (m :: * -> *) a.
(ReadTCState m, MonadTCState m) =>
m a -> m (a, Set TCWarning)
warningsAddedBy m a
cont

  let
    isError TCWarning' a
warn = case a -> DiagnosticReason
forall a. Diagnostic a => a -> DiagnosticReason
diagnosticReason (TCWarning' a -> a
forall diag. TCWarning' diag -> diag
tcWarning TCWarning' a
warn) of
      DiagError{} -> Bool
True
      DiagnosticReason
_           -> Bool
False

  res <$ Set1.unlessNull (Set.filter isError warns) \Set1 TCWarning
errs -> do
    String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.term.recover" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Set String -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ((TCWarning -> String) -> Set TCWarning -> Set String
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (ShowS
forall a. Show a => a -> String
show ShowS -> (TCWarning -> String) -> TCWarning -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> String
forall diag. TCWarning' diag -> String
tcWarningString) ((TCWarning -> Bool) -> Set TCWarning -> Set TCWarning
forall a. (a -> Bool) -> Set a -> Set a
Set.filter TCWarning -> Bool
forall {a}. Diagnostic a => TCWarning' a -> Bool
isError Set TCWarning
warns))
    TCWarning -> m () -> m ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (Set1 TCWarning -> TCWarning
forall a. NESet a -> a
Set1.findMin Set1 TCWarning
errs) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
      TypeError -> m ()
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Set1 TCWarning -> TypeError
NonFatalErrors Set1 TCWarning
errs
{-# SPECIALIZE withBatchedErrors :: TCM a -> TCM a #-}

-- $twoStep
--
-- One pattern for locally making use of errors as control flow is using
-- a transformer like @'Control.Monad.Except.ExceptT' 'TCErr' 'TCM'@,
-- where we can thrown an error both in the underlying @'TCM'@ (where it
-- will be subject to recovery by any ambient @'catchError' \@'TCM'@) or
-- in directly in the transformed monad (which will be caught locally).
--
-- The functions 'suspendErrors', 'softTypeError' and 'hardTypeError'
-- mediate this interaction. Importantly, they can all be used directly
-- at @'TCM'@, where the error will be thrown normally.

-- | Catch /any/ errors thrown during execution of the continuation and
-- re-raise them in the monad @m@ instead.
--
-- This applies equally to recoverable and unrecoverable errors.
suspendErrors :: (MonadTCM m, MonadError TCErr m) => TCM a -> m a
suspendErrors :: forall (m :: * -> *) a.
(MonadTCM m, MonadError TCErr m) =>
TCM a -> m a
suspendErrors TCM a
f = do
  ok <- TCM (Either TCErr a) -> m (Either TCErr a)
forall a. TCM a -> m a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Either TCErr a) -> m (Either TCErr a))
-> TCM (Either TCErr a) -> m (Either TCErr a)
forall a b. (a -> b) -> a -> b
$ (a -> Either TCErr a
forall a b. b -> Either a b
Right (a -> Either TCErr a) -> TCM a -> TCM (Either TCErr a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM a
f) TCM (Either TCErr a)
-> (TCErr -> TCM (Either TCErr a)) -> TCM (Either TCErr a)
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` (Either TCErr a -> TCM (Either TCErr a)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either TCErr a -> TCM (Either TCErr a))
-> (TCErr -> Either TCErr a) -> TCErr -> TCM (Either TCErr a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCErr -> Either TCErr a
forall a b. a -> Either a b
Left)
  either throwError return ok
{-# INLINE suspendErrors #-}

-- | Throw a /recoverable/ error, regardless of any surrounding
-- 'withHardErrors'.
--
-- If @m@ is a monad supporting its own error handling, the error is
-- thrown there, instead of in the 'TCM'.
softTypeError :: (HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m, Diagnostic e) => e -> m a
softTypeError :: forall (m :: * -> *) e a.
(HasCallStack, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 Diagnostic e) =>
e -> m a
softTypeError e
err = (CallStack -> m a) -> m a
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack \CallStack
loc -> Lens' TCEnv Bool -> (Bool -> Bool) -> m a -> m a
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eHardErrors (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True) (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$
  TCErr -> m a
forall a. TCErr -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCErr -> m a) -> m TCErr -> m a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< CallStack -> e -> m TCErr
forall (m :: * -> *) e a.
(MonadTCError m, Diagnostic e) =>
CallStack -> e -> m a
typeError' CallStack
loc e
err
{-# INLINE softTypeError #-}

-- | Throw an /unrecoverable/ error.
--
-- Regardless of whether @m@ is a monad implementing its own error
-- handling, the error is thrown in the 'TCM'.
hardTypeError :: (HasCallStack, MonadTCM m, Diagnostic e) => e -> m a
hardTypeError :: forall (m :: * -> *) e a.
(HasCallStack, MonadTCM m, Diagnostic e) =>
e -> m a
hardTypeError = (CallStack -> e -> m a) -> e -> m a
forall b. HasCallStack => (CallStack -> b) -> b
withCallerCallStack \CallStack
loc -> m a -> m a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
withHardErrors (m a -> m a) -> (e -> m a) -> e -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCM a -> m a
forall a. TCM a -> m a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM a -> m a) -> (e -> TCM a) -> e -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> e -> TCM a
forall (m :: * -> *) e a.
(MonadTCError m, Diagnostic e) =>
CallStack -> e -> m a
typeError' CallStack
loc
{-# INLINE hardTypeError #-}

-- | Recover from type-checking errors in a computation by recording the
-- diagnostic as a warning and returning a new metavariable.
deferredErrorTerm
  :: Comparison -- ^ How to check the result type.
  -> Type       -- ^ The expected type.
  -> DeferredError
  -> TCM Term
deferredErrorTerm :: Comparison -> Type -> DeferredError -> TCM Term
deferredErrorTerm Comparison
cmp Type
wanted DeferredError
err = do
  let
    errorMeta :: MetaId -> TCM Bool
    errorMeta :: MetaId -> TCMT IO Bool
errorMeta MetaId
mid = MetaId -> TCMT IO (Maybe (Either RemoteMetaVariable MetaVariable))
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
lookupMeta MetaId
mid TCMT IO (Maybe (Either RemoteMetaVariable MetaVariable))
-> (Maybe (Either RemoteMetaVariable MetaVariable) -> Bool)
-> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
      Maybe (Either RemoteMetaVariable MetaVariable)
Nothing         -> Bool
False
      Just Left{}     -> Bool
False
      Just (Right MetaVariable
mv) -> MetaVariable -> Bool
mvError MetaVariable
mv

  ty <- Type -> TCMT IO (Blocked Type)
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Type
wanted
  should <- case ty of
    NotBlocked{}      -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
    Blocked Blocker
blocker Type
_ -> (MetaId -> TCMT IO Bool) -> Set MetaId -> TCMT IO Bool
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Monad m) =>
(a -> m Bool) -> f a -> m Bool
allM ((Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bool -> Bool
not (TCMT IO Bool -> TCMT IO Bool)
-> (MetaId -> TCMT IO Bool) -> MetaId -> TCMT IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> TCMT IO Bool
errorMeta) (Blocker -> Set MetaId
allBlockingMetas Blocker
blocker)

  reportSDoc "tc.term.recover" 30 $ vcat
    [ "recovering from type error:"
    , nest 2 (prettyTCM err)
    , "expected type:" <+> pretty ty
    , "will warn?" <+> pretty should
    , "warnings of error:" $$ nest 2 (vcat $ toList (err ^. errState . stTCWarnings) <&> pure . tcWarningDoc)
    ]

  -- add the new warning, if we think it will be useful.
  when should $ warnDeferredError err

  -- then, inherit any error-warnings present in the error's state,
  -- since they may be other deferred errors.
  traverse_ (addWarning True) $ nonFatalErrors $ classifyWarnings $ err ^. errState . stTCWarnings

  (mid, tm) <- newValueMeta DontRunMetaOccursCheck cmp wanted
  tm <$ updateMetaVar mid \MetaVariable
mv -> MetaVariable
mv
    { mvError  = True
    , mvFrozen = Frozen
    }

-- | Execute a 'Traversable' container of 'TCM' actions, allowing each
-- action to succeed or fail individually, but succeeding only if
-- /every/ computation succeeds.
--
-- Here, "failure" is as per 'withBatchedError's: recoverable errors in
-- each continuation are turned into warnings, and the overall
-- computation fails if it contributes any 'DiagError's to the warning
-- state.
sequenceErrors :: Traversable f => f (TCM a) -> TCM (f a)
sequenceErrors :: forall (f :: * -> *) a. Traversable f => f (TCM a) -> TCM (f a)
sequenceErrors =
    (f (Maybe a) -> f a) -> TCMT IO (f (Maybe a)) -> TCMT IO (f a)
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Maybe a -> a) -> f (Maybe a) -> f a
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe a
forall a. HasCallStack => a
__IMPOSSIBLE__))
  (TCMT IO (f (Maybe a)) -> TCMT IO (f a))
-> (f (TCM a) -> TCMT IO (f (Maybe a)))
-> f (TCM a)
-> TCMT IO (f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCMT IO (f (Maybe a)) -> TCMT IO (f (Maybe a))
forall (m :: * -> *) a.
(MonadTrace m, MonadTCState m, MonadError TCErr m, MonadDebug m) =>
m a -> m a
withBatchedErrors
  (TCMT IO (f (Maybe a)) -> TCMT IO (f (Maybe a)))
-> (f (TCM a) -> TCMT IO (f (Maybe a)))
-> f (TCM a)
-> TCMT IO (f (Maybe a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TCM a -> TCMT IO (Maybe a)) -> f (TCM a) -> TCMT IO (f (Maybe a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse ((DeferredError -> TCMT IO (Maybe a))
-> TCMT IO (Maybe a) -> TCMT IO (Maybe a)
forall (m :: * -> *) a.
MonadError TCErr m =>
(DeferredError -> m a) -> m a -> m a
handleRecoverableError ((Maybe a
forall a. Maybe a
Nothing Maybe a -> TCM () -> TCMT IO (Maybe a)
forall a b. a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) (TCM () -> TCMT IO (Maybe a))
-> (DeferredError -> TCM ()) -> DeferredError -> TCMT IO (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeferredError -> TCM ()
warnDeferredError) (TCMT IO (Maybe a) -> TCMT IO (Maybe a))
-> (TCM a -> TCMT IO (Maybe a)) -> TCM a -> TCMT IO (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Maybe a) -> TCM a -> TCMT IO (Maybe a)
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Maybe a
forall a. a -> Maybe a
Just)

-- | As 'sequenceErrors', but discarding the result.
sequenceErrors_ :: Traversable f => f (TCM a) -> TCM ()
sequenceErrors_ :: forall (f :: * -> *) a. Traversable f => f (TCM a) -> TCM ()
sequenceErrors_ = TCMT IO (f a) -> TCM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (TCMT IO (f a) -> TCM ())
-> (f (TCM a) -> TCMT IO (f a)) -> f (TCM a) -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (TCM a) -> TCMT IO (f a)
forall (f :: * -> *) a. Traversable f => f (TCM a) -> TCM (f a)
sequenceErrors