    module Agda.TypeChecking.Monad.Trace where

    import Prelude hiding (null)

    import Control.Monad.Except
    import Control.Monad.Reader
    import Control.Monad.State
    import Control.Monad.Trans.Identity
    import Control.Monad.Writer

    import qualified Data.Set as Set

    import Agda.Syntax.Position
    import qualified Agda.Syntax.Position as P

    import Agda.Interaction.Response
    import Agda.Interaction.Highlighting.Precise
    import Agda.Interaction.Highlighting.Range (rToR, minus)

    import Agda.TypeChecking.Monad.Base
      hiding (ModuleInfo, MetaInfo, Primitive, Constructor, Record, Function, Datatype)
    import Agda.TypeChecking.Monad.Debug
    import Agda.TypeChecking.Monad.State

    import Agda.Utils.Function

    import qualified Agda.Utils.Maybe.Strict as Strict
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Pretty (prettyShow)

    ---------------------------------------------------------------------------
    -- * Trace
    ---------------------------------------------------------------------------

    interestingCall :: Call -> Bool
    interestingCall :: Call -> Bool
    interestingCall = \case
        InferVar{}              -> Bool
    False
        InferDef{}              -> Bool
    False
        CheckArguments Range
    _ [] Type
    _ Maybe Type
    _ -> Bool
    False
        SetRange{}              -> Bool
    False
        NoHighlighting{}        -> Bool
    False
        -- Andreas, 2019-08-07, expanded catch-all pattern.
        -- The previous presence of a catch-all raises the following question:
        -- are all of the following really interesting?
        CheckClause{}             -> Bool
    True
        CheckLHS{}                -> Bool
    True
        CheckPattern{}            -> Bool
    True
        CheckPatternLinearityType{}  -> Bool
    True
        CheckPatternLinearityValue{} -> Bool
    True
        CheckLetBinding{}         -> Bool
    True
        InferExpr{}               -> Bool
    True
        CheckExprCall{}           -> Bool
    True
        CheckDotPattern{}         -> Bool
    True
        IsTypeCall{}              -> Bool
    True
        IsType_{}                 -> Bool
    True
        CheckArguments{}          -> Bool
    True
        CheckMetaSolution{}       -> Bool
    True
        CheckTargetType{}         -> Bool
    True
        CheckDataDef{}            -> Bool
    True
        CheckRecDef{}             -> Bool
    True
        CheckConstructor{}        -> Bool
    True
        CheckConstructorFitsIn{}  -> Bool
    True
        CheckFunDefCall{}         -> Bool
    True
        CheckPragma{}             -> Bool
    True
        CheckPrimitive{}          -> Bool
    True
        CheckIsEmpty{}            -> Bool
    True
        CheckConfluence{}         -> Bool
    True
        CheckWithFunctionType{}   -> Bool
    True
        CheckSectionApplication{} -> Bool
    True
        CheckNamedWhere{}         -> Bool
    True
        ScopeCheckExpr{}          -> Bool
    True
        ScopeCheckDeclaration{}   -> Bool
    True
        ScopeCheckLHS{}           -> Bool
    True
        CheckProjection{}         -> Bool
    True
        ModuleContents{}          -> Bool
    True

    class (MonadTCEnv m, ReadTCState m) => MonadTrace m where

      -- | Record a function call in the trace.
      traceCall :: Call -> m a -> m a
      traceCall Call
    call m a
    m = do
        Closure Call
    cl <- Call -> m (Closure Call)
    forall (m :: * -> *) a.
    (MonadTCEnv m, ReadTCState m) =>
    a -> m (Closure a)
    buildClosure Call
    call
        Closure Call -> m a -> m a
    forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
    traceClosureCall Closure Call
    cl m a
    m

      traceCallM :: m Call -> m a -> m a
      traceCallM m Call
    call m a
    m = (Call -> m a -> m a) -> m a -> Call -> m a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Call -> m a -> m a
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall m a
    m (Call -> m a) -> m Call -> m a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m Call
    call

      -- | Reset 'envCall' to previous value in the continuation.
      --
      -- Caveat: if the last 'traceCall' did not set an 'interestingCall',
      -- for example, only set the 'Range' with 'SetRange',
      -- we will revert to the last interesting call.
      traceCallCPS :: Call -> ((a -> m b) -> m b) -> ((a -> m b) -> m b)
      traceCallCPS Call
    call (a -> m b) -> m b
    k a -> m b
    ret = do
        Maybe (Closure Call)
    mcall <- (TCEnv -> Maybe (Closure Call)) -> m (Maybe (Closure Call))
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Maybe (Closure Call)
    envCall
        Call -> m b -> m b
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall Call
    call (m b -> m b) -> m b -> m b
    forall a b. (a -> b) -> a -> b
    $ (a -> m b) -> m b
    k ((a -> m b) -> m b) -> (a -> m b) -> m b
    forall a b. (a -> b) -> a -> b
    $ \ a
    a -> do
          (m b -> m b)
    -> (Closure Call -> m b -> m b)
    -> Maybe (Closure Call)
    -> m b
    -> m b
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe m b -> m b
    forall a. a -> a
    id Closure Call -> m b -> m b
    forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
    traceClosureCall Maybe (Closure Call)
    mcall (m b -> m b) -> m b -> m b
    forall a b. (a -> b) -> a -> b
    $ a -> m b
    ret a
    a

      traceClosureCall :: Closure Call -> m a -> m a

      -- | Lispify and print the given highlighting information.
      printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()

      default printHighlightingInfo
        :: (MonadTrans t, MonadTrace n, t n ~ m)
        => RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
      printHighlightingInfo RemoveTokenBasedHighlighting
    r HighlightingInfo
    i = n () -> t n ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (n () -> t n ()) -> n () -> t n ()
    forall a b. (a -> b) -> a -> b
    $ RemoveTokenBasedHighlighting -> HighlightingInfo -> n ()
    forall (m :: * -> *).
    MonadTrace m =>
    RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
    printHighlightingInfo RemoveTokenBasedHighlighting
    r HighlightingInfo
    i

    instance MonadTrace m => MonadTrace (IdentityT m) where
      traceClosureCall :: forall a. Closure Call -> IdentityT m a -> IdentityT m a
    traceClosureCall Closure Call
    c IdentityT m a
    f = m a -> IdentityT m a
    forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
    IdentityT (m a -> IdentityT m a) -> m a -> IdentityT m a
    forall a b. (a -> b) -> a -> b
    $ Closure Call -> m a -> m a
    forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
    traceClosureCall Closure Call
    c (m a -> m a) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ IdentityT m a -> m a
    forall {k} (f :: k -> *) (a :: k). IdentityT f a -> f a
    runIdentityT IdentityT m a
    f

    instance MonadTrace m => MonadTrace (ReaderT r m) where
      traceClosureCall :: forall a. Closure Call -> ReaderT r m a -> ReaderT r m a
    traceClosureCall Closure Call
    c ReaderT r m a
    f = (r -> m a) -> ReaderT r m a
    forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
    ReaderT ((r -> m a) -> ReaderT r m a) -> (r -> m a) -> ReaderT r m a
    forall a b. (a -> b) -> a -> b
    $ \r
    r -> Closure Call -> m a -> m a
    forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
    traceClosureCall Closure Call
    c (m a -> m a) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ ReaderT r m a -> r -> m a
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT ReaderT r m a
    f r
    r

    instance MonadTrace m => MonadTrace (StateT s m) where
      traceClosureCall :: forall a. Closure Call -> StateT s m a -> StateT s m a
    traceClosureCall Closure Call
    c StateT s m a
    f = (s -> m (a, s)) -> StateT s m a
    forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
    StateT (Closure Call -> m (a, s) -> m (a, s)
    forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
    traceClosureCall Closure Call
    c (m (a, s) -> m (a, s)) -> (s -> m (a, s)) -> s -> m (a, s)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . StateT s m a -> s -> m (a, s)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT StateT s m a
    f)

    instance (MonadTrace m, Monoid w) => MonadTrace (WriterT w m) where
      traceClosureCall :: forall a. Closure Call -> WriterT w m a -> WriterT w m a
    traceClosureCall Closure Call
    c WriterT w m a
    f = m (a, w) -> WriterT w m a
    forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
    WriterT (m (a, w) -> WriterT w m a) -> m (a, w) -> WriterT w m a
    forall a b. (a -> b) -> a -> b
    $ Closure Call -> m (a, w) -> m (a, w)
    forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
    traceClosureCall Closure Call
    c (m (a, w) -> m (a, w)) -> m (a, w) -> m (a, w)
    forall a b. (a -> b) -> a -> b
    $ WriterT w m a -> m (a, w)
    forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
    runWriterT WriterT w m a
    f

    instance MonadTrace m => MonadTrace (ExceptT e m) where
      traceClosureCall :: forall a. Closure Call -> ExceptT e m a -> ExceptT e m a
    traceClosureCall Closure Call
    c ExceptT e m a
    f = m (Either e a) -> ExceptT e m a
    forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
    ExceptT (m (Either e a) -> ExceptT e m a)
    -> m (Either e a) -> ExceptT e m a
    forall a b. (a -> b) -> a -> b
    $ Closure Call -> m (Either e a) -> m (Either e a)
    forall (m :: * -> *) a. MonadTrace m => Closure Call -> m a -> m a
    traceClosureCall Closure Call
    c (m (Either e a) -> m (Either e a))
    -> m (Either e a) -> m (Either e a)
    forall a b. (a -> b) -> a -> b
    $ ExceptT e m a -> m (Either e a)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT ExceptT e m a
    f

    instance MonadTrace TCM where
      traceClosureCall :: forall a. Closure Call -> TCM a -> TCM a
    traceClosureCall Closure Call
    cl TCM a
    m = do
        -- Andreas, 2016-09-13 issue #2177
        -- Since the fix of #2092 we may report an error outside the current file.
        -- (For instance, if we import a module which then happens to have the
        -- wrong name.)
        -- Thus, we no longer crash, but just report the alien range.
        -- -- Andreas, 2015-02-09 Make sure we do not set a range
        -- -- outside the current file
        [Char] -> VerboseLevel -> TCM () -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> VerboseLevel -> m () -> m ()
    verboseS [Char]
    "check.ranges" VerboseLevel
    90 (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          Maybe AbsolutePath -> (AbsolutePath -> TCM ()) -> TCM ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    Strict.whenJust (Range -> Maybe AbsolutePath
    rangeFile Range
    callRange) ((AbsolutePath -> TCM ()) -> TCM ())
    -> (AbsolutePath -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \AbsolutePath
    f -> do
            Maybe AbsolutePath
    currentFile <- (TCEnv -> Maybe AbsolutePath) -> TCMT IO (Maybe AbsolutePath)
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Maybe AbsolutePath
    envCurrentPath
            Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Maybe AbsolutePath
    currentFile Maybe AbsolutePath -> Maybe AbsolutePath -> Bool
    forall a. Eq a => a -> a -> Bool
    /= AbsolutePath -> Maybe AbsolutePath
    forall a. a -> Maybe a
    Just AbsolutePath
    f) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
              [Char] -> VerboseLevel -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> VerboseLevel -> [Char] -> m ()
    reportSLn [Char]
    "check.ranges" VerboseLevel
    90 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                Call -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Call
    call [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
                [Char]
    " is setting the current range to " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Range -> [Char]
    forall a. Show a => a -> [Char]
    show Range
    callRange [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
                [Char]
    " which is outside of the current file " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Maybe AbsolutePath -> [Char]
    forall a. Show a => a -> [Char]
    show Maybe AbsolutePath
    currentFile

        -- Compute update to 'Range' and 'Call' components of 'TCEnv'.
        let withCall :: TCM a -> TCM a
    withCall = (TCEnv -> TCEnv) -> TCM a -> TCM a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> TCM a -> TCM a)
    -> (TCEnv -> TCEnv) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $ ((TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv)
    -> (TCEnv -> TCEnv) -> [TCEnv -> TCEnv] -> TCEnv -> TCEnv
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    (.) TCEnv -> TCEnv
    forall a. a -> a
    id ([TCEnv -> TCEnv] -> TCEnv -> TCEnv)
    -> [TCEnv -> TCEnv] -> TCEnv -> TCEnv
    forall a b. (a -> b) -> a -> b
    $ [[TCEnv -> TCEnv]] -> [TCEnv -> TCEnv]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[TCEnv -> TCEnv]] -> [TCEnv -> TCEnv])
    -> [[TCEnv -> TCEnv]] -> [TCEnv -> TCEnv]
    forall a b. (a -> b) -> a -> b
    $
              [ [ \TCEnv
    e -> TCEnv
    e { envCall :: Maybe (Closure Call)
    envCall = Closure Call -> Maybe (Closure Call)
    forall a. a -> Maybe a
    Just Closure Call
    cl } | Call -> Bool
    interestingCall Call
    call ]
              , [ \TCEnv
    e -> TCEnv
    e { envHighlightingRange :: Range
    envHighlightingRange = Range
    callRange }
                | Bool
    callHasRange Bool -> Bool -> Bool
    && Bool
    highlightCall
                  Bool -> Bool -> Bool
    || Bool
    isNoHighlighting
                ]
              , [ \TCEnv
    e -> TCEnv
    e { envRange :: Range
    envRange = Range
    callRange } | Bool
    callHasRange ]
              ]

        -- For interactive highlighting, also wrap computation @m@ in 'highlightAsTypeChecked':
        TCMT IO Bool -> TCM a -> TCM a -> TCM a
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifNotM (Bool -> TCMT IO Bool
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    highlightCall TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` do (HighlightingLevel
    Interactive HighlightingLevel -> HighlightingLevel -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (HighlightingLevel -> Bool)
    -> (TCEnv -> HighlightingLevel) -> TCEnv -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCEnv -> HighlightingLevel
    envHighlightingLevel (TCEnv -> Bool) -> TCMT IO TCEnv -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO TCEnv
    forall (m :: * -> *). MonadTCEnv m => m TCEnv
    askTC)
          {-then-} (TCM a -> TCM a
    withCall TCM a
    m)
          {-else-} (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $ do
            Range
    oldRange <- TCEnv -> Range
    envHighlightingRange (TCEnv -> Range) -> TCMT IO TCEnv -> TCMT IO Range
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO TCEnv
    forall (m :: * -> *). MonadTCEnv m => m TCEnv
    askTC
            Range -> Range -> TCM a -> TCM a
    forall (m :: * -> *) a.
    MonadTrace m =>
    Range -> Range -> m a -> m a
    highlightAsTypeChecked Range
    oldRange Range
    callRange (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $
              TCM a -> TCM a
    withCall TCM a
    m
        where
        call :: Call
    call = Closure Call -> Call
    forall a. Closure a -> a
    clValue Closure Call
    cl
        callRange :: Range
    callRange = Call -> Range
    forall a. HasRange a => a -> Range
    getRange Call
    call
        callHasRange :: Bool
    callHasRange = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Range -> Bool
    forall a. Null a => a -> Bool
    null Range
    callRange

        -- Should the given call trigger interactive highlighting?
        highlightCall :: Bool
    highlightCall = case Call
    call of
          CheckClause{}             -> Bool
    True
          CheckLHS{}                -> Bool
    True
          CheckPattern{}            -> Bool
    True
          CheckPatternLinearityType{}  -> Bool
    False
          CheckPatternLinearityValue{} -> Bool
    False
          CheckLetBinding{}         -> Bool
    True
          InferExpr{}               -> Bool
    True
          CheckExprCall{}           -> Bool
    True
          CheckDotPattern{}         -> Bool
    True
          IsTypeCall{}              -> Bool
    True
          IsType_{}                 -> Bool
    True
          InferVar{}                -> Bool
    True
          InferDef{}                -> Bool
    True
          CheckArguments{}          -> Bool
    True
          CheckMetaSolution{}       -> Bool
    False
          CheckTargetType{}         -> Bool
    False
          CheckDataDef{}            -> Bool
    True
          CheckRecDef{}             -> Bool
    True
          CheckConstructor{}        -> Bool
    True
          CheckConstructorFitsIn{}  -> Bool
    False
          CheckFunDefCall Range
    _ QName
    _ [Clause]
    _ Bool
    h   -> Bool
    h
          CheckPragma{}             -> Bool
    True
          CheckPrimitive{}          -> Bool
    True
          CheckIsEmpty{}            -> Bool
    True
          CheckConfluence{}         -> Bool
    False
          CheckWithFunctionType{}   -> Bool
    True
          CheckSectionApplication{} -> Bool
    True
          CheckNamedWhere{}         -> Bool
    False
          ScopeCheckExpr{}          -> Bool
    False
          ScopeCheckDeclaration{}   -> Bool
    False
          ScopeCheckLHS{}           -> Bool
    False
          NoHighlighting{}          -> Bool
    True
          CheckProjection{}         -> Bool
    False
          SetRange{}                -> Bool
    False
          ModuleContents{}          -> Bool
    False

        isNoHighlighting :: Bool
    isNoHighlighting = case Call
    call of
          NoHighlighting{} -> Bool
    True
          Call
    _ -> Bool
    False

      printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
    printHighlightingInfo RemoveTokenBasedHighlighting
    remove HighlightingInfo
    info = do
        ModuleToSource
    modToSrc <- Lens' ModuleToSource TCState -> TCMT IO ModuleToSource
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' ModuleToSource TCState
    stModuleToSource
        HighlightingMethod
    method   <- Lens' HighlightingMethod TCEnv -> TCMT IO HighlightingMethod
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' HighlightingMethod TCEnv
    eHighlightingMethod
        [Char] -> VerboseLevel -> [[Char]] -> TCM ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    [Char] -> VerboseLevel -> a -> m ()
    reportS [Char]
    "highlighting" VerboseLevel
    50
          [ [Char]
    "Printing highlighting info:"
          , HighlightingInfo -> [Char]
    forall a. Show a => a -> [Char]
    show HighlightingInfo
    info
          , [Char]
    "  modToSrc = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ ModuleToSource -> [Char]
    forall a. Show a => a -> [Char]
    show ModuleToSource
    modToSrc
          ]
        Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (HighlightingInfo -> Bool
    forall a. Null a => a -> Bool
    null HighlightingInfo
    info) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          Response -> TCM ()
    appInteractionOutputCallback (Response -> TCM ()) -> Response -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
              HighlightingInfo
    -> RemoveTokenBasedHighlighting
    -> HighlightingMethod
    -> ModuleToSource
    -> Response
    Resp_HighlightingInfo HighlightingInfo
    info RemoveTokenBasedHighlighting
    remove HighlightingMethod
    method ModuleToSource
    modToSrc

    getCurrentRange :: MonadTCEnv m => m Range
    getCurrentRange :: forall (m :: * -> *). MonadTCEnv m => m Range
    getCurrentRange = (TCEnv -> Range) -> m Range
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Range
    envRange

    -- | Sets the current range (for error messages etc.) to the range
    --   of the given object, if it has a range (i.e., its range is not 'noRange').
    setCurrentRange :: (MonadTrace m, HasRange x) => x -> m a -> m a
    setCurrentRange :: forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange x
    x = Bool -> (m a -> m a) -> m a -> m a
    forall a. Bool -> (a -> a) -> a -> a
    applyUnless (Range -> Bool
    forall a. Null a => a -> Bool
    null Range
    r) ((m a -> m a) -> m a -> m a) -> (m a -> m a) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ Call -> m a -> m a
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall (Call -> m a -> m a) -> Call -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ Range -> Call
    SetRange Range
    r
      where r :: Range
    r = x -> Range
    forall a. HasRange a => a -> Range
    getRange x
    x

    -- | @highlightAsTypeChecked rPre r m@ runs @m@ and returns its
    --   result. Additionally, some code may be highlighted:
    --
    -- * If @r@ is non-empty and not a sub-range of @rPre@ (after
    --   'P.continuousPerLine' has been applied to both): @r@ is
    --   highlighted as being type-checked while @m@ is running (this
    --   highlighting is removed if @m@ completes /successfully/).
    --
    -- * Otherwise: Highlighting is removed for @rPre - r@ before @m@
    --   runs, and if @m@ completes successfully, then @rPre - r@ is
    --   highlighted as being type-checked.

    highlightAsTypeChecked
      :: (MonadTrace m)
      => Range   -- ^ @rPre@
      -> Range   -- ^ @r@
      -> m a
      -> m a
    highlightAsTypeChecked :: forall (m :: * -> *) a.
    MonadTrace m =>
    Range -> Range -> m a -> m a
    highlightAsTypeChecked Range
    rPre Range
    r m a
    m
      | Range
    r Range -> Range -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Range
    forall a. Range' a
    noRange Bool -> Bool -> Bool
    && Ranges
    delta Ranges -> Ranges -> Bool
    forall a. Eq a => a -> a -> Bool
    == Ranges
    rPre' = Ranges -> Aspects -> Aspects -> m a
    wrap Ranges
    r'    Aspects
    highlight Aspects
    clear
      | Bool
    otherwise                      = Ranges -> Aspects -> Aspects -> m a
    wrap Ranges
    delta Aspects
    clear     Aspects
    highlight
      where
      rPre' :: Ranges
    rPre'     = Range -> Ranges
    rToR (Range -> Range
    forall a. Ord a => Range' a -> Range' a
    P.continuousPerLine Range
    rPre)
      r' :: Ranges
    r'        = Range -> Ranges
    rToR (Range -> Range
    forall a. Ord a => Range' a -> Range' a
    P.continuousPerLine Range
    r)
      delta :: Ranges
    delta     = Ranges
    rPre' Ranges -> Ranges -> Ranges
    `minus` Ranges
    r'
      clear :: Aspects
    clear     = Aspects
    forall a. Monoid a => a
    mempty
      highlight :: Aspects
    highlight = Aspects
    parserBased { otherAspects :: Set OtherAspect
    otherAspects = OtherAspect -> Set OtherAspect
    forall a. a -> Set a
    Set.singleton OtherAspect
    TypeChecks }

      wrap :: Ranges -> Aspects -> Aspects -> m a
    wrap Ranges
    rs Aspects
    x Aspects
    y = do
        Ranges -> Aspects -> m ()
    forall {m :: * -> *}. MonadTrace m => Ranges -> Aspects -> m ()
    p Ranges
    rs Aspects
    x
        a
    v <- m a
    m
        Ranges -> Aspects -> m ()
    forall {m :: * -> *}. MonadTrace m => Ranges -> Aspects -> m ()
    p Ranges
    rs Aspects
    y
        a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    v
        where
        p :: Ranges -> Aspects -> m ()
    p Ranges
    rs Aspects
    x = RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
    forall (m :: * -> *).
    MonadTrace m =>
    RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
    printHighlightingInfo RemoveTokenBasedHighlighting
    KeepHighlighting (Ranges -> Aspects -> HighlightingInfo
    forall a m. IsBasicRangeMap a m => Ranges -> a -> m
    singleton Ranges
    rs Aspects
    x)