    -- | Data structures for the type checker.
    --
    -- Part of "Agda.TypeChecking.Monad.Base", extracted to avoid import cycles.

    module Agda.TypeChecking.Monad.Base.Types
      ( module Agda.TypeChecking.Monad.Base.Types
      , module X
      )
    where

    import Prelude hiding (null)

    import Control.DeepSeq                ( NFData )
    import Data.EnumMap                   ( EnumMap )
    import Data.Functor                   ( (<&>) )
    import Data.Map                       ( Map )
    import GHC.Generics                   ( Generic )

    import Agda.Syntax.Common
      ( LensArgInfo(..), LensCohesion, LensHiding, LensModality, LensOrigin, LensQuantity, LensRelevance, LensModalPolarity )

    import Agda.Syntax.Info               ( MetaNameSuggestion )
    import Agda.Syntax.Internal           ( Dom, MetaId, Name, Type )
    import Agda.Syntax.TopLevelModuleName as X ( TopLevelModuleName )

    import Agda.Utils.FileId              as X ( FileId, FileDictBuilder )
    import Agda.Utils.FileName            as X ( AbsolutePath )
    import Agda.Utils.Lens                ( Lens', (&&&), iso )
    import Agda.Utils.Null                ( Null(..) )

    ---------------------------------------------------------------------------
    -- * Context
    ---------------------------------------------------------------------------

    -- | The @Context@ is a stack of 'ContextEntry's.
    type Context = [ContextEntry]

    data ContextEntry
      = CtxVar
        { ContextEntry -> Name
    ceName :: Name
        , ContextEntry -> Dom Type
    ceType :: Dom Type
        }
      -- N.B. 2024-11-29 there might be CtxLet in the future.
      deriving (Int -> ContextEntry -> ShowS
    [ContextEntry] -> ShowS
    ContextEntry -> String
    (Int -> ContextEntry -> ShowS)
    -> (ContextEntry -> String)
    -> ([ContextEntry] -> ShowS)
    -> Show ContextEntry
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> ContextEntry -> ShowS
    showsPrec :: Int -> ContextEntry -> ShowS
    $cshow :: ContextEntry -> String
    show :: ContextEntry -> String
    $cshowList :: [ContextEntry] -> ShowS
    showList :: [ContextEntry] -> ShowS
    Show, (forall x. ContextEntry -> Rep ContextEntry x)
    -> (forall x. Rep ContextEntry x -> ContextEntry)
    -> Generic ContextEntry
    forall x. Rep ContextEntry x -> ContextEntry
    forall x. ContextEntry -> Rep ContextEntry x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. ContextEntry -> Rep ContextEntry x
    from :: forall x. ContextEntry -> Rep ContextEntry x
    $cto :: forall x. Rep ContextEntry x -> ContextEntry
    to :: forall x. Rep ContextEntry x -> ContextEntry
    Generic)

    instance LensArgInfo ContextEntry where
      getArgInfo :: ContextEntry -> ArgInfo
    getArgInfo (CtxVar Name
    _ Dom Type
    a) = Dom Type -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo Dom Type
    a
      mapArgInfo :: (ArgInfo -> ArgInfo) -> ContextEntry -> ContextEntry
    mapArgInfo ArgInfo -> ArgInfo
    f (CtxVar Name
    x Dom Type
    a) = Name -> Dom Type -> ContextEntry
    CtxVar Name
    x (Dom Type -> ContextEntry) -> Dom Type -> ContextEntry
    forall a b. (a -> b) -> a -> b
    $ (ArgInfo -> ArgInfo) -> Dom Type -> Dom Type
    forall a. LensArgInfo a => (ArgInfo -> ArgInfo) -> a -> a
    mapArgInfo ArgInfo -> ArgInfo
    f Dom Type
    a

    instance LensModality  ContextEntry
    instance LensRelevance ContextEntry
    instance LensCohesion  ContextEntry
    instance LensOrigin    ContextEntry
    instance LensQuantity  ContextEntry
    instance LensHiding    ContextEntry
    instance LensModalPolarity ContextEntry

    ---------------------------------------------------------------------------
    -- * Conversion
    ---------------------------------------------------------------------------

    data Comparison = CmpEq | CmpLeq
      deriving (Comparison -> Comparison -> Bool
    (Comparison -> Comparison -> Bool)
    -> (Comparison -> Comparison -> Bool) -> Eq Comparison
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Comparison -> Comparison -> Bool
    == :: Comparison -> Comparison -> Bool
    $c/= :: Comparison -> Comparison -> Bool
    /= :: Comparison -> Comparison -> Bool
    Eq, Int -> Comparison -> ShowS
    [Comparison] -> ShowS
    Comparison -> String
    (Int -> Comparison -> ShowS)
    -> (Comparison -> String)
    -> ([Comparison] -> ShowS)
    -> Show Comparison
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Comparison -> ShowS
    showsPrec :: Int -> Comparison -> ShowS
    $cshow :: Comparison -> String
    show :: Comparison -> String
    $cshowList :: [Comparison] -> ShowS
    showList :: [Comparison] -> ShowS
    Show, (forall x. Comparison -> Rep Comparison x)
    -> (forall x. Rep Comparison x -> Comparison) -> Generic Comparison
    forall x. Rep Comparison x -> Comparison
    forall x. Comparison -> Rep Comparison x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. Comparison -> Rep Comparison x
    from :: forall x. Comparison -> Rep Comparison x
    $cto :: forall x. Rep Comparison x -> Comparison
    to :: forall x. Rep Comparison x -> Comparison
    Generic)

    -- | Polarity for equality and subtype checking.
    data Polarity
      = Covariant      -- ^ monotone
      | Contravariant  -- ^ antitone
      | Invariant      -- ^ no information (mixed variance)
      | Nonvariant     -- ^ constant
      deriving (Int -> Polarity -> ShowS
    [Polarity] -> ShowS
    Polarity -> String
    (Int -> Polarity -> ShowS)
    -> (Polarity -> String) -> ([Polarity] -> ShowS) -> Show Polarity
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Polarity -> ShowS
    showsPrec :: Int -> Polarity -> ShowS
    $cshow :: Polarity -> String
    show :: Polarity -> String
    $cshowList :: [Polarity] -> ShowS
    showList :: [Polarity] -> ShowS
    Show, Polarity -> Polarity -> Bool
    (Polarity -> Polarity -> Bool)
    -> (Polarity -> Polarity -> Bool) -> Eq Polarity
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Polarity -> Polarity -> Bool
    == :: Polarity -> Polarity -> Bool
    $c/= :: Polarity -> Polarity -> Bool
    /= :: Polarity -> Polarity -> Bool
    Eq, (forall x. Polarity -> Rep Polarity x)
    -> (forall x. Rep Polarity x -> Polarity) -> Generic Polarity
    forall x. Rep Polarity x -> Polarity
    forall x. Polarity -> Rep Polarity x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. Polarity -> Rep Polarity x
    from :: forall x. Polarity -> Rep Polarity x
    $cto :: forall x. Rep Polarity x -> Polarity
    to :: forall x. Rep Polarity x -> Polarity
    Generic)

    ---------------------------------------------------------------------------
    -- * Cubical
    ---------------------------------------------------------------------------

    -- | Datatype representing a single boundary condition:
    --   x_0 = u_0, ... ,x_n = u_n ⊢ t = ?n es
    data IPFace' t = IPFace'
      { forall t. IPFace' t -> [(t, t)]
    faceEqns :: [(t, t)]
      , forall t. IPFace' t -> t
    faceRHS  :: t
      }

    ---------------------------------------------------------------------------
    -- * Highlighting
    ---------------------------------------------------------------------------

    -- | How much highlighting should be sent to the user interface?

    data HighlightingLevel
      = None
      | NonInteractive
      | Interactive
        -- ^ This includes both non-interactive highlighting and
        -- interactive highlighting of the expression that is currently
        -- being type-checked.
        deriving (HighlightingLevel -> HighlightingLevel -> Bool
    (HighlightingLevel -> HighlightingLevel -> Bool)
    -> (HighlightingLevel -> HighlightingLevel -> Bool)
    -> Eq HighlightingLevel
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: HighlightingLevel -> HighlightingLevel -> Bool
    == :: HighlightingLevel -> HighlightingLevel -> Bool
    $c/= :: HighlightingLevel -> HighlightingLevel -> Bool
    /= :: HighlightingLevel -> HighlightingLevel -> Bool
    Eq, Eq HighlightingLevel
    Eq HighlightingLevel =>
    (HighlightingLevel -> HighlightingLevel -> Ordering)
    -> (HighlightingLevel -> HighlightingLevel -> Bool)
    -> (HighlightingLevel -> HighlightingLevel -> Bool)
    -> (HighlightingLevel -> HighlightingLevel -> Bool)
    -> (HighlightingLevel -> HighlightingLevel -> Bool)
    -> (HighlightingLevel -> HighlightingLevel -> HighlightingLevel)
    -> (HighlightingLevel -> HighlightingLevel -> HighlightingLevel)
    -> Ord HighlightingLevel
    HighlightingLevel -> HighlightingLevel -> Bool
    HighlightingLevel -> HighlightingLevel -> Ordering
    HighlightingLevel -> HighlightingLevel -> HighlightingLevel
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: HighlightingLevel -> HighlightingLevel -> Ordering
    compare :: HighlightingLevel -> HighlightingLevel -> Ordering
    $c< :: HighlightingLevel -> HighlightingLevel -> Bool
    < :: HighlightingLevel -> HighlightingLevel -> Bool
    $c<= :: HighlightingLevel -> HighlightingLevel -> Bool
    <= :: HighlightingLevel -> HighlightingLevel -> Bool
    $c> :: HighlightingLevel -> HighlightingLevel -> Bool
    > :: HighlightingLevel -> HighlightingLevel -> Bool
    $c>= :: HighlightingLevel -> HighlightingLevel -> Bool
    >= :: HighlightingLevel -> HighlightingLevel -> Bool
    $cmax :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel
    max :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel
    $cmin :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel
    min :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel
    Ord, Int -> HighlightingLevel -> ShowS
    [HighlightingLevel] -> ShowS
    HighlightingLevel -> String
    (Int -> HighlightingLevel -> ShowS)
    -> (HighlightingLevel -> String)
    -> ([HighlightingLevel] -> ShowS)
    -> Show HighlightingLevel
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> HighlightingLevel -> ShowS
    showsPrec :: Int -> HighlightingLevel -> ShowS
    $cshow :: HighlightingLevel -> String
    show :: HighlightingLevel -> String
    $cshowList :: [HighlightingLevel] -> ShowS
    showList :: [HighlightingLevel] -> ShowS
    Show, ReadPrec [HighlightingLevel]
    ReadPrec HighlightingLevel
    Int -> ReadS HighlightingLevel
    ReadS [HighlightingLevel]
    (Int -> ReadS HighlightingLevel)
    -> ReadS [HighlightingLevel]
    -> ReadPrec HighlightingLevel
    -> ReadPrec [HighlightingLevel]
    -> Read HighlightingLevel
    forall a.
    (Int -> ReadS a)
    -> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
    $creadsPrec :: Int -> ReadS HighlightingLevel
    readsPrec :: Int -> ReadS HighlightingLevel
    $creadList :: ReadS [HighlightingLevel]
    readList :: ReadS [HighlightingLevel]
    $creadPrec :: ReadPrec HighlightingLevel
    readPrec :: ReadPrec HighlightingLevel
    $creadListPrec :: ReadPrec [HighlightingLevel]
    readListPrec :: ReadPrec [HighlightingLevel]
    Read, (forall x. HighlightingLevel -> Rep HighlightingLevel x)
    -> (forall x. Rep HighlightingLevel x -> HighlightingLevel)
    -> Generic HighlightingLevel
    forall x. Rep HighlightingLevel x -> HighlightingLevel
    forall x. HighlightingLevel -> Rep HighlightingLevel x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. HighlightingLevel -> Rep HighlightingLevel x
    from :: forall x. HighlightingLevel -> Rep HighlightingLevel x
    $cto :: forall x. Rep HighlightingLevel x -> HighlightingLevel
    to :: forall x. Rep HighlightingLevel x -> HighlightingLevel
    Generic)

    -- | How should highlighting be sent to the user interface?

    data HighlightingMethod
      = Direct
        -- ^ Via stdout.
      | Indirect
        -- ^ Both via files and via stdout.
        deriving (HighlightingMethod -> HighlightingMethod -> Bool
    (HighlightingMethod -> HighlightingMethod -> Bool)
    -> (HighlightingMethod -> HighlightingMethod -> Bool)
    -> Eq HighlightingMethod
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: HighlightingMethod -> HighlightingMethod -> Bool
    == :: HighlightingMethod -> HighlightingMethod -> Bool
    $c/= :: HighlightingMethod -> HighlightingMethod -> Bool
    /= :: HighlightingMethod -> HighlightingMethod -> Bool
    Eq, Int -> HighlightingMethod -> ShowS
    [HighlightingMethod] -> ShowS
    HighlightingMethod -> String
    (Int -> HighlightingMethod -> ShowS)
    -> (HighlightingMethod -> String)
    -> ([HighlightingMethod] -> ShowS)
    -> Show HighlightingMethod
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> HighlightingMethod -> ShowS
    showsPrec :: Int -> HighlightingMethod -> ShowS
    $cshow :: HighlightingMethod -> String
    show :: HighlightingMethod -> String
    $cshowList :: [HighlightingMethod] -> ShowS
    showList :: [HighlightingMethod] -> ShowS
    Show, ReadPrec [HighlightingMethod]
    ReadPrec HighlightingMethod
    Int -> ReadS HighlightingMethod
    ReadS [HighlightingMethod]
    (Int -> ReadS HighlightingMethod)
    -> ReadS [HighlightingMethod]
    -> ReadPrec HighlightingMethod
    -> ReadPrec [HighlightingMethod]
    -> Read HighlightingMethod
    forall a.
    (Int -> ReadS a)
    -> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
    $creadsPrec :: Int -> ReadS HighlightingMethod
    readsPrec :: Int -> ReadS HighlightingMethod
    $creadList :: ReadS [HighlightingMethod]
    readList :: ReadS [HighlightingMethod]
    $creadPrec :: ReadPrec HighlightingMethod
    readPrec :: ReadPrec HighlightingMethod
    $creadListPrec :: ReadPrec [HighlightingMethod]
    readListPrec :: ReadPrec [HighlightingMethod]
    Read, (forall x. HighlightingMethod -> Rep HighlightingMethod x)
    -> (forall x. Rep HighlightingMethod x -> HighlightingMethod)
    -> Generic HighlightingMethod
    forall x. Rep HighlightingMethod x -> HighlightingMethod
    forall x. HighlightingMethod -> Rep HighlightingMethod x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. HighlightingMethod -> Rep HighlightingMethod x
    from :: forall x. HighlightingMethod -> Rep HighlightingMethod x
    $cto :: forall x. Rep HighlightingMethod x -> HighlightingMethod
    to :: forall x. Rep HighlightingMethod x -> HighlightingMethod
    Generic)

    ---------------------------------------------------------------------------
    -- * Managing file names
    ---------------------------------------------------------------------------

    -- | Discern Agda's primitive modules from other file modules.
    --   @IsPrimitiveModule `implies` IsBuiltinModuleWithSafePostulate `implies` isBuiltinModule.

    --   Keep constructors in this order!
    data IsBuiltinModule
      = IsPrimitiveModule
          -- ^ Very magical module, e.g. @Agda.Primitive@.
      | IsBuiltinModuleWithSafePostulates
          -- ^ Safe module, e.g. @Agda.Builtin.Equality@.
      | IsBuiltinModule
          -- ^ Any builtin module.
      deriving (IsBuiltinModule -> IsBuiltinModule -> Bool
    (IsBuiltinModule -> IsBuiltinModule -> Bool)
    -> (IsBuiltinModule -> IsBuiltinModule -> Bool)
    -> Eq IsBuiltinModule
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: IsBuiltinModule -> IsBuiltinModule -> Bool
    == :: IsBuiltinModule -> IsBuiltinModule -> Bool
    $c/= :: IsBuiltinModule -> IsBuiltinModule -> Bool
    /= :: IsBuiltinModule -> IsBuiltinModule -> Bool
    Eq, Eq IsBuiltinModule
    Eq IsBuiltinModule =>
    (IsBuiltinModule -> IsBuiltinModule -> Ordering)
    -> (IsBuiltinModule -> IsBuiltinModule -> Bool)
    -> (IsBuiltinModule -> IsBuiltinModule -> Bool)
    -> (IsBuiltinModule -> IsBuiltinModule -> Bool)
    -> (IsBuiltinModule -> IsBuiltinModule -> Bool)
    -> (IsBuiltinModule -> IsBuiltinModule -> IsBuiltinModule)
    -> (IsBuiltinModule -> IsBuiltinModule -> IsBuiltinModule)
    -> Ord IsBuiltinModule
    IsBuiltinModule -> IsBuiltinModule -> Bool
    IsBuiltinModule -> IsBuiltinModule -> Ordering
    IsBuiltinModule -> IsBuiltinModule -> IsBuiltinModule
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: IsBuiltinModule -> IsBuiltinModule -> Ordering
    compare :: IsBuiltinModule -> IsBuiltinModule -> Ordering
    $c< :: IsBuiltinModule -> IsBuiltinModule -> Bool
    < :: IsBuiltinModule -> IsBuiltinModule -> Bool
    $c<= :: IsBuiltinModule -> IsBuiltinModule -> Bool
    <= :: IsBuiltinModule -> IsBuiltinModule -> Bool
    $c> :: IsBuiltinModule -> IsBuiltinModule -> Bool
    > :: IsBuiltinModule -> IsBuiltinModule -> Bool
    $c>= :: IsBuiltinModule -> IsBuiltinModule -> Bool
    >= :: IsBuiltinModule -> IsBuiltinModule -> Bool
    $cmax :: IsBuiltinModule -> IsBuiltinModule -> IsBuiltinModule
    max :: IsBuiltinModule -> IsBuiltinModule -> IsBuiltinModule
    $cmin :: IsBuiltinModule -> IsBuiltinModule -> IsBuiltinModule
    min :: IsBuiltinModule -> IsBuiltinModule -> IsBuiltinModule
    Ord, Int -> IsBuiltinModule -> ShowS
    [IsBuiltinModule] -> ShowS
    IsBuiltinModule -> String
    (Int -> IsBuiltinModule -> ShowS)
    -> (IsBuiltinModule -> String)
    -> ([IsBuiltinModule] -> ShowS)
    -> Show IsBuiltinModule
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> IsBuiltinModule -> ShowS
    showsPrec :: Int -> IsBuiltinModule -> ShowS
    $cshow :: IsBuiltinModule -> String
    show :: IsBuiltinModule -> String
    $cshowList :: [IsBuiltinModule] -> ShowS
    showList :: [IsBuiltinModule] -> ShowS
    Show, (forall x. IsBuiltinModule -> Rep IsBuiltinModule x)
    -> (forall x. Rep IsBuiltinModule x -> IsBuiltinModule)
    -> Generic IsBuiltinModule
    forall x. Rep IsBuiltinModule x -> IsBuiltinModule
    forall x. IsBuiltinModule -> Rep IsBuiltinModule x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. IsBuiltinModule -> Rep IsBuiltinModule x
    from :: forall x. IsBuiltinModule -> Rep IsBuiltinModule x
    $cto :: forall x. Rep IsBuiltinModule x -> IsBuiltinModule
    to :: forall x. Rep IsBuiltinModule x -> IsBuiltinModule
    Generic)

    -- | Collection of 'FileId's of primitive modules.

    type BuiltinModuleIds = EnumMap FileId IsBuiltinModule

    -- | Translation between 'AbsolutePath' and 'FileId' that also knows about Agda's builtin modules.

    data FileDictWithBuiltins = FileDictWithBuiltins
      { FileDictWithBuiltins -> FileDictBuilder
    fileDictBuilder  :: !FileDictBuilder
          -- ^ (Building a) translation between 'AbsolutePath' and 'FileId'.
      , FileDictWithBuiltins -> BuiltinModuleIds
    builtinModuleIds :: !BuiltinModuleIds
          -- ^ For the known 'FileId's, remember whether they refer to Agda's builtin modules.
      , FileDictWithBuiltins -> PrimitiveLibDir
    primitiveLibDir  :: !PrimitiveLibDir
          -- ^ The absolute path to the directory with the builtin modules.
          --   Needs to be set upon initialization.
      }
      deriving (forall x. FileDictWithBuiltins -> Rep FileDictWithBuiltins x)
    -> (forall x. Rep FileDictWithBuiltins x -> FileDictWithBuiltins)
    -> Generic FileDictWithBuiltins
    forall x. Rep FileDictWithBuiltins x -> FileDictWithBuiltins
    forall x. FileDictWithBuiltins -> Rep FileDictWithBuiltins x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. FileDictWithBuiltins -> Rep FileDictWithBuiltins x
    from :: forall x. FileDictWithBuiltins -> Rep FileDictWithBuiltins x
    $cto :: forall x. Rep FileDictWithBuiltins x -> FileDictWithBuiltins
    to :: forall x. Rep FileDictWithBuiltins x -> FileDictWithBuiltins
    Generic

    type PrimitiveLibDir = AbsolutePath

    -- | 'SourceFile's must exist and be registered in our file dictionary.

    newtype SourceFile = SourceFile { SourceFile -> FileId
    srcFileId :: FileId }
      deriving (SourceFile -> SourceFile -> Bool
    (SourceFile -> SourceFile -> Bool)
    -> (SourceFile -> SourceFile -> Bool) -> Eq SourceFile
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: SourceFile -> SourceFile -> Bool
    == :: SourceFile -> SourceFile -> Bool
    $c/= :: SourceFile -> SourceFile -> Bool
    /= :: SourceFile -> SourceFile -> Bool
    Eq, Eq SourceFile
    Eq SourceFile =>
    (SourceFile -> SourceFile -> Ordering)
    -> (SourceFile -> SourceFile -> Bool)
    -> (SourceFile -> SourceFile -> Bool)
    -> (SourceFile -> SourceFile -> Bool)
    -> (SourceFile -> SourceFile -> Bool)
    -> (SourceFile -> SourceFile -> SourceFile)
    -> (SourceFile -> SourceFile -> SourceFile)
    -> Ord SourceFile
    SourceFile -> SourceFile -> Bool
    SourceFile -> SourceFile -> Ordering
    SourceFile -> SourceFile -> SourceFile
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: SourceFile -> SourceFile -> Ordering
    compare :: SourceFile -> SourceFile -> Ordering
    $c< :: SourceFile -> SourceFile -> Bool
    < :: SourceFile -> SourceFile -> Bool
    $c<= :: SourceFile -> SourceFile -> Bool
    <= :: SourceFile -> SourceFile -> Bool
    $c> :: SourceFile -> SourceFile -> Bool
    > :: SourceFile -> SourceFile -> Bool
    $c>= :: SourceFile -> SourceFile -> Bool
    >= :: SourceFile -> SourceFile -> Bool
    $cmax :: SourceFile -> SourceFile -> SourceFile
    max :: SourceFile -> SourceFile -> SourceFile
    $cmin :: SourceFile -> SourceFile -> SourceFile
    min :: SourceFile -> SourceFile -> SourceFile
    Ord, Int -> SourceFile -> ShowS
    [SourceFile] -> ShowS
    SourceFile -> String
    (Int -> SourceFile -> ShowS)
    -> (SourceFile -> String)
    -> ([SourceFile] -> ShowS)
    -> Show SourceFile
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> SourceFile -> ShowS
    showsPrec :: Int -> SourceFile -> ShowS
    $cshow :: SourceFile -> String
    show :: SourceFile -> String
    $cshowList :: [SourceFile] -> ShowS
    showList :: [SourceFile] -> ShowS
    Show, (forall x. SourceFile -> Rep SourceFile x)
    -> (forall x. Rep SourceFile x -> SourceFile) -> Generic SourceFile
    forall x. Rep SourceFile x -> SourceFile
    forall x. SourceFile -> Rep SourceFile x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. SourceFile -> Rep SourceFile x
    from :: forall x. SourceFile -> Rep SourceFile x
    $cto :: forall x. Rep SourceFile x -> SourceFile
    to :: forall x. Rep SourceFile x -> SourceFile
    Generic)

    -- | Maps top-level module names to the corresponding source file ids.

    type ModuleToSourceId = Map TopLevelModuleName SourceFile

    data ModuleToSource = ModuleToSource
      { ModuleToSource -> FileDictWithBuiltins
    fileDict         :: !FileDictWithBuiltins
      , ModuleToSource -> ModuleToSourceId
    moduleToSourceId :: !ModuleToSourceId
      }

    -- ** Lenses

    lensFileDictFileDictBuilder :: Lens' FileDictWithBuiltins FileDictBuilder
    lensFileDictFileDictBuilder :: Lens' FileDictWithBuiltins FileDictBuilder
    lensFileDictFileDictBuilder FileDictBuilder -> f FileDictBuilder
    f FileDictWithBuiltins
    s = FileDictBuilder -> f FileDictBuilder
    f (FileDictWithBuiltins -> FileDictBuilder
    fileDictBuilder FileDictWithBuiltins
    s) f FileDictBuilder
    -> (FileDictBuilder -> FileDictWithBuiltins)
    -> f FileDictWithBuiltins
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ FileDictBuilder
    x -> FileDictWithBuiltins
    s { fileDictBuilder = x }

    lensFileDictBuiltinModuleIds :: Lens' FileDictWithBuiltins BuiltinModuleIds
    lensFileDictBuiltinModuleIds :: Lens' FileDictWithBuiltins BuiltinModuleIds
    lensFileDictBuiltinModuleIds BuiltinModuleIds -> f BuiltinModuleIds
    f FileDictWithBuiltins
    s = BuiltinModuleIds -> f BuiltinModuleIds
    f (FileDictWithBuiltins -> BuiltinModuleIds
    builtinModuleIds FileDictWithBuiltins
    s) f BuiltinModuleIds
    -> (BuiltinModuleIds -> FileDictWithBuiltins)
    -> f FileDictWithBuiltins
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ BuiltinModuleIds
    x -> FileDictWithBuiltins
    s { builtinModuleIds = x }

    lensFileDictPrimitiveLibDir :: Lens' FileDictWithBuiltins PrimitiveLibDir
    lensFileDictPrimitiveLibDir :: Lens' FileDictWithBuiltins PrimitiveLibDir
    lensFileDictPrimitiveLibDir PrimitiveLibDir -> f PrimitiveLibDir
    f FileDictWithBuiltins
    s = PrimitiveLibDir -> f PrimitiveLibDir
    f (FileDictWithBuiltins -> PrimitiveLibDir
    primitiveLibDir FileDictWithBuiltins
    s) f PrimitiveLibDir
    -> (PrimitiveLibDir -> FileDictWithBuiltins)
    -> f FileDictWithBuiltins
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ PrimitiveLibDir
    x -> FileDictWithBuiltins
    s { primitiveLibDir = x }

    lensPairModuleToSource :: Lens' (FileDictWithBuiltins, ModuleToSourceId) ModuleToSource
    lensPairModuleToSource :: Lens' (FileDictWithBuiltins, ModuleToSourceId) ModuleToSource
    lensPairModuleToSource = ((FileDictWithBuiltins, ModuleToSourceId) -> ModuleToSource)
    -> (ModuleToSource -> (FileDictWithBuiltins, ModuleToSourceId))
    -> Lens' (FileDictWithBuiltins, ModuleToSourceId) ModuleToSource
    forall o i. (o -> i) -> (i -> o) -> Lens' o i
    iso ((FileDictWithBuiltins -> ModuleToSourceId -> ModuleToSource)
    -> (FileDictWithBuiltins, ModuleToSourceId) -> ModuleToSource
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry FileDictWithBuiltins -> ModuleToSourceId -> ModuleToSource
    ModuleToSource) (ModuleToSource -> FileDictWithBuiltins
    fileDict (ModuleToSource -> FileDictWithBuiltins)
    -> (ModuleToSource -> ModuleToSourceId)
    -> ModuleToSource
    -> (FileDictWithBuiltins, ModuleToSourceId)
    forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
    forall (a :: * -> * -> *) b c c'.
    Arrow a =>
    a b c -> a b c' -> a b (c, c')
    &&& ModuleToSource -> ModuleToSourceId
    moduleToSourceId)

    ---------------------------------------------------------------------------
    -- * Meta variables
    ---------------------------------------------------------------------------

    -- | For printing, we couple a meta with its name suggestion.
    data NamedMeta = NamedMeta
      { NamedMeta -> String
    nmSuggestion :: MetaNameSuggestion
      , NamedMeta -> MetaId
    nmid         :: MetaId
      }

    -- Feel free to move more types from Agda.TypeChecking.Monad.Base here when needed...

    -- Null instances

    -- Andreas, 2024-11-10: Let's not have these instances because there is no default primLibDir:
    --
    -- instance Null FileDictWithBuiltins where
    --   empty = FileDictWithBuiltins empty empty __IMPOSSIBLE__
    --   null (FileDictWithBuiltins a b _primLibDir) = null a && null b
    --
    -- instance Null ModuleToSource where
    --   empty = ModuleToSource empty empty
    --   null (ModuleToSource dict m2s) = null dict && null m2s

    -- NFData instances

    instance NFData ContextEntry
    instance NFData FileDictWithBuiltins
    instance NFData SourceFile
    instance NFData IsBuiltinModule