    {-# LANGUAGE CPP #-}
    {-# LANGUAGE NondecreasingIndentation #-}

    {-| This module deals with finding imported modules and loading their
        interface files.
    -}
    module Agda.Interaction.Imports
      ( Mode, pattern ScopeCheck, pattern TypeCheck

      , CheckResult (CheckResult)
      , crModuleInfo
      , crInterface
      , crWarnings
      , crMode
      , crSource

      , Source(..)
      , scopeCheckImport
      , parseSource
      , typeCheckMain
      , getNonMainInterface
      , getNonMainModuleInfo
      , getInterface
      , importPrimitiveModules
      , raiseNonFatalErrors

      -- Currently only used by test/api/Issue1168.hs:
      , readInterface
      ) where

    import Prelude hiding (null)

    import Control.Monad.Except        ( MonadError(..), ExceptT, runExceptT, withExceptT )
    import Control.Monad.IO.Class      ( MonadIO(..) )
    import Control.Monad.State         ( MonadState(..), execStateT )
    import Control.Monad.Trans.Maybe
    import qualified Control.Exception as E

    import Data.Either
    import Data.List (intercalate)
    import qualified Data.List as List
    import Data.Maybe
    import Data.Map (Map)
    import qualified Data.Map as Map
    import qualified Data.HashMap.Strict as HMap
    import Data.Set (Set)
    import qualified Data.Set as Set
    import Data.Text (Text)
    import qualified Data.Text as T
    import qualified Data.Text.Lazy as TL

    import System.Directory (doesFileExist, removeFile)
    import System.FilePath  ( (</>) )

    import Agda.Benchmarking

    import qualified Agda.Syntax.Abstract as A
    import qualified Agda.Syntax.Concrete as C
    import Agda.Syntax.Concrete.Attribute
    import Agda.Syntax.Abstract.Name
    import Agda.Syntax.Common
    import Agda.Syntax.Common.Pretty hiding (Mode)
    import Agda.Syntax.Parser
    import Agda.Syntax.Position
    import Agda.Syntax.Scope.Base
    import Agda.Syntax.TopLevelModuleName
    import Agda.Syntax.Translation.ConcreteToAbstract
      ( TopLevel( TopLevel )
      , TopLevelInfo( TopLevelInfo, topLevelDecls, topLevelScope)
      , checkAttributes, concreteToAbstract_
      )
    import qualified Agda.Syntax.Translation.ConcreteToAbstract as CToA

    import Agda.TypeChecking.InstanceArguments
    import Agda.TypeChecking.Errors
    import Agda.TypeChecking.Warnings hiding (warnings)
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Rewriting.Confluence ( checkConfluenceOfRules, sortRulesOfSymbol )
    import Agda.TypeChecking.MetaVars ( openMetasToPostulates )
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Serialise
    import Agda.TypeChecking.Primitive
    import Agda.TypeChecking.Pretty as P
    import Agda.TypeChecking.DeadCode
    import qualified Agda.TypeChecking.Monad.Benchmark as Bench

    import Agda.TheTypeChecker

    import Agda.Interaction.BasicOps ( getGoals, showGoals )
    import Agda.Interaction.FindFile
    import Agda.Interaction.Highlighting.Generate
    import qualified Agda.Interaction.Highlighting.Precise as Highlighting ( convert )
    import Agda.Interaction.Highlighting.Vim
    import Agda.Interaction.Library
    import Agda.Interaction.Options
    import qualified Agda.Interaction.Options.Lenses as Lens
    import Agda.Interaction.Options.Warnings (unsolvedWarnings)
    import Agda.Interaction.Response
      (RemoveTokenBasedHighlighting(KeepHighlighting))

    import Agda.Utils.CallStack (HasCallStack)
    import Agda.Utils.FileName
    import Agda.Utils.Hash
    import Agda.Utils.IO.Binary
    import Agda.Utils.Lens
    import Agda.Utils.List ( nubOn )
    import Agda.Utils.Maybe
    import qualified Agda.Utils.Maybe.Strict as Strict
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import qualified Agda.Utils.ProfileOptions as Profile
    import Agda.Utils.Singleton
    import qualified Agda.Utils.Set1 as Set1
    import qualified Agda.Utils.Trie as Trie

    import Agda.Utils.Impossible

    -- | Whether to ignore interfaces (@.agdai@) other than built-in modules

    ignoreInterfaces :: HasOptions m => m Bool
    ignoreInterfaces :: forall (m :: * -> *). HasOptions m => m Bool
    ignoreInterfaces = CommandLineOptions -> Bool
    optIgnoreInterfaces (CommandLineOptions -> Bool) -> m CommandLineOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions

    -- | Whether to ignore all interface files (@.agdai@)

    ignoreAllInterfaces :: HasOptions m => m Bool
    ignoreAllInterfaces :: forall (m :: * -> *). HasOptions m => m Bool
    ignoreAllInterfaces = CommandLineOptions -> Bool
    optIgnoreAllInterfaces (CommandLineOptions -> Bool) -> m CommandLineOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions

    -- | The decorated source code.

    data Source = Source
      { Source -> Text
    srcText        :: TL.Text               -- ^ Source code.
      , Source -> FileType
    srcFileType    :: FileType              -- ^ Source file type
      , Source -> SourceFile
    srcOrigin      :: SourceFile            -- ^ Source location at the time of its parsing
      , Source -> Module
    srcModule      :: C.Module              -- ^ The parsed module.
      , Source -> TopLevelModuleName
    srcModuleName  :: TopLevelModuleName    -- ^ The top-level module name.
      , Source -> [AgdaLibFile]
    srcProjectLibs :: [AgdaLibFile]         -- ^ The .agda-lib file(s) of the project this file belongs to.
      , Source -> Attributes
    srcAttributes  :: !Attributes
        -- ^ Every encountered attribute.
      }

    -- | Parses a source file and prepares the 'Source' record.

    parseSource :: SourceFile -> TCM Source
    parseSource :: SourceFile -> TCM Source
    parseSource SourceFile
    sourceFile = Account (BenchPhase (TCMT IO)) -> TCM Source -> TCM Source
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (TCMT IO)
    Phase
    Bench.Parsing] (TCM Source -> TCM Source) -> TCM Source -> TCM Source
    forall a b. (a -> b) -> a -> b
    $ do
      -- Issue #7303:
      -- The parser previously used mdo to avoid the duplicate parsing for the
      -- bootstrapping of the TopLevelModuleName in Range.
      -- But that made ranges blackholes during parsing,
      -- introducing regression #7301, fragility of the API as observed in #7492,
      -- and debugging headaches as ranges could not be showed during parsing.
      -- Now we bite the bullet to parse the source twice,
      -- until a better management of ranges comes about.
      --
      -- (E.g. it is unclear why ranges need the file name/id in place
      -- so early, as all the ranges from one file have the same file id.
      -- It would be sufficient to fill in the file name/id when the mixing
      -- with other files starts, e.g. during scope checking.)

      f <- SourceFile -> TCMT IO AbsolutePath
    forall (m :: * -> *). MonadFileId m => SourceFile -> m AbsolutePath
    srcFilePath SourceFile
    sourceFile

      -- Read the source text.
      let rf0 = AbsolutePath -> Maybe TopLevelModuleName -> RangeFile
    mkRangeFile AbsolutePath
    f Maybe TopLevelModuleName
    forall a. Maybe a
    Nothing
      setCurrentRange (beginningOfFile rf0) do

      source <- runPM $ readFilePM rf0
      let txt = Text -> [Char]
    TL.unpack Text
    source

      -- Bootstrapping: parse the module name.
      parsedModName0 <- moduleName f . fst . fst =<< do
        runPMDropWarnings $ parseFile moduleParser rf0 txt

      -- Now parse again, with module name present to be filled into the ranges.
      let rf = AbsolutePath -> Maybe TopLevelModuleName -> RangeFile
    mkRangeFile AbsolutePath
    f (Maybe TopLevelModuleName -> RangeFile)
    -> Maybe TopLevelModuleName -> RangeFile
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleName -> Maybe TopLevelModuleName
    forall a. a -> Maybe a
    Just TopLevelModuleName
    parsedModName0
      ((parsedMod, attrs), fileType) <- runPM $ parseFile moduleParser rf txt
      parsedModName                  <- moduleName f parsedMod

      libs <- getAgdaLibFiles f parsedModName
      return Source
        { srcText        = source
        , srcFileType    = fileType
        , srcOrigin      = sourceFile
        , srcModule      = parsedMod
        , srcModuleName  = parsedModName
        , srcProjectLibs = libs
        , srcAttributes  = attrs
        }

    -- | Computes the module name of the top-level module in the given file.
    --
    -- If no top-level module name is given, then an attempt is made to
    -- use the file name as a module name.

    moduleName ::
         AbsolutePath
         -- ^ The path to the file.
      -> C.Module
         -- ^ The parsed module.
      -> TCM TopLevelModuleName
    moduleName :: AbsolutePath -> Module -> TCM TopLevelModuleName
    moduleName AbsolutePath
    file Module
    parsedModule = Account (BenchPhase (TCMT IO))
    -> TCM TopLevelModuleName -> TCM TopLevelModuleName
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (TCMT IO)
    Phase
    Bench.ModuleName] (TCM TopLevelModuleName -> TCM TopLevelModuleName)
    -> TCM TopLevelModuleName -> TCM TopLevelModuleName
    forall a b. (a -> b) -> a -> b
    $ do
      let defaultName :: [Char]
    defaultName = AbsolutePath -> [Char]
    rootNameModule AbsolutePath
    file
          raw :: RawTopLevelModuleName
    raw         = Module -> RawTopLevelModuleName
    rawTopLevelModuleNameForModule Module
    parsedModule
      RawTopLevelModuleName -> TCM TopLevelModuleName
    topLevelModuleName (RawTopLevelModuleName -> TCM TopLevelModuleName)
    -> TCMT IO RawTopLevelModuleName -> TCM TopLevelModuleName
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< if RawTopLevelModuleName -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName RawTopLevelModuleName
    raw
        then Range
    -> TCMT IO RawTopLevelModuleName -> TCMT IO RawTopLevelModuleName
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange (AbsolutePath -> Range
    rangeFromAbsolutePath AbsolutePath
    file) do
          m <- PM QName -> TCM QName
    forall a. PM a -> TCM a
    runPM ((QName, Attributes) -> QName
    forall a b. (a, b) -> a
    fst ((QName, Attributes) -> QName)
    -> PM (QName, Attributes) -> PM QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser QName -> [Char] -> PM (QName, Attributes)
    forall a. Parser a -> [Char] -> PM (a, Attributes)
    parse Parser QName
    moduleNameParser [Char]
    defaultName)
                 TCM QName -> (TCErr -> TCM QName) -> TCM QName
    forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \TCErr
    _ ->
               TypeError -> TCM QName
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM QName) -> TypeError -> TCM QName
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath -> InvalidFileNameReason -> TypeError
    InvalidFileName AbsolutePath
    file InvalidFileNameReason
    DoesNotCorrespondToValidModuleName
          case m of
            C.Qual{} ->
              TypeError -> TCMT IO RawTopLevelModuleName
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO RawTopLevelModuleName)
    -> TypeError -> TCMT IO RawTopLevelModuleName
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath -> InvalidFileNameReason -> TypeError
    InvalidFileName AbsolutePath
    file (InvalidFileNameReason -> TypeError)
    -> InvalidFileNameReason -> TypeError
    forall a b. (a -> b) -> a -> b
    $
                Text -> InvalidFileNameReason
    RootNameModuleNotAQualifiedModuleName (Text -> InvalidFileNameReason) -> Text -> InvalidFileNameReason
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Text
    T.pack [Char]
    defaultName
            C.QName{} ->
              RawTopLevelModuleName -> TCMT IO RawTopLevelModuleName
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (RawTopLevelModuleName -> TCMT IO RawTopLevelModuleName)
    -> RawTopLevelModuleName -> TCMT IO RawTopLevelModuleName
    forall a b. (a -> b) -> a -> b
    $ RawTopLevelModuleName
                { rawModuleNameRange :: Range
    rawModuleNameRange = QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    m
                , rawModuleNameParts :: TopLevelModuleNameParts
    rawModuleNameParts = Text -> TopLevelModuleNameParts
    forall el coll. Singleton el coll => el -> coll
    singleton ([Char] -> Text
    T.pack [Char]
    defaultName)
                , rawModuleNameInferred :: Bool
    rawModuleNameInferred = Bool
    True
                    -- Andreas, 2025-06-21, issue #7953:
                    -- Remember we made up this module name to improve errors.
                }
        else RawTopLevelModuleName -> TCMT IO RawTopLevelModuleName
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return RawTopLevelModuleName
    raw

    srcDefaultPragmas :: Source -> [OptionsPragma]
    srcDefaultPragmas :: Source -> [OptionsPragma]
    srcDefaultPragmas Source
    src = (AgdaLibFile -> OptionsPragma) -> [AgdaLibFile] -> [OptionsPragma]
    forall a b. (a -> b) -> [a] -> [b]
    map AgdaLibFile -> OptionsPragma
    _libPragmas (Source -> [AgdaLibFile]
    srcProjectLibs Source
    src)

    srcFilePragmas :: Source -> [OptionsPragma]
    srcFilePragmas :: Source -> [OptionsPragma]
    srcFilePragmas Source
    src = [OptionsPragma]
    pragmas
      where
      cpragmas :: [Pragma]
    cpragmas = Module -> [Pragma]
    C.modPragmas (Source -> Module
    srcModule Source
    src)
      pragmas :: [OptionsPragma]
    pragmas = [ OptionsPragma
                    { pragmaStrings :: [[Char]]
    pragmaStrings = [[Char]]
    opts
                    , pragmaRange :: Range
    pragmaRange   = Range
    r
                    }
                | C.OptionsPragma Range
    r [[Char]]
    opts <- [Pragma]
    cpragmas
                ]

    -- | Set options from a 'Source' pragma, using the source
    --   ranges of the pragmas for error reporting. Flag to check consistency.
    setOptionsFromSourcePragmas :: Bool -> Source -> TCM ()
    setOptionsFromSourcePragmas :: Bool -> Source -> TCM ()
    setOptionsFromSourcePragmas Bool
    checkOpts Source
    src = do
      (OptionsPragma -> TCM ()) -> [OptionsPragma] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ OptionsPragma -> TCM ()
    setOpts (Source -> [OptionsPragma]
    srcDefaultPragmas Source
    src)
      (OptionsPragma -> TCM ()) -> [OptionsPragma] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ OptionsPragma -> TCM ()
    setOpts (Source -> [OptionsPragma]
    srcFilePragmas    Source
    src)
      where
        setOpts :: OptionsPragma -> TCM ()
    setOpts | Bool
    checkOpts = OptionsPragma -> TCM ()
    checkAndSetOptionsFromPragma
                | Bool
    otherwise = OptionsPragma -> TCM ()
    setOptionsFromPragma

    -- | Is the aim to type-check the top-level module, or only to
    -- scope-check it?

    data Mode
      = ScopeCheck
      | TypeCheck
      deriving (Mode -> Mode -> Bool
    (Mode -> Mode -> Bool) -> (Mode -> Mode -> Bool) -> Eq Mode
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Mode -> Mode -> Bool
    == :: Mode -> Mode -> Bool
    $c/= :: Mode -> Mode -> Bool
    /= :: Mode -> Mode -> Bool
    Eq, Int -> Mode -> ShowS
    [Mode] -> ShowS
    Mode -> [Char]
    (Int -> Mode -> ShowS)
    -> (Mode -> [Char]) -> ([Mode] -> ShowS) -> Show Mode
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Mode -> ShowS
    showsPrec :: Int -> Mode -> ShowS
    $cshow :: Mode -> [Char]
    show :: Mode -> [Char]
    $cshowList :: [Mode] -> ShowS
    showList :: [Mode] -> ShowS
    Show)

    -- | Are we loading the interface for the user-loaded file
    --   or for an import?
    data MainInterface
      = MainInterface Mode -- ^ For the main file.
                           --
                           --   In this case state changes inflicted by
                           --   'createInterface' are preserved.
      | NotMainInterface   -- ^ For an imported file.
                           --
                           --   In this case state changes inflicted by
                           --   'createInterface' are not preserved.
      deriving (MainInterface -> MainInterface -> Bool
    (MainInterface -> MainInterface -> Bool)
    -> (MainInterface -> MainInterface -> Bool) -> Eq MainInterface
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: MainInterface -> MainInterface -> Bool
    == :: MainInterface -> MainInterface -> Bool
    $c/= :: MainInterface -> MainInterface -> Bool
    /= :: MainInterface -> MainInterface -> Bool
    Eq, Int -> MainInterface -> ShowS
    [MainInterface] -> ShowS
    MainInterface -> [Char]
    (Int -> MainInterface -> ShowS)
    -> (MainInterface -> [Char])
    -> ([MainInterface] -> ShowS)
    -> Show MainInterface
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> MainInterface -> ShowS
    showsPrec :: Int -> MainInterface -> ShowS
    $cshow :: MainInterface -> [Char]
    show :: MainInterface -> [Char]
    $cshowList :: [MainInterface] -> ShowS
    showList :: [MainInterface] -> ShowS
    Show)

    -- | Should state changes inflicted by 'createInterface' be preserved?

    includeStateChanges :: MainInterface -> Bool
    includeStateChanges :: MainInterface -> Bool
    includeStateChanges (MainInterface Mode
    _) = Bool
    True
    includeStateChanges MainInterface
    NotMainInterface  = Bool
    False

    -- | The kind of interface produced by 'createInterface'
    moduleCheckMode :: MainInterface -> ModuleCheckMode
    moduleCheckMode :: MainInterface -> ModuleCheckMode
    moduleCheckMode = \case
        MainInterface Mode
    TypeCheck                       -> ModuleCheckMode
    ModuleTypeChecked
        MainInterface
    NotMainInterface                              -> ModuleCheckMode
    ModuleTypeChecked
        MainInterface Mode
    ScopeCheck                      -> ModuleCheckMode
    ModuleScopeChecked

    -- | Merge an interface into the current proof state.
    mergeInterface :: Interface -> TCM ()
    mergeInterface :: Interface -> TCM ()
    mergeInterface Interface
    i = do
        let sig :: Signature
    sig     = Interface -> Signature
    iSignature Interface
    i
            builtin :: [(SomeBuiltin, Builtin (PrimitiveId, QName))]
    builtin = Map SomeBuiltin (Builtin (PrimitiveId, QName))
    -> [(SomeBuiltin, Builtin (PrimitiveId, QName))]
    forall k a. Map k a -> [(k, a)]
    Map.toAscList (Map SomeBuiltin (Builtin (PrimitiveId, QName))
     -> [(SomeBuiltin, Builtin (PrimitiveId, QName))])
    -> Map SomeBuiltin (Builtin (PrimitiveId, QName))
    -> [(SomeBuiltin, Builtin (PrimitiveId, QName))]
    forall a b. (a -> b) -> a -> b
    $ Interface -> Map SomeBuiltin (Builtin (PrimitiveId, QName))
    iBuiltin Interface
    i
            primOrBi :: (a, Builtin a) -> Either a (a, Builtin pf)
    primOrBi = \case
              (a
    _, Prim a
    x)                     -> a -> Either a (a, Builtin pf)
    forall a b. a -> Either a b
    Left a
    x
              (a
    x, Builtin Term
    t)                  -> (a, Builtin pf) -> Either a (a, Builtin pf)
    forall a b. b -> Either a b
    Right (a
    x, Term -> Builtin pf
    forall pf. Term -> Builtin pf
    Builtin Term
    t)
              (a
    x, BuiltinRewriteRelations Set QName
    xs) -> (a, Builtin pf) -> Either a (a, Builtin pf)
    forall a b. b -> Either a b
    Right (a
    x, Set QName -> Builtin pf
    forall pf. Set QName -> Builtin pf
    BuiltinRewriteRelations Set QName
    xs)
            ([(PrimitiveId, QName)]
    prim, [(SomeBuiltin, Builtin PrimFun)]
    bi') = [Either (PrimitiveId, QName) (SomeBuiltin, Builtin PrimFun)]
    -> ([(PrimitiveId, QName)], [(SomeBuiltin, Builtin PrimFun)])
    forall a b. [Either a b] -> ([a], [b])
    partitionEithers ([Either (PrimitiveId, QName) (SomeBuiltin, Builtin PrimFun)]
     -> ([(PrimitiveId, QName)], [(SomeBuiltin, Builtin PrimFun)]))
    -> [Either (PrimitiveId, QName) (SomeBuiltin, Builtin PrimFun)]
    -> ([(PrimitiveId, QName)], [(SomeBuiltin, Builtin PrimFun)])
    forall a b. (a -> b) -> a -> b
    $ ((SomeBuiltin, Builtin (PrimitiveId, QName))
     -> Either (PrimitiveId, QName) (SomeBuiltin, Builtin PrimFun))
    -> [(SomeBuiltin, Builtin (PrimitiveId, QName))]
    -> [Either (PrimitiveId, QName) (SomeBuiltin, Builtin PrimFun)]
    forall a b. (a -> b) -> [a] -> [b]
    map (SomeBuiltin, Builtin (PrimitiveId, QName))
    -> Either (PrimitiveId, QName) (SomeBuiltin, Builtin PrimFun)
    forall {a} {a} {pf}. (a, Builtin a) -> Either a (a, Builtin pf)
    primOrBi [(SomeBuiltin, Builtin (PrimitiveId, QName))]
    builtin
            bi :: Map SomeBuiltin (Builtin PrimFun)
    bi      = [(SomeBuiltin, Builtin PrimFun)]
    -> Map SomeBuiltin (Builtin PrimFun)
    forall k a. [(k, a)] -> Map k a
    Map.fromDistinctAscList [(SomeBuiltin, Builtin PrimFun)]
    bi'
            warns :: Set TCWarning
    warns   = Interface -> Set TCWarning
    iWarnings Interface
    i
        bs <- (TCState -> Map SomeBuiltin (Builtin PrimFun))
    -> TCMT IO (Map SomeBuiltin (Builtin PrimFun))
    forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
    getsTC TCState -> Map SomeBuiltin (Builtin PrimFun)
    stBuiltinThings
        reportSLn "import.iface.merge" 10 $ "Merging interface " ++ prettyShow (iTopLevelModuleName i)
        reportSLn "import.iface.merge" 20 $
          "  Current builtins " ++ show (Map.keys bs) ++ "\n" ++
          "  New builtins     " ++ show (Map.keys bi)
        let check (BuiltinName BuiltinId
    b) (Builtin Term
    x) (Builtin Term
    y)
                  | Term
    x Term -> Term -> Bool
    forall a. Eq a => a -> a -> Bool
    == Term
    y    = () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                  | Bool
    otherwise = TypeError -> m ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m ()) -> TypeError -> m ()
    forall a b. (a -> b) -> a -> b
    $ BuiltinId -> Term -> Term -> TypeError
    DuplicateBuiltinBinding BuiltinId
    b Term
    x Term
    y
            check SomeBuiltin
    _ (BuiltinRewriteRelations Set QName
    xs) (BuiltinRewriteRelations Set QName
    ys) = () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            check SomeBuiltin
    _ Builtin pf
    _ Builtin pf
    _ = m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        sequence_ $ Map.intersectionWithKey check bs bi
        addImportedThings
          sig
          (iMetaBindings i)
          bi
          (iPatternSyns i)
          (iDisplayForms i)
          (iUserWarnings i)
          (iPartialDefs i)
          warns
          (iOpaqueBlocks i)
          (iOpaqueNames i)
        reportSLn "import.iface.merge" 50 $
          "  Rebinding primitives " ++ show prim
        mapM_ rebind prim
        whenJustM (optConfluenceCheck <$> pragmaOptions) \ ConfluenceCheck
    confChk -> do
          let rews :: [RewriteRule]
    rews = [[RewriteRule]] -> [RewriteRule]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[RewriteRule]] -> [RewriteRule])
    -> [[RewriteRule]] -> [RewriteRule]
    forall a b. (a -> b) -> a -> b
    $ HashMap QName [RewriteRule] -> [[RewriteRule]]
    forall k v. HashMap k v -> [v]
    HMap.elems (HashMap QName [RewriteRule] -> [[RewriteRule]])
    -> HashMap QName [RewriteRule] -> [[RewriteRule]]
    forall a b. (a -> b) -> a -> b
    $ Signature
    sig Signature
    -> Lens' Signature (HashMap QName [RewriteRule])
    -> HashMap QName [RewriteRule]
    forall o i. o -> Lens' o i -> i
    ^. (HashMap QName [RewriteRule] -> f (HashMap QName [RewriteRule]))
    -> Signature -> f Signature
    Lens' Signature (HashMap QName [RewriteRule])
    sigRewriteRules
          [Char] -> Int -> TCM () -> TCM ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
    verboseS [Char]
    "import.iface.confluence" Int
    20 do
            if [RewriteRule] -> Bool
    forall a. Null a => a -> Bool
    null [RewriteRule]
    rews then [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "" Int
    1 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  No rewrite rules imported"
            else do
              [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "" Int
    1 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    P.vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ (TCMT IO Doc -> TCMT IO Doc) -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    P.nest Int
    2) ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $
                TCMT IO Doc
    "Checking confluence of imported rewrite rules" TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. a -> [a] -> [a]
    :
                (RewriteRule -> TCMT IO Doc) -> [RewriteRule] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ((TCMT IO Doc
    "-" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    P.<+>) (TCMT IO Doc -> TCMT IO Doc)
    -> (RewriteRule -> TCMT IO Doc) -> RewriteRule -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM (QName -> TCMT IO Doc)
    -> (RewriteRule -> QName) -> RewriteRule -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RewriteRule -> QName
    rewName) [RewriteRule]
    rews

          -- Andreas, 2025-06-28, PR #7934 and issue #7969:
          -- Global confluence checker requires rules to be sorted
          -- according to the generality of their lhs
          Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (ConfluenceCheck
    confChk ConfluenceCheck -> ConfluenceCheck -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConfluenceCheck
    GlobalConfluenceCheck) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            [QName] -> (QName -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ ((QName -> QName) -> [QName] -> [QName]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    nubOn QName -> QName
    forall a. a -> a
    id ([QName] -> [QName]) -> [QName] -> [QName]
    forall a b. (a -> b) -> a -> b
    $ (RewriteRule -> QName) -> [RewriteRule] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map RewriteRule -> QName
    rewHead [RewriteRule]
    rews) QName -> TCM ()
    sortRulesOfSymbol
          ConfluenceCheck -> [RewriteRule] -> TCM ()
    checkConfluenceOfRules ConfluenceCheck
    confChk [RewriteRule]
    rews
        where
            rebind :: (PrimitiveId, QName) -> TCM ()
    rebind (PrimitiveId
    x, QName
    q) = do
                PrimImpl _ pf <- PrimitiveId -> TCM PrimitiveImpl
    lookupPrimitiveFunction PrimitiveId
    x
                stImportedBuiltins `modifyTCLens` Map.insert (someBuiltin x) (Prim pf{ primFunName = q })

    addImportedThings
      :: Signature
      -> RemoteMetaStore
      -> BuiltinThings
      -> A.PatternSynDefns
      -> DisplayForms
      -> UserWarnings      -- ^ Imported user warnings
      -> Set QName             -- ^ Name of imported definitions which are partial
      -> Set TCWarning
      -> Map OpaqueId OpaqueBlock
      -> Map QName OpaqueId
      -> TCM ()
    addImportedThings :: Signature
    -> RemoteMetaStore
    -> Map SomeBuiltin (Builtin PrimFun)
    -> PatternSynDefns
    -> DisplayForms
    -> UserWarnings
    -> Set QName
    -> Set TCWarning
    -> Map OpaqueId OpaqueBlock
    -> Map QName OpaqueId
    -> TCM ()
    addImportedThings Signature
    isig RemoteMetaStore
    metas Map SomeBuiltin (Builtin PrimFun)
    ibuiltin PatternSynDefns
    patsyns DisplayForms
    display UserWarnings
    userwarn
                      Set QName
    partialdefs Set TCWarning
    warnings Map OpaqueId OpaqueBlock
    oblock Map QName OpaqueId
    oid = do
      (Signature -> f Signature) -> TCState -> f TCState
    Lens' TCState Signature
    stImports              Lens' TCState Signature -> (Signature -> Signature) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` \ Signature
    imp -> Signature -> Signature -> Signature
    unionSignature Signature
    imp Signature
    isig
      (RemoteMetaStore -> f RemoteMetaStore) -> TCState -> f TCState
    Lens' TCState RemoteMetaStore
    stImportedMetaStore    Lens' TCState RemoteMetaStore
    -> (RemoteMetaStore -> RemoteMetaStore) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` RemoteMetaStore -> RemoteMetaStore -> RemoteMetaStore
    forall k v. Eq k => HashMap k v -> HashMap k v -> HashMap k v
    HMap.union RemoteMetaStore
    metas
      (Map SomeBuiltin (Builtin PrimFun)
     -> f (Map SomeBuiltin (Builtin PrimFun)))
    -> TCState -> f TCState
    Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
    stImportedBuiltins     Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
    -> (Map SomeBuiltin (Builtin PrimFun)
        -> Map SomeBuiltin (Builtin PrimFun))
    -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` \ Map SomeBuiltin (Builtin PrimFun)
    imp -> Map SomeBuiltin (Builtin PrimFun)
    -> Map SomeBuiltin (Builtin PrimFun)
    -> Map SomeBuiltin (Builtin PrimFun)
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union Map SomeBuiltin (Builtin PrimFun)
    imp Map SomeBuiltin (Builtin PrimFun)
    ibuiltin
      (UserWarnings -> f UserWarnings) -> TCState -> f TCState
    Lens' TCState UserWarnings
    stImportedUserWarnings Lens' TCState UserWarnings
    -> (UserWarnings -> UserWarnings) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` \ UserWarnings
    imp -> UserWarnings -> UserWarnings -> UserWarnings
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union UserWarnings
    imp UserWarnings
    userwarn
      (Set QName -> f (Set QName)) -> TCState -> f TCState
    Lens' TCState (Set QName)
    stImportedPartialDefs  Lens' TCState (Set QName) -> (Set QName -> Set QName) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` \ Set QName
    imp -> Set QName -> Set QName -> Set QName
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union Set QName
    imp Set QName
    partialdefs
      (PatternSynDefns -> f PatternSynDefns) -> TCState -> f TCState
    Lens' TCState PatternSynDefns
    stPatternSynImports    Lens' TCState PatternSynDefns
    -> (PatternSynDefns -> PatternSynDefns) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` \ PatternSynDefns
    imp -> PatternSynDefns -> PatternSynDefns -> PatternSynDefns
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union PatternSynDefns
    imp PatternSynDefns
    patsyns
      (DisplayForms -> f DisplayForms) -> TCState -> f TCState
    Lens' TCState DisplayForms
    stImportedDisplayForms Lens' TCState DisplayForms
    -> (DisplayForms -> DisplayForms) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` \ DisplayForms
    imp -> ([LocalDisplayForm] -> [LocalDisplayForm] -> [LocalDisplayForm])
    -> DisplayForms -> DisplayForms -> DisplayForms
    forall k v.
    Eq k =>
    (v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
    HMap.unionWith [LocalDisplayForm] -> [LocalDisplayForm] -> [LocalDisplayForm]
    forall a. [a] -> [a] -> [a]
    (++) DisplayForms
    imp DisplayForms
    display
      (Set TCWarning -> f (Set TCWarning)) -> TCState -> f TCState
    Lens' TCState (Set TCWarning)
    stTCWarnings           Lens' TCState (Set TCWarning)
    -> (Set TCWarning -> Set TCWarning) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` \ Set TCWarning
    imp -> Set TCWarning -> Set TCWarning -> Set TCWarning
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union Set TCWarning
    imp Set TCWarning
    warnings
      (Map OpaqueId OpaqueBlock -> f (Map OpaqueId OpaqueBlock))
    -> TCState -> f TCState
    Lens' TCState (Map OpaqueId OpaqueBlock)
    stOpaqueBlocks         Lens' TCState (Map OpaqueId OpaqueBlock)
    -> (Map OpaqueId OpaqueBlock -> Map OpaqueId OpaqueBlock) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` \ Map OpaqueId OpaqueBlock
    imp -> Map OpaqueId OpaqueBlock
    imp Map OpaqueId OpaqueBlock
    -> Map OpaqueId OpaqueBlock -> Map OpaqueId OpaqueBlock
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    `Map.union` Map OpaqueId OpaqueBlock
    oblock
      (Map QName OpaqueId -> f (Map QName OpaqueId))
    -> TCState -> f TCState
    Lens' TCState (Map QName OpaqueId)
    stOpaqueIds            Lens' TCState (Map QName OpaqueId)
    -> (Map QName OpaqueId -> Map QName OpaqueId) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    `modifyTCLens` \ Map QName OpaqueId
    imp -> Map QName OpaqueId
    imp Map QName OpaqueId -> Map QName OpaqueId -> Map QName OpaqueId
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    `Map.union` Map QName OpaqueId
    oid

    -- | Scope checks the given module, generating an interface or retrieving an existing one.
    --   Returns the module name and exported scope from the interface.
    --
    scopeCheckImport ::
         TopLevelModuleName
      -> TCM (ModuleName, Map ModuleName Scope)
    scopeCheckImport :: TopLevelModuleName -> TCM (ModuleName, Map ModuleName Scope)
    scopeCheckImport TopLevelModuleName
    top = do
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.scope" Int
    15 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Scope checking " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ TopLevelModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow TopLevelModuleName
    top
        [Char] -> Int -> TCM () -> TCM ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
    verboseS [Char]
    "import.scope" Int
    30 (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          visited <- Doc -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow (Doc -> [Char]) -> TCMT IO Doc -> TCMT IO [Char]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Doc
    forall (m :: * -> *). ReadTCState m => m Doc
    getPrettyVisitedModules
          reportSLn "import.scope" 30 $ "  visited: " ++ visited
        -- Since scopeCheckImport is called from the scope checker,
        -- we need to reimburse her account.
        i <- Account (BenchPhase (TCMT IO))
    -> TCMT IO Interface -> TCMT IO Interface
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [] (TCMT IO Interface -> TCMT IO Interface)
    -> TCMT IO Interface -> TCMT IO Interface
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleName -> Maybe Source -> TCMT IO Interface
    getNonMainInterface TopLevelModuleName
    top Maybe Source
    forall a. Maybe a
    Nothing
        addImport top

        -- Print list of imported modules in current state.
        verboseS "import.iface.imports" 10 do
          imports <- Set.toList <$> useTC stImportedModules
          reportSLn "import.iface.imports" 10 $ intercalate "\n" $
            unwords [prettyShow top, "added, all imports:"] :
            map (\ TopLevelModuleName
    x -> [[Char]] -> [Char]
    unwords [ [Char]
    " ", [Char]
    "-", TopLevelModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow TopLevelModuleName
    x ]) imports

        -- Print list of transitively imported modules in current state.
        verboseS "import.iface.imports" 20 do
          imports <- Set.toList <$> useTC stImportedModulesTransitive
          reportSLn "import.iface.imports" 10 $ intercalate "\n" $
            unwords [prettyShow top, "added, all transitive imports:"] :
            map (\ TopLevelModuleName
    x -> [[Char]] -> [Char]
    unwords [ [Char]
    " ", [Char]
    "-", TopLevelModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow TopLevelModuleName
    x ]) imports

        -- If that interface was supposed to raise a warning on import, do so.
        whenJust (iImportWarning i) $ warning . UserWarning

        -- let s = publicModules $ iInsideScope i
        let s = Interface -> Map ModuleName Scope
    iScope Interface
    i
        return (iModuleName i, s)

    -- | If the module has already been visited (without warnings), then
    -- its interface is returned directly. Otherwise the computation is
    -- used to find the interface and the computed interface is stored for
    -- potential later use.

    alreadyVisited :: TopLevelModuleName ->
                      MainInterface ->
                      PragmaOptions ->
                      TCM ModuleInfo ->
                      TCM ModuleInfo
    alreadyVisited :: TopLevelModuleName
    -> MainInterface
    -> PragmaOptions
    -> TCM ModuleInfo
    -> TCM ModuleInfo
    alreadyVisited TopLevelModuleName
    x MainInterface
    isMain PragmaOptions
    currentOptions TCM ModuleInfo
    getModule =
      case MainInterface
    isMain of
        MainInterface Mode
    TypeCheck                       -> ModuleCheckMode -> TCM ModuleInfo
    useExistingOrLoadAndRecordVisited ModuleCheckMode
    ModuleTypeChecked
        MainInterface
    NotMainInterface                              -> ModuleCheckMode -> TCM ModuleInfo
    useExistingOrLoadAndRecordVisited ModuleCheckMode
    ModuleTypeChecked
        MainInterface Mode
    ScopeCheck                      -> ModuleCheckMode -> TCM ModuleInfo
    useExistingOrLoadAndRecordVisited ModuleCheckMode
    ModuleScopeChecked
      where
      useExistingOrLoadAndRecordVisited :: ModuleCheckMode -> TCM ModuleInfo
      useExistingOrLoadAndRecordVisited :: ModuleCheckMode -> TCM ModuleInfo
    useExistingOrLoadAndRecordVisited ModuleCheckMode
    mode = TCM ModuleInfo -> TCMT IO (Maybe ModuleInfo) -> TCM ModuleInfo
    forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
    fromMaybeM TCM ModuleInfo
    loadAndRecordVisited (ModuleCheckMode -> TCMT IO (Maybe ModuleInfo)
    existingWithoutWarnings ModuleCheckMode
    mode)

      -- Case: already visited.
      --
      -- A module with warnings should never be allowed to be
      -- imported from another module.
      existingWithoutWarnings :: ModuleCheckMode -> TCM (Maybe ModuleInfo)
      existingWithoutWarnings :: ModuleCheckMode -> TCMT IO (Maybe ModuleInfo)
    existingWithoutWarnings ModuleCheckMode
    mode = MaybeT (TCMT IO) ModuleInfo -> TCMT IO (Maybe ModuleInfo)
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT (TCMT IO) ModuleInfo -> TCMT IO (Maybe ModuleInfo))
    -> MaybeT (TCMT IO) ModuleInfo -> TCMT IO (Maybe ModuleInfo)
    forall a b. (a -> b) -> a -> b
    $ ExceptT [Char] (TCMT IO) ModuleInfo -> MaybeT (TCMT IO) ModuleInfo
    forall (m :: * -> *) e a. Functor m => ExceptT e m a -> MaybeT m a
    exceptToMaybeT (ExceptT [Char] (TCMT IO) ModuleInfo
     -> MaybeT (TCMT IO) ModuleInfo)
    -> ExceptT [Char] (TCMT IO) ModuleInfo
    -> MaybeT (TCMT IO) ModuleInfo
    forall a b. (a -> b) -> a -> b
    $ do
        mi <- [Char]
    -> MaybeT (TCMT IO) ModuleInfo
    -> ExceptT [Char] (TCMT IO) ModuleInfo
    forall (m :: * -> *) e a.
    Functor m =>
    e -> MaybeT m a -> ExceptT e m a
    maybeToExceptT [Char]
    "interface has not been visited in this context" (MaybeT (TCMT IO) ModuleInfo
     -> ExceptT [Char] (TCMT IO) ModuleInfo)
    -> MaybeT (TCMT IO) ModuleInfo
    -> ExceptT [Char] (TCMT IO) ModuleInfo
    forall a b. (a -> b) -> a -> b
    $ TCMT IO (Maybe ModuleInfo) -> MaybeT (TCMT IO) ModuleInfo
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (TCMT IO (Maybe ModuleInfo) -> MaybeT (TCMT IO) ModuleInfo)
    -> TCMT IO (Maybe ModuleInfo) -> MaybeT (TCMT IO) ModuleInfo
    forall a b. (a -> b) -> a -> b
    $
          TopLevelModuleName -> TCMT IO (Maybe ModuleInfo)
    forall (m :: * -> *).
    ReadTCState m =>
    TopLevelModuleName -> m (Maybe ModuleInfo)
    getVisitedModule TopLevelModuleName
    x

        when (miMode mi < mode) $
          throwError "previously-visited interface was not sufficiently checked"

        unless (null $ miWarnings mi) $
          throwError "previously-visited interface had warnings"

        reportSLn "import.visit" 10 $ "  Already visited " ++ prettyShow x

        lift $ processResultingModule mi

      processResultingModule :: ModuleInfo -> TCM ModuleInfo
      processResultingModule :: ModuleInfo -> TCM ModuleInfo
    processResultingModule ModuleInfo
    mi = do
        let ModuleInfo { miInterface :: ModuleInfo -> Interface
    miInterface = Interface
    i, miPrimitive :: ModuleInfo -> Bool
    miPrimitive = Bool
    isPrim, miWarnings :: ModuleInfo -> Set TCWarning
    miWarnings = Set TCWarning
    ws } = ModuleInfo
    mi

        -- Check that imported options are compatible with current ones (issue #2487),
        -- but give primitive modules a pass
        -- compute updated warnings if needed
        wt <- Set TCWarning -> Maybe (Set TCWarning) -> Set TCWarning
    forall a. a -> Maybe a -> a
    fromMaybe Set TCWarning
    ws (Maybe (Set TCWarning) -> Set TCWarning)
    -> TCMT IO (Maybe (Set TCWarning)) -> TCMT IO (Set TCWarning)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MainInterface
    -> Bool
    -> PragmaOptions
    -> Interface
    -> TCMT IO (Maybe (Set TCWarning))
    getOptionsCompatibilityWarnings MainInterface
    isMain Bool
    isPrim PragmaOptions
    currentOptions Interface
    i

        return mi { miWarnings = wt }

      loadAndRecordVisited :: TCM ModuleInfo
      loadAndRecordVisited :: TCM ModuleInfo
    loadAndRecordVisited = do
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.visit" Int
    5 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  Getting interface for " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ TopLevelModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow TopLevelModuleName
    x
        mi <- ModuleInfo -> TCM ModuleInfo
    processResultingModule (ModuleInfo -> TCM ModuleInfo) -> TCM ModuleInfo -> TCM ModuleInfo
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCM ModuleInfo
    getModule
        reportSLn "import.visit" 5 $ "  Now we've looked at " ++ prettyShow x

        -- Interfaces are not stored if we are only scope-checking, or
        -- if any warnings were encountered.
        case (isMain, null $ miWarnings mi) of
          (MainInterface Mode
    ScopeCheck, Bool
    _) -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          (MainInterface
    _, Bool
    False)                    -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          (MainInterface, Bool)
    _                             -> ModuleInfo -> TCM ()
    storeDecodedModule ModuleInfo
    mi

        reportS "warning.import" 10
          [ "module: " ++ show (moduleNameParts x)
          , "WarningOnImport: " ++ show (iImportWarning (miInterface mi))
          ]

        visitModule mi
        return mi

    -- | The result and associated parameters of a type-checked file,
    --   when invoked directly via interaction or a backend.
    --   Note that the constructor is not exported.

    data CheckResult = CheckResult'
      { CheckResult -> ModuleInfo
    crModuleInfo :: ModuleInfo
      , CheckResult -> Source
    crSource'    :: Source
      }

    -- | Flattened unidirectional pattern for 'CheckResult' for destructuring inside
    --   the 'ModuleInfo' field.
    pattern CheckResult :: Interface -> Set TCWarning -> ModuleCheckMode -> Source -> CheckResult
    pattern $mCheckResult :: forall {r}.
    CheckResult
    -> (Interface -> Set TCWarning -> ModuleCheckMode -> Source -> r)
    -> ((# #) -> r)
    -> r
    CheckResult { CheckResult -> Interface
    crInterface, CheckResult -> Set TCWarning
    crWarnings, CheckResult -> ModuleCheckMode
    crMode, CheckResult -> Source
    crSource } <- CheckResult'
        { crModuleInfo = ModuleInfo
            { miInterface = crInterface
            , miWarnings = crWarnings
            , miMode = crMode
            }
        , crSource' = crSource
        }

    -- | Type checks the main file of the interaction.
    --   This could be the file loaded in the interacting editor (emacs),
    --   or the file passed on the command line.
    --
    --   First, the primitive modules are imported.
    --   Then, @getInterface@ is called to do the main work.
    --
    --   If the 'Mode' is 'ScopeCheck', then type-checking is not
    --   performed, only scope-checking. (This may include type-checking
    --   of imported modules.) In this case the generated, partial
    --   interface is not stored in the state ('stDecodedModules'). Note,
    --   however, that if the file has already been type-checked, then a
    --   complete interface is returned.

    typeCheckMain
      :: Mode
         -- ^ Should the file be type-checked, or only scope-checked?
      -> Source
         -- ^ The decorated source code.
      -> TCM CheckResult
    typeCheckMain :: Mode -> Source -> TCM CheckResult
    typeCheckMain Mode
    mode Source
    src = do
      -- liftIO $ putStrLn $ "This is typeCheckMain " ++ prettyShow f
      -- liftIO . putStrLn . show =<< getVerbosity

      -- For the main interface, we also remember the pragmas from the file
      Bool -> Source -> TCM ()
    setOptionsFromSourcePragmas Bool
    True Source
    src

      -- Import the Agda.Primitive modules
      TCM ()
    importPrimitiveModules

      -- Now do the type checking via getInterface.
      TopLevelModuleName -> SourceFile -> TCM ()
    checkModuleName' (Source -> TopLevelModuleName
    srcModuleName Source
    src) (Source -> SourceFile
    srcOrigin Source
    src)

      mi <- TopLevelModuleName
    -> MainInterface -> Maybe Source -> TCM ModuleInfo
    getInterface (Source -> TopLevelModuleName
    srcModuleName Source
    src) (Mode -> MainInterface
    MainInterface Mode
    mode) (Source -> Maybe Source
    forall a. a -> Maybe a
    Just Source
    src)

      stCurrentModule `setTCLens'`
        Just ( iModuleName (miInterface mi)
             , iTopLevelModuleName (miInterface mi)
             )

      return $ CheckResult' mi src

    -- Andreas, 2016-07-11, issue 2092
    -- The error range should be set to the file with the wrong module name
    -- not the importing one (which would be the default).
    checkModuleName' :: TopLevelModuleName' Range -> SourceFile -> TCM ()
    checkModuleName' :: TopLevelModuleName -> SourceFile -> TCM ()
    checkModuleName' TopLevelModuleName
    m SourceFile
    f =
      TopLevelModuleName -> TCM () -> TCM ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange TopLevelModuleName
    m (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleName
    -> SourceFile -> Maybe TopLevelModuleName -> TCM ()
    checkModuleName TopLevelModuleName
    m SourceFile
    f Maybe TopLevelModuleName
    forall a. Maybe a
    Nothing

    -- | Import the primitive modules (unless --no-load-primitives).
    importPrimitiveModules :: TCM ()
    importPrimitiveModules :: TCM ()
    importPrimitiveModules = TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (PragmaOptions -> Bool
    optLoadPrimitives (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
      [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.main" Int
    10 [Char]
    "Importing the primitive modules."
      libdirPrim <- Lens' TCState AbsolutePath -> TCMT IO AbsolutePath
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (AbsolutePath -> f AbsolutePath) -> TCState -> f TCState
    Lens' TCState AbsolutePath
    stPrimitiveLibDir
      reportSLn "import.main" 20 $ "Library primitive dir = " ++ show libdirPrim
      -- Turn off import-chasing messages.
      -- We have to modify the persistent verbosity setting, since
      -- getInterface resets the current verbosity settings to the persistent ones.

      bracket_ (getsTC Lens.getPersistentVerbosity) Lens.putPersistentVerbosity $ do
        Lens.modifyPersistentVerbosity
          (Strict.Just . Trie.insert [] 0 . Strict.fromMaybe Trie.empty)
          -- set root verbosity to 0

        -- We don't want to generate highlighting information for Agda.Primitive.
        withHighlightingLevel None $
          forM_ (map (filePath libdirPrim </>) $ Set.toList primitiveModules) \ [Char]
    f -> do
            sf <- AbsolutePath -> TCMT IO SourceFile
    forall (m :: * -> *). MonadFileId m => AbsolutePath -> m SourceFile
    srcFromPath ([Char] -> AbsolutePath
    mkAbsolute [Char]
    f)
            primSource <- parseSource sf
            checkModuleName' (srcModuleName primSource) (srcOrigin primSource)
            void $ getNonMainInterface (srcModuleName primSource) (Just primSource)

      reportSLn "import.main" 10 $ "Done importing the primitive modules."

    -- | Tries to return the interface associated to the given (imported) module.
    --   The time stamp of the relevant interface file is also returned.
    --   Calls itself recursively for the imports of the given module.
    --   May type check the module.
    --   An error is raised if a warning is encountered.
    --
    --   Do not use this for the main file, use 'typeCheckMain' instead.

    getNonMainInterface
      :: TopLevelModuleName
      -> Maybe Source
         -- ^ Optional: the source code and some information about the source code.
      -> TCM Interface
    getNonMainInterface :: TopLevelModuleName -> Maybe Source -> TCMT IO Interface
    getNonMainInterface TopLevelModuleName
    x Maybe Source
    msrc = do
      mi <- TopLevelModuleName -> Maybe Source -> TCM ModuleInfo
    getNonMainModuleInfo TopLevelModuleName
    x Maybe Source
    msrc
      tcWarningsToError $ Set.toAscList $ miWarnings mi
      return (miInterface mi)

    getNonMainModuleInfo
      :: TopLevelModuleName
      -> Maybe Source
         -- ^ Optional: the source code and some information about the source code.
      -> TCM ModuleInfo
    getNonMainModuleInfo :: TopLevelModuleName -> Maybe Source -> TCM ModuleInfo
    getNonMainModuleInfo TopLevelModuleName
    x Maybe Source
    msrc =
      -- Preserve/restore the current pragma options, which will be mutated when loading
      -- and checking the interface.
      TCMT IO PragmaOptions
    -> (PragmaOptions -> TCM ()) -> TCM ModuleInfo -> TCM ModuleInfo
    forall (m :: * -> *) a b.
    Monad m =>
    m a -> (a -> m ()) -> m b -> m b
    bracket_ (Lens' TCState PragmaOptions -> TCMT IO PragmaOptions
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
    Lens' TCState PragmaOptions
    stPragmaOptions) ((PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
    Lens' TCState PragmaOptions
    stPragmaOptions Lens' TCState PragmaOptions -> PragmaOptions -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> a -> m ()
    `setTCLens`) (TCM ModuleInfo -> TCM ModuleInfo)
    -> TCM ModuleInfo -> TCM ModuleInfo
    forall a b. (a -> b) -> a -> b
    $
               TopLevelModuleName
    -> MainInterface -> Maybe Source -> TCM ModuleInfo
    getInterface TopLevelModuleName
    x MainInterface
    NotMainInterface Maybe Source
    msrc

    -- | A more precise variant of 'getNonMainInterface'. If warnings are
    -- encountered then they are returned instead of being turned into
    -- errors.

    getInterface
      :: TopLevelModuleName
      -> MainInterface
      -> Maybe Source
         -- ^ Optional: the source code and some information about the source code.
      -> TCM ModuleInfo
    getInterface :: TopLevelModuleName
    -> MainInterface -> Maybe Source -> TCM ModuleInfo
    getInterface TopLevelModuleName
    x MainInterface
    isMain Maybe Source
    msrc =
      TopLevelModuleName -> TCM ModuleInfo -> TCM ModuleInfo
    forall a. TopLevelModuleName -> TCM a -> TCM a
    addImportCycleCheck TopLevelModuleName
    x (TCM ModuleInfo -> TCM ModuleInfo)
    -> TCM ModuleInfo -> TCM ModuleInfo
    forall a b. (a -> b) -> a -> b
    $ do
         -- We remember but reset the pragma options locally
         -- Issue #3644 (Abel 2020-05-08): Set approximate range for errors in options
         currentOptions <- Lens' TCState PragmaOptions -> TCMT IO PragmaOptions
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
    Lens' TCState PragmaOptions
    stPragmaOptions
         setCurrentRange (C.modPragmas . srcModule <$> msrc) $
           -- Now reset the options
           setCommandLineOptions . stPersistentOptions . stPersistentState =<< getTC

         alreadyVisited x isMain currentOptions $ do
          file <- case msrc of
            Maybe Source
    Nothing  -> TopLevelModuleName -> TCMT IO SourceFile
    findFile TopLevelModuleName
    x
            Just Source
    src -> do
              -- Andreas, 2021-08-17, issue #5508.
              -- So it happened with @msrc == Just{}@ that the file was not added to @ModuleToSource@,
              -- only with @msrc == Nothing@ (then @findFile@ does it).
              -- As a consequence, the file was added later, but with a file name constructed
              -- from a module name.  As #5508 shows, this can be fatal in case-insensitive file systems.
              -- The file name (with case variant) then no longer maps to the module name.
              -- To prevent this, we register the connection in @ModuleToSource@ here,
              -- where we have the correct spelling of the file name.
              let file :: SourceFile
    file = Source -> SourceFile
    srcOrigin Source
    src
              Lens' TCState (Map TopLevelModuleName SourceFile)
    -> (Map TopLevelModuleName SourceFile
        -> Map TopLevelModuleName SourceFile)
    -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    modifyTCLens (Map TopLevelModuleName SourceFile
     -> f (Map TopLevelModuleName SourceFile))
    -> TCState -> f TCState
    Lens' TCState (Map TopLevelModuleName SourceFile)
    stModuleToSourceId ((Map TopLevelModuleName SourceFile
      -> Map TopLevelModuleName SourceFile)
     -> TCM ())
    -> (Map TopLevelModuleName SourceFile
        -> Map TopLevelModuleName SourceFile)
    -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleName
    -> SourceFile
    -> Map TopLevelModuleName SourceFile
    -> Map TopLevelModuleName SourceFile
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert TopLevelModuleName
    x SourceFile
    file
              SourceFile -> TCMT IO SourceFile
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure SourceFile
    file
          reportSDoc "import.iface" 15 do
            path <- srcFilePath file
            P.text $ List.intercalate "\n" $ map ("  " ++)
              [ "module: " ++ prettyShow x
              , "file:   " ++ prettyShow path
              ]

          reportSLn "import.iface" 15 $ "  Check for cycle"
          checkForImportCycle

          -- -- Andreas, 2014-10-20 AIM XX:
          -- -- Always retype-check the main file to get the iInsideScope
          -- -- which is no longer serialized.
          -- let maySkip = isMain == NotMainInterface
          -- Andreas, 2015-07-13: Serialize iInsideScope again.
          -- Andreas, 2020-05-13 issue #4647: don't skip if reload because of top-level command
          stored <- runExceptT $ Bench.billTo [Bench.Import] $ do
            getStoredInterface x file msrc

          let recheck = \[Char]
    reason -> do
                [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface" Int
    5 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Char]
    "  ", TopLevelModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow TopLevelModuleName
    x, [Char]
    " is not up-to-date because ", [Char]
    reason, [Char]
    "."]
                CommandLineOptions -> TCM ()
    setCommandLineOptions (CommandLineOptions -> TCM ())
    -> (TCState -> CommandLineOptions) -> TCState -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PersistentTCState -> CommandLineOptions
    stPersistentOptions (PersistentTCState -> CommandLineOptions)
    -> (TCState -> PersistentTCState) -> TCState -> CommandLineOptions
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCState -> PersistentTCState
    stPersistentState (TCState -> TCM ()) -> TCMT IO TCState -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC
                modl <- case MainInterface
    isMain of
                  MainInterface Mode
    _ -> TopLevelModuleName
    -> SourceFile -> MainInterface -> Maybe Source -> TCM ModuleInfo
    createInterface TopLevelModuleName
    x SourceFile
    file MainInterface
    isMain Maybe Source
    msrc
                  MainInterface
    NotMainInterface -> TopLevelModuleName -> SourceFile -> Maybe Source -> TCM ModuleInfo
    createInterfaceIsolated TopLevelModuleName
    x SourceFile
    file Maybe Source
    msrc

                -- Ensure that the given module name matches the one in the file.
                let topLevelName = Interface -> TopLevelModuleName
    iTopLevelModuleName (ModuleInfo -> Interface
    miInterface ModuleInfo
    modl)
                unless (topLevelName == x) do
                  path <- srcFilePath file
                  typeError $ OverlappingProjects path topLevelName x

                return modl

          either recheck pure stored

    -- | If checking produced non-benign warnings, error out.
    --
    raiseNonFatalErrors :: (HasOptions m, MonadTCError m)
      => CheckResult  -- ^ E.g. obtained from 'typeCheckMain'.
      -> m ()
    raiseNonFatalErrors :: forall (m :: * -> *).
    (HasOptions m, MonadTCError m) =>
    CheckResult -> m ()
    raiseNonFatalErrors CheckResult
    result = do
      m (Set TCWarning) -> (Set1 TCWarning -> m ()) -> m ()
    forall (m :: * -> *) a.
    Monad m =>
    m (Set a) -> (Set1 a -> m ()) -> m ()
    Set1.unlessNullM (Set TCWarning -> m (Set TCWarning)
    forall (m :: * -> *).
    HasOptions m =>
    Set TCWarning -> m (Set TCWarning)
    applyFlagsToTCWarnings (CheckResult -> Set TCWarning
    crWarnings CheckResult
    result)) ((Set1 TCWarning -> m ()) -> m ())
    -> (Set1 TCWarning -> m ()) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \ Set1 TCWarning
    ws ->
        TypeError -> m ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m ()) -> TypeError -> m ()
    forall a b. (a -> b) -> a -> b
    $ Set1 TCWarning -> TypeError
    NonFatalErrors Set1 TCWarning
    ws

    -- | Check if the options used for checking an imported module are
    --   compatible with the current options. Raises Non-fatal errors if
    --   not.
    checkOptionsCompatible ::
      PragmaOptions -> PragmaOptions -> TopLevelModuleName -> TCM Bool
    checkOptionsCompatible :: PragmaOptions
    -> PragmaOptions -> TopLevelModuleName -> TCMT IO Bool
    checkOptionsCompatible PragmaOptions
    current PragmaOptions
    imported TopLevelModuleName
    importedModule = (StateT Bool (TCMT IO) () -> Bool -> TCMT IO Bool)
    -> Bool -> StateT Bool (TCMT IO) () -> TCMT IO Bool
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip StateT Bool (TCMT IO) () -> Bool -> TCMT IO Bool
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
    execStateT Bool
    True (StateT Bool (TCMT IO) () -> TCMT IO Bool)
    -> StateT Bool (TCMT IO) () -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ do
      [Char] -> Int -> TCMT IO Doc -> StateT Bool (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "import.iface.options" Int
    25 (TCMT IO Doc -> StateT Bool (TCMT IO) ())
    -> TCMT IO Doc -> StateT Bool (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    P.nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "current options  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    P.<+> PragmaOptions -> TCMT IO Doc
    forall {m :: * -> *}.
    (Applicative m, Semigroup (m Doc), IsString (m Doc)) =>
    PragmaOptions -> m Doc
    showOptions PragmaOptions
    current
      [Char] -> Int -> TCMT IO Doc -> StateT Bool (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "import.iface.options" Int
    25 (TCMT IO Doc -> StateT Bool (TCMT IO) ())
    -> TCMT IO Doc -> StateT Bool (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    P.nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "imported options =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    P.<+> PragmaOptions -> TCMT IO Doc
    forall {m :: * -> *}.
    (Applicative m, Semigroup (m Doc), IsString (m Doc)) =>
    PragmaOptions -> m Doc
    showOptions PragmaOptions
    imported
      [InfectiveCoinfectiveOption]
    -> (InfectiveCoinfectiveOption -> StateT Bool (TCMT IO) ())
    -> StateT Bool (TCMT IO) ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [InfectiveCoinfectiveOption]
    infectiveCoinfectiveOptions ((InfectiveCoinfectiveOption -> StateT Bool (TCMT IO) ())
     -> StateT Bool (TCMT IO) ())
    -> (InfectiveCoinfectiveOption -> StateT Bool (TCMT IO) ())
    -> StateT Bool (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ \InfectiveCoinfectiveOption
    opt -> do
        Bool -> StateT Bool (TCMT IO) () -> StateT Bool (TCMT IO) ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (InfectiveCoinfectiveOption
    -> PragmaOptions -> PragmaOptions -> Bool
    icOptionOK InfectiveCoinfectiveOption
    opt PragmaOptions
    current PragmaOptions
    imported) (StateT Bool (TCMT IO) () -> StateT Bool (TCMT IO) ())
    -> StateT Bool (TCMT IO) () -> StateT Bool (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ do
          Bool -> StateT Bool (TCMT IO) ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put Bool
    False
          Warning -> StateT Bool (TCMT IO) ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> StateT Bool (TCMT IO) ())
    -> Warning -> StateT Bool (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $
            (case InfectiveCoinfectiveOption -> InfectiveCoinfective
    icOptionKind InfectiveCoinfectiveOption
    opt of
               InfectiveCoinfective
    Infective   -> Doc -> Warning
    InfectiveImport
               InfectiveCoinfective
    Coinfective -> Doc -> Warning
    CoInfectiveImport)
            (InfectiveCoinfectiveOption -> TopLevelModuleName -> Doc
    icOptionWarning InfectiveCoinfectiveOption
    opt TopLevelModuleName
    importedModule)
      where
      showOptions :: PragmaOptions -> m Doc
    showOptions PragmaOptions
    opts =
        [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    P.prettyList ([m Doc] -> m Doc) -> [m Doc] -> m Doc
    forall a b. (a -> b) -> a -> b
    $
        (InfectiveCoinfectiveOption -> m Doc)
    -> [InfectiveCoinfectiveOption] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (\InfectiveCoinfectiveOption
    opt -> ([Char] -> m Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    P.text (InfectiveCoinfectiveOption -> [Char]
    icOptionDescription InfectiveCoinfectiveOption
    opt) m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    <> m Doc
    ": ") m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    P.<+>
                     Bool -> m Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    P.pretty (InfectiveCoinfectiveOption -> PragmaOptions -> Bool
    icOptionActive InfectiveCoinfectiveOption
    opt PragmaOptions
    opts))
          [InfectiveCoinfectiveOption]
    infectiveCoinfectiveOptions

    -- | Compare options and return collected warnings.
    -- | Returns `Nothing` if warning collection was skipped.

    getOptionsCompatibilityWarnings :: MainInterface -> Bool -> PragmaOptions -> Interface -> TCM (Maybe (Set TCWarning))
    getOptionsCompatibilityWarnings :: MainInterface
    -> Bool
    -> PragmaOptions
    -> Interface
    -> TCMT IO (Maybe (Set TCWarning))
    getOptionsCompatibilityWarnings MainInterface
    isMain Bool
    isPrim PragmaOptions
    currentOptions Interface
    i = MaybeT (TCMT IO) (Set TCWarning) -> TCMT IO (Maybe (Set TCWarning))
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT (TCMT IO) (Set TCWarning)
     -> TCMT IO (Maybe (Set TCWarning)))
    -> MaybeT (TCMT IO) (Set TCWarning)
    -> TCMT IO (Maybe (Set TCWarning))
    forall a b. (a -> b) -> a -> b
    $ ExceptT [Char] (TCMT IO) (Set TCWarning)
    -> MaybeT (TCMT IO) (Set TCWarning)
    forall (m :: * -> *) e a. Functor m => ExceptT e m a -> MaybeT m a
    exceptToMaybeT (ExceptT [Char] (TCMT IO) (Set TCWarning)
     -> MaybeT (TCMT IO) (Set TCWarning))
    -> ExceptT [Char] (TCMT IO) (Set TCWarning)
    -> MaybeT (TCMT IO) (Set TCWarning)
    forall a b. (a -> b) -> a -> b
    $ do
      -- We're just dropping these reasons-for-skipping messages for now.
      -- They weren't logged before, but they're nice for documenting the early returns.
      Bool -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when Bool
    isPrim (ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ())
    -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $
        [Char] -> ExceptT [Char] (TCMT IO) ()
    forall a. [Char] -> ExceptT [Char] (TCMT IO) a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError [Char]
    "Options consistency checking disabled for always-available primitive module"
      ExceptT [Char] (TCMT IO) Bool
    -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (TCMT IO Bool -> ExceptT [Char] (TCMT IO) Bool
    forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO Bool -> ExceptT [Char] (TCMT IO) Bool)
    -> TCMT IO Bool -> ExceptT [Char] (TCMT IO) Bool
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    -> PragmaOptions -> TopLevelModuleName -> TCMT IO Bool
    checkOptionsCompatible PragmaOptions
    currentOptions (Interface -> PragmaOptions
    iOptionsUsed Interface
    i)
                      (Interface -> TopLevelModuleName
    iTopLevelModuleName Interface
    i)) (ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ())
    -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $
        [Char] -> ExceptT [Char] (TCMT IO) ()
    forall a. [Char] -> ExceptT [Char] (TCMT IO) a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError [Char]
    "No warnings to collect because options were compatible"
      TCMT IO (Set TCWarning) -> ExceptT [Char] (TCMT IO) (Set TCWarning)
    forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO (Set TCWarning)
     -> ExceptT [Char] (TCMT IO) (Set TCWarning))
    -> TCMT IO (Set TCWarning)
    -> ExceptT [Char] (TCMT IO) (Set TCWarning)
    forall a b. (a -> b) -> a -> b
    $ MainInterface -> WhichWarnings -> TCMT IO (Set TCWarning)
    forall (m :: * -> *).
    (ReadTCState m, MonadWarning m, MonadTCM m) =>
    MainInterface -> WhichWarnings -> m (Set TCWarning)
    getAllWarnings' MainInterface
    isMain WhichWarnings
    ErrorWarnings

    -- | Try to get the interface from interface file or cache.

    getStoredInterface :: HasCallStack
      => TopLevelModuleName
         -- ^ Module name of file we process.
      -> SourceFile
         -- ^ File we process.
      -> Maybe Source
      -> ExceptT String TCM ModuleInfo
    getStoredInterface :: HasCallStack =>
    TopLevelModuleName
    -> SourceFile
    -> Maybe Source
    -> ExceptT [Char] (TCMT IO) ModuleInfo
    getStoredInterface TopLevelModuleName
    x file :: SourceFile
    file@(SourceFile FileId
    fi) Maybe Source
    msrc = do
      -- Check whether interface file exists and is in cache
      --  in the correct version (as testified by the interface file hash).
      --
      -- This is a lazy action which may be skipped if there is no cached interface
      -- and we're ignoring interface files for some reason.
      let getIFileHashesET :: ExceptT [Char] (TCMT IO) (InterfaceFile, (Hash, Hash))
    getIFileHashesET = do
            -- Check that the interface file exists and return its hash.
            ifile <- [Char]
    -> MaybeT (TCMT IO) InterfaceFile
    -> ExceptT [Char] (TCMT IO) InterfaceFile
    forall (m :: * -> *) e a.
    Functor m =>
    e -> MaybeT m a -> ExceptT e m a
    maybeToExceptT [Char]
    "the interface file could not be found" (MaybeT (TCMT IO) InterfaceFile
     -> ExceptT [Char] (TCMT IO) InterfaceFile)
    -> MaybeT (TCMT IO) InterfaceFile
    -> ExceptT [Char] (TCMT IO) InterfaceFile
    forall a b. (a -> b) -> a -> b
    $ TCMT IO (Maybe InterfaceFile) -> MaybeT (TCMT IO) InterfaceFile
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (TCMT IO (Maybe InterfaceFile) -> MaybeT (TCMT IO) InterfaceFile)
    -> TCMT IO (Maybe InterfaceFile) -> MaybeT (TCMT IO) InterfaceFile
    forall a b. (a -> b) -> a -> b
    $
              HasCallStack => SourceFile -> TCMT IO (Maybe InterfaceFile)
    SourceFile -> TCMT IO (Maybe InterfaceFile)
    findInterfaceFile' SourceFile
    file

            -- Check that the interface file exists and return its hash.
            hashes <- maybeToExceptT "the interface file hash could not be read" $ MaybeT $ liftIO $
              getInterfaceFileHashes ifile

            return (ifile, hashes)

      -- Examine the hash of the interface file. If it is different from the
      -- stored version (in stDecodedModules), or if there is no stored version,
      -- read and decode it. Otherwise use the stored version.
      --
      -- This is a lazy action which may be skipped if the cached or on-disk interface
      -- is invalid, missing, or skipped for some other reason.
      let checkSourceHashET :: Hash -> ExceptT [Char] (TCMT IO) ()
    checkSourceHashET Hash
    ifaceH = do
            sourceH <- case Maybe Source
    msrc of
                        Maybe Source
    Nothing -> do
                          path <- SourceFile -> ExceptT [Char] (TCMT IO) AbsolutePath
    forall (m :: * -> *). MonadFileId m => SourceFile -> m AbsolutePath
    srcFilePath SourceFile
    file
                          liftIO $ hashTextFile path
                        Just Source
    src -> Hash -> ExceptT [Char] (TCMT IO) Hash
    forall a. a -> ExceptT [Char] (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Hash -> ExceptT [Char] (TCMT IO) Hash)
    -> Hash -> ExceptT [Char] (TCMT IO) Hash
    forall a b. (a -> b) -> a -> b
    $ Text -> Hash
    hashText (Source -> Text
    srcText Source
    src)

            unless (sourceH == ifaceH) $
              throwError $ concat
                [ "the source hash (", show sourceH, ")"
                , " does not match the source hash for the interface (", show ifaceH, ")"
                ]

            reportSLn "import.iface" 5 $ concat ["  ", prettyShow x, " is up-to-date."]

      let
        -- Load or reload the interface file, if possible.
        loadInterfaceFile :: [Char] -> ExceptT [Char] (TCMT IO) ModuleInfo
    loadInterfaceFile [Char]
    whyNotCached =
          ShowS
    -> ExceptT [Char] (TCMT IO) ModuleInfo
    -> ExceptT [Char] (TCMT IO) ModuleInfo
    forall (m :: * -> *) e e' a.
    Functor m =>
    (e -> e') -> ExceptT e m a -> ExceptT e' m a
    withExceptT (\[Char]
    e -> [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Char]
    whyNotCached, [Char]
    " and ", [Char]
    e]) (ExceptT [Char] (TCMT IO) ModuleInfo
     -> ExceptT [Char] (TCMT IO) ModuleInfo)
    -> ExceptT [Char] (TCMT IO) ModuleInfo
    -> ExceptT [Char] (TCMT IO) ModuleInfo
    forall a b. (a -> b) -> a -> b
    $ do
          ExceptT [Char] (TCMT IO) Bool
    -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM ExceptT [Char] (TCMT IO) Bool
    forall (m :: * -> *). HasOptions m => m Bool
    ignoreAllInterfaces (ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ())
    -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $
            [Char] -> ExceptT [Char] (TCMT IO) ()
    forall a. [Char] -> ExceptT [Char] (TCMT IO) a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError [Char]
    "we're ignoring all interface files"

          ExceptT [Char] (TCMT IO) Bool
    -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM ExceptT [Char] (TCMT IO) Bool
    forall (m :: * -> *). HasOptions m => m Bool
    ignoreInterfaces (ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ())
    -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $
            ExceptT [Char] (TCMT IO) (Maybe IsBuiltinModule)
    -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall (m :: * -> *) a. Monad m => m (Maybe a) -> m () -> m ()
    whenNothingM (FileId -> ExceptT [Char] (TCMT IO) (Maybe IsBuiltinModule)
    forall (m :: * -> *).
    ReadTCState m =>
    FileId -> m (Maybe IsBuiltinModule)
    isBuiltinModule FileId
    fi) (ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ())
    -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $
                [Char] -> ExceptT [Char] (TCMT IO) ()
    forall a. [Char] -> ExceptT [Char] (TCMT IO) a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError [Char]
    "we're ignoring non-builtin interface files"

          (ifile, hashes) <- ExceptT [Char] (TCMT IO) (InterfaceFile, (Hash, Hash))
    getIFileHashesET

          let ifp = (AbsolutePath -> [Char]
    filePath (AbsolutePath -> [Char])
    -> (InterfaceFile -> AbsolutePath) -> InterfaceFile -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . InterfaceFile -> AbsolutePath
    intFilePath (InterfaceFile -> [Char]) -> InterfaceFile -> [Char]
    forall a b. (a -> b) -> a -> b
    $ InterfaceFile
    ifile)

          Bench.billTo [Bench.Deserialization] $ do
            checkSourceHashET (fst hashes)

            reportSLn "import.iface" 5 $ "  no stored version, reading " ++ ifp

            i <- maybeToExceptT "bad interface, re-type checking" $ MaybeT $
              readInterface ifile

            -- Ensure that the given module name matches the one in the file.
            let topLevelName = Interface -> TopLevelModuleName
    iTopLevelModuleName Interface
    i
            unless (topLevelName == x) do
              path <- srcFilePath file
              lift $ typeError $ OverlappingProjects path topLevelName x

            isPrimitiveMod <- isPrimitiveModule fi

            lift $ chaseMsg "Loading " x $ Just ifp
            -- print imported warnings
            reportWarningsForModule x $ iWarnings i

            loadDecodedModule file $ ModuleInfo
              { miInterface = i
              , miWarnings = empty
              , miPrimitive = isPrimitiveMod
              , miMode = ModuleTypeChecked
              }

      -- Check if we have cached the module.
      cachedE <- ExceptT [Char] (ExceptT [Char] (TCMT IO)) ModuleInfo
    -> ExceptT [Char] (TCMT IO) (Either [Char] ModuleInfo)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (ExceptT [Char] (ExceptT [Char] (TCMT IO)) ModuleInfo
     -> ExceptT [Char] (TCMT IO) (Either [Char] ModuleInfo))
    -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ModuleInfo
    -> ExceptT [Char] (TCMT IO) (Either [Char] ModuleInfo)
    forall a b. (a -> b) -> a -> b
    $ [Char]
    -> MaybeT (ExceptT [Char] (TCMT IO)) ModuleInfo
    -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ModuleInfo
    forall (m :: * -> *) e a.
    Functor m =>
    e -> MaybeT m a -> ExceptT e m a
    maybeToExceptT [Char]
    "the interface has not been decoded" (MaybeT (ExceptT [Char] (TCMT IO)) ModuleInfo
     -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ModuleInfo)
    -> MaybeT (ExceptT [Char] (TCMT IO)) ModuleInfo
    -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ModuleInfo
    forall a b. (a -> b) -> a -> b
    $ ExceptT [Char] (TCMT IO) (Maybe ModuleInfo)
    -> MaybeT (ExceptT [Char] (TCMT IO)) ModuleInfo
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (ExceptT [Char] (TCMT IO) (Maybe ModuleInfo)
     -> MaybeT (ExceptT [Char] (TCMT IO)) ModuleInfo)
    -> ExceptT [Char] (TCMT IO) (Maybe ModuleInfo)
    -> MaybeT (ExceptT [Char] (TCMT IO)) ModuleInfo
    forall a b. (a -> b) -> a -> b
    $
          TCMT IO (Maybe ModuleInfo)
    -> ExceptT [Char] (TCMT IO) (Maybe ModuleInfo)
    forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO (Maybe ModuleInfo)
     -> ExceptT [Char] (TCMT IO) (Maybe ModuleInfo))
    -> TCMT IO (Maybe ModuleInfo)
    -> ExceptT [Char] (TCMT IO) (Maybe ModuleInfo)
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleName -> TCMT IO (Maybe ModuleInfo)
    getDecodedModule TopLevelModuleName
    x

      case cachedE of
        Left [Char]
    whyNotCached -> [Char] -> ExceptT [Char] (TCMT IO) ModuleInfo
    loadInterfaceFile [Char]
    whyNotCached

        -- If it's cached ignoreInterfaces has no effect;
        -- to avoid typechecking a file more than once.
        Right ModuleInfo
    mi -> do
          (ifile, hashes) <- ExceptT [Char] (TCMT IO) (InterfaceFile, (Hash, Hash))
    getIFileHashesET

          let ifp = AbsolutePath -> [Char]
    filePath (AbsolutePath -> [Char]) -> AbsolutePath -> [Char]
    forall a b. (a -> b) -> a -> b
    $ InterfaceFile -> AbsolutePath
    intFilePath InterfaceFile
    ifile
          let i = ModuleInfo -> Interface
    miInterface ModuleInfo
    mi

          -- Make sure the hashes match.
          let cachedIfaceHash = Interface -> Hash
    iFullHash Interface
    i
          let fileIfaceHash = (Hash, Hash) -> Hash
    forall a b. (a, b) -> b
    snd (Hash, Hash)
    hashes
          if cachedIfaceHash /= fileIfaceHash then do
            lift $ dropDecodedModule x
            reportSLn "import.iface" 50 $ "  cached hash = " ++ show cachedIfaceHash
            reportSLn "import.iface" 50 $ "  stored hash = " ++ show fileIfaceHash
            reportSLn "import.iface" 5 $ "  file is newer, re-reading " ++ ifp
            loadInterfaceFile $ concat
              [ "the cached interface hash (", show cachedIfaceHash, ")"
              , " does not match interface file (", show fileIfaceHash, ")"
              ]
           else Bench.billTo [Bench.Deserialization] $ do
            checkSourceHashET (iSourceHash i)

            reportSLn "import.iface" 5 $ "  using stored version of " ++ filePath (intFilePath ifile)
            loadDecodedModule file mi

    -- | Report those given warnings that come from the given module.

    reportWarningsForModule :: MonadDebug m => TopLevelModuleName -> Set TCWarning -> m ()
    reportWarningsForModule :: forall (m :: * -> *).
    MonadDebug m =>
    TopLevelModuleName -> Set TCWarning -> m ()
    reportWarningsForModule TopLevelModuleName
    x Set TCWarning
    warns = do
      [TCWarning] -> ([TCWarning] -> m ()) -> m ()
    forall (m :: * -> *) a.
    (Monad m, Null a) =>
    a -> (a -> m ()) -> m ()
    unlessNull ((TCWarning -> Bool) -> [TCWarning] -> [TCWarning]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((Maybe TopLevelModuleName -> Maybe (Maybe TopLevelModuleName)
    forall a. a -> Maybe a
    Strict.Just (TopLevelModuleName -> Maybe TopLevelModuleName
    forall a. a -> Maybe a
    Just TopLevelModuleName
    x) Maybe (Maybe TopLevelModuleName)
    -> Maybe (Maybe TopLevelModuleName) -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Maybe (Maybe TopLevelModuleName) -> Bool)
    -> (TCWarning -> Maybe (Maybe TopLevelModuleName))
    -> TCWarning
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (RangeFile -> Maybe TopLevelModuleName)
    -> Maybe RangeFile -> Maybe (Maybe TopLevelModuleName)
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap RangeFile -> Maybe TopLevelModuleName
    rangeFileName (Maybe RangeFile -> Maybe (Maybe TopLevelModuleName))
    -> (TCWarning -> Maybe RangeFile)
    -> TCWarning
    -> Maybe (Maybe TopLevelModuleName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCWarning -> Maybe RangeFile
    tcWarningOrigin) ([TCWarning] -> [TCWarning]) -> [TCWarning] -> [TCWarning]
    forall a b. (a -> b) -> a -> b
    $ Set TCWarning -> [TCWarning]
    forall a. Set a -> [a]
    Set.toAscList Set TCWarning
    warns) \ [TCWarning]
    ws ->
        [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    alwaysReportSDoc [Char]
    "warning" Int
    1 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    P.vsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ (TCWarning -> TCMT IO Doc) -> [TCWarning] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map TCWarning -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => TCWarning -> m Doc
    P.prettyTCM [TCWarning]
    ws

    -- | Check whether the loaded module is up-to-date
    --   and merge into state if this is the case.
    --
    loadDecodedModule
      :: SourceFile
         -- ^ File we process.
      -> ModuleInfo
         -- ^ The interface we loaded or created.
      -> ExceptT String TCM ModuleInfo
    loadDecodedModule :: SourceFile -> ModuleInfo -> ExceptT [Char] (TCMT IO) ModuleInfo
    loadDecodedModule sf :: SourceFile
    sf@(SourceFile FileId
    fi) ModuleInfo
    mi = do
      file <- SourceFile -> ExceptT [Char] (TCMT IO) AbsolutePath
    forall (m :: * -> *). MonadFileId m => SourceFile -> m AbsolutePath
    srcFilePath SourceFile
    sf
      let fp      = AbsolutePath -> [Char]
    filePath AbsolutePath
    file
      let i       = ModuleInfo -> Interface
    miInterface ModuleInfo
    mi
      let imports = Interface -> [(TopLevelModuleName, Hash)]
    iImportedModules Interface
    i
      let name    = Interface -> TopLevelModuleName
    iTopLevelModuleName Interface
    i

      -- Print imported modules.
      verboseS "import.iface.imports" 5 $ unless (null imports) $
        reportSLn "import.iface.imports" 5 $ intercalate "\n" $
          unwords [ prettyShow name, "imports:" ] :
          map (\ (TopLevelModuleName
    x, Hash
    hash) -> [[Char]] -> [Char]
    unwords [ [Char]
    " ", [Char]
    "-", TopLevelModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow TopLevelModuleName
    x, [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Char]
    "(hash: ", Hash -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Hash
    hash, [Char]
    ")"] ])
            imports

      -- We set the pragma options of the skipped file here, so that
      -- we can check that they are compatible with those of the
      -- imported modules. Also, if the top-level file is skipped we
      -- want the pragmas to apply to interactive commands in the UI.
      -- Jesper, 2021-04-18: Check for changed options in library files!
      -- (see #5250)
      libOptions <- lift $ getLibraryOptions file name
      lift $ mapM_ setOptionsFromPragma (libOptions ++ iFilePragmaOptions i)

      -- Check that options that matter haven't changed compared to
      -- current options (issue #2487).
      whenNothingM (isBuiltinModule fi) do
        current <- useTC stPragmaOptions
        when (recheckBecausePragmaOptionsChanged (iOptionsUsed i) current) $
          throwError "options changed"

      -- If any of the imports are newer we need to re-typecheck.
      badHashMessages <- fmap lefts $ forM imports \ (TopLevelModuleName
    impName, Hash
    impHash) -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ()
    -> ExceptT [Char] (TCMT IO) (Either [Char] ())
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT do
        [Char]
    -> Int -> [Char] -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface" Int
    30 ([Char] -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ())
    -> [Char] -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Char]
    "Checking that module hash of import ", TopLevelModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow TopLevelModuleName
    impName, [Char]
    " matches ", Hash -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Hash
    impHash ]
        latestImpHash <- ExceptT [Char] (TCMT IO) Hash
    -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) Hash
    forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (ExceptT [Char] (TCMT IO) Hash
     -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) Hash)
    -> ExceptT [Char] (TCMT IO) Hash
    -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) Hash
    forall a b. (a -> b) -> a -> b
    $ TCM Hash -> ExceptT [Char] (TCMT IO) Hash
    forall (m :: * -> *) a. Monad m => m a -> ExceptT [Char] m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM Hash -> ExceptT [Char] (TCMT IO) Hash)
    -> TCM Hash -> ExceptT [Char] (TCMT IO) Hash
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleName -> TCM Hash -> TCM Hash
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange TopLevelModuleName
    impName (TCM Hash -> TCM Hash) -> TCM Hash -> TCM Hash
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleName -> TCM Hash
    moduleHash TopLevelModuleName
    impName
        reportSLn "import.iface" 30 $ concat ["Done checking module hash of import ", prettyShow impName]
        when (impHash /= latestImpHash) $
          throwError $ concat
            [ "module hash for imported module ", prettyShow impName, " is out of date"
            , " (import cached=", prettyShow impHash, ", latest=", prettyShow latestImpHash, ")"
            ]

      unlessNull badHashMessages (throwError . unlines)

      reportSLn "import.iface" 5 $ prettyShow name ++ ": interface is valid and can be merged into the state."
      lift $ mergeInterface i
      Bench.billTo [Bench.Highlighting] $
        lift $ ifTopLevelAndHighlightingLevelIs NonInteractive $
          highlightFromInterface i sf

      return mi

    -- | Run the type checker on a file and create an interface.
    --
    --   Mostly, this function calls 'createInterface'.
    --   But if it is not the main module we check,
    --   we do it in a fresh state, suitably initialize,
    --   in order to forget some state changes after successful type checking.

    createInterfaceIsolated
      :: TopLevelModuleName
         -- ^ Module name of file we process.
      -> SourceFile
         -- ^ File we process.
      -> Maybe Source
         -- ^ Optional: the source code and some information about the source code.
      -> TCM ModuleInfo
    createInterfaceIsolated :: TopLevelModuleName -> SourceFile -> Maybe Source -> TCM ModuleInfo
    createInterfaceIsolated TopLevelModuleName
    x SourceFile
    file Maybe Source
    msrc = do
          TCM ()
    forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
    cleanCachedLog

          ms          <- TCMT IO [TopLevelModuleName]
    getImportPath
          range       <- asksTC envRange
          call        <- asksTC envCall
          mf          <- useTC stModuleToSource
          vs          <- getVisitedModules
          ds          <- getDecodedModules
          opts        <- stPersistentOptions . stPersistentState <$> getTC
          isig        <- useTC stImports
          metas       <- useTC stImportedMetaStore
          ibuiltin    <- useTC stImportedBuiltins
          display     <- useTC stImportsDisplayForms
          userwarn    <- useTC stImportedUserWarnings
          partialdefs <- useTC stImportedPartialDefs
          opaqueblk   <- useTC stOpaqueBlocks
          opaqueid    <- useTC stOpaqueIds
          ipatsyns <- getPatternSynImports
          ho       <- getInteractionOutputCallback
          -- Every interface is treated in isolation. Note: Some changes to
          -- the persistent state may not be preserved if an error other
          -- than a type error or an IO exception is encountered in an
          -- imported module.
          (mi, newModToSource, newDecodedModules) <- (either throwError pure =<<) $
               withoutCache $
               -- The cache should not be used for an imported module, and it
               -- should be restored after the module has been type-checked
               freshTCM $
                 withImportPath ms $
                 localTC (\TCEnv
    e -> TCEnv
    e
                                  -- Andreas, 2014-08-18:
                                  -- Preserve the range of import statement
                                  -- for reporting termination errors in
                                  -- imported modules:
                                { envRange              = range
                                , envCall               = call
                                }) $ do
                   setDecodedModules ds
                   setCommandLineOptions opts
                   setInteractionOutputCallback ho
                   stModuleToSource `setTCLens` mf
                   setVisitedModules vs
                   addImportedThings isig metas ibuiltin ipatsyns display
                     userwarn partialdefs empty opaqueblk opaqueid

                   r  <- createInterface x file NotMainInterface msrc
                   mf' <- useTC stModuleToSource
                   ds' <- getDecodedModules
                   return (r, mf', ds')

          stModuleToSource `setTCLens` newModToSource
          setDecodedModules newDecodedModules

          -- We skip the file which has just been type-checked to
          -- be able to forget some of the local state from
          -- checking the module.
          -- Note that this doesn't actually read the interface
          -- file, only the cached interface. (This comment is not
          -- correct, see
          -- test/Fail/customised/NestedProjectRoots.err.)
          validated <- runExceptT $ loadDecodedModule file mi

          -- NOTE: This attempts to type-check FOREVER if for some
          -- reason it continually fails to validate interface.
          let recheckOnError = \[Char]
    msg -> do
                [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    alwaysReportSLn [Char]
    "import.iface" Int
    1 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Failed to validate just-loaded interface: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    msg
                TopLevelModuleName -> SourceFile -> Maybe Source -> TCM ModuleInfo
    createInterfaceIsolated TopLevelModuleName
    x SourceFile
    file Maybe Source
    msrc

          either recheckOnError pure validated

    -- | Formats and outputs the "Checking", "Finished" and "Loading " messages.

    chaseMsg
      :: String               -- ^ The prefix, like @Checking@, @Finished@, @Loading @.
      -> TopLevelModuleName   -- ^ The module name.
      -> Maybe String         -- ^ Optionally: the file name.
      -> TCM ()
    chaseMsg :: [Char] -> TopLevelModuleName -> Maybe [Char] -> TCM ()
    chaseMsg [Char]
    kind TopLevelModuleName
    x Maybe [Char]
    file = do
      indentation <- (Int -> Char -> [Char]
    forall a. Int -> a -> [a]
    `replicate` Char
    ' ') (Int -> [Char]) -> TCMT IO Int -> TCMT IO [Char]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TCEnv -> Int) -> TCMT IO Int
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC (Int -> Int
    forall a. Enum a => a -> a
    pred (Int -> Int) -> (TCEnv -> Int) -> TCEnv -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [TopLevelModuleName] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length ([TopLevelModuleName] -> Int)
    -> (TCEnv -> [TopLevelModuleName]) -> TCEnv -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCEnv -> [TopLevelModuleName]
    envImportPath)
      traceImports <- optTraceImports <$> commandLineOptions
      let maybeFile = Maybe [Char] -> [Char] -> ShowS -> [Char]
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe [Char]
    file [Char]
    "." (ShowS -> [Char]) -> ShowS -> [Char]
    forall a b. (a -> b) -> a -> b
    $ \ [Char]
    f -> [Char]
    " (" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    f [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ")."
          vLvl | [Char]
    kind [Char] -> [Char] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Char]
    "Checking"
                 Bool -> Bool -> Bool
    && Integer
    traceImports Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    0 = Int
    1
               | [Char]
    kind [Char] -> [Char] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Char]
    "Finished"
                 Bool -> Bool -> Bool
    && Integer
    traceImports Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    1 = Int
    1
               | [Char] -> [Char] -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    List.isPrefixOf [Char]
    "Loading" [Char]
    kind
                 Bool -> Bool -> Bool
    && Integer
    traceImports Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    2 = Int
    1
               | Bool
    otherwise = Int
    2
      alwaysReportSLn "import.chase" vLvl $ concat
        [ indentation, kind, " ", prettyShow x, maybeFile ]

    -- | Print the highlighting information contained in the given interface.

    highlightFromInterface
      :: Interface
      -> SourceFile
         -- ^ The corresponding file.
      -> TCM ()
    highlightFromInterface :: Interface -> SourceFile -> TCM ()
    highlightFromInterface Interface
    i SourceFile
    sf = do
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "import.iface" Int
    5 do
        file <- SourceFile -> TCMT IO AbsolutePath
    forall (m :: * -> *). MonadFileId m => SourceFile -> m AbsolutePath
    srcFilePath SourceFile
    sf
        P.text $ "Generating syntax info for " ++ filePath file ++
          " (read from interface)."
      RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
    forall (m :: * -> *).
    MonadTrace m =>
    RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
    printHighlightingInfo RemoveTokenBasedHighlighting
    KeepHighlighting (Interface -> HighlightingInfo
    iHighlighting Interface
    i)

    -- | Read interface file corresponding to a module.

    readInterface :: InterfaceFile -> TCM (Maybe Interface)
    readInterface :: InterfaceFile -> TCMT IO (Maybe Interface)
    readInterface InterfaceFile
    file = do
        let ifp :: [Char]
    ifp = AbsolutePath -> [Char]
    filePath (AbsolutePath -> [Char]) -> AbsolutePath -> [Char]
    forall a b. (a -> b) -> a -> b
    $ InterfaceFile -> AbsolutePath
    intFilePath InterfaceFile
    file
        -- Decode the interface file
        (s, close) <- IO (ByteString, IO ()) -> TCMT IO (ByteString, IO ())
    forall a. IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (ByteString, IO ()) -> TCMT IO (ByteString, IO ()))
    -> IO (ByteString, IO ()) -> TCMT IO (ByteString, IO ())
    forall a b. (a -> b) -> a -> b
    $ [Char] -> IO (ByteString, IO ())
    readBinaryFile' [Char]
    ifp
        do  mi <- liftIO . E.evaluate =<< decodeInterface s

            -- Close the file. Note
            -- ⑴ that evaluate ensures that i is evaluated to WHNF (before
            --   the next IO operation is executed), and
            -- ⑵ that decode returns Nothing if an error is encountered,
            -- so it is safe to close the file here.
            liftIO close

            return $ constructIScope <$> mi
          -- Catch exceptions and close
          `catchError` \TCErr
    e -> IO () -> TCM ()
    forall a. IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO IO ()
    close TCM () -> TCMT IO (Maybe Interface) -> TCMT IO (Maybe Interface)
    forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> TCErr -> TCMT IO (Maybe Interface)
    forall {a}. TCErr -> TCMT IO (Maybe a)
    handler TCErr
    e
      -- Catch exceptions
      TCMT IO (Maybe Interface)
    -> (TCErr -> TCMT IO (Maybe Interface))
    -> TCMT IO (Maybe Interface)
    forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` TCErr -> TCMT IO (Maybe Interface)
    forall {a}. TCErr -> TCMT IO (Maybe a)
    handler
      where
        handler :: TCErr -> TCMT IO (Maybe a)
    handler = \case
          IOException Maybe TCState
    _ Range
    _ IOException
    e -> do
            [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    alwaysReportSLn [Char]
    "" Int
    0 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "IO exception: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ IOException -> [Char]
    forall a. Show a => a -> [Char]
    show IOException
    e
            Maybe a -> TCMT IO (Maybe a)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe a
    forall a. Maybe a
    Nothing   -- Work-around for file locking bug.
                             -- TODO: What does this refer to? Please
                             -- document.
          TCErr
    e -> TCErr -> TCMT IO (Maybe a)
    forall a. TCErr -> TCMT IO a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    e

    -- | Writes the given interface to the given file.
    --
    -- The written interface is decoded and returned.

    writeInterface :: AbsolutePath -> Interface -> TCM Interface
    writeInterface :: AbsolutePath -> Interface -> TCMT IO Interface
    writeInterface AbsolutePath
    file Interface
    i = let fp :: [Char]
    fp = AbsolutePath -> [Char]
    filePath AbsolutePath
    file in do
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.write" Int
    5  ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          [Char]
    "Writing interface file " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    fp [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "."
        -- Andreas, 2015-07-13
        -- After QName memoization (AIM XXI), scope serialization might be cheap enough.
        -- -- Andreas, Makoto, 2014-10-18 AIM XX:
        -- -- iInsideScope is bloating the interface files, so we do not serialize it?
        -- i <- return $
        --   i { iInsideScope  = emptyScopeInfo
        --     }
        -- [Old: Andreas, 2016-02-02 this causes issue #1804, so don't do it:]
        -- Andreas, 2020-05-13, #1804, #4647: removed private declarations
        -- only when we actually write the interface.
        let
          filteredIface :: Interface
    filteredIface = Interface
    i { iInsideScope = withoutPrivates $ iInsideScope i }
        filteredIface <- Interface -> TCMT IO Interface
    pruneTemporaryInstances Interface
    filteredIface
        reportSLn "import.iface.write" 50 $
          "Writing interface file with hash " ++ show (iFullHash filteredIface) ++ "."
        encodedIface <- encodeFile fp filteredIface
        reportSLn "import.iface.write" 5 "Wrote interface file."
        fromMaybe __IMPOSSIBLE__ <$> (Bench.billTo [Bench.Deserialization] (decode encodedIface))
      TCMT IO Interface
    -> (TCErr -> TCMT IO Interface) -> TCMT IO Interface
    forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \TCErr
    e -> do
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    alwaysReportSLn [Char]
    "" Int
    1 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          [Char]
    "Failed to write interface " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    fp [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "."
        IO () -> TCM ()
    forall a. IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCM ()) -> IO () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          IO Bool -> IO () -> IO ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM ([Char] -> IO Bool
    doesFileExist [Char]
    fp) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> IO ()
    removeFile [Char]
    fp
        TCErr -> TCMT IO Interface
    forall a. TCErr -> TCMT IO a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    e

    -- | Tries to type check a module and write out its interface. The
    -- function only writes out an interface file if it does not encounter
    -- any warnings.
    --
    -- If appropriate this function writes out syntax highlighting
    -- information.

    createInterface
      :: TopLevelModuleName    -- ^ The expected module name.
      -> SourceFile            -- ^ The file to type check.
      -> MainInterface         -- ^ Are we dealing with the main module?
      -> Maybe Source      -- ^ Optional information about the source code.
      -> TCM ModuleInfo
    createInterface :: TopLevelModuleName
    -> SourceFile -> MainInterface -> Maybe Source -> TCM ModuleInfo
    createInterface TopLevelModuleName
    mname sf :: SourceFile
    sf@(SourceFile FileId
    sfi) MainInterface
    isMain Maybe Source
    msrc = do
      file <- SourceFile -> TCMT IO AbsolutePath
    forall (m :: * -> *). MonadFileId m => SourceFile -> m AbsolutePath
    srcFilePath SourceFile
    sf
      let fp = AbsolutePath -> [Char]
    filePath AbsolutePath
    file
      let checkMsg = case MainInterface
    isMain of
                       MainInterface Mode
    ScopeCheck -> [Char]
    "Reading "
                       MainInterface
    _                        -> [Char]
    "Checking"
          withMsgs = TCM () -> (() -> TCM ()) -> TCM ModuleInfo -> TCM ModuleInfo
    forall (m :: * -> *) a b.
    Monad m =>
    m a -> (a -> m ()) -> m b -> m b
    bracket_
           ([Char] -> TopLevelModuleName -> Maybe [Char] -> TCM ()
    chaseMsg [Char]
    checkMsg TopLevelModuleName
    mname (Maybe [Char] -> TCM ()) -> Maybe [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    fp)
           (TCM () -> () -> TCM ()
    forall a b. a -> b -> a
    const (TCM () -> () -> TCM ()) -> TCM () -> () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do ws <- WhichWarnings -> TCMT IO (Set TCWarning)
    forall (m :: * -> *).
    (ReadTCState m, MonadWarning m, MonadTCM m) =>
    WhichWarnings -> m (Set TCWarning)
    getAllWarnings WhichWarnings
    AllWarnings
                       let classified = [TCWarning] -> WarningsAndNonFatalErrors
    classifyWarnings ([TCWarning] -> WarningsAndNonFatalErrors)
    -> [TCWarning] -> WarningsAndNonFatalErrors
    forall a b. (a -> b) -> a -> b
    $ Set TCWarning -> [TCWarning]
    forall a. Set a -> [a]
    Set.toAscList Set TCWarning
    ws
                       reportWarningsForModule mname $ tcWarnings classified
                       when (null (nonFatalErrors classified)) $ chaseMsg "Finished" mname Nothing)

      withMsgs $
        Bench.billTo [Bench.TopModule mname] $
        localTC (\ TCEnv
    e -> TCEnv
    e { envCurrentPath = Just sfi }) do

        let onlyScope = MainInterface
    isMain MainInterface -> MainInterface -> Bool
    forall a. Eq a => a -> a -> Bool
    == Mode -> MainInterface
    MainInterface Mode
    ScopeCheck

        reportSLn "import.iface.create" 5 $
          "Creating interface for " ++ prettyShow mname ++ "..."
        verboseS "import.iface.create" 10 $ do
          visited <- prettyShow <$> getPrettyVisitedModules
          reportSLn "import.iface.create" 10 $ "  visited: " ++ visited

        src <- maybe (parseSource sf) pure msrc

        srcPath <- srcFilePath $ srcOrigin src

        fileTokenInfo <- Bench.billTo [Bench.Highlighting] $
          generateTokenInfoFromSource
            (let !top = Source -> TopLevelModuleName
    srcModuleName Source
    src in
             mkRangeFile srcPath (Just top))
            (TL.unpack $ srcText src)
        stTokens `modifyTCLens` (fileTokenInfo <>)

        -- Only check consistency if not main (we check consistency for the main module in
        -- `typeCheckMain`.
        let checkConsistency | MainInterface{} <- MainInterface
    isMain = Bool
    False
                             | Bool
    otherwise                 = Bool
    True
        setOptionsFromSourcePragmas checkConsistency src
        checkAttributes (srcAttributes src)
        syntactic <- optSyntacticEquality <$> pragmaOptions
        localTC (\TCEnv
    env -> TCEnv
    env { envSyntacticEqualityFuel = syntactic }) $ do

        verboseS "import.iface.create" 15 $ do
          nestingLevel      <- asksTC (pred . length . envImportPath)
          highlightingLevel <- asksTC envHighlightingLevel
          reportSLn "import.iface.create" 15 $ unlines
            [ "  nesting      level: " ++ show nestingLevel
            , "  highlighting level: " ++ show highlightingLevel
            ]

        -- Scope checking.
        reportSLn "import.iface.create" 7 $ prettyShow mname ++ ": Starting scope checking."
        topLevel <- Bench.billTo [Bench.Scoping] $ do
          let topDecls = Module -> [Declaration]
    C.modDecls (Module -> [Declaration]) -> Module -> [Declaration]
    forall a b. (a -> b) -> a -> b
    $ Source -> Module
    srcModule Source
    src
          concreteToAbstract_ (TopLevel (srcOrigin src) mname topDecls)
        reportSLn "import.iface.create" 7 $ prettyShow mname ++ ": Finished scope checking."

        let ds    = TopLevelInfo -> [Declaration]
    topLevelDecls TopLevelInfo
    topLevel
            scope = TopLevelInfo -> ScopeInfo
    topLevelScope TopLevelInfo
    topLevel

        -- Highlighting from scope checker.
        reportSLn "import.iface.highlight" 15 $ prettyShow mname ++ ": Starting highlighting from scope."
        Bench.billTo [Bench.Highlighting] $ do
          -- Generate and print approximate syntax highlighting info.
          ifTopLevelAndHighlightingLevelIs NonInteractive $
            printHighlightingInfo KeepHighlighting fileTokenInfo
          ifTopLevelAndHighlightingLevelIsOr NonInteractive onlyScope $
            mapM_ (\ Declaration
    d -> Declaration -> Level -> Bool -> TCM ()
    generateAndPrintSyntaxInfo Declaration
    d Level
    Partial Bool
    onlyScope) ds
        reportSLn "import.iface.highlight" 15 $ prettyShow mname ++ ": Finished highlighting from scope."

        -- Type checking.

        -- Now that all the options are in we can check if caching should
        -- be on.
        activateLoadedFileCache

        -- invalidate cache if pragmas change, TODO move
        cachingStarts
        opts <- useTC stPragmaOptions
        me <- readFromCachedLog
        case me of
          Just (Pragmas PragmaOptions
    opts', PostScopeState
    _) | PragmaOptions
    opts PragmaOptions -> PragmaOptions -> Bool
    forall a. Eq a => a -> a -> Bool
    == PragmaOptions
    opts'
            -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          Maybe (TypeCheckAction, PostScopeState)
    _ -> do
            [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "cache" Int
    10 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "pragma changed: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Bool -> [Char]
    forall a. Show a => a -> [Char]
    show (Maybe (TypeCheckAction, PostScopeState) -> Bool
    forall a. Maybe a -> Bool
    isJust Maybe (TypeCheckAction, PostScopeState)
    me)
            TCM ()
    forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
    cleanCachedLog
        writeToCurrentLog $ Pragmas opts

        if onlyScope
          then do
            reportSLn "import.iface.create" 7 $ prettyShow mname ++ ": Skipping type checking."
            cacheCurrentLog
          else do
            reportSLn "import.iface.create" 7 $ prettyShow mname ++ ": Starting type checking."
            Bench.billTo [Bench.Typing] $ mapM_ checkDeclCached ds `finally_` cacheCurrentLog
            reportSLn "import.iface.create" 7 $ prettyShow mname ++ ": Finished type checking."

        -- Ulf, 2013-11-09: Since we're rethrowing the error, leave it up to the
        -- code that handles that error to reset the state.
        -- Ulf, 2013-11-13: Errors are now caught and highlighted in InteractionTop.
        -- catchError_ (checkDecls ds) $ \e -> do
        --   ifTopLevelAndHighlightingLevelIs NonInteractive $
        --     printErrorInfo e
        --   throwError e

        unfreezeMetas

        -- Profiling: Count number of metas.
        whenProfile Profile.Metas $ do
          m <- fresh
          tickN "metas" (fromIntegral (metaId m))

        -- Highlighting from type checker.
        reportSLn "import.iface.highlight" 15 $ prettyShow mname ++ ": Starting highlighting from type info."
        Bench.billTo [Bench.Highlighting] $ do

          -- Move any remaining token highlighting to stSyntaxInfo.
          toks <- useTC stTokens
          ifTopLevelAndHighlightingLevelIs NonInteractive $
            printHighlightingInfo KeepHighlighting toks
          stTokens `setTCLens` mempty

          -- Grabbing warnings and unsolved metas to highlight them
          warnings <- getAllWarnings AllWarnings
          unless (null warnings) $ reportSDoc "import.iface.highlight" 20 $
            "collected warnings: " <> prettyTCM warnings
          unsolved <- getAllUnsolvedWarnings
          unless (null unsolved) $ reportSDoc "import.iface.highlight" 20 $
            "collected unsolved: " <> prettyTCM unsolved
          let warningInfo =
                HighlightingInfoBuilder -> HighlightingInfo
    forall a b. Convert a b => a -> b
    Highlighting.convert (HighlightingInfoBuilder -> HighlightingInfo)
    -> HighlightingInfoBuilder -> HighlightingInfo
    forall a b. (a -> b) -> a -> b
    $ (TCWarning -> HighlightingInfoBuilder)
    -> Set TCWarning -> HighlightingInfoBuilder
    forall m a. Monoid m => (a -> m) -> Set a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap TCWarning -> HighlightingInfoBuilder
    warningHighlighting (Set TCWarning -> HighlightingInfoBuilder)
    -> Set TCWarning -> HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $ [TCWarning] -> Set TCWarning
    forall a. Ord a => [a] -> Set a
    Set.fromList [TCWarning]
    unsolved Set TCWarning -> Set TCWarning -> Set TCWarning
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.union` Set TCWarning
    warnings

          stSyntaxInfo `modifyTCLens` \HighlightingInfo
    inf -> (HighlightingInfo
    inf HighlightingInfo -> HighlightingInfo -> HighlightingInfo
    forall a. Monoid a => a -> a -> a
    `mappend` HighlightingInfo
    toks) HighlightingInfo -> HighlightingInfo -> HighlightingInfo
    forall a. Monoid a => a -> a -> a
    `mappend` HighlightingInfo
    warningInfo

          whenM (optGenerateVimFile <$> commandLineOptions) $
            -- Generate Vim file.
            withScope_ scope $ generateVimFile $ filePath $ srcPath
        reportSLn "import.iface.create" 15 $ prettyShow mname ++ ": Finished highlighting from type info."

        setScope scope
        reportSLn "scope.top" 50 $ "SCOPE " ++ show scope

        -- TODO: It would be nice if unsolved things were highlighted
        -- after every mutual block.

        openMetas <- getOpenMetas
        unless (null openMetas) $ do
          reportSLn "import.metas" 10 $ prettyShow mname ++ ": We have unsolved metas."
          reportSLn "import.metas" 10 =<< showGoals =<< getGoals

        ifTopLevelAndHighlightingLevelIs NonInteractive printUnsolvedInfo

        -- Andreas, 2016-08-03, issue #964
        -- When open metas are allowed,
        -- permanently freeze them now by turning them into postulates.
        -- This will enable serialization.
        -- savedMetaStore <- useTC stMetaStore
        unless (includeStateChanges isMain) $
          -- Andreas, 2018-11-15, re issue #3393:
          -- We do not get here when checking the main module
          -- (then includeStateChanges is True).
          whenM (optAllowUnsolved <$> pragmaOptions) $ do
            reportSLn "import.iface.create" 7 $ prettyShow mname ++ ": Turning unsolved metas (if any) into postulates."
            withCurrentModule (scope ^. scopeCurrent) openMetasToPostulates
            -- Clear constraints as they might refer to what
            -- they think are open metas.
            stAwakeConstraints    `setTCLens` []
            stSleepingConstraints `setTCLens` []

        -- Serialization.
        reportSLn "import.iface.create" 7 $ prettyShow mname ++ ": Starting serialization."
        i <- Bench.billTo [Bench.Serialization, Bench.BuildInterface] $
          buildInterface src topLevel

        reportS "tc.top" 101 $
          "Signature:" :
          [ unlines
              [ prettyShow q
              , "  type: " ++ show (defType def)
              , "  def:  " ++ show cc
              ]
          | (q, def) <- HMap.toList $ iSignature i ^. sigDefinitions,
            Function{ funCompiled = cc } <- [theDef def]
          ]
        reportSLn "import.iface.create" 7 $ prettyShow mname ++ ": Finished serialization."

        mallWarnings <- getAllWarnings' isMain ErrorWarnings

        reportSLn "import.iface.create" 7 $ prettyShow mname ++ ": Considering writing to interface file."
        finalIface <- constructIScope <$> case (null mallWarnings, isMain) of
          (Bool
    False, MainInterface
    _) -> do
            -- Andreas, 2018-11-15, re issue #3393
            -- The following is not sufficient to fix #3393
            -- since the replacement of metas by postulates did not happen.
            -- -- | not (allowUnsolved && all (isUnsolvedWarning . tcWarning) allWarnings) -> do
            [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.create" Int
    7 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow TopLevelModuleName
    mname [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ": We have warnings, skipping writing interface file."
            Interface -> TCMT IO Interface
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Interface
    i
          (Bool
    True, MainInterface Mode
    ScopeCheck) -> do
            [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.create" Int
    7 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow TopLevelModuleName
    mname [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ": We are just scope-checking, skipping writing interface file."
            Interface -> TCMT IO Interface
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Interface
    i
          (Bool
    True, MainInterface
    _) -> Account (BenchPhase (TCMT IO))
    -> TCMT IO Interface -> TCMT IO Interface
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (TCMT IO)
    Phase
    Bench.Serialization] (TCMT IO Interface -> TCMT IO Interface)
    -> TCMT IO Interface -> TCMT IO Interface
    forall a b. (a -> b) -> a -> b
    $ do
            [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.create" Int
    7 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow TopLevelModuleName
    mname [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ": Actually calling writeInterface."
            -- The file was successfully type-checked (and no warnings were
            -- encountered), so the interface should be written out.
            ifile <- HasCallStack => SourceFile -> TCMT IO AbsolutePath
    SourceFile -> TCMT IO AbsolutePath
    toIFile SourceFile
    sf
            serializedIface <- writeInterface ifile i
            reportSLn "import.iface.create" 7 $ prettyShow mname ++ ": Finished writing to interface file."
            return serializedIface

        -- -- Restore the open metas, as we might continue in interaction mode.
        -- Actually, we do not serialize the metas if checking the MainInterface
        -- stMetaStore `setTCLens` savedMetaStore

        -- Profiling: Print statistics.
        printStatistics (Just mname) =<< getStatistics

        -- Get the statistics of the current module
        -- and add it to the accumulated statistics.
        localStatistics <- getStatistics
        lensAccumStatistics `modifyTCLens` Map.unionWith (+) localStatistics
        reportSLn "import.iface" 25 $ prettyShow mname ++ ": Added statistics to the accumulated statistics."

        isPrimitiveMod <- isPrimitiveModule sfi

        return ModuleInfo
          { miInterface = finalIface
          , miWarnings = mallWarnings
          , miPrimitive = isPrimitiveMod
          , miMode = moduleCheckMode isMain
          }

    -- | Expert version of 'getAllWarnings'; if 'isMain' is a
    -- 'MainInterface', the warnings definitely include also unsolved
    -- warnings.

    getAllWarnings' :: (ReadTCState m, MonadWarning m, MonadTCM m) => MainInterface -> WhichWarnings -> m (Set TCWarning)
    getAllWarnings' :: forall (m :: * -> *).
    (ReadTCState m, MonadWarning m, MonadTCM m) =>
    MainInterface -> WhichWarnings -> m (Set TCWarning)
    getAllWarnings' (MainInterface Mode
    _) = Set WarningName -> WhichWarnings -> m (Set TCWarning)
    forall (m :: * -> *).
    (ReadTCState m, MonadWarning m, MonadTCM m) =>
    Set WarningName -> WhichWarnings -> m (Set TCWarning)
    getAllWarningsPreserving Set WarningName
    unsolvedWarnings
    getAllWarnings' MainInterface
    NotMainInterface  = Set WarningName -> WhichWarnings -> m (Set TCWarning)
    forall (m :: * -> *).
    (ReadTCState m, MonadWarning m, MonadTCM m) =>
    Set WarningName -> WhichWarnings -> m (Set TCWarning)
    getAllWarningsPreserving Set WarningName
    forall a. Set a
    Set.empty

    -- Andreas, issue 964: not checking null interactionPoints
    -- anymore; we want to serialize with open interaction points now!

    -- | Reconstruct the 'iScope' (not serialized)
    --   from the 'iInsideScope' (serialized).

    constructIScope :: Interface -> Interface
    constructIScope :: Interface -> Interface
    constructIScope Interface
    i = [Phase] -> Interface -> Interface
    forall a. [Phase] -> a -> a
    billToPure [ Phase
    Deserialization ] (Interface -> Interface) -> Interface -> Interface
    forall a b. (a -> b) -> a -> b
    $
      Interface
    i{ iScope = publicModules $ iInsideScope i }

    -- | Builds an interface for the current module, which should already
    --   have been successfully type checked.
    buildInterface
      :: Source
         -- ^ 'Source' for the current module.
      -> TopLevelInfo
         -- ^ 'TopLevelInfo' scope information for the current module.
      -> TCM Interface
    buildInterface :: Source -> TopLevelInfo -> TCMT IO Interface
    buildInterface Source
    src TopLevelInfo
    topLevel = do
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface" Int
    5 [Char]
    "Building interface..."
        let mname :: ModuleName
    mname = TopLevelInfo -> ModuleName
    CToA.topLevelModuleName TopLevelInfo
    topLevel
            source :: Text
    source   = Source -> Text
    srcText Source
    src
            fileType :: FileType
    fileType = Source -> FileType
    srcFileType Source
    src
            defPragmas :: [OptionsPragma]
    defPragmas = Source -> [OptionsPragma]
    srcDefaultPragmas Source
    src
            filePragmas :: [OptionsPragma]
    filePragmas  = Source -> [OptionsPragma]
    srcFilePragmas Source
    src

        -- Andreas, 2014-05-03: killRange did not result in significant reduction
        -- of .agdai file size, and lost a few seconds performance on library-test.
        -- Andreas, Makoto, 2014-10-18 AIM XX: repeating the experiment
        -- with discarding also the nameBindingSite in QName:
        -- Saves 10% on serialization time (and file size)!
        --
        -- NOTE: We no longer discard all nameBindingSites (but the commit
        -- that introduced this change seems to have made Agda a bit
        -- faster and interface file sizes a bit smaller, at least for the
        -- standard library).
        !mhs <- (TopLevelModuleName -> TCMT IO (TopLevelModuleName, Hash))
    -> [TopLevelModuleName] -> TCMT IO [(TopLevelModuleName, Hash)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (\TopLevelModuleName
    top -> (TopLevelModuleName
    top,) (Hash -> (TopLevelModuleName, Hash))
    -> TCM Hash -> TCMT IO (TopLevelModuleName, Hash)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TopLevelModuleName -> TCM Hash
    moduleHash TopLevelModuleName
    top) ([TopLevelModuleName] -> TCMT IO [(TopLevelModuleName, Hash)])
    -> (Set TopLevelModuleName -> [TopLevelModuleName])
    -> Set TopLevelModuleName
    -> TCMT IO [(TopLevelModuleName, Hash)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set TopLevelModuleName -> [TopLevelModuleName]
    forall a. Set a -> [a]
    Set.toAscList (Set TopLevelModuleName -> TCMT IO [(TopLevelModuleName, Hash)])
    -> TCMT IO (Set TopLevelModuleName)
    -> TCMT IO [(TopLevelModuleName, Hash)]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Lens' TCState (Set TopLevelModuleName)
    -> TCMT IO (Set TopLevelModuleName)
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (Set TopLevelModuleName -> f (Set TopLevelModuleName))
    -> TCState -> f TCState
    Lens' TCState (Set TopLevelModuleName)
    stImportedModules
        !foreignCode <- useTC stForeignCode

        let !scope = TopLevelInfo -> ScopeInfo
    topLevelScope TopLevelInfo
    topLevel

        (!solvedMetas, !definitions, !displayForms) <- eliminateDeadCode scope
        !sig <- set sigDefinitions definitions <$> getSignature

        -- Andreas, 2015-02-09 kill ranges in pattern synonyms before
        -- serialization to avoid error locations pointing to external files
        -- when expanding a pattern synonym.
        !patsyns <- killRange <$> getPatternSyns

        !userwarns   <- useTC stLocalUserWarnings
        !importwarn  <- useTC stWarningOnImport
        !syntaxInfo  <- useTC stSyntaxInfo
        !optionsUsed <- useTC stPragmaOptions
        !partialDefs <- useTC stLocalPartialDefs

        -- Only serialise the opaque blocks actually defined in this
        -- top-level module.
        !opaqueBlocks' <- useTC stOpaqueBlocks
        !opaqueIds' <- useTC stOpaqueIds
        let
          !mh = TopLevelModuleName -> ModuleNameHash
    forall range. TopLevelModuleName' range -> ModuleNameHash
    moduleNameId (Source -> TopLevelModuleName
    srcModuleName Source
    src)
          !opaqueBlocks = (OpaqueId -> OpaqueBlock -> Bool)
    -> Map OpaqueId OpaqueBlock -> Map OpaqueId OpaqueBlock
    forall k a. (k -> a -> Bool) -> Map k a -> Map k a
    Map.filterWithKey (\(OpaqueId Hash
    _ ModuleNameHash
    mod) OpaqueBlock
    _ -> ModuleNameHash
    mod ModuleNameHash -> ModuleNameHash -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModuleNameHash
    mh) Map OpaqueId OpaqueBlock
    opaqueBlocks'
          isLocal QName
    qnm = case Name -> NameId
    nameId (QName -> Name
    qnameName QName
    qnm) of
            NameId Hash
    _ ModuleNameHash
    mh' -> ModuleNameHash
    mh' ModuleNameHash -> ModuleNameHash -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModuleNameHash
    mh
          !opaqueIds = (QName -> OpaqueId -> Bool)
    -> Map QName OpaqueId -> Map QName OpaqueId
    forall k a. (k -> a -> Bool) -> Map k a -> Map k a
    Map.filterWithKey (\QName
    qnm (OpaqueId Hash
    _ ModuleNameHash
    mod) -> QName -> Bool
    isLocal QName
    qnm Bool -> Bool -> Bool
    || ModuleNameHash
    mod ModuleNameHash -> ModuleNameHash -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModuleNameHash
    mh) Map QName OpaqueId
    opaqueIds'

        !builtin  <- Map.mapWithKey (\ SomeBuiltin
    x Builtin PrimFun
    b -> SomeBuiltin -> PrimFun -> (PrimitiveId, QName)
    primName SomeBuiltin
    x (PrimFun -> (PrimitiveId, QName))
    -> Builtin PrimFun -> Builtin (PrimitiveId, QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Builtin PrimFun
    b) <$> useTC stLocalBuiltins
        !warnings <- Set.filter (isSourceCodeWarning . warningName . tcWarning) <$> getAllWarnings AllWarnings

        let !i = Interface
              { iSourceHash :: Hash
    iSourceHash           = Text -> Hash
    hashText Text
    source
              , iSource :: Text
    iSource               = Text
    source
              , iFileType :: FileType
    iFileType             = FileType
    fileType
              , iImportedModules :: [(TopLevelModuleName, Hash)]
    iImportedModules      = [(TopLevelModuleName, Hash)]
    mhs
              , iModuleName :: ModuleName
    iModuleName           = ModuleName
    mname
              , iTopLevelModuleName :: TopLevelModuleName
    iTopLevelModuleName   = Source -> TopLevelModuleName
    srcModuleName Source
    src
              , iScope :: Map ModuleName Scope
    iScope                = Map ModuleName Scope
    forall a. Null a => a
    empty -- publicModules scope
              , iInsideScope :: ScopeInfo
    iInsideScope          = ScopeInfo
    scope
              , iSignature :: Signature
    iSignature            = Signature
    sig
              , iMetaBindings :: RemoteMetaStore
    iMetaBindings         = RemoteMetaStore
    solvedMetas
              , iDisplayForms :: DisplayForms
    iDisplayForms         = DisplayForms
    displayForms
              , iUserWarnings :: UserWarnings
    iUserWarnings         = UserWarnings
    userwarns
              , iImportWarning :: Maybe Text
    iImportWarning        = Maybe Text
    importwarn
              , iBuiltin :: Map SomeBuiltin (Builtin (PrimitiveId, QName))
    iBuiltin              = Map SomeBuiltin (Builtin (PrimitiveId, QName))
    builtin
              , iForeignCode :: Map Text ForeignCodeStack
    iForeignCode          = Map Text ForeignCodeStack
    foreignCode
              , iHighlighting :: HighlightingInfo
    iHighlighting         = HighlightingInfo
    syntaxInfo
              , iDefaultPragmaOptions :: [OptionsPragma]
    iDefaultPragmaOptions = [OptionsPragma]
    defPragmas
              , iFilePragmaOptions :: [OptionsPragma]
    iFilePragmaOptions    = [OptionsPragma]
    filePragmas
              , iOptionsUsed :: PragmaOptions
    iOptionsUsed          = PragmaOptions
    optionsUsed
              , iPatternSyns :: PatternSynDefns
    iPatternSyns          = PatternSynDefns
    patsyns
              , iWarnings :: Set TCWarning
    iWarnings             = Set TCWarning
    warnings
              , iPartialDefs :: Set QName
    iPartialDefs          = Set QName
    partialDefs
              , iOpaqueBlocks :: Map OpaqueId OpaqueBlock
    iOpaqueBlocks         = Map OpaqueId OpaqueBlock
    opaqueBlocks
              , iOpaqueNames :: Map QName OpaqueId
    iOpaqueNames          = Map QName OpaqueId
    opaqueIds
              }
        !i <-
          ifM (optSaveMetas <$> pragmaOptions)
            (return i)
            (do reportSLn "import.iface" 7
                  "  instantiating all metavariables in interface"
                Bench.billTo [Bench.InterfaceInstantiateFull] $ liftReduce $ instantiateFull' i)
        reportSLn "import.iface" 7 "  interface complete"
        return i

        where
          primName :: SomeBuiltin -> PrimFun -> (PrimitiveId, QName)
    primName (PrimitiveName PrimitiveId
    x) PrimFun
    b = (PrimitiveId
    x, PrimFun -> QName
    primFunName PrimFun
    b)
          primName (BuiltinName BuiltinId
    x)   PrimFun
    b = (PrimitiveId, QName)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Returns (iSourceHash, iFullHash)
    --   We do not need to check that the file exist because we only
    --   accept @InterfaceFile@ as an input and not arbitrary @AbsolutePath@!
    getInterfaceFileHashes :: InterfaceFile -> IO (Maybe (Hash, Hash))
    getInterfaceFileHashes :: InterfaceFile -> IO (Maybe (Hash, Hash))
    getInterfaceFileHashes InterfaceFile
    fp = do
      let ifile :: [Char]
    ifile = AbsolutePath -> [Char]
    filePath (AbsolutePath -> [Char]) -> AbsolutePath -> [Char]
    forall a b. (a -> b) -> a -> b
    $ InterfaceFile -> AbsolutePath
    intFilePath InterfaceFile
    fp
      (s, close) <- [Char] -> IO (ByteString, IO ())
    readBinaryFile' [Char]
    ifile
      let hs = ByteString -> Maybe (Hash, Hash)
    decodeHashes ByteString
    s
      maybe 0 (uncurry (+)) hs `seq` close
      return hs

    moduleHash :: TopLevelModuleName -> TCM Hash
    moduleHash :: TopLevelModuleName -> TCM Hash
    moduleHash TopLevelModuleName
    m = Interface -> Hash
    iFullHash (Interface -> Hash) -> TCMT IO Interface -> TCM Hash
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TopLevelModuleName -> Maybe Source -> TCMT IO Interface
    getNonMainInterface TopLevelModuleName
    m Maybe Source
    forall a. Maybe a
    Nothing