    -- | Lenses for 'TCState' and more.

    module Agda.TypeChecking.Monad.State where

    import qualified Control.Exception as E

    import Control.DeepSeq           (rnf)
    import Control.Exception         (evaluate)
    import Control.Monad.Trans       (MonadIO, liftIO)
    import Control.Monad.Trans.Maybe (MaybeT(MaybeT), runMaybeT)

    import Data.Maybe
    import qualified Data.EnumMap.Strict as EnumMap
    import qualified Data.HashMap.Strict as HMap
    import qualified Data.Map as Map
    import Data.Set (Set)
    import qualified Data.Set as Set

    import Agda.Benchmarking

    import Agda.Compiler.Backend.Base (pattern Backend, backendName, mayEraseType)

    import Agda.Interaction.Library ( classifyBuiltinModule_ )
    import Agda.Interaction.Response
      (InteractionOutputCallback, Response)

    import Agda.Syntax.Common
    import Agda.Syntax.Scope.Base
    import qualified Agda.Syntax.Concrete.Name as C
    import Agda.Syntax.Abstract (PatternSynDefn, PatternSynDefns)
    import Agda.Syntax.Abstract.PatternSynonyms
    import Agda.Syntax.Abstract.Name
    import Agda.Syntax.Internal
    import Agda.Syntax.Position
    import Agda.Syntax.TopLevelModuleName

    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Warnings

    import Agda.TypeChecking.Monad.Debug (reportSDoc, reportSLn, verboseS)
    import Agda.TypeChecking.Positivity.Occurrence
    import Agda.TypeChecking.CompiledClause

    import qualified Agda.Utils.BiMap as BiMap
    import Agda.Utils.FileId ( File, getIdFile, registerFileId' )
    import Agda.Utils.Lens
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Syntax.Common.Pretty
    import Agda.Utils.Tuple

    import Agda.Utils.Impossible

    -- | Resets the non-persistent part of the type checking state.

    resetState :: TCM ()
    resetState :: TCM ()
    resetState = (TCState -> TCState) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (TCState -> TCState) -> m ()
    modifyTC \ TCState
    s -> PersistentTCState -> TCState
    initStateFromPersistentState (TCState
    s TCState -> Lens' TCState PersistentTCState -> PersistentTCState
    forall o i. o -> Lens' o i -> i
    ^. (PersistentTCState -> f PersistentTCState) -> TCState -> f TCState
    Lens' TCState PersistentTCState
    lensPersistentState)

    -- | Resets all of the type checking state.
    --
    --   Keep only the session state (backend information, 'Benchmark', file ids).

    resetAllState :: TCM ()
    resetAllState :: TCM ()
    resetAllState = (TCState -> TCState) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (TCState -> TCState) -> m ()
    modifyTC \ TCState
    s -> SessionTCState -> TCState
    initStateFromSessionState (TCState
    s TCState -> Lens' TCState SessionTCState -> SessionTCState
    forall o i. o -> Lens' o i -> i
    ^. (SessionTCState -> f SessionTCState) -> TCState -> f TCState
    Lens' TCState SessionTCState
    lensSessionState)

    -- | Overwrite the 'TCState', but not the 'SessionTCState' part.
    putTCPreservingSession :: TCState -> TCM ()
    putTCPreservingSession :: TCState -> TCM ()
    putTCPreservingSession = TCMT IO (SessionTCState, Statistics)
    -> ((SessionTCState, Statistics) -> TCM ()) -> TCM () -> TCM ()
    forall (m :: * -> *) a b.
    Monad m =>
    m a -> (a -> m ()) -> m b -> m b
    bracket_ TCMT IO (SessionTCState, Statistics)
    get (SessionTCState, Statistics) -> TCM ()
    forall {m :: * -> *}.
    MonadTCState m =>
    (SessionTCState, Statistics) -> m ()
    put (TCM () -> TCM ()) -> (TCState -> TCM ()) -> TCState -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCState -> TCM ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    putTC where
      get :: TCMT IO (SessionTCState, Statistics)
    get = (,) (SessionTCState -> Statistics -> (SessionTCState, Statistics))
    -> TCMT IO SessionTCState
    -> TCMT IO (Statistics -> (SessionTCState, Statistics))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCState SessionTCState -> TCMT IO SessionTCState
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (SessionTCState -> f SessionTCState) -> TCState -> f TCState
    Lens' TCState SessionTCState
    lensSessionState TCMT IO (Statistics -> (SessionTCState, Statistics))
    -> TCMT IO Statistics -> TCMT IO (SessionTCState, Statistics)
    forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Lens' TCState Statistics -> TCMT IO Statistics
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (Statistics -> f Statistics) -> TCState -> f TCState
    Lens' TCState Statistics
    stStatistics

      put :: (SessionTCState, Statistics) -> m ()
    put (SessionTCState
    sess, Statistics
    stat) = do
        Lens' TCState SessionTCState -> SessionTCState -> m ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> a -> m ()
    setTCLens (SessionTCState -> f SessionTCState) -> TCState -> f TCState
    Lens' TCState SessionTCState
    lensSessionState SessionTCState
    sess
        Lens' TCState Statistics -> Statistics -> m ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> a -> m ()
    setTCLens (Statistics -> f Statistics) -> TCState -> f TCState
    Lens' TCState Statistics
    stStatistics Statistics
    stat

    -- | Restore 'TCState' after performing subcomputation.
    --
    --   In contrast to 'Agda.Utils.Monad.localState', the
    --   'SessionTCState' from the subcomputation is saved.
    localTCState :: TCM a -> TCM a
    localTCState :: forall a. TCM a -> TCM a
    localTCState = TCMT IO TCState -> (TCState -> TCM ()) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a b.
    Monad m =>
    m a -> (a -> m ()) -> m b -> m b
    bracket_ TCMT IO TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC TCState -> TCM ()
    putTCPreservingSession

    -- | Same as 'localTCState' but also returns the state in which we were just
    --   before reverting it.
    localTCStateSaving :: TCM a -> TCM (a, TCState)
    localTCStateSaving :: forall a. TCM a -> TCM (a, TCState)
    localTCStateSaving TCM a
    compute = TCM (a, TCState) -> TCM (a, TCState)
    forall a. TCM a -> TCM a
    localTCState (TCM (a, TCState) -> TCM (a, TCState))
    -> TCM (a, TCState) -> TCM (a, TCState)
    forall a b. (a -> b) -> a -> b
    $ (a -> TCState -> (a, TCState))
    -> TCM a -> TCMT IO TCState -> TCM (a, TCState)
    forall a b c. (a -> b -> c) -> TCMT IO a -> TCMT IO b -> TCMT IO c
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 (,) TCM a
    compute TCMT IO TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC

    -- | Same as 'localTCState' but keep all warnings.
    localTCStateSavingWarnings :: TCM a -> TCM a
    localTCStateSavingWarnings :: forall a. TCM a -> TCM a
    localTCStateSavingWarnings TCM a
    compute = do
      (result, newState) <- TCM a -> TCM (a, TCState)
    forall a. TCM a -> TCM (a, TCState)
    localTCStateSaving TCM a
    compute
      modifyTC $ over stTCWarnings $ const $ newState ^. stTCWarnings
      return result

    -- | A fresh TCM instance.
    --
    -- The computation is run in a fresh state, with the exception that
    -- the persistent state is preserved. If the computation changes the
    -- state, then these changes are ignored, except for changes to the
    -- persistent state. (Changes to the persistent state are also ignored
    -- if errors other than type errors or IO exceptions are encountered.)

    freshTCM :: TCM a -> TCM (Either TCErr a)
    freshTCM :: forall a. TCM a -> TCM (Either TCErr a)
    freshTCM TCM a
    m = do

      -- Run m in fresh TCM that only kept the current persistent state.
      ps <- Lens' TCState PersistentTCState -> TCMT IO PersistentTCState
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (PersistentTCState -> f PersistentTCState) -> TCState -> f TCState
    Lens' TCState PersistentTCState
    lensPersistentState
      let s0 = PersistentTCState -> TCState
    initStateFromPersistentState PersistentTCState
    ps
      r <- liftIO $ (Right <$> runTCM initEnv s0 m) `E.catch` (return . Left)

      -- Keep m's changes to the persistent state, if possible.
      let keepPersistent TCState
    s = Lens' TCState PersistentTCState -> PersistentTCState -> m ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> a -> m ()
    setTCLens (PersistentTCState -> f PersistentTCState) -> TCState -> f TCState
    Lens' TCState PersistentTCState
    lensPersistentState (PersistentTCState -> m ()) -> PersistentTCState -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCState
    s TCState -> Lens' TCState PersistentTCState -> PersistentTCState
    forall o i. o -> Lens' o i -> i
    ^. (PersistentTCState -> f PersistentTCState) -> TCState -> f TCState
    Lens' TCState PersistentTCState
    lensPersistentState
      case r of
        Right (a
    a, TCState
    s) -> a -> Either TCErr a
    forall a b. b -> Either a b
    Right a
    a Either TCErr a -> TCM () -> TCMT IO (Either TCErr a)
    forall a b. a -> TCMT IO b -> TCMT IO a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ TCState -> TCM ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    keepPersistent TCState
    s
        Left TCErr
    err -> TCErr -> Either TCErr a
    forall a b. a -> Either a b
    Left TCErr
    err Either TCErr a -> TCM () -> TCMT IO (Either TCErr a)
    forall a b. a -> TCMT IO b -> TCMT IO a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$
          case TCErr
    err of
            TypeError { tcErrState :: TCErr -> TCState
    tcErrState = TCState
    s } -> TCState -> TCM ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    keepPersistent TCState
    s
            IOException (Just TCState
    s) Range
    _ IOException
    _     -> TCState -> TCM ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    keepPersistent TCState
    s
            IOException Maybe TCState
    Nothing  Range
    _ IOException
    _     -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            GenericException [Char]
    _           -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            ParserError ParseError
    _                -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            PatternErr Blocker
    _                 -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    ---------------------------------------------------------------------------
    -- * Lens for persistent states and its fields
    ---------------------------------------------------------------------------

    updatePersistentState
      :: (PersistentTCState -> PersistentTCState) -> (TCState -> TCState)
    updatePersistentState :: (PersistentTCState -> PersistentTCState) -> TCState -> TCState
    updatePersistentState PersistentTCState -> PersistentTCState
    f TCState
    s = TCState
    s { stPersistentState = f (stPersistentState s) }

    modifyPersistentState :: (PersistentTCState -> PersistentTCState) -> TCM ()
    modifyPersistentState :: (PersistentTCState -> PersistentTCState) -> TCM ()
    modifyPersistentState = (TCState -> TCState) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (TCState -> TCState) -> m ()
    modifyTC ((TCState -> TCState) -> TCM ())
    -> ((PersistentTCState -> PersistentTCState) -> TCState -> TCState)
    -> (PersistentTCState -> PersistentTCState)
    -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (PersistentTCState -> PersistentTCState) -> TCState -> TCState
    updatePersistentState

    -- | Lens for 'stAccumStatistics'.

    lensAccumStatisticsP :: Lens' PersistentTCState Statistics
    lensAccumStatisticsP :: Lens' PersistentTCState Statistics
    lensAccumStatisticsP Statistics -> f Statistics
    f PersistentTCState
    s = Statistics -> f Statistics
    f (PersistentTCState -> Statistics
    stAccumStatistics PersistentTCState
    s) f Statistics
    -> (Statistics -> PersistentTCState) -> f PersistentTCState
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Statistics
    a ->
      PersistentTCState
    s { stAccumStatistics = a }

    lensAccumStatistics :: Lens' TCState Statistics
    lensAccumStatistics :: Lens' TCState Statistics
    lensAccumStatistics =  (PersistentTCState -> f PersistentTCState) -> TCState -> f TCState
    Lens' TCState PersistentTCState
    lensPersistentState ((PersistentTCState -> f PersistentTCState)
     -> TCState -> f TCState)
    -> ((Statistics -> f Statistics)
        -> PersistentTCState -> f PersistentTCState)
    -> (Statistics -> f Statistics)
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Statistics -> f Statistics)
    -> PersistentTCState -> f PersistentTCState
    Lens' PersistentTCState Statistics
    lensAccumStatisticsP

    ---------------------------------------------------------------------------
    -- * Scope
    ---------------------------------------------------------------------------

    {-# INLINE getScope #-}
    -- | Get the current scope.
    getScope :: ReadTCState m => m ScopeInfo
    getScope :: forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope = Lens' TCState ScopeInfo -> m ScopeInfo
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (ScopeInfo -> f ScopeInfo) -> TCState -> f TCState
    Lens' TCState ScopeInfo
    stScope

    {-# INLINE setScope #-}
    -- | Set the current scope.
    setScope :: ScopeInfo -> TCM ()
    setScope :: ScopeInfo -> TCM ()
    setScope ScopeInfo
    scope = (ScopeInfo -> ScopeInfo) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (ScopeInfo -> ScopeInfo) -> m ()
    modifyScope (ScopeInfo -> ScopeInfo -> ScopeInfo
    forall a b. a -> b -> a
    const ScopeInfo
    scope)

    {-# INLINE modifyScope_ #-}
    -- | Modify the current scope without updating the inverse maps.
    modifyScope_ :: MonadTCState m => (ScopeInfo -> ScopeInfo) -> m ()
    modifyScope_ :: forall (m :: * -> *).
    MonadTCState m =>
    (ScopeInfo -> ScopeInfo) -> m ()
    modifyScope_ ScopeInfo -> ScopeInfo
    f = (ScopeInfo -> f ScopeInfo) -> TCState -> f TCState
    Lens' TCState ScopeInfo
    stScope Lens' TCState ScopeInfo -> (ScopeInfo -> ScopeInfo) -> m ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` ScopeInfo -> ScopeInfo
    f

    {-# INLINE modifyScope #-}
    -- | Modify the current scope.
    modifyScope :: MonadTCState m => (ScopeInfo -> ScopeInfo) -> m ()
    modifyScope :: forall (m :: * -> *).
    MonadTCState m =>
    (ScopeInfo -> ScopeInfo) -> m ()
    modifyScope ScopeInfo -> ScopeInfo
    f = (ScopeInfo -> ScopeInfo) -> m ()
    forall (m :: * -> *).
    MonadTCState m =>
    (ScopeInfo -> ScopeInfo) -> m ()
    modifyScope_ (ScopeInfo -> ScopeInfo
    recomputeInverseScopeMaps (ScopeInfo -> ScopeInfo)
    -> (ScopeInfo -> ScopeInfo) -> ScopeInfo -> ScopeInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ScopeInfo -> ScopeInfo
    f)

    {-# INLINE useScope #-}
    -- | Get a part of the current scope.
    useScope :: ReadTCState m => Lens' ScopeInfo a -> m a
    useScope :: forall (m :: * -> *) a. ReadTCState m => Lens' ScopeInfo a -> m a
    useScope Lens' ScopeInfo a
    l = Lens' TCState a -> m a
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (Lens' TCState a -> m a) -> Lens' TCState a -> m a
    forall a b. (a -> b) -> a -> b
    $ (ScopeInfo -> f ScopeInfo) -> TCState -> f TCState
    Lens' TCState ScopeInfo
    stScope ((ScopeInfo -> f ScopeInfo) -> TCState -> f TCState)
    -> ((a -> f a) -> ScopeInfo -> f ScopeInfo)
    -> (a -> f a)
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> f a) -> ScopeInfo -> f ScopeInfo
    Lens' ScopeInfo a
    l

    {-# INLINE locallyScope #-}
    -- | Run a computation in a modified scope.
    locallyScope :: ReadTCState m => Lens' ScopeInfo a -> (a -> a) -> m b -> m b
    locallyScope :: forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' ScopeInfo a -> (a -> a) -> m b -> m b
    locallyScope Lens' ScopeInfo a
    l = Lens' TCState a -> (a -> a) -> m b -> m b
    forall a b. Lens' TCState a -> (a -> a) -> m b -> m b
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' TCState a -> (a -> a) -> m b -> m b
    locallyTCState (Lens' TCState a -> (a -> a) -> m b -> m b)
    -> Lens' TCState a -> (a -> a) -> m b -> m b
    forall a b. (a -> b) -> a -> b
    $ (ScopeInfo -> f ScopeInfo) -> TCState -> f TCState
    Lens' TCState ScopeInfo
    stScope ((ScopeInfo -> f ScopeInfo) -> TCState -> f TCState)
    -> ((a -> f a) -> ScopeInfo -> f ScopeInfo)
    -> (a -> f a)
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> f a) -> ScopeInfo -> f ScopeInfo
    Lens' ScopeInfo a
    l

    {-# INLINE withScope #-}
    -- | Run a computation in a local scope.
    withScope :: ReadTCState m => ScopeInfo -> m a -> m (a, ScopeInfo)
    withScope :: forall (m :: * -> *) a.
    ReadTCState m =>
    ScopeInfo -> m a -> m (a, ScopeInfo)
    withScope ScopeInfo
    s m a
    m = Lens' TCState ScopeInfo
    -> (ScopeInfo -> ScopeInfo) -> m (a, ScopeInfo) -> m (a, ScopeInfo)
    forall a b. Lens' TCState a -> (a -> a) -> m b -> m b
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' TCState a -> (a -> a) -> m b -> m b
    locallyTCState (ScopeInfo -> f ScopeInfo) -> TCState -> f TCState
    Lens' TCState ScopeInfo
    stScope (ScopeInfo -> ScopeInfo
    recomputeInverseScopeMaps (ScopeInfo -> ScopeInfo)
    -> (ScopeInfo -> ScopeInfo) -> ScopeInfo -> ScopeInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ScopeInfo -> ScopeInfo -> ScopeInfo
    forall a b. a -> b -> a
    const ScopeInfo
    s) (m (a, ScopeInfo) -> m (a, ScopeInfo))
    -> m (a, ScopeInfo) -> m (a, ScopeInfo)
    forall a b. (a -> b) -> a -> b
    $ (,) (a -> ScopeInfo -> (a, ScopeInfo))
    -> m a -> m (ScopeInfo -> (a, ScopeInfo))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m a
    m m (ScopeInfo -> (a, ScopeInfo)) -> m ScopeInfo -> m (a, ScopeInfo)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> m ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope

    {-# INLINE withScope_ #-}
    -- | Same as 'withScope', but discard the scope from the computation.
    withScope_ :: ReadTCState m => ScopeInfo -> m a -> m a
    withScope_ :: forall (m :: * -> *) a. ReadTCState m => ScopeInfo -> m a -> m a
    withScope_ ScopeInfo
    s m a
    m = (a, ScopeInfo) -> a
    forall a b. (a, b) -> a
    fst ((a, ScopeInfo) -> a) -> m (a, ScopeInfo) -> m a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ScopeInfo -> m a -> m (a, ScopeInfo)
    forall (m :: * -> *) a.
    ReadTCState m =>
    ScopeInfo -> m a -> m (a, ScopeInfo)
    withScope ScopeInfo
    s m a
    m

    -- | Discard any changes to the scope by a computation.
    localScope :: TCM a -> TCM a
    localScope :: forall a. TCM a -> TCM a
    localScope TCM a
    m = do
      scope <- TCMT IO ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope
      x <- m
      setScope scope
      return x

    -- | Scope error.
    notInScopeError :: C.QName -> TCM a
    notInScopeError :: forall a. QName -> TCM a
    notInScopeError QName
    x = do
      [Char] -> Int -> [Char] -> TCM ()
    printScope [Char]
    "unbound" Int
    25 [Char]
    ""
      TypeError -> TCMT IO a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ QName -> TypeError
    NotInScope QName
    x

    notInScopeWarning :: C.QName -> TCM ()
    notInScopeWarning :: QName -> TCM ()
    notInScopeWarning QName
    x = do
      [Char] -> Int -> [Char] -> TCM ()
    printScope [Char]
    "unbound" Int
    25 [Char]
    ""
      Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> Warning -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> Warning
    NotInScopeW QName
    x

    -- | Debug print the scope.
    printScope :: String -> Int -> String -> TCM ()
    printScope :: [Char] -> Int -> [Char] -> TCM ()
    printScope [Char]
    tag Int
    v [Char]
    s = [Char] -> Int -> TCM () -> TCM ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
    verboseS ([Char]
    "scope." [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    tag) Int
    v (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
      scope <- TCMT IO ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope
      reportSDoc ("scope." ++ tag) v $ return $ vcat [ text s, pretty scope ]

    ---------------------------------------------------------------------------
    -- * Signature
    ---------------------------------------------------------------------------

    -- ** Lens for 'stSignature' and 'stImports'

    {-# INLINE modifySignature  #-}
    modifySignature :: MonadTCState m => (Signature -> Signature) -> m ()
    modifySignature :: forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature Signature -> Signature
    f = (Signature -> f Signature) -> TCState -> f TCState
    Lens' TCState Signature
    stSignature Lens' TCState Signature -> (Signature -> Signature) -> m ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` Signature -> Signature
    f

    {-# INLINE modifyImportedSignature #-}
    modifyImportedSignature :: MonadTCState m => (Signature -> Signature) -> m ()
    modifyImportedSignature :: forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifyImportedSignature Signature -> Signature
    f = (Signature -> f Signature) -> TCState -> f TCState
    Lens' TCState Signature
    stImports Lens' TCState Signature -> (Signature -> Signature) -> m ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` Signature -> Signature
    f

    {-# INLINE getSignature #-}
    getSignature :: ReadTCState m => m Signature
    getSignature :: forall (m :: * -> *). ReadTCState m => m Signature
    getSignature = Lens' TCState Signature -> m Signature
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (Signature -> f Signature) -> TCState -> f TCState
    Lens' TCState Signature
    stSignature

    {-# SPECIALIZE modifyGlobalDefinition :: QName -> (Definition -> Definition) -> TCM () #-}
    -- | Update a possibly imported definition. Warning: changes made to imported
    --   definitions (during type checking) will not persist outside the current
    --   module. This function is currently used to update the compiled
    --   representation of a function during compilation.
    modifyGlobalDefinition :: MonadTCState m => QName -> (Definition -> Definition) -> m ()
    modifyGlobalDefinition :: forall (m :: * -> *).
    MonadTCState m =>
    QName -> (Definition -> Definition) -> m ()
    modifyGlobalDefinition QName
    q Definition -> Definition
    f = do
      (Signature -> Signature) -> m ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature         ((Signature -> Signature) -> m ())
    -> (Signature -> Signature) -> m ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    q Definition -> Definition
    f
      (Signature -> Signature) -> m ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifyImportedSignature ((Signature -> Signature) -> m ())
    -> (Signature -> Signature) -> m ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    q Definition -> Definition
    f

    {-# INLINE setSignature #-}
    setSignature :: MonadTCState m => Signature -> m ()
    setSignature :: forall (m :: * -> *). MonadTCState m => Signature -> m ()
    setSignature Signature
    sig = (Signature -> Signature) -> m ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> m ())
    -> (Signature -> Signature) -> m ()
    forall a b. (a -> b) -> a -> b
    $ Signature -> Signature -> Signature
    forall a b. a -> b -> a
    const Signature
    sig

    {-# SPECIALIZE withSignature :: Signature -> TCM a -> TCM a #-}
    -- | Run some computation in a different signature, restore original signature.
    withSignature :: (ReadTCState m, MonadTCState m) => Signature -> m a -> m a
    withSignature :: forall (m :: * -> *) a.
    (ReadTCState m, MonadTCState m) =>
    Signature -> m a -> m a
    withSignature Signature
    sig m a
    m = do
      sig0 <- m Signature
    forall (m :: * -> *). ReadTCState m => m Signature
    getSignature
      setSignature sig
      r <- m
      setSignature sig0
      return r

    -- ** Modifiers for rewrite rules
    addRewriteRulesFor :: QName -> RewriteRules -> [QName] -> Signature -> Signature
    addRewriteRulesFor :: QName -> RewriteRules -> [QName] -> Signature -> Signature
    addRewriteRulesFor QName
    f RewriteRules
    rews [QName]
    matchables =
        Lens' Signature (HashMap QName RewriteRules)
    -> LensMap Signature (HashMap QName RewriteRules)
    forall o i. Lens' o i -> LensMap o i
    over (HashMap QName RewriteRules -> f (HashMap QName RewriteRules))
    -> Signature -> f Signature
    Lens' Signature (HashMap QName RewriteRules)
    sigRewriteRules ((RewriteRules -> RewriteRules -> RewriteRules)
    -> QName
    -> RewriteRules
    -> HashMap QName RewriteRules
    -> HashMap QName RewriteRules
    forall k v.
    (Eq k, Hashable k) =>
    (v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
    HMap.insertWith RewriteRules -> RewriteRules -> RewriteRules
    forall a. Monoid a => a -> a -> a
    mappend QName
    f RewriteRules
    rews)
      (Signature -> Signature)
    -> (Signature -> Signature) -> Signature -> Signature
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    f ((Defn -> Defn) -> Definition -> Definition
    updateTheDef Defn -> Defn
    setNotInjective (Definition -> Definition)
    -> (Definition -> Definition) -> Definition -> Definition
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Definition
    setCopatternLHS)
      (Signature -> Signature)
    -> (Signature -> Signature) -> Signature -> Signature
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (QName -> [QName] -> Signature -> Signature
    setMatchableSymbols QName
    f [QName]
    matchables)
        where
          setNotInjective :: Defn -> Defn
    setNotInjective def :: Defn
    def@Function{} = Defn
    def { funInv = NotInjective }
          setNotInjective Defn
    def            = Defn
    def

          setCopatternLHS :: Definition -> Definition
    setCopatternLHS =
            (Bool -> Bool) -> Definition -> Definition
    updateDefCopatternLHS (Bool -> Bool -> Bool
    || (RewriteRule -> Bool) -> RewriteRules -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any RewriteRule -> Bool
    hasProjectionPattern RewriteRules
    rews)

          hasProjectionPattern :: RewriteRule -> Bool
    hasProjectionPattern RewriteRule
    rew = (Elim' NLPat -> Bool) -> [Elim' NLPat] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (Maybe (ProjOrigin, QName) -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe (ProjOrigin, QName) -> Bool)
    -> (Elim' NLPat -> Maybe (ProjOrigin, QName))
    -> Elim' NLPat
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Elim' NLPat -> Maybe (ProjOrigin, QName)
    forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
    isProjElim) ([Elim' NLPat] -> Bool) -> [Elim' NLPat] -> Bool
    forall a b. (a -> b) -> a -> b
    $ RewriteRule -> [Elim' NLPat]
    rewPats RewriteRule
    rew

    setMatchableSymbols :: QName -> [QName] -> Signature -> Signature
    setMatchableSymbols :: QName -> [QName] -> Signature -> Signature
    setMatchableSymbols QName
    f [QName]
    matchables =
      (QName -> (Signature -> Signature) -> Signature -> Signature)
    -> (Signature -> Signature) -> [QName] -> Signature -> Signature
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr ((Signature -> Signature)
    -> (Signature -> Signature) -> Signature -> Signature
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    (.) ((Signature -> Signature)
     -> (Signature -> Signature) -> Signature -> Signature)
    -> (QName -> Signature -> Signature)
    -> QName
    -> (Signature -> Signature)
    -> Signature
    -> Signature
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (\QName
    g -> QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    g Definition -> Definition
    setMatchable)) Signature -> Signature
    forall a. a -> a
    id [QName]
    matchables
        where
          setMatchable :: Definition -> Definition
    setMatchable Definition
    def = Definition
    def { defMatchable = Set.insert f $ defMatchable def }

    -- ** 'modify' methods for the signature

    modifyRecEta :: MonadTCState m => QName -> (EtaEquality -> EtaEquality) -> m ()
    modifyRecEta :: forall (m :: * -> *).
    MonadTCState m =>
    QName -> (EtaEquality -> EtaEquality) -> m ()
    modifyRecEta QName
    q EtaEquality -> EtaEquality
    f =
      (Signature -> Signature) -> m ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> m ())
    -> (Signature -> Signature) -> m ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    q ((Definition -> Definition) -> Signature -> Signature)
    -> (Definition -> Definition) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ Lens' Definition EtaEquality -> LensMap Definition EtaEquality
    forall o i. Lens' o i -> LensMap o i
    over ((Defn -> f Defn) -> Definition -> f Definition
    Lens' Definition Defn
    lensTheDef ((Defn -> f Defn) -> Definition -> f Definition)
    -> ((EtaEquality -> f EtaEquality) -> Defn -> f Defn)
    -> (EtaEquality -> f EtaEquality)
    -> Definition
    -> f Definition
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (RecordData -> f RecordData) -> Defn -> f Defn
    Lens' Defn RecordData
    lensRecord ((RecordData -> f RecordData) -> Defn -> f Defn)
    -> ((EtaEquality -> f EtaEquality) -> RecordData -> f RecordData)
    -> (EtaEquality -> f EtaEquality)
    -> Defn
    -> f Defn
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (EtaEquality -> f EtaEquality) -> RecordData -> f RecordData
    Lens' RecordData EtaEquality
    lensRecEta) EtaEquality -> EtaEquality
    f

    -- ** Modifiers for parts of the signature

    lookupDefinition :: QName -> Signature -> Maybe Definition
    lookupDefinition :: QName -> Signature -> Maybe Definition
    lookupDefinition QName
    q Signature
    sig = QName -> HashMap QName Definition -> Maybe Definition
    forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
    HMap.lookup QName
    q (HashMap QName Definition -> Maybe Definition)
    -> HashMap QName Definition -> Maybe Definition
    forall a b. (a -> b) -> a -> b
    $ Signature
    sig Signature
    -> Lens' Signature (HashMap QName Definition)
    -> HashMap QName Definition
    forall o i. o -> Lens' o i -> i
    ^. (HashMap QName Definition -> f (HashMap QName Definition))
    -> Signature -> f Signature
    Lens' Signature (HashMap QName Definition)
    sigDefinitions

    updateDefinitions :: (Definitions -> Definitions) -> Signature -> Signature
    updateDefinitions :: (HashMap QName Definition -> HashMap QName Definition)
    -> Signature -> Signature
    updateDefinitions = Lens' Signature (HashMap QName Definition)
    -> (HashMap QName Definition -> HashMap QName Definition)
    -> Signature
    -> Signature
    forall o i. Lens' o i -> LensMap o i
    over (HashMap QName Definition -> f (HashMap QName Definition))
    -> Signature -> f Signature
    Lens' Signature (HashMap QName Definition)
    sigDefinitions

    updateDefinition :: QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition :: QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    q Definition -> Definition
    f = (HashMap QName Definition -> HashMap QName Definition)
    -> Signature -> Signature
    updateDefinitions ((HashMap QName Definition -> HashMap QName Definition)
     -> Signature -> Signature)
    -> (HashMap QName Definition -> HashMap QName Definition)
    -> Signature
    -> Signature
    forall a b. (a -> b) -> a -> b
    $ (Definition -> Definition)
    -> QName -> HashMap QName Definition -> HashMap QName Definition
    forall k v.
    (Eq k, Hashable k) =>
    (v -> v) -> k -> HashMap k v -> HashMap k v
    HMap.adjust Definition -> Definition
    f QName
    q

    updateTheDef :: (Defn -> Defn) -> (Definition -> Definition)
    updateTheDef :: (Defn -> Defn) -> Definition -> Definition
    updateTheDef Defn -> Defn
    f Definition
    def = Definition
    def { theDef = f (theDef def) }

    updateDefType :: (Type -> Type) -> (Definition -> Definition)
    updateDefType :: (Type -> Type) -> Definition -> Definition
    updateDefType Type -> Type
    f Definition
    def = Definition
    def { defType = f (defType def) }

    updateDefArgOccurrences :: ([Occurrence] -> [Occurrence]) -> (Definition -> Definition)
    updateDefArgOccurrences :: ([Occurrence] -> [Occurrence]) -> Definition -> Definition
    updateDefArgOccurrences [Occurrence] -> [Occurrence]
    f Definition
    def = Definition
    def { defArgOccurrences = f (defArgOccurrences def) }

    updateDefPolarity :: ([Polarity] -> [Polarity]) -> (Definition -> Definition)
    updateDefPolarity :: ([Polarity] -> [Polarity]) -> Definition -> Definition
    updateDefPolarity [Polarity] -> [Polarity]
    f Definition
    def = Definition
    def { defPolarity = f (defPolarity def) }

    updateDefCompiledRep :: (CompiledRepresentation -> CompiledRepresentation) -> (Definition -> Definition)
    updateDefCompiledRep :: (CompiledRepresentation -> CompiledRepresentation)
    -> Definition -> Definition
    updateDefCompiledRep CompiledRepresentation -> CompiledRepresentation
    f Definition
    def = Definition
    def { defCompiledRep = f (defCompiledRep def) }

    addCompilerPragma :: BackendName -> CompilerPragma -> Definition -> Definition
    addCompilerPragma :: BackendName -> CompilerPragma -> Definition -> Definition
    addCompilerPragma BackendName
    backend CompilerPragma
    pragma = (CompiledRepresentation -> CompiledRepresentation)
    -> Definition -> Definition
    updateDefCompiledRep ((CompiledRepresentation -> CompiledRepresentation)
     -> Definition -> Definition)
    -> (CompiledRepresentation -> CompiledRepresentation)
    -> Definition
    -> Definition
    forall a b. (a -> b) -> a -> b
    $ ([CompilerPragma] -> [CompilerPragma] -> [CompilerPragma])
    -> BackendName
    -> [CompilerPragma]
    -> CompiledRepresentation
    -> CompiledRepresentation
    forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
    Map.insertWith [CompilerPragma] -> [CompilerPragma] -> [CompilerPragma]
    forall a. [a] -> [a] -> [a]
    (++) BackendName
    backend [CompilerPragma
    pragma]

    updateFunClauses :: ([Clause] -> [Clause]) -> (Defn -> Defn)
    updateFunClauses :: ([Clause] -> [Clause]) -> Defn -> Defn
    updateFunClauses [Clause] -> [Clause]
    f def :: Defn
    def@Function{ funClauses :: Defn -> [Clause]
    funClauses = [Clause]
    cs} = Defn
    def { funClauses = f cs }
    updateFunClauses [Clause] -> [Clause]
    f Defn
    _                              = Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    updateCovering :: ([Clause] -> [Clause]) -> (Defn -> Defn)
    updateCovering :: ([Clause] -> [Clause]) -> Defn -> Defn
    updateCovering [Clause] -> [Clause]
    f def :: Defn
    def@Function{ funCovering :: Defn -> [Clause]
    funCovering = [Clause]
    cs} = Defn
    def { funCovering = f cs }
    updateCovering [Clause] -> [Clause]
    f Defn
    _                               = Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    updateCompiledClauses :: (Maybe CompiledClauses -> Maybe CompiledClauses) -> (Defn -> Defn)
    updateCompiledClauses :: (Maybe CompiledClauses -> Maybe CompiledClauses) -> Defn -> Defn
    updateCompiledClauses Maybe CompiledClauses -> Maybe CompiledClauses
    f def :: Defn
    def@Function{ funCompiled :: Defn -> Maybe CompiledClauses
    funCompiled = Maybe CompiledClauses
    cc} = Defn
    def { funCompiled = f cc }
    updateCompiledClauses Maybe CompiledClauses -> Maybe CompiledClauses
    f Defn
    _                              = Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    updateDefCopatternLHS :: (Bool -> Bool) -> Definition -> Definition
    updateDefCopatternLHS :: (Bool -> Bool) -> Definition -> Definition
    updateDefCopatternLHS Bool -> Bool
    f def :: Definition
    def@Defn{ defCopatternLHS :: Definition -> Bool
    defCopatternLHS = Bool
    b } = Definition
    def { defCopatternLHS = f b }

    updateDefBlocked :: (Blocked_ -> Blocked_) -> Definition -> Definition
    updateDefBlocked :: (Blocked_ -> Blocked_) -> Definition -> Definition
    updateDefBlocked Blocked_ -> Blocked_
    f def :: Definition
    def@Defn{ defBlocked :: Definition -> Blocked_
    defBlocked = Blocked_
    b } = Definition
    def { defBlocked = f b }

    ---------------------------------------------------------------------------
    -- * File identification
    ---------------------------------------------------------------------------

    -- | Translate an absolute path to a file id, and register a new file id
    --   if the path has not seen before.
    --   Also register whether the path belongs to one of Agda's builtin modules.
    --
    registerFileIdWithBuiltin :: File -> FileDictWithBuiltins -> (FileId, FileDictWithBuiltins)
    registerFileIdWithBuiltin :: File -> FileDictWithBuiltins -> (FileId, FileDictWithBuiltins)
    registerFileIdWithBuiltin File
    f (FileDictWithBuiltins FileDictBuilder
    d BuiltinModuleIds
    b File
    primLibDir) =
      (FileId
    fi, FileDictBuilder -> BuiltinModuleIds -> File -> FileDictWithBuiltins
    FileDictWithBuiltins FileDictBuilder
    d' BuiltinModuleIds
    b' File
    primLibDir)
      where
        ((FileId
    fi, Bool
    new), FileDictBuilder
    d') = File -> FileDictBuilder -> ((FileId, Bool), FileDictBuilder)
    registerFileId' File
    f FileDictBuilder
    d
        b' :: BuiltinModuleIds
    b' = case File -> File -> Maybe IsBuiltinModule
    classifyBuiltinModule_ File
    primLibDir File
    f of
          Maybe IsBuiltinModule
    Nothing -> BuiltinModuleIds
    b
          Just IsBuiltinModule
    c  -> FileId -> IsBuiltinModule -> BuiltinModuleIds -> BuiltinModuleIds
    forall k a. Enum k => k -> a -> EnumMap k a -> EnumMap k a
    EnumMap.insert FileId
    fi IsBuiltinModule
    c BuiltinModuleIds
    b

    instance MonadIO m => MonadFileId (TCMT m) where
      fileFromId :: FileId -> TCMT m File
    fileFromId FileId
    fi = Lens' TCState FileDictWithBuiltins -> TCMT m FileDictWithBuiltins
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (FileDictWithBuiltins -> f FileDictWithBuiltins)
    -> TCState -> f TCState
    Lens' TCState FileDictWithBuiltins
    stFileDict TCMT m FileDictWithBuiltins
    -> (FileDictWithBuiltins -> File) -> TCMT m File
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> (FileDictWithBuiltins -> FileId -> File
    forall a. GetIdFile a => a -> FileId -> File
    `getIdFile` FileId
    fi)
      idFromFile :: File -> TCMT m FileId
    idFromFile = Lens' TCState FileDictWithBuiltins
    -> (FileDictWithBuiltins -> (FileId, FileDictWithBuiltins))
    -> TCMT m FileId
    forall (m :: * -> *) a r.
    (MonadTCState m, ReadTCState m) =>
    Lens' TCState a -> (a -> (r, a)) -> m r
    stateTCLens (FileDictWithBuiltins -> f FileDictWithBuiltins)
    -> TCState -> f TCState
    Lens' TCState FileDictWithBuiltins
    stFileDict ((FileDictWithBuiltins -> (FileId, FileDictWithBuiltins))
     -> TCMT m FileId)
    -> (File -> FileDictWithBuiltins -> (FileId, FileDictWithBuiltins))
    -> File
    -> TCMT m FileId
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . File -> FileDictWithBuiltins -> (FileId, FileDictWithBuiltins)
    registerFileIdWithBuiltin

    -- | Does the given 'FileId' belong to one of Agda's builtin modules?

    isBuiltinModule :: ReadTCState m => FileId -> m (Maybe IsBuiltinModule)
    isBuiltinModule :: forall (m :: * -> *).
    ReadTCState m =>
    FileId -> m (Maybe IsBuiltinModule)
    isBuiltinModule FileId
    fi = FileId -> BuiltinModuleIds -> Maybe IsBuiltinModule
    forall k a. Enum k => k -> EnumMap k a -> Maybe a
    EnumMap.lookup FileId
    fi (BuiltinModuleIds -> Maybe IsBuiltinModule)
    -> m BuiltinModuleIds -> m (Maybe IsBuiltinModule)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCState BuiltinModuleIds -> m BuiltinModuleIds
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (BuiltinModuleIds -> f BuiltinModuleIds) -> TCState -> f TCState
    Lens' TCState BuiltinModuleIds
    stBuiltinModuleIds

    -- | Does the given 'FileId' belong to one of Agda's builtin modules that only uses safe postulates?
    --
    -- Implies @isJust . 'isBuiltinModule'@.

    isBuiltinModuleWithSafePostulates :: ReadTCState m => FileId -> m Bool
    isBuiltinModuleWithSafePostulates :: forall (m :: * -> *). ReadTCState m => FileId -> m Bool
    isBuiltinModuleWithSafePostulates FileId
    fi = do
      FileId -> m (Maybe IsBuiltinModule)
    forall (m :: * -> *).
    ReadTCState m =>
    FileId -> m (Maybe IsBuiltinModule)
    isBuiltinModule FileId
    fi m (Maybe IsBuiltinModule)
    -> (Maybe IsBuiltinModule -> Bool) -> m Bool
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \case
        Maybe IsBuiltinModule
    Nothing                                -> Bool
    False
        Just IsBuiltinModule
    IsBuiltinModule                   -> Bool
    False
        Just IsBuiltinModule
    IsBuiltinModuleWithSafePostulates -> Bool
    True
        Just IsBuiltinModule
    IsPrimitiveModule                 -> Bool
    True

    -- | Does the given 'FileId' belong to one of Agda's magical primitive modules?
    --
    -- Implies 'isBuiltinModuleWithSafePostulates'.

    isPrimitiveModule :: ReadTCState m => FileId -> m Bool
    isPrimitiveModule :: forall (m :: * -> *). ReadTCState m => FileId -> m Bool
    isPrimitiveModule  FileId
    fi = do
      FileId -> m (Maybe IsBuiltinModule)
    forall (m :: * -> *).
    ReadTCState m =>
    FileId -> m (Maybe IsBuiltinModule)
    isBuiltinModule FileId
    fi m (Maybe IsBuiltinModule)
    -> (Maybe IsBuiltinModule -> Bool) -> m Bool
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \case
        Maybe IsBuiltinModule
    Nothing                                -> Bool
    False
        Just IsBuiltinModule
    IsBuiltinModule                   -> Bool
    False
        Just IsBuiltinModule
    IsBuiltinModuleWithSafePostulates -> Bool
    False
        Just IsBuiltinModule
    IsPrimitiveModule                 -> Bool
    True

    ---------------------------------------------------------------------------
    -- * Top level module
    ---------------------------------------------------------------------------

    -- | Tries to convert a raw top-level module name to a top-level
    -- module name.

    topLevelModuleName :: RawTopLevelModuleName -> TCM TopLevelModuleName
    topLevelModuleName :: RawTopLevelModuleName -> TCM TopLevelModuleName
    topLevelModuleName RawTopLevelModuleName
    raw = do
      hash <- RawTopLevelModuleName
    -> BiMap RawTopLevelModuleName ModuleNameHash
    -> Maybe ModuleNameHash
    forall k v. Ord k => k -> BiMap k v -> Maybe v
    BiMap.lookup RawTopLevelModuleName
    raw (BiMap RawTopLevelModuleName ModuleNameHash
     -> Maybe ModuleNameHash)
    -> TCMT IO (BiMap RawTopLevelModuleName ModuleNameHash)
    -> TCMT IO (Maybe ModuleNameHash)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCState (BiMap RawTopLevelModuleName ModuleNameHash)
    -> TCMT IO (BiMap RawTopLevelModuleName ModuleNameHash)
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (BiMap RawTopLevelModuleName ModuleNameHash
     -> f (BiMap RawTopLevelModuleName ModuleNameHash))
    -> TCState -> f TCState
    Lens' TCState (BiMap RawTopLevelModuleName ModuleNameHash)
    stTopLevelModuleNames
      case hash of
        Just ModuleNameHash
    hash -> TopLevelModuleName -> TCM TopLevelModuleName
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (RawTopLevelModuleName -> ModuleNameHash -> TopLevelModuleName
    unsafeTopLevelModuleName RawTopLevelModuleName
    raw ModuleNameHash
    hash)
        Maybe ModuleNameHash
    Nothing   -> do
          let hash :: ModuleNameHash
    hash = RawTopLevelModuleName -> ModuleNameHash
    hashRawTopLevelModuleName RawTopLevelModuleName
    raw
          Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (ModuleNameHash
    hash ModuleNameHash -> ModuleNameHash -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModuleNameHash
    noModuleNameHash) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ RawTopLevelModuleName -> Maybe RawTopLevelModuleName -> TypeError
    ModuleNameHashCollision RawTopLevelModuleName
    raw Maybe RawTopLevelModuleName
    forall a. Maybe a
    Nothing
          raw' <- Tag ModuleNameHash
    -> BiMap RawTopLevelModuleName ModuleNameHash
    -> Maybe RawTopLevelModuleName
    forall v k. Ord (Tag v) => Tag v -> BiMap k v -> Maybe k
    BiMap.invLookup Tag ModuleNameHash
    ModuleNameHash
    hash (BiMap RawTopLevelModuleName ModuleNameHash
     -> Maybe RawTopLevelModuleName)
    -> TCMT IO (BiMap RawTopLevelModuleName ModuleNameHash)
    -> TCMT IO (Maybe RawTopLevelModuleName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCState (BiMap RawTopLevelModuleName ModuleNameHash)
    -> TCMT IO (BiMap RawTopLevelModuleName ModuleNameHash)
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (BiMap RawTopLevelModuleName ModuleNameHash
     -> f (BiMap RawTopLevelModuleName ModuleNameHash))
    -> TCState -> f TCState
    Lens' TCState (BiMap RawTopLevelModuleName ModuleNameHash)
    stTopLevelModuleNames
          case raw' of
            Just RawTopLevelModuleName
    raw' -> TypeError -> TCM TopLevelModuleName
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM TopLevelModuleName)
    -> TypeError -> TCM TopLevelModuleName
    forall a b. (a -> b) -> a -> b
    $ RawTopLevelModuleName -> Maybe RawTopLevelModuleName -> TypeError
    ModuleNameHashCollision RawTopLevelModuleName
    raw (RawTopLevelModuleName -> Maybe RawTopLevelModuleName
    forall a. a -> Maybe a
    Just RawTopLevelModuleName
    raw')
            Maybe RawTopLevelModuleName
    Nothing -> do
              (BiMap RawTopLevelModuleName ModuleNameHash
     -> f (BiMap RawTopLevelModuleName ModuleNameHash))
    -> TCState -> f TCState
    Lens' TCState (BiMap RawTopLevelModuleName ModuleNameHash)
    stTopLevelModuleNames Lens' TCState (BiMap RawTopLevelModuleName ModuleNameHash)
    -> (BiMap RawTopLevelModuleName ModuleNameHash
        -> BiMap RawTopLevelModuleName ModuleNameHash)
    -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens'`
                RawTopLevelModuleName
    -> ModuleNameHash
    -> BiMap RawTopLevelModuleName ModuleNameHash
    -> BiMap RawTopLevelModuleName ModuleNameHash
    forall k v.
    (Ord k, HasTag v, Ord (Tag v)) =>
    k -> v -> BiMap k v -> BiMap k v
    BiMap.insert (KillRangeT RawTopLevelModuleName
    forall a. KillRange a => KillRangeT a
    killRange RawTopLevelModuleName
    raw) ModuleNameHash
    hash
              TopLevelModuleName -> TCM TopLevelModuleName
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (RawTopLevelModuleName -> ModuleNameHash -> TopLevelModuleName
    unsafeTopLevelModuleName RawTopLevelModuleName
    raw ModuleNameHash
    hash)

    -- | Set the top-level module. This affects the global module id of freshly
    --   generated names.

    setTopLevelModule :: TopLevelModuleName -> TCM ()
    setTopLevelModule :: TopLevelModuleName -> TCM ()
    setTopLevelModule TopLevelModuleName
    top = do
      let hash :: ModuleNameHash
    hash = TopLevelModuleName -> ModuleNameHash
    forall range. TopLevelModuleName' range -> ModuleNameHash
    moduleNameId TopLevelModuleName
    top
      (NameId -> f NameId) -> TCState -> f TCState
    Lens' TCState NameId
    stFreshNameId Lens' TCState NameId -> NameId -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> a -> m ()
    `setTCLens'` Word64 -> ModuleNameHash -> NameId
    NameId Word64
    0 ModuleNameHash
    hash
      (OpaqueId -> f OpaqueId) -> TCState -> f TCState
    Lens' TCState OpaqueId
    stFreshOpaqueId Lens' TCState OpaqueId -> OpaqueId -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> a -> m ()
    `setTCLens'` Word64 -> ModuleNameHash -> OpaqueId
    OpaqueId Word64
    0 ModuleNameHash
    hash
      (MetaId -> f MetaId) -> TCState -> f TCState
    Lens' TCState MetaId
    stFreshMetaId Lens' TCState MetaId -> MetaId -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> a -> m ()
    `setTCLens'`
        MetaId { metaId :: Word64
    metaId     = Word64
    0
               , metaModule :: ModuleNameHash
    metaModule = ModuleNameHash
    hash
               }

    -- | The name of the current top-level module, if any.
    {-# SPECIALIZE
        currentTopLevelModule :: TCM (Maybe TopLevelModuleName) #-}
    {-# SPECIALIZE
        currentTopLevelModule :: ReduceM (Maybe TopLevelModuleName) #-}
    currentTopLevelModule ::
      (MonadTCEnv m, ReadTCState m) => m (Maybe TopLevelModuleName)
    currentTopLevelModule :: forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    m (Maybe TopLevelModuleName)
    currentTopLevelModule = do
      Lens' TCState (Maybe (ModuleName, TopLevelModuleName))
    -> m (Maybe (ModuleName, TopLevelModuleName))
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (Maybe (ModuleName, TopLevelModuleName)
     -> f (Maybe (ModuleName, TopLevelModuleName)))
    -> TCState -> f TCState
    Lens' TCState (Maybe (ModuleName, TopLevelModuleName))
    stCurrentModule m (Maybe (ModuleName, TopLevelModuleName))
    -> (Maybe (ModuleName, TopLevelModuleName)
        -> m (Maybe TopLevelModuleName))
    -> m (Maybe TopLevelModuleName)
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Just (ModuleName
    _, TopLevelModuleName
    top) -> Maybe TopLevelModuleName -> m (Maybe TopLevelModuleName)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TopLevelModuleName -> Maybe TopLevelModuleName
    forall a. a -> Maybe a
    Just TopLevelModuleName
    top)
        Maybe (ModuleName, TopLevelModuleName)
    Nothing       -> [TopLevelModuleName] -> Maybe TopLevelModuleName
    forall a. [a] -> Maybe a
    listToMaybe ([TopLevelModuleName] -> Maybe TopLevelModuleName)
    -> m [TopLevelModuleName] -> m (Maybe TopLevelModuleName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TCEnv -> [TopLevelModuleName]) -> m [TopLevelModuleName]
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> [TopLevelModuleName]
    envImportPath

    -- | Use a different top-level module for a computation. Used when generating
    --   names for imported modules.
    withTopLevelModule :: TopLevelModuleName -> TCM a -> TCM a
    withTopLevelModule :: forall a. TopLevelModuleName -> TCM a -> TCM a
    withTopLevelModule TopLevelModuleName
    x TCM a
    m = do
      nextN <- Lens' TCState NameId -> TCMT IO NameId
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (NameId -> f NameId) -> TCState -> f TCState
    Lens' TCState NameId
    stFreshNameId
      nextM <- useTC stFreshMetaId
      nextO <- useTC stFreshOpaqueId
      setTopLevelModule x
      y <- m
      stFreshMetaId `setTCLens` nextM
      stFreshNameId `setTCLens` nextN
      stFreshOpaqueId `setTCLens` nextO
      return y

    {-# SPECIALIZE currentModuleNameHash :: TCM ModuleNameHash #-}
    currentModuleNameHash :: ReadTCState m => m ModuleNameHash
    currentModuleNameHash :: forall (m :: * -> *). ReadTCState m => m ModuleNameHash
    currentModuleNameHash = do
      NameId _ h <- Lens' TCState NameId -> m NameId
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (NameId -> f NameId) -> TCState -> f TCState
    Lens' TCState NameId
    stFreshNameId
      return h

    ---------------------------------------------------------------------------
    -- * Backends and foreign code
    ---------------------------------------------------------------------------

    -- | Look for a backend of the given name.

    lookupBackend :: ReadTCState m => BackendName -> m (Maybe Backend)
    lookupBackend :: forall (m :: * -> *).
    ReadTCState m =>
    BackendName -> m (Maybe Backend)
    lookupBackend BackendName
    name = Lens' TCState [Backend] -> m [Backend]
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC ([Backend] -> f [Backend]) -> TCState -> f TCState
    Lens' TCState [Backend]
    stBackends m [Backend] -> ([Backend] -> Maybe Backend) -> m (Maybe Backend)
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ [Backend]
    backends ->
      [Backend] -> Maybe Backend
    forall a. [a] -> Maybe a
    listToMaybe [ Backend
    b | b :: Backend
    b@(Backend Backend'_boot Definition (TCMT IO) opts env menv mod def
    b') <- [Backend]
    backends, Backend'_boot Definition (TCMT IO) opts env menv mod def
    -> BackendName
    forall definition (tcm :: * -> *) opts env menv mod def.
    Backend'_boot definition tcm opts env menv mod def -> BackendName
    backendName Backend'_boot Definition (TCMT IO) opts env menv mod def
    b' BackendName -> BackendName -> Bool
    forall a. Eq a => a -> a -> Bool
    == BackendName
    name ]

    -- | Get the currently active backend (if any).

    activeBackend :: TCM (Maybe Backend)
    activeBackend :: TCM (Maybe Backend)
    activeBackend = MaybeT (TCMT IO) Backend -> TCM (Maybe Backend)
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT (TCMT IO) Backend -> TCM (Maybe Backend))
    -> MaybeT (TCMT IO) Backend -> TCM (Maybe Backend)
    forall a b. (a -> b) -> a -> b
    $ do
      bname <- TCMT IO (Maybe BackendName) -> MaybeT (TCMT IO) BackendName
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (TCMT IO (Maybe BackendName) -> MaybeT (TCMT IO) BackendName)
    -> TCMT IO (Maybe BackendName) -> MaybeT (TCMT IO) BackendName
    forall a b. (a -> b) -> a -> b
    $ (TCEnv -> Maybe BackendName) -> TCMT IO (Maybe BackendName)
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Maybe BackendName
    envActiveBackendName
      lift $ fromMaybe __IMPOSSIBLE__ <$> lookupBackend bname

    -- | Ask the active backend whether a type may be erased.
    --   See issue #3732.

    activeBackendMayEraseType :: QName -> TCM Bool
    activeBackendMayEraseType :: QName -> TCM Bool
    activeBackendMayEraseType QName
    q = do
      Backend b <- Backend -> Maybe Backend -> Backend
    forall a. a -> Maybe a -> a
    fromMaybe Backend
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Backend -> Backend)
    -> TCM (Maybe Backend) -> TCMT IO Backend
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCM (Maybe Backend)
    activeBackend
      mayEraseType b q

    addForeignCode :: BackendName -> String -> TCM ()
    addForeignCode :: BackendName -> [Char] -> TCM ()
    addForeignCode BackendName
    backend [Char]
    code = do
      r <- (TCEnv -> Range) -> TCMT IO Range
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Range
    envRange  -- can't use TypeChecking.Monad.Trace.getCurrentRange without cycle
      modifyTCLens (stForeignCode . key backend) $
        Just . ForeignCodeStack . (ForeignCode r code :) . maybe [] getForeignCodeStack

    ---------------------------------------------------------------------------
    -- * Interaction output callback
    ---------------------------------------------------------------------------

    getInteractionOutputCallback :: ReadTCState m => m InteractionOutputCallback
    getInteractionOutputCallback :: forall (m :: * -> *). ReadTCState m => m InteractionOutputCallback
    getInteractionOutputCallback
      = (TCState -> InteractionOutputCallback)
    -> m InteractionOutputCallback
    forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
    getsTC ((TCState -> InteractionOutputCallback)
     -> m InteractionOutputCallback)
    -> (TCState -> InteractionOutputCallback)
    -> m InteractionOutputCallback
    forall a b. (a -> b) -> a -> b
    $ PersistentTCState -> InteractionOutputCallback
    stInteractionOutputCallback (PersistentTCState -> InteractionOutputCallback)
    -> (TCState -> PersistentTCState)
    -> TCState
    -> InteractionOutputCallback
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCState -> PersistentTCState
    stPersistentState

    appInteractionOutputCallback :: Response -> TCM ()
    appInteractionOutputCallback :: InteractionOutputCallback
    appInteractionOutputCallback Response
    r
      = TCMT IO InteractionOutputCallback
    forall (m :: * -> *). ReadTCState m => m InteractionOutputCallback
    getInteractionOutputCallback TCMT IO InteractionOutputCallback
    -> (InteractionOutputCallback -> TCM ()) -> TCM ()
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \ InteractionOutputCallback
    cb -> InteractionOutputCallback
    cb Response
    r

    setInteractionOutputCallback :: InteractionOutputCallback -> TCM ()
    setInteractionOutputCallback :: InteractionOutputCallback -> TCM ()
    setInteractionOutputCallback InteractionOutputCallback
    cb
      = (PersistentTCState -> PersistentTCState) -> TCM ()
    modifyPersistentState ((PersistentTCState -> PersistentTCState) -> TCM ())
    -> (PersistentTCState -> PersistentTCState) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ PersistentTCState
    s -> PersistentTCState
    s { stInteractionOutputCallback = cb }

    ---------------------------------------------------------------------------
    -- * Pattern synonyms
    ---------------------------------------------------------------------------

    getPatternSyns :: ReadTCState m => m PatternSynDefns
    getPatternSyns :: forall (m :: * -> *). ReadTCState m => m PatternSynDefns
    getPatternSyns = Lens' TCState PatternSynDefns -> m PatternSynDefns
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (PatternSynDefns -> f PatternSynDefns) -> TCState -> f TCState
    Lens' TCState PatternSynDefns
    stPatternSyns

    setPatternSyns :: PatternSynDefns -> TCM ()
    setPatternSyns :: PatternSynDefns -> TCM ()
    setPatternSyns PatternSynDefns
    m = (PatternSynDefns -> PatternSynDefns) -> TCM ()
    modifyPatternSyns (PatternSynDefns -> PatternSynDefns -> PatternSynDefns
    forall a b. a -> b -> a
    const PatternSynDefns
    m)

    -- | Lens for 'stPatternSyns'.
    modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()
    modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()
    modifyPatternSyns PatternSynDefns -> PatternSynDefns
    f = (PatternSynDefns -> f PatternSynDefns) -> TCState -> f TCState
    Lens' TCState PatternSynDefns
    stPatternSyns Lens' TCState PatternSynDefns
    -> (PatternSynDefns -> PatternSynDefns) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` PatternSynDefns -> PatternSynDefns
    f

    getPatternSynImports :: ReadTCState m => m PatternSynDefns
    getPatternSynImports :: forall (m :: * -> *). ReadTCState m => m PatternSynDefns
    getPatternSynImports = Lens' TCState PatternSynDefns -> m PatternSynDefns
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (PatternSynDefns -> f PatternSynDefns) -> TCState -> f TCState
    Lens' TCState PatternSynDefns
    stPatternSynImports

    -- | Get both local and imported pattern synonyms
    getAllPatternSyns :: ReadTCState m => m PatternSynDefns
    getAllPatternSyns :: forall (m :: * -> *). ReadTCState m => m PatternSynDefns
    getAllPatternSyns = PatternSynDefns -> PatternSynDefns -> PatternSynDefns
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union (PatternSynDefns -> PatternSynDefns -> PatternSynDefns)
    -> m PatternSynDefns -> m (PatternSynDefns -> PatternSynDefns)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PatternSynDefns
    forall (m :: * -> *). ReadTCState m => m PatternSynDefns
    getPatternSyns m (PatternSynDefns -> PatternSynDefns)
    -> m PatternSynDefns -> m PatternSynDefns
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> m PatternSynDefns
    forall (m :: * -> *). ReadTCState m => m PatternSynDefns
    getPatternSynImports

    lookupPatternSyn :: AmbiguousQName -> TCM PatternSynDefn
    lookupPatternSyn :: AmbiguousQName -> TCM PatternSynDefn
    lookupPatternSyn (AmbQ List1 QName
    xs) = do
      defs <- (QName -> TCM PatternSynDefn)
    -> List1 QName -> TCMT IO (NonEmpty PatternSynDefn)
    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) -> NonEmpty a -> f (NonEmpty b)
    traverse QName -> TCM PatternSynDefn
    lookupSinglePatternSyn List1 QName
    xs
      case mergePatternSynDefs defs of
        Just PatternSynDefn
    def   -> PatternSynDefn -> TCM PatternSynDefn
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return PatternSynDefn
    def
        Maybe PatternSynDefn
    Nothing    -> TypeError -> TCM PatternSynDefn
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM PatternSynDefn)
    -> TypeError -> TCM PatternSynDefn
    forall a b. (a -> b) -> a -> b
    $ List1 (QName, PatternSynDefn) -> TypeError
    CannotResolveAmbiguousPatternSynonym (List1 (QName, PatternSynDefn) -> TypeError)
    -> List1 (QName, PatternSynDefn) -> TypeError
    forall a b. (a -> b) -> a -> b
    $ List1 QName
    -> NonEmpty PatternSynDefn -> List1 (QName, PatternSynDefn)
    forall a b. NonEmpty a -> NonEmpty b -> NonEmpty (a, b)
    List1.zip List1 QName
    xs NonEmpty PatternSynDefn
    defs

    lookupSinglePatternSyn :: QName -> TCM PatternSynDefn
    lookupSinglePatternSyn :: QName -> TCM PatternSynDefn
    lookupSinglePatternSyn QName
    x = do
        s <- TCMT IO PatternSynDefns
    forall (m :: * -> *). ReadTCState m => m PatternSynDefns
    getPatternSyns
        case Map.lookup x s of
            Just PatternSynDefn
    d  -> PatternSynDefn -> TCM PatternSynDefn
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return PatternSynDefn
    d
            Maybe PatternSynDefn
    Nothing -> do
                si <- TCMT IO PatternSynDefns
    forall (m :: * -> *). ReadTCState m => m PatternSynDefns
    getPatternSynImports
                case Map.lookup x si of
                    Just PatternSynDefn
    d  -> PatternSynDefn -> TCM PatternSynDefn
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return PatternSynDefn
    d
                    Maybe PatternSynDefn
    Nothing -> QName -> TCM PatternSynDefn
    forall a. QName -> TCM a
    notInScopeError (QName -> TCM PatternSynDefn) -> QName -> TCM PatternSynDefn
    forall a b. (a -> b) -> a -> b
    $ QName -> QName
    qnameToConcrete QName
    x

    ---------------------------------------------------------------------------
    -- * Instance definitions
    ---------------------------------------------------------------------------

    -- | Lens for 'stInstanceDefs'.
    updateInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> (TCState -> TCState)
    updateInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCState -> TCState
    updateInstanceDefs = Lens' TCState TempInstanceTable
    -> (TempInstanceTable -> TempInstanceTable) -> TCState -> TCState
    forall o i. Lens' o i -> LensMap o i
    over (TempInstanceTable -> f TempInstanceTable) -> TCState -> f TCState
    Lens' TCState TempInstanceTable
    stInstanceDefs

    modifyInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCM ()
    modifyInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCM ()
    modifyInstanceDefs = (TCState -> TCState) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (TCState -> TCState) -> m ()
    modifyTC ((TCState -> TCState) -> TCM ())
    -> ((TempInstanceTable -> TempInstanceTable) -> TCState -> TCState)
    -> (TempInstanceTable -> TempInstanceTable)
    -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (TempInstanceTable -> TempInstanceTable) -> TCState -> TCState
    updateInstanceDefs

    getAllInstanceDefs :: TCM TempInstanceTable
    getAllInstanceDefs :: TCM TempInstanceTable
    getAllInstanceDefs = do
      (table, xs) <- Lens' TCState TempInstanceTable -> TCM TempInstanceTable
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (TempInstanceTable -> f TempInstanceTable) -> TCState -> f TCState
    Lens' TCState TempInstanceTable
    stInstanceDefs
      itable <- useTC (stImports . sigInstances)
      let table' = InstanceTable
    table InstanceTable -> InstanceTable -> InstanceTable
    forall a. Semigroup a => a -> a -> a
    <> InstanceTable
    itable
      () <- liftIO $ evaluate (rnf table')
      return (table', xs)

    getAnonInstanceDefs :: TCM (Set QName)
    getAnonInstanceDefs :: TCM (Set QName)
    getAnonInstanceDefs = TempInstanceTable -> Set QName
    forall a b. (a, b) -> b
    snd (TempInstanceTable -> Set QName)
    -> TCM TempInstanceTable -> TCM (Set QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCM TempInstanceTable
    getAllInstanceDefs

    -- | Remove an instance from the set of unresolved instances.
    clearUnknownInstance :: QName -> TCM ()
    clearUnknownInstance :: QName -> TCM ()
    clearUnknownInstance QName
    q = (TempInstanceTable -> TempInstanceTable) -> TCM ()
    modifyInstanceDefs ((TempInstanceTable -> TempInstanceTable) -> TCM ())
    -> (TempInstanceTable -> TempInstanceTable) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (Set QName -> Set QName) -> TempInstanceTable -> TempInstanceTable
    forall b d a. (b -> d) -> (a, b) -> (a, d)
    mapSnd ((Set QName -> Set QName)
     -> TempInstanceTable -> TempInstanceTable)
    -> (Set QName -> Set QName)
    -> TempInstanceTable
    -> TempInstanceTable
    forall a b. (a -> b) -> a -> b
    $ QName -> Set QName -> Set QName
    forall a. Ord a => a -> Set a -> Set a
    Set.delete QName
    q

    -- | Add an instance whose type is still unresolved.
    addUnknownInstance :: QName -> TCM ()
    addUnknownInstance :: QName -> TCM ()
    addUnknownInstance QName
    x = do
      [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.decl.instance" Int
    10 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        [Char]
    "adding definition " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    x [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
        [Char]
    " to the instance table (the type is not yet known)"
      (TempInstanceTable -> TempInstanceTable) -> TCM ()
    modifyInstanceDefs ((TempInstanceTable -> TempInstanceTable) -> TCM ())
    -> (TempInstanceTable -> TempInstanceTable) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (Set QName -> Set QName) -> TempInstanceTable -> TempInstanceTable
    forall b d a. (b -> d) -> (a, b) -> (a, d)
    mapSnd ((Set QName -> Set QName)
     -> TempInstanceTable -> TempInstanceTable)
    -> (Set QName -> Set QName)
    -> TempInstanceTable
    -> TempInstanceTable
    forall a b. (a -> b) -> a -> b
    $ QName -> Set QName -> Set QName
    forall a. Ord a => a -> Set a -> Set a
    Set.insert QName
    x