    module Agda.TypeChecking.Monad.Caching
      ( -- * Log reading/writing operations
        writeToCurrentLog
      , readFromCachedLog
      , cleanCachedLog
      , cacheCurrentLog

        -- * Activating/deactivating
      , activateLoadedFileCache
      , cachingStarts
      , areWeCaching
      , localCache, withoutCache

        -- * Restoring the 'PostScopeState'
      , restorePostScopeState
      ) where

    import Agda.Syntax.Common

    import Agda.Interaction.Options

    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Monad.Debug

    import qualified Agda.Utils.BiMap as BiMap
    import Agda.Utils.Lens
    import Agda.Utils.Monad
    import Agda.Utils.Null (empty)

    import Agda.Utils.Impossible

    -- | To be called before any write or restore calls.
    {-# SPECIALIZE cachingStarts :: TCM () #-}
    cachingStarts :: (MonadDebug m, MonadTCState m, ReadTCState m) => m ()
    cachingStarts :: forall (m :: * -> *).
    (MonadDebug m, MonadTCState m, ReadTCState m) =>
    m ()
    cachingStarts = do
        NameId Word64
    _ ModuleNameHash
    m <- Lens' NameId TCState -> m NameId
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' NameId TCState
    stFreshNameId
        Lens' NameId TCState
    stFreshNameId Lens' NameId TCState -> NameId -> m ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    `setTCLens` Word64 -> ModuleNameHash -> NameId
    NameId Word64
    1 ModuleNameHash
    m
        Lens' Bool TCState
    stAreWeCaching Lens' Bool TCState -> Bool -> m ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    `setTCLens` Bool
    True
        ModuleNameHash -> m ()
    forall {m :: * -> *}.
    (MonadTCState m, ReadTCState m, MonadDebug m) =>
    ModuleNameHash -> m ()
    validateCache ModuleNameHash
    m -- fixes issue #4835
        where
          validateCache :: ModuleNameHash -> m ()
    validateCache ModuleNameHash
    m = (m (Maybe (TypeCheckAction, PostScopeState))
    -> m (Maybe (TypeCheckAction, PostScopeState))
    forall (m :: * -> *) a.
    (MonadTCState m, ReadTCState m) =>
    m a -> m a
    localCache m (Maybe (TypeCheckAction, PostScopeState))
    forall (m :: * -> *).
    (MonadDebug m, MonadTCState m, ReadTCState m) =>
    m (Maybe (TypeCheckAction, PostScopeState))
    readFromCachedLog) m (Maybe (TypeCheckAction, PostScopeState))
    -> (Maybe (TypeCheckAction, PostScopeState) -> m ()) -> m ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            Just (TypeCheckAction
    _ , PostScopeState
    s) -> do
              let NameId Word64
    _ ModuleNameHash
    m' = PostScopeState -> NameId
    stPostFreshNameId PostScopeState
    s
              Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (ModuleNameHash
    m' ModuleNameHash -> ModuleNameHash -> Bool
    forall a. Eq a => a -> a -> Bool
    /= ModuleNameHash
    m) m ()
    forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
    cleanCachedLog
            Maybe (TypeCheckAction, PostScopeState)
    _ -> do
              () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    areWeCaching :: (ReadTCState m) => m Bool
    areWeCaching :: forall (m :: * -> *). ReadTCState m => m Bool
    areWeCaching = Lens' Bool TCState -> m Bool
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' Bool TCState
    stAreWeCaching

    -- | Writes a 'TypeCheckAction' to the current log, using the current
    -- 'PostScopeState'
    {-# SPECIALIZE writeToCurrentLog :: TypeCheckAction -> TCM () #-}
    writeToCurrentLog :: (MonadDebug m, MonadTCState m, ReadTCState m) => TypeCheckAction -> m ()
    writeToCurrentLog :: forall (m :: * -> *).
    (MonadDebug m, MonadTCState m, ReadTCState m) =>
    TypeCheckAction -> m ()
    writeToCurrentLog !TypeCheckAction
    d = do
      VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    reportSLn VerboseKey
    "cache" VerboseLevel
    10 (VerboseKey -> m ()) -> VerboseKey -> m ()
    forall a b. (a -> b) -> a -> b
    $ VerboseKey
    "cachePostScopeState"
      !PostScopeState
    l <- (TCState -> PostScopeState) -> m PostScopeState
    forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
    getsTC TCState -> PostScopeState
    stPostScopeState
      (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
    modifyCache ((Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ())
    -> (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
    forall a b. (a -> b) -> a -> b
    $ (LoadedFileCache -> LoadedFileCache)
    -> Maybe LoadedFileCache -> Maybe LoadedFileCache
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((LoadedFileCache -> LoadedFileCache)
     -> Maybe LoadedFileCache -> Maybe LoadedFileCache)
    -> (LoadedFileCache -> LoadedFileCache)
    -> Maybe LoadedFileCache
    -> Maybe LoadedFileCache
    forall a b. (a -> b) -> a -> b
    $ \LoadedFileCache
    lfc -> LoadedFileCache
    lfc{ lfcCurrent :: CurrentTypeCheckLog
    lfcCurrent = (TypeCheckAction
    d, PostScopeState
    l) (TypeCheckAction, PostScopeState)
    -> CurrentTypeCheckLog -> CurrentTypeCheckLog
    forall a. a -> [a] -> [a]
    : LoadedFileCache -> CurrentTypeCheckLog
    lfcCurrent LoadedFileCache
    lfc}

    {-# SPECIALIZE restorePostScopeState :: PostScopeState -> TCM () #-}
    restorePostScopeState :: (MonadDebug m, MonadTCState m) => PostScopeState -> m ()
    restorePostScopeState :: forall (m :: * -> *).
    (MonadDebug m, MonadTCState m) =>
    PostScopeState -> m ()
    restorePostScopeState PostScopeState
    pss = do
      VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    reportSLn VerboseKey
    "cache" VerboseLevel
    10 (VerboseKey -> m ()) -> VerboseKey -> m ()
    forall a b. (a -> b) -> a -> b
    $ VerboseKey
    "restorePostScopeState"
      (TCState -> TCState) -> m ()
    forall (m :: * -> *).
    MonadTCState m =>
    (TCState -> TCState) -> m ()
    modifyTC ((TCState -> TCState) -> m ()) -> (TCState -> TCState) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \TCState
    s ->
        let ipoints :: BiMap InteractionId InteractionPoint
    ipoints = TCState
    sTCState
    -> Lens' (BiMap InteractionId InteractionPoint) TCState
    -> BiMap InteractionId InteractionPoint
    forall o i. o -> Lens' i o -> i
    ^.Lens' (BiMap InteractionId InteractionPoint) TCState
    stInteractionPoints
            ws :: [TCWarning]
    ws = TCState
    sTCState -> Lens' [TCWarning] TCState -> [TCWarning]
    forall o i. o -> Lens' i o -> i
    ^.Lens' [TCWarning] TCState
    stTCWarnings
            pss' :: PostScopeState
    pss' = PostScopeState
    pss{stPostInteractionPoints :: BiMap InteractionId InteractionPoint
    stPostInteractionPoints = PostScopeState -> BiMap InteractionId InteractionPoint
    stPostInteractionPoints PostScopeState
    pss BiMap InteractionId InteractionPoint
    -> BiMap InteractionId InteractionPoint
    -> BiMap InteractionId InteractionPoint
    forall {k}.
    Ord k =>
    BiMap k InteractionPoint
    -> BiMap k InteractionPoint -> BiMap k InteractionPoint
    `mergeIPMap` BiMap InteractionId InteractionPoint
    ipoints
                      ,stPostTCWarnings :: [TCWarning]
    stPostTCWarnings = PostScopeState -> [TCWarning]
    stPostTCWarnings PostScopeState
    pss [TCWarning] -> [TCWarning] -> [TCWarning]
    `mergeWarnings` [TCWarning]
    ws
                      }
        in  TCState
    s{stPostScopeState :: PostScopeState
    stPostScopeState = PostScopeState
    pss'}
      where
        mergeIPMap :: BiMap k InteractionPoint
    -> BiMap k InteractionPoint -> BiMap k InteractionPoint
    mergeIPMap BiMap k InteractionPoint
    lm BiMap k InteractionPoint
    sm = (k -> InteractionPoint -> InteractionPoint)
    -> BiMap k InteractionPoint -> BiMap k InteractionPoint
    forall k v.
    (Ord k, Ord (Tag v), HasTag v) =>
    (k -> v -> v) -> BiMap k v -> BiMap k v
    BiMap.mapWithKey (\k
    k InteractionPoint
    v -> InteractionPoint
    -> (InteractionPoint -> InteractionPoint)
    -> Maybe InteractionPoint
    -> InteractionPoint
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe InteractionPoint
    v (InteractionPoint -> InteractionPoint -> InteractionPoint
    `mergeIP` InteractionPoint
    v) (k -> BiMap k InteractionPoint -> Maybe InteractionPoint
    forall k v. Ord k => k -> BiMap k v -> Maybe v
    BiMap.lookup k
    k BiMap k InteractionPoint
    lm)) BiMap k InteractionPoint
    sm
        -- see #1338 on why we need to use the new ranges.
        mergeIP :: InteractionPoint -> InteractionPoint -> InteractionPoint
    mergeIP InteractionPoint
    li InteractionPoint
    si = InteractionPoint
    li { ipRange :: Range
    ipRange = InteractionPoint -> Range
    ipRange InteractionPoint
    si }

        mergeWarnings :: [TCWarning] -> [TCWarning] -> [TCWarning]
    mergeWarnings [TCWarning]
    loading [TCWarning]
    current = [ TCWarning
    w | TCWarning
    w <- [TCWarning]
    current, Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ TCWarning -> Bool
    tcWarningCached TCWarning
    w ]
                                     [TCWarning] -> [TCWarning] -> [TCWarning]
    forall a. [a] -> [a] -> [a]
    ++ [ TCWarning
    w | TCWarning
    w <- [TCWarning]
    loading,       TCWarning -> Bool
    tcWarningCached TCWarning
    w ]

    {-# SPECIALIZE modifyCache :: (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> TCM () #-}
    modifyCache
      :: MonadTCState m
      => (Maybe LoadedFileCache -> Maybe LoadedFileCache)
      -> m ()
    modifyCache :: forall (m :: * -> *).
    MonadTCState m =>
    (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
    modifyCache = Lens' (Maybe LoadedFileCache) TCState
    -> (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    modifyTCLens Lens' (Maybe LoadedFileCache) TCState
    stLoadedFileCache

    {-# SPECIALIZE getCache :: TCM (Maybe LoadedFileCache) #-}
    getCache :: ReadTCState m => m (Maybe LoadedFileCache)
    getCache :: forall (m :: * -> *). ReadTCState m => m (Maybe LoadedFileCache)
    getCache = Lens' (Maybe LoadedFileCache) TCState -> m (Maybe LoadedFileCache)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Maybe LoadedFileCache) TCState
    stLoadedFileCache

    {-# SPECIALIZE putCache :: Maybe LoadedFileCache -> TCM () #-}
    putCache :: MonadTCState m => Maybe LoadedFileCache -> m ()
    putCache :: forall (m :: * -> *).
    MonadTCState m =>
    Maybe LoadedFileCache -> m ()
    putCache = Lens' (Maybe LoadedFileCache) TCState
    -> Maybe LoadedFileCache -> m ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    setTCLens Lens' (Maybe LoadedFileCache) TCState
    stLoadedFileCache

    -- | Runs the action and restores the current cache at the end of it.
    {-# SPECIALIZE localCache :: TCM a -> TCM a #-}
    localCache :: (MonadTCState m, ReadTCState m) => m a -> m a
    localCache :: forall (m :: * -> *) a.
    (MonadTCState m, ReadTCState m) =>
    m a -> m a
    localCache = m (Maybe LoadedFileCache)
    -> (Maybe LoadedFileCache -> m ()) -> m a -> m a
    forall (m :: * -> *) a b.
    Monad m =>
    m a -> (a -> m ()) -> m b -> m b
    bracket_ m (Maybe LoadedFileCache)
    forall (m :: * -> *). ReadTCState m => m (Maybe LoadedFileCache)
    getCache Maybe LoadedFileCache -> m ()
    forall (m :: * -> *).
    MonadTCState m =>
    Maybe LoadedFileCache -> m ()
    putCache

    -- | Runs the action without cache and restores the current cache at
    -- the end of it.
    {-# SPECIALIZE withoutCache :: TCM a -> TCM a #-}
    withoutCache :: (MonadTCState m, ReadTCState m) => m a -> m a
    withoutCache :: forall (m :: * -> *) a.
    (MonadTCState m, ReadTCState m) =>
    m a -> m a
    withoutCache m a
    m = m a -> m a
    forall (m :: * -> *) a.
    (MonadTCState m, ReadTCState m) =>
    m a -> m a
    localCache (m a -> m a) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ do
        Maybe LoadedFileCache -> m ()
    forall (m :: * -> *).
    MonadTCState m =>
    Maybe LoadedFileCache -> m ()
    putCache Maybe LoadedFileCache
    forall a. Null a => a
    empty
        m a
    m

    -- | Reads the next entry in the cached type check log, if present.
    {-# SPECIALIZE readFromCachedLog :: TCM (Maybe (TypeCheckAction, PostScopeState)) #-}
    readFromCachedLog :: (MonadDebug m, MonadTCState m, ReadTCState m) => m (Maybe (TypeCheckAction, PostScopeState))
    readFromCachedLog :: forall (m :: * -> *).
    (MonadDebug m, MonadTCState m, ReadTCState m) =>
    m (Maybe (TypeCheckAction, PostScopeState))
    readFromCachedLog = do
      VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    reportSLn VerboseKey
    "cache" VerboseLevel
    10 (VerboseKey -> m ()) -> VerboseKey -> m ()
    forall a b. (a -> b) -> a -> b
    $ VerboseKey
    "getCachedTypeCheckAction"
      m (Maybe LoadedFileCache)
    forall (m :: * -> *). ReadTCState m => m (Maybe LoadedFileCache)
    getCache m (Maybe LoadedFileCache)
    -> (Maybe LoadedFileCache
        -> m (Maybe (TypeCheckAction, PostScopeState)))
    -> m (Maybe (TypeCheckAction, PostScopeState))
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Just LoadedFileCache
    lfc | ((TypeCheckAction, PostScopeState)
    entry : CurrentTypeCheckLog
    entries) <- LoadedFileCache -> CurrentTypeCheckLog
    lfcCached LoadedFileCache
    lfc -> do
          Maybe LoadedFileCache -> m ()
    forall (m :: * -> *).
    MonadTCState m =>
    Maybe LoadedFileCache -> m ()
    putCache (Maybe LoadedFileCache -> m ()) -> Maybe LoadedFileCache -> m ()
    forall a b. (a -> b) -> a -> b
    $ LoadedFileCache -> Maybe LoadedFileCache
    forall a. a -> Maybe a
    Just LoadedFileCache
    lfc{lfcCached :: CurrentTypeCheckLog
    lfcCached = CurrentTypeCheckLog
    entries}
          Maybe (TypeCheckAction, PostScopeState)
    -> m (Maybe (TypeCheckAction, PostScopeState))
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((TypeCheckAction, PostScopeState)
    -> Maybe (TypeCheckAction, PostScopeState)
    forall a. a -> Maybe a
    Just (TypeCheckAction, PostScopeState)
    entry)
        Maybe LoadedFileCache
    _ -> do
          Maybe (TypeCheckAction, PostScopeState)
    -> m (Maybe (TypeCheckAction, PostScopeState))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (TypeCheckAction, PostScopeState)
    forall a. Maybe a
    Nothing

    -- | Empties the "to read" CachedState. To be used when it gets invalid.
    {-# SPECIALIZE cleanCachedLog :: TCM () #-}
    cleanCachedLog :: (MonadDebug m, MonadTCState m) => m ()
    cleanCachedLog :: forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
    cleanCachedLog = do
      VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    reportSLn VerboseKey
    "cache" VerboseLevel
    10 (VerboseKey -> m ()) -> VerboseKey -> m ()
    forall a b. (a -> b) -> a -> b
    $ VerboseKey
    "cleanCachedLog"
      (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
    modifyCache ((Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ())
    -> (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
    forall a b. (a -> b) -> a -> b
    $ (LoadedFileCache -> LoadedFileCache)
    -> Maybe LoadedFileCache -> Maybe LoadedFileCache
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((LoadedFileCache -> LoadedFileCache)
     -> Maybe LoadedFileCache -> Maybe LoadedFileCache)
    -> (LoadedFileCache -> LoadedFileCache)
    -> Maybe LoadedFileCache
    -> Maybe LoadedFileCache
    forall a b. (a -> b) -> a -> b
    $ \LoadedFileCache
    lfc -> LoadedFileCache
    lfc{lfcCached :: CurrentTypeCheckLog
    lfcCached = []}

    -- | Makes sure that the 'stLoadedFileCache' is 'Just', with a clean
    -- current log. Crashes is 'stLoadedFileCache' is already active with a
    -- dirty log.  Should be called when we start typechecking the current
    -- file.
    {-# SPECIALIZE activateLoadedFileCache :: TCM () #-}
    activateLoadedFileCache :: (HasOptions m, MonadDebug m, MonadTCState m) => m ()
    activateLoadedFileCache :: forall (m :: * -> *).
    (HasOptions m, MonadDebug m, MonadTCState m) =>
    m ()
    activateLoadedFileCache = do
      VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    reportSLn VerboseKey
    "cache" VerboseLevel
    10 (VerboseKey -> m ()) -> VerboseKey -> m ()
    forall a b. (a -> b) -> a -> b
    $ VerboseKey
    "activateLoadedFileCache"

      m Bool -> m () -> m ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (CommandLineOptions -> Bool
    optGHCiInteraction (CommandLineOptions -> Bool) -> m CommandLineOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $
        m Bool -> m () -> m ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM m Bool
    forall (m :: * -> *). HasOptions m => m Bool
    enableCaching (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
          (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
    modifyCache ((Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ())
    -> (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \case
             Maybe LoadedFileCache
    Nothing                          -> LoadedFileCache -> Maybe LoadedFileCache
    forall a. a -> Maybe a
    Just (LoadedFileCache -> Maybe LoadedFileCache)
    -> LoadedFileCache -> Maybe LoadedFileCache
    forall a b. (a -> b) -> a -> b
    $ CurrentTypeCheckLog -> CurrentTypeCheckLog -> LoadedFileCache
    LoadedFileCache [] []
             Just LoadedFileCache
    lfc | CurrentTypeCheckLog -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null (LoadedFileCache -> CurrentTypeCheckLog
    lfcCurrent LoadedFileCache
    lfc) -> LoadedFileCache -> Maybe LoadedFileCache
    forall a. a -> Maybe a
    Just LoadedFileCache
    lfc
             Maybe LoadedFileCache
    _                                -> Maybe LoadedFileCache
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Caches the current type check log.  Discardes the old cache.  Does
    -- nothing if caching is inactive.
    {-# SPECIALIZE cacheCurrentLog :: TCM () #-}
    cacheCurrentLog :: (MonadDebug m, MonadTCState m) => m ()
    cacheCurrentLog :: forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
    cacheCurrentLog = do
      VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> VerboseLevel -> VerboseKey -> m ()
    reportSLn VerboseKey
    "cache" VerboseLevel
    10 (VerboseKey -> m ()) -> VerboseKey -> m ()
    forall a b. (a -> b) -> a -> b
    $ VerboseKey
    "cacheCurrentTypeCheckLog"
      (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
    modifyCache ((Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ())
    -> (Maybe LoadedFileCache -> Maybe LoadedFileCache) -> m ()
    forall a b. (a -> b) -> a -> b
    $ (LoadedFileCache -> LoadedFileCache)
    -> Maybe LoadedFileCache -> Maybe LoadedFileCache
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((LoadedFileCache -> LoadedFileCache)
     -> Maybe LoadedFileCache -> Maybe LoadedFileCache)
    -> (LoadedFileCache -> LoadedFileCache)
    -> Maybe LoadedFileCache
    -> Maybe LoadedFileCache
    forall a b. (a -> b) -> a -> b
    $ \LoadedFileCache
    lfc ->
        LoadedFileCache
    lfc{lfcCached :: CurrentTypeCheckLog
    lfcCached = CurrentTypeCheckLog -> CurrentTypeCheckLog
    forall a. [a] -> [a]
    reverse (LoadedFileCache -> CurrentTypeCheckLog
    lfcCurrent LoadedFileCache
    lfc), lfcCurrent :: CurrentTypeCheckLog
    lfcCurrent = []}