    {-# LANGUAGE CPP #-}

    {-| 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

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

    import Prelude hiding (null)

    import Control.Monad               ( forM, forM_, void )
    import Control.Monad.Except
    import Control.Monad.IO.Class      ( MonadIO(..) )
    import Control.Monad.State
    import Control.Monad.Trans.Maybe
    import qualified Control.Exception as E

    #if __GLASGOW_HASKELL__ < 808
    import Control.Monad.Fail (MonadFail)
    #endif

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

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

    import Agda.Benchmarking

    import qualified Agda.Syntax.Abstract as A
    import qualified Agda.Syntax.Concrete as C
    import Agda.Syntax.Abstract.Name
    import Agda.Syntax.Common
    import Agda.Syntax.Parser
    import Agda.Syntax.Position
    import Agda.Syntax.Scope.Base
    import Agda.Syntax.Translation.ConcreteToAbstract

    import Agda.TypeChecking.Errors
    import Agda.TypeChecking.Warnings hiding (warnings)
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Rewriting.Confluence ( checkConfluenceOfRules )
    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 Agda.Interaction.Highlighting.Precise  ( 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.FileName
    import Agda.Utils.Lens
    import Agda.Utils.Maybe
    import qualified Agda.Utils.Maybe.Strict as Strict
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.IO.Binary
    import Agda.Utils.Pretty hiding (Mode)
    import Agda.Utils.Hash
    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  :: C.TopLevelModuleName  -- ^ The top-level module name.
      , Source -> [AgdaLibFile]
    srcProjectLibs :: [AgdaLibFile]         -- ^ The .agda-lib file(s) of the project this file belongs to.
      }

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

    parseSource :: SourceFile -> TCM Source
    parseSource :: SourceFile -> TCM Source
    parseSource sourceFile :: SourceFile
    sourceFile@(SourceFile AbsolutePath
    f) = 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
      Text
    source                <- PM Text -> TCM Text
    forall a. PM a -> TCM a
    runPM (PM Text -> TCM Text) -> PM Text -> TCM Text
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath -> PM Text
    readFilePM AbsolutePath
    f
      (Module
    parsedMod, FileType
    fileType) <- PM (Module, FileType) -> TCM (Module, FileType)
    forall a. PM a -> TCM a
    runPM (PM (Module, FileType) -> TCM (Module, FileType))
    -> PM (Module, FileType) -> TCM (Module, FileType)
    forall a b. (a -> b) -> a -> b
    $
                               Parser Module -> AbsolutePath -> [Char] -> PM (Module, FileType)
    forall a.
    Show a =>
    Parser a -> AbsolutePath -> [Char] -> PM (a, FileType)
    parseFile Parser Module
    moduleParser AbsolutePath
    f ([Char] -> PM (Module, FileType))
    -> [Char] -> PM (Module, FileType)
    forall a b. (a -> b) -> a -> b
    $ Text -> [Char]
    TL.unpack Text
    source
      TopLevelModuleName
    parsedModName         <- AbsolutePath -> Module -> TCM TopLevelModuleName
    moduleName AbsolutePath
    f Module
    parsedMod
      [AgdaLibFile]
    libs <- [Char] -> TCM [AgdaLibFile]
    getAgdaLibFiles ([Char] -> TCM [AgdaLibFile]) -> [Char] -> TCM [AgdaLibFile]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Char]
    takeDirectory ([Char] -> [Char]) -> [Char] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath -> [Char]
    filePath AbsolutePath
    f
      Source -> TCM Source
    forall (m :: * -> *) a. Monad m => a -> m a
    return Source :: Text
    -> FileType
    -> SourceFile
    -> Module
    -> TopLevelModuleName
    -> [AgdaLibFile]
    -> Source
    Source
        { srcText :: Text
    srcText        = Text
    source
        , srcFileType :: FileType
    srcFileType    = FileType
    fileType
        , srcOrigin :: SourceFile
    srcOrigin      = SourceFile
    sourceFile
        , srcModule :: Module
    srcModule      = Module
    parsedMod
        , srcModuleName :: TopLevelModuleName
    srcModuleName  = TopLevelModuleName
    parsedModName
        , srcProjectLibs :: [AgdaLibFile]
    srcProjectLibs = [AgdaLibFile]
    libs
        }

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

    srcFilePragmas :: Source -> [OptionsPragma]
    srcFilePragmas :: Source -> [[[Char]]]
    srcFilePragmas Source
    src = [[[Char]]]
    pragmas
      where
      cpragmas :: [Pragma]
    cpragmas = Module -> [Pragma]
    C.modPragmas (Source -> Module
    srcModule Source
    src)
      pragmas :: [[[Char]]]
    pragmas = [ [[Char]]
    opts | C.OptionsPragma Range
    _ [[Char]]
    opts <- [Pragma]
    cpragmas ]

    srcPragmas :: Source -> [OptionsPragma]
    srcPragmas :: Source -> [[[Char]]]
    srcPragmas Source
    src = Source -> [[[Char]]]
    srcDefaultPragmas Source
    src [[[Char]]] -> [[[Char]]] -> [[[Char]]]
    forall a. [a] -> [a] -> [a]
    ++ Source -> [[[Char]]]
    srcFilePragmas Source
    src

    -- | Set options from a 'Source' pragma, using the source
    --   ranges of the pragmas for error reporting.
    setOptionsFromSourcePragmas :: Source -> TCM ()
    setOptionsFromSourcePragmas :: Source -> TCM ()
    setOptionsFromSourcePragmas Source
    src =
      [Pragma] -> TCM () -> TCM ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange (Module -> [Pragma]
    C.modPragmas (Module -> [Pragma]) -> (Source -> Module) -> Source -> [Pragma]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Source -> Module
    srcModule (Source -> [Pragma]) -> Source -> [Pragma]
    forall a b. (a -> b) -> a -> b
    $ Source
    src) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        ([[Char]] -> TCM ()) -> [[[Char]]] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ [[Char]] -> TCM ()
    setOptionsFromPragma (Source -> [[[Char]]]
    srcPragmas Source
    src)

    -- | 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
    /= :: Mode -> Mode -> Bool
    $c/= :: Mode -> Mode -> Bool
    == :: Mode -> Mode -> Bool
    $c== :: Mode -> Mode -> Bool
    Eq, Int -> Mode -> [Char] -> [Char]
    [Mode] -> [Char] -> [Char]
    Mode -> [Char]
    (Int -> Mode -> [Char] -> [Char])
    -> (Mode -> [Char]) -> ([Mode] -> [Char] -> [Char]) -> Show Mode
    forall a.
    (Int -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    showList :: [Mode] -> [Char] -> [Char]
    $cshowList :: [Mode] -> [Char] -> [Char]
    show :: Mode -> [Char]
    $cshow :: Mode -> [Char]
    showsPrec :: Int -> Mode -> [Char] -> [Char]
    $cshowsPrec :: Int -> Mode -> [Char] -> [Char]
    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
    /= :: MainInterface -> MainInterface -> Bool
    $c/= :: MainInterface -> MainInterface -> Bool
    == :: MainInterface -> MainInterface -> Bool
    $c== :: MainInterface -> MainInterface -> Bool
    Eq, Int -> MainInterface -> [Char] -> [Char]
    [MainInterface] -> [Char] -> [Char]
    MainInterface -> [Char]
    (Int -> MainInterface -> [Char] -> [Char])
    -> (MainInterface -> [Char])
    -> ([MainInterface] -> [Char] -> [Char])
    -> Show MainInterface
    forall a.
    (Int -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    showList :: [MainInterface] -> [Char] -> [Char]
    $cshowList :: [MainInterface] -> [Char] -> [Char]
    show :: MainInterface -> [Char]
    $cshow :: MainInterface -> [Char]
    showsPrec :: Int -> MainInterface -> [Char] -> [Char]
    $cshowsPrec :: Int -> MainInterface -> [Char] -> [Char]
    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 :: [([Char], Builtin ([Char], QName))]
    builtin = Map [Char] (Builtin ([Char], QName))
    -> [([Char], Builtin ([Char], QName))]
    forall k a. Map k a -> [(k, a)]
    Map.toAscList (Map [Char] (Builtin ([Char], QName))
     -> [([Char], Builtin ([Char], QName))])
    -> Map [Char] (Builtin ([Char], QName))
    -> [([Char], Builtin ([Char], QName))]
    forall a b. (a -> b) -> a -> b
    $ Interface -> Map [Char] (Builtin ([Char], QName))
    iBuiltin Interface
    i
            prim :: [([Char], QName)]
    prim    = [ ([Char], QName)
    x | ([Char]
    _,Prim ([Char], QName)
    x) <- [([Char], Builtin ([Char], QName))]
    builtin ]
            bi :: Map [Char] (Builtin PrimFun)
    bi      = [([Char], Builtin PrimFun)] -> Map [Char] (Builtin PrimFun)
    forall k a. [(k, a)] -> Map k a
    Map.fromDistinctAscList [ ([Char]
    x, Term -> Builtin PrimFun
    forall pf. Term -> Builtin pf
    Builtin Term
    t) | ([Char]
    x, Builtin Term
    t) <- [([Char], Builtin ([Char], QName))]
    builtin ]
                        -- Andreas, 2021-08-19: this seeming identity filters out the @Prim@s
                        -- and converts the type.
            warns :: [TCWarning]
    warns   = Interface -> [TCWarning]
    iWarnings Interface
    i
        Map [Char] (Builtin PrimFun)
    bs <- (TCState -> Map [Char] (Builtin PrimFun))
    -> TCMT IO (Map [Char] (Builtin PrimFun))
    forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
    getsTC TCState -> Map [Char] (Builtin PrimFun)
    stBuiltinThings
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.merge" Int
    10 [Char]
    "Merging interface"
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.merge" Int
    20 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          [Char]
    "  Current builtins " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [[Char]] -> [Char]
    forall a. Show a => a -> [Char]
    show (Map [Char] (Builtin PrimFun) -> [[Char]]
    forall k a. Map k a -> [k]
    Map.keys Map [Char] (Builtin PrimFun)
    bs) [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "\n" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
          [Char]
    "  New builtins     " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [[Char]] -> [Char]
    forall a. Show a => a -> [Char]
    show (Map [Char] (Builtin PrimFun) -> [[Char]]
    forall k a. Map k a -> [k]
    Map.keys Map [Char] (Builtin PrimFun)
    bi)
        let check :: [Char] -> Builtin pf -> Builtin pf -> m ()
    check [Char]
    b (Builtin Term
    x) (Builtin Term
    y)
                  | Term
    x Term -> Term -> Bool
    forall a. Eq a => a -> a -> Bool
    == Term
    y    = () -> m ()
    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
    $ [Char] -> Term -> Term -> TypeError
    DuplicateBuiltinBinding [Char]
    b Term
    x Term
    y
            check [Char]
    _ Builtin pf
    _ Builtin pf
    _ = m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Map [Char] (TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, Monad m) =>
    t (m a) -> m ()
    sequence_ (Map [Char] (TCM ()) -> TCM ()) -> Map [Char] (TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ([Char] -> Builtin PrimFun -> Builtin PrimFun -> TCM ())
    -> Map [Char] (Builtin PrimFun)
    -> Map [Char] (Builtin PrimFun)
    -> Map [Char] (TCM ())
    forall k a b c.
    Ord k =>
    (k -> a -> b -> c) -> Map k a -> Map k b -> Map k c
    Map.intersectionWithKey [Char] -> Builtin PrimFun -> Builtin PrimFun -> TCM ()
    forall {m :: * -> *} {pf} {pf}.
    (MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
    [Char] -> Builtin pf -> Builtin pf -> m ()
    check Map [Char] (Builtin PrimFun)
    bs Map [Char] (Builtin PrimFun)
    bi
        Signature
    -> Map [Char] (Builtin PrimFun)
    -> PatternSynDefns
    -> DisplayForms
    -> Map QName Text
    -> Set QName
    -> [TCWarning]
    -> TCM ()
    addImportedThings Signature
    sig Map [Char] (Builtin PrimFun)
    bi
          (Interface -> PatternSynDefns
    iPatternSyns Interface
    i)
          (Interface -> DisplayForms
    iDisplayForms Interface
    i)
          (Interface -> Map QName Text
    iUserWarnings Interface
    i)
          (Interface -> Set QName
    iPartialDefs Interface
    i)
          [TCWarning]
    warns
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.merge" Int
    20 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          [Char]
    "  Rebinding primitives " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [([Char], QName)] -> [Char]
    forall a. Show a => a -> [Char]
    show [([Char], QName)]
    prim
        (([Char], QName) -> TCM ()) -> [([Char], QName)] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ ([Char], QName) -> TCM ()
    rebind [([Char], QName)]
    prim
        TCMT IO (Maybe ConfluenceCheck)
    -> (ConfluenceCheck -> TCM ()) -> TCM ()
    forall (m :: * -> *) a.
    Monad m =>
    m (Maybe a) -> (a -> m ()) -> m ()
    whenJustM (PragmaOptions -> Maybe ConfluenceCheck
    optConfluenceCheck (PragmaOptions -> Maybe ConfluenceCheck)
    -> TCMT IO PragmaOptions -> TCMT IO (Maybe ConfluenceCheck)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions) ((ConfluenceCheck -> TCM ()) -> TCM ())
    -> (ConfluenceCheck -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ConfluenceCheck
    confChk -> do
          [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.confluence" Int
    20 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  Checking confluence of imported rewrite rules"
          ConfluenceCheck -> [RewriteRule] -> TCM ()
    checkConfluenceOfRules ConfluenceCheck
    confChk ([RewriteRule] -> TCM ()) -> [RewriteRule] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [[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' (HashMap QName [RewriteRule]) Signature
    -> HashMap QName [RewriteRule]
    forall o i. o -> Lens' i o -> i
    ^. Lens' (HashMap QName [RewriteRule]) Signature
    sigRewriteRules
        where
            rebind :: ([Char], QName) -> TCM ()
    rebind ([Char]
    x, QName
    q) = do
                PrimImpl Type
    _ PrimFun
    pf <- [Char] -> TCM PrimitiveImpl
    lookupPrimitiveFunction [Char]
    x
                Lens' (Map [Char] (Builtin PrimFun)) TCState
    stImportedBuiltins Lens' (Map [Char] (Builtin PrimFun)) TCState
    -> (Map [Char] (Builtin PrimFun) -> Map [Char] (Builtin PrimFun))
    -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    `modifyTCLens` [Char]
    -> Builtin PrimFun
    -> Map [Char] (Builtin PrimFun)
    -> Map [Char] (Builtin PrimFun)
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert [Char]
    x (PrimFun -> Builtin PrimFun
    forall pf. pf -> Builtin pf
    Prim PrimFun
    pf{ primFunName :: QName
    primFunName = QName
    q })

    addImportedThings
      :: Signature
      -> BuiltinThings PrimFun
      -> A.PatternSynDefns
      -> DisplayForms
      -> Map A.QName Text      -- ^ Imported user warnings
      -> Set QName             -- ^ Name of imported definitions which are partial
      -> [TCWarning]
      -> TCM ()
    addImportedThings :: Signature
    -> Map [Char] (Builtin PrimFun)
    -> PatternSynDefns
    -> DisplayForms
    -> Map QName Text
    -> Set QName
    -> [TCWarning]
    -> TCM ()
    addImportedThings Signature
    isig Map [Char] (Builtin PrimFun)
    ibuiltin PatternSynDefns
    patsyns DisplayForms
    display Map QName Text
    userwarn Set QName
    partialdefs [TCWarning]
    warnings = do
      Lens' Signature TCState
    stImports              Lens' Signature TCState -> (Signature -> Signature) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    `modifyTCLens` \ Signature
    imp -> [Signature] -> Signature
    unionSignatures [Signature
    imp, Signature
    isig]
      Lens' (Map [Char] (Builtin PrimFun)) TCState
    stImportedBuiltins     Lens' (Map [Char] (Builtin PrimFun)) TCState
    -> (Map [Char] (Builtin PrimFun) -> Map [Char] (Builtin PrimFun))
    -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    `modifyTCLens` \ Map [Char] (Builtin PrimFun)
    imp -> Map [Char] (Builtin PrimFun)
    -> Map [Char] (Builtin PrimFun) -> Map [Char] (Builtin PrimFun)
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union Map [Char] (Builtin PrimFun)
    imp Map [Char] (Builtin PrimFun)
    ibuiltin
      Lens' (Map QName Text) TCState
    stImportedUserWarnings Lens' (Map QName Text) TCState
    -> (Map QName Text -> Map QName Text) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    `modifyTCLens` \ Map QName Text
    imp -> Map QName Text -> Map QName Text -> Map QName Text
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union Map QName Text
    imp Map QName Text
    userwarn
      Lens' (Set QName) TCState
    stImportedPartialDefs  Lens' (Set QName) TCState -> (Set QName -> Set QName) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (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
      Lens' PatternSynDefns TCState
    stPatternSynImports    Lens' PatternSynDefns TCState
    -> (PatternSynDefns -> PatternSynDefns) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (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
      Lens' DisplayForms TCState
    stImportedDisplayForms Lens' DisplayForms TCState
    -> (DisplayForms -> DisplayForms) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    `modifyTCLens` \ DisplayForms
    imp -> ([Open DisplayForm] -> [Open DisplayForm] -> [Open DisplayForm])
    -> DisplayForms -> DisplayForms -> DisplayForms
    forall k v.
    (Eq k, Hashable k) =>
    (v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
    HMap.unionWith [Open DisplayForm] -> [Open DisplayForm] -> [Open DisplayForm]
    forall a. [a] -> [a] -> [a]
    (++) DisplayForms
    imp DisplayForms
    display
      Lens' [TCWarning] TCState
    stTCWarnings           Lens' [TCWarning] TCState -> ([TCWarning] -> [TCWarning]) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    `modifyTCLens` \ [TCWarning]
    imp -> [TCWarning]
    imp [TCWarning] -> [TCWarning] -> [TCWarning]
    forall a. Eq a => [a] -> [a] -> [a]
    `List.union` [TCWarning]
    warnings
      Signature -> TCM ()
    addImportedInstances Signature
    isig

    -- | Scope checks the given module. A proper version of the module
    -- name (with correct definition sites) is returned.

    scopeCheckImport :: ModuleName -> TCM (ModuleName, Map ModuleName Scope)
    scopeCheckImport :: ModuleName -> TCM (ModuleName, Map ModuleName Scope)
    scopeCheckImport ModuleName
    x = do
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.scope" Int
    5 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Scope checking " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ ModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow ModuleName
    x
        [Char] -> Int -> TCM () -> TCM ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
    verboseS [Char]
    "import.scope" Int
    10 (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          [Char]
    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
          [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.scope" Int
    10 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  visited: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    visited
        -- Since scopeCheckImport is called from the scope checker,
        -- we need to reimburse her account.
        Interface
    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 (ModuleName -> TopLevelModuleName
    toTopLevelModuleName ModuleName
    x) Maybe Source
    forall a. Maybe a
    Nothing
        ModuleName -> TCM ()
    addImport ModuleName
    x

        -- If that interface was supposed to raise a warning on import, do so.
        Maybe Text -> (Text -> TCM ()) -> TCM ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust (Interface -> Maybe Text
    iImportWarning Interface
    i) ((Text -> TCM ()) -> TCM ()) -> (Text -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> (Text -> Warning) -> Text -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Text -> Warning
    UserWarning

        -- let s = publicModules $ iInsideScope i
        let s :: Map ModuleName Scope
    s = Interface -> Map ModuleName Scope
    iScope Interface
    i
        (ModuleName, Map ModuleName Scope)
    -> TCM (ModuleName, Map ModuleName Scope)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Interface -> ModuleName
    iModuleName Interface
    i ModuleName -> QName -> ModuleName
    `withRangesOfQ` ModuleName -> QName
    mnameToConcrete ModuleName
    x, Map ModuleName Scope
    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 :: C.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
        ModuleInfo
    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

        Bool -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (ModuleInfo -> ModuleCheckMode
    miMode ModuleInfo
    mi ModuleCheckMode -> ModuleCheckMode -> Bool
    forall a. Ord a => a -> a -> Bool
    < ModuleCheckMode
    mode) (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 e (m :: * -> *) a. MonadError e m => e -> m a
    throwError [Char]
    "previously-visited interface was not sufficiently checked"

        Bool -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([TCWarning] -> Bool
    forall a. Null a => a -> Bool
    null ([TCWarning] -> Bool) -> [TCWarning] -> Bool
    forall a b. (a -> b) -> a -> b
    $ ModuleInfo -> [TCWarning]
    miWarnings ModuleInfo
    mi) (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 e (m :: * -> *) a. MonadError e m => e -> m a
    throwError [Char]
    "previously-visited interface had warnings"

        [Char] -> Int -> [Char] -> ExceptT [Char] (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.visit" Int
    10 ([Char] -> ExceptT [Char] (TCMT IO) ())
    -> [Char] -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  Already visited " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ TopLevelModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow TopLevelModuleName
    x

        TCM ModuleInfo -> ExceptT [Char] (TCMT IO) ModuleInfo
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM ModuleInfo -> ExceptT [Char] (TCMT IO) ModuleInfo)
    -> TCM ModuleInfo -> ExceptT [Char] (TCMT IO) ModuleInfo
    forall a b. (a -> b) -> a -> b
    $ ModuleInfo -> TCM ModuleInfo
    processResultingModule ModuleInfo
    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 -> [TCWarning]
    miWarnings = [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
        [TCWarning]
    wt <- [TCWarning] -> Maybe [TCWarning] -> [TCWarning]
    forall a. a -> Maybe a -> a
    fromMaybe [TCWarning]
    ws (Maybe [TCWarning] -> [TCWarning])
    -> TCMT IO (Maybe [TCWarning]) -> TCMT IO [TCWarning]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (MainInterface
    -> Bool
    -> PragmaOptions
    -> Interface
    -> TCMT IO (Maybe [TCWarning])
    getOptionsCompatibilityWarnings MainInterface
    isMain Bool
    isPrim PragmaOptions
    currentOptions Interface
    i)

        ModuleInfo -> TCM ModuleInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return ModuleInfo
    mi { miWarnings :: [TCWarning]
    miWarnings = [TCWarning]
    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] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ TopLevelModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow TopLevelModuleName
    x
        ModuleInfo
    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
        [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]
    "  Now we've looked at " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ TopLevelModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow TopLevelModuleName
    x

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

        [Char] -> Int -> [[Char]] -> TCM ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    [Char] -> Int -> a -> m ()
    reportS [Char]
    "warning.import" Int
    10
          [ [Char]
    "module: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ List1 [Char] -> [Char]
    forall a. Show a => a -> [Char]
    show (TopLevelModuleName -> List1 [Char]
    C.moduleNameParts TopLevelModuleName
    x)
          , [Char]
    "WarningOnImport: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Maybe Text -> [Char]
    forall a. Show a => a -> [Char]
    show (Interface -> Maybe Text
    iImportWarning (ModuleInfo -> Interface
    miInterface ModuleInfo
    mi))
          ]

        ModuleInfo -> TCM ()
    visitModule ModuleInfo
    mi
        ModuleInfo -> TCM ModuleInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return ModuleInfo
    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 -> [TCWarning] -> ModuleCheckMode -> Source -> CheckResult
    pattern $mCheckResult :: forall {r}.
    CheckResult
    -> (Interface -> [TCWarning] -> ModuleCheckMode -> Source -> r)
    -> (Void# -> r)
    -> r
    CheckResult { CheckResult -> Interface
    crInterface, CheckResult -> [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
      [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.main" Int
    10 [Char]
    "Importing the primitive modules."
      [Char]
    libdirPrim <- IO [Char] -> TCMT IO [Char]
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO IO [Char]
    getPrimitiveLibDir
      [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.main" Int
    20 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Library primitive dir = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [Char]
    forall a. Show a => a -> [Char]
    show [Char]
    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.
      TCMT IO PersistentVerbosity
    -> (PersistentVerbosity -> TCM ()) -> TCM () -> TCM ()
    forall (m :: * -> *) a b.
    Monad m =>
    m a -> (a -> m ()) -> m b -> m b
    bracket_ ((TCState -> PersistentVerbosity) -> TCMT IO PersistentVerbosity
    forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
    getsTC TCState -> PersistentVerbosity
    forall a. LensPersistentVerbosity a => a -> PersistentVerbosity
    Lens.getPersistentVerbosity) PersistentVerbosity -> TCM ()
    forall (m :: * -> *). MonadTCState m => PersistentVerbosity -> m ()
    Lens.putPersistentVerbosity (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        (PersistentVerbosity -> PersistentVerbosity) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (PersistentVerbosity -> PersistentVerbosity) -> m ()
    Lens.modifyPersistentVerbosity ([[Char]] -> PersistentVerbosity -> PersistentVerbosity
    forall k v. Ord k => [k] -> Trie k v -> Trie k v
    Trie.delete [])  -- set root verbosity to 0

        -- We don't want to generate highlighting information for Agda.Primitive.
        HighlightingLevel -> TCM () -> TCM ()
    forall a. HighlightingLevel -> TCM a -> TCM a
    withHighlightingLevel HighlightingLevel
    None (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          Set [Char] -> ([Char] -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ (([Char] -> [Char]) -> Set [Char] -> Set [Char]
    forall b a. Ord b => (a -> b) -> Set a -> Set b
    Set.map ([Char]
    libdirPrim [Char] -> [Char] -> [Char]
    </>) Set [Char]
    Lens.primitiveModules) (([Char] -> TCM ()) -> TCM ()) -> ([Char] -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \[Char]
    f -> do
            Source
    primSource <- SourceFile -> TCM Source
    parseSource (AbsolutePath -> SourceFile
    SourceFile (AbsolutePath -> SourceFile) -> AbsolutePath -> SourceFile
    forall a b. (a -> b) -> a -> b
    $ [Char] -> AbsolutePath
    mkAbsolute [Char]
    f)
            TopLevelModuleName -> SourceFile -> TCM ()
    checkModuleName' (Source -> TopLevelModuleName
    srcModuleName Source
    primSource) (Source -> SourceFile
    srcOrigin Source
    primSource)
            TCMT IO Interface -> TCM ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void (TCMT IO Interface -> TCM ()) -> TCMT IO Interface -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleName -> Maybe Source -> TCMT IO Interface
    getNonMainInterface (Source -> TopLevelModuleName
    srcModuleName Source
    primSource) (Source -> Maybe Source
    forall a. a -> Maybe a
    Just Source
    primSource)

      [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.main" Int
    10 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Done importing the primitive modules."

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

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

      ModuleInfo
    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)

      Lens' (Maybe ModuleName) TCState
    stCurrentModule Lens' (Maybe ModuleName) TCState -> Maybe ModuleName -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    `setTCLens` ModuleName -> Maybe ModuleName
    forall a. a -> Maybe a
    Just (Interface -> ModuleName
    iModuleName (ModuleInfo -> Interface
    miInterface ModuleInfo
    mi))

      CheckResult -> TCM CheckResult
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CheckResult -> TCM CheckResult) -> CheckResult -> TCM CheckResult
    forall a b. (a -> b) -> a -> b
    $ ModuleInfo -> Source -> CheckResult
    CheckResult' ModuleInfo
    mi Source
    src
      where
      checkModuleName' :: TopLevelModuleName -> SourceFile -> TCM ()
    checkModuleName' TopLevelModuleName
    m SourceFile
    f =
        -- 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).
        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

    -- | 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
      :: C.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
      -- Preserve/restore the current pragma options, which will be mutated when loading
      -- and checking the interface.
      ModuleInfo
    mi <- 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' PragmaOptions TCState -> TCMT IO PragmaOptions
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' PragmaOptions TCState
    stPragmaOptions) (Lens' PragmaOptions TCState
    stPragmaOptions Lens' PragmaOptions TCState -> PragmaOptions -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> 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
      [TCWarning] -> TCM ()
    tcWarningsToError ([TCWarning] -> TCM ()) -> [TCWarning] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ModuleInfo -> [TCWarning]
    miWarnings ModuleInfo
    mi
      Interface -> TCMT IO Interface
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ModuleInfo -> Interface
    miInterface ModuleInfo
    mi)

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

    getInterface
      :: C.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
         PragmaOptions
    currentOptions <- Lens' PragmaOptions TCState -> TCMT IO PragmaOptions
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' PragmaOptions TCState
    stPragmaOptions
         Maybe [Pragma] -> TCM () -> TCM ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange (Module -> [Pragma]
    C.modPragmas (Module -> [Pragma]) -> (Source -> Module) -> Source -> [Pragma]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Source -> Module
    srcModule (Source -> [Pragma]) -> Maybe Source -> Maybe [Pragma]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe Source
    msrc) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
           -- Now reset the options
           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

         TopLevelModuleName
    -> MainInterface
    -> PragmaOptions
    -> TCM ModuleInfo
    -> TCM ModuleInfo
    alreadyVisited TopLevelModuleName
    x MainInterface
    isMain PragmaOptions
    currentOptions (TCM ModuleInfo -> TCM ModuleInfo)
    -> TCM ModuleInfo -> TCM ModuleInfo
    forall a b. (a -> b) -> a -> b
    $ do
          SourceFile
    file <- case Maybe Source
    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' (Map TopLevelModuleName AbsolutePath) TCState
    -> (Map TopLevelModuleName AbsolutePath
        -> Map TopLevelModuleName AbsolutePath)
    -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    modifyTCLens Lens' (Map TopLevelModuleName AbsolutePath) TCState
    stModuleToSource ((Map TopLevelModuleName AbsolutePath
      -> Map TopLevelModuleName AbsolutePath)
     -> TCM ())
    -> (Map TopLevelModuleName AbsolutePath
        -> Map TopLevelModuleName AbsolutePath)
    -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleName
    -> AbsolutePath
    -> Map TopLevelModuleName AbsolutePath
    -> Map TopLevelModuleName AbsolutePath
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert TopLevelModuleName
    x (SourceFile -> AbsolutePath
    srcFilePath SourceFile
    file)
              SourceFile -> TCMT IO SourceFile
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure SourceFile
    file
          [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface" Int
    15 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    List.intercalate [Char]
    "\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ ([Char] -> [Char]) -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char]
    "  " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++)
            [ [Char]
    "module: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ TopLevelModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow TopLevelModuleName
    x
            , [Char]
    "file:   " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ SourceFile -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow SourceFile
    file
            ]

          [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface" Int
    10 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  Check for cycle"
          TCM ()
    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
          Either [Char] ModuleInfo
    stored <- ExceptT [Char] (TCMT IO) ModuleInfo
    -> TCM (Either [Char] ModuleInfo)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (ExceptT [Char] (TCMT IO) ModuleInfo
     -> TCM (Either [Char] ModuleInfo))
    -> ExceptT [Char] (TCMT IO) ModuleInfo
    -> TCM (Either [Char] ModuleInfo)
    forall a b. (a -> b) -> a -> b
    $ Account (BenchPhase (ExceptT [Char] (TCMT IO)))
    -> ExceptT [Char] (TCMT IO) ModuleInfo
    -> ExceptT [Char] (TCMT IO) ModuleInfo
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (ExceptT [Char] (TCMT IO))
    Phase
    Bench.Import] (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
            TopLevelModuleName
    -> SourceFile
    -> Maybe Source
    -> ExceptT [Char] (TCMT IO) ModuleInfo
    getStoredInterface TopLevelModuleName
    x SourceFile
    file Maybe Source
    msrc

          let recheck :: [Char] -> TCM ModuleInfo
    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
                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

          ([Char] -> TCM ModuleInfo)
    -> (ModuleInfo -> TCM ModuleInfo)
    -> Either [Char] ModuleInfo
    -> TCM ModuleInfo
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either [Char] -> TCM ModuleInfo
    recheck ModuleInfo -> TCM ModuleInfo
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Either [Char] ModuleInfo
    stored

    -- | 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 -> ModuleName -> TCM Bool
    checkOptionsCompatible :: PragmaOptions -> PragmaOptions -> ModuleName -> TCM Bool
    checkOptionsCompatible PragmaOptions
    current PragmaOptions
    imported ModuleName
    importedModule = (StateT Bool (TCMT IO) () -> Bool -> TCM Bool)
    -> Bool -> StateT Bool (TCMT IO) () -> TCM Bool
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip StateT Bool (TCMT IO) () -> Bool -> TCM Bool
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
    execStateT Bool
    True (StateT Bool (TCMT IO) () -> TCM Bool)
    -> StateT Bool (TCMT IO) () -> TCM 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
    5 (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
    5 (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
      [(PragmaOptions -> Bool, [Char])]
    -> ((PragmaOptions -> Bool, [Char]) -> StateT Bool (TCMT IO) ())
    -> StateT Bool (TCMT IO) ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [(PragmaOptions -> Bool, [Char])]
    coinfectiveOptions (((PragmaOptions -> Bool, [Char]) -> StateT Bool (TCMT IO) ())
     -> StateT Bool (TCMT IO) ())
    -> ((PragmaOptions -> Bool, [Char]) -> StateT Bool (TCMT IO) ())
    -> StateT Bool (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ \ (PragmaOptions -> Bool
    opt, [Char]
    optName) -> do
        Bool -> StateT Bool (TCMT IO) () -> StateT Bool (TCMT IO) ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (PragmaOptions -> Bool
    opt PragmaOptions
    current Bool -> Bool -> Bool
    `implies` PragmaOptions -> Bool
    opt 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 ([Char] -> ModuleName -> Warning
    CoInfectiveImport [Char]
    optName ModuleName
    importedModule)
      [(PragmaOptions -> Bool, [Char])]
    -> ((PragmaOptions -> Bool, [Char]) -> StateT Bool (TCMT IO) ())
    -> StateT Bool (TCMT IO) ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [(PragmaOptions -> Bool, [Char])]
    infectiveOptions (((PragmaOptions -> Bool, [Char]) -> StateT Bool (TCMT IO) ())
     -> StateT Bool (TCMT IO) ())
    -> ((PragmaOptions -> Bool, [Char]) -> StateT Bool (TCMT IO) ())
    -> StateT Bool (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ \ (PragmaOptions -> Bool
    opt, [Char]
    optName) -> do
        Bool -> StateT Bool (TCMT IO) () -> StateT Bool (TCMT IO) ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (PragmaOptions -> Bool
    opt PragmaOptions
    imported Bool -> Bool -> Bool
    `implies` PragmaOptions -> Bool
    opt PragmaOptions
    current) (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 ([Char] -> ModuleName -> Warning
    InfectiveImport [Char]
    optName ModuleName
    importedModule)
      where
        implies :: Bool -> Bool -> Bool
        Bool
    p implies :: Bool -> Bool -> Bool
    `implies` Bool
    q = Bool
    p Bool -> Bool -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Bool
    q

        showOptions :: PragmaOptions -> m Doc
    showOptions PragmaOptions
    opts = [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    P.prettyList (((PragmaOptions -> Bool, [Char]) -> m Doc)
    -> [(PragmaOptions -> Bool, [Char])] -> [m Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (\ (PragmaOptions -> Bool
    o, [Char]
    n) -> ([Char] -> m Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    P.text [Char]
    n 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 (PragmaOptions -> Bool
    o PragmaOptions
    opts))
                                     ([(PragmaOptions -> Bool, [Char])]
    coinfectiveOptions [(PragmaOptions -> Bool, [Char])]
    -> [(PragmaOptions -> Bool, [Char])]
    -> [(PragmaOptions -> Bool, [Char])]
    forall a. [a] -> [a] -> [a]
    ++ [(PragmaOptions -> Bool, [Char])]
    infectiveOptions))

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

    getOptionsCompatibilityWarnings :: MainInterface -> Bool -> PragmaOptions -> Interface -> TCM (Maybe [TCWarning])
    getOptionsCompatibilityWarnings :: MainInterface
    -> Bool
    -> PragmaOptions
    -> Interface
    -> TCMT IO (Maybe [TCWarning])
    getOptionsCompatibilityWarnings MainInterface
    isMain Bool
    isPrim PragmaOptions
    currentOptions Interface
    i = MaybeT (TCMT IO) [TCWarning] -> TCMT IO (Maybe [TCWarning])
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT (TCMT IO) [TCWarning] -> TCMT IO (Maybe [TCWarning]))
    -> MaybeT (TCMT IO) [TCWarning] -> TCMT IO (Maybe [TCWarning])
    forall a b. (a -> b) -> a -> b
    $ ExceptT [Char] (TCMT IO) [TCWarning]
    -> MaybeT (TCMT IO) [TCWarning]
    forall (m :: * -> *) e a. Functor m => ExceptT e m a -> MaybeT m a
    exceptToMaybeT (ExceptT [Char] (TCMT IO) [TCWarning]
     -> MaybeT (TCMT IO) [TCWarning])
    -> ExceptT [Char] (TCMT IO) [TCWarning]
    -> MaybeT (TCMT IO) [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 (f :: * -> *). Applicative f => Bool -> f () -> f ()
    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 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 (TCM Bool -> ExceptT [Char] (TCMT IO) Bool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM Bool -> ExceptT [Char] (TCMT IO) Bool)
    -> TCM Bool -> ExceptT [Char] (TCMT IO) Bool
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions -> PragmaOptions -> ModuleName -> TCM Bool
    checkOptionsCompatible PragmaOptions
    currentOptions (Interface -> PragmaOptions
    iOptionsUsed Interface
    i) (Interface -> ModuleName
    iModuleName 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 e (m :: * -> *) a. MonadError e m => e -> m a
    throwError [Char]
    "No warnings to collect because options were compatible"
      TCMT IO [TCWarning] -> ExceptT [Char] (TCMT IO) [TCWarning]
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO [TCWarning] -> ExceptT [Char] (TCMT IO) [TCWarning])
    -> TCMT IO [TCWarning] -> ExceptT [Char] (TCMT IO) [TCWarning]
    forall a b. (a -> b) -> a -> b
    $ MainInterface -> WhichWarnings -> TCMT IO [TCWarning]
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m, MonadWarning m) =>
    MainInterface -> WhichWarnings -> m [TCWarning]
    getAllWarnings' MainInterface
    isMain WhichWarnings
    ErrorWarnings

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

    getStoredInterface
      :: C.TopLevelModuleName
         -- ^ Module name of file we process.
      -> SourceFile
         -- ^ File we process.
      -> Maybe Source
      -> ExceptT String TCM ModuleInfo
    getStoredInterface :: TopLevelModuleName
    -> SourceFile
    -> Maybe Source
    -> ExceptT [Char] (TCMT IO) ModuleInfo
    getStoredInterface TopLevelModuleName
    x SourceFile
    file 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.
            InterfaceFile
    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
    $
              SourceFile -> TCMT IO (Maybe InterfaceFile)
    findInterfaceFile' SourceFile
    file

            -- Check that the interface file exists and return its hash.
            (Hash, Hash)
    hashes <- [Char]
    -> MaybeT (TCMT IO) (Hash, Hash)
    -> ExceptT [Char] (TCMT IO) (Hash, Hash)
    forall (m :: * -> *) e a.
    Functor m =>
    e -> MaybeT m a -> ExceptT e m a
    maybeToExceptT [Char]
    "the interface file hash could not be read" (MaybeT (TCMT IO) (Hash, Hash)
     -> ExceptT [Char] (TCMT IO) (Hash, Hash))
    -> MaybeT (TCMT IO) (Hash, Hash)
    -> ExceptT [Char] (TCMT IO) (Hash, Hash)
    forall a b. (a -> b) -> a -> b
    $ TCMT IO (Maybe (Hash, Hash)) -> MaybeT (TCMT IO) (Hash, Hash)
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (TCMT IO (Maybe (Hash, Hash)) -> MaybeT (TCMT IO) (Hash, Hash))
    -> TCMT IO (Maybe (Hash, Hash)) -> MaybeT (TCMT IO) (Hash, Hash)
    forall a b. (a -> b) -> a -> b
    $ IO (Maybe (Hash, Hash)) -> TCMT IO (Maybe (Hash, Hash))
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (Maybe (Hash, Hash)) -> TCMT IO (Maybe (Hash, Hash)))
    -> IO (Maybe (Hash, Hash)) -> TCMT IO (Maybe (Hash, Hash))
    forall a b. (a -> b) -> a -> b
    $
              InterfaceFile -> IO (Maybe (Hash, Hash))
    getInterfaceFileHashes InterfaceFile
    ifile

            (InterfaceFile, (Hash, Hash))
    -> ExceptT [Char] (TCMT IO) (InterfaceFile, (Hash, Hash))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (InterfaceFile
    ifile, (Hash, Hash)
    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
            Hash
    sourceH <- case Maybe Source
    msrc of
                        Maybe Source
    Nothing -> IO Hash -> ExceptT [Char] (TCMT IO) Hash
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO Hash -> ExceptT [Char] (TCMT IO) Hash)
    -> IO Hash -> ExceptT [Char] (TCMT IO) Hash
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath -> IO Hash
    hashTextFile (SourceFile -> AbsolutePath
    srcFilePath SourceFile
    file)
                        Just Source
    src -> Hash -> ExceptT [Char] (TCMT IO) Hash
    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)

            Bool -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Hash
    sourceH Hash -> Hash -> Bool
    forall a. Eq a => a -> a -> Bool
    == Hash
    ifaceH) (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 e (m :: * -> *) a. MonadError e m => e -> m a
    throwError ([Char] -> ExceptT [Char] (TCMT IO) ())
    -> [Char] -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
                [ [Char]
    "the source hash (", Hash -> [Char]
    forall a. Show a => a -> [Char]
    show Hash
    sourceH, [Char]
    ")"
                , [Char]
    " does not match the source hash for the interface (", Hash -> [Char]
    forall a. Show a => a -> [Char]
    show Hash
    ifaceH, [Char]
    ")"
                ]

            [Char] -> Int -> [Char] -> ExceptT [Char] (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface" Int
    5 ([Char] -> ExceptT [Char] (TCMT IO) ())
    -> [Char] -> ExceptT [Char] (TCMT IO) ()
    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 up-to-date."]

      -- Check if we have cached the module.
      Either [Char] ModuleInfo
    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 (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 Either [Char] ModuleInfo
    cachedE of
        -- If it's cached ignoreInterfaces has no effect;
        -- to avoid typechecking a file more than once.
        Right ModuleInfo
    mi -> do
          (InterfaceFile
    ifile, (Hash, Hash)
    hashes) <- ExceptT [Char] (TCMT IO) (InterfaceFile, (Hash, Hash))
    getIFileHashesET

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

          -- Make sure the hashes match.
          let cachedIfaceHash :: Hash
    cachedIfaceHash = Interface -> Hash
    iFullHash Interface
    i
          let fileIfaceHash :: Hash
    fileIfaceHash = (Hash, Hash) -> Hash
    forall a b. (a, b) -> b
    snd (Hash, Hash)
    hashes
          Bool -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Hash
    cachedIfaceHash Hash -> Hash -> Bool
    forall a. Eq a => a -> a -> Bool
    == Hash
    fileIfaceHash) (ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ())
    -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ do
            TCM () -> ExceptT [Char] (TCMT IO) ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM () -> ExceptT [Char] (TCMT IO) ())
    -> TCM () -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleName -> TCM ()
    dropDecodedModule TopLevelModuleName
    x
            [Char] -> Int -> [Char] -> ExceptT [Char] (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface" Int
    50 ([Char] -> ExceptT [Char] (TCMT IO) ())
    -> [Char] -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  cached hash = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Hash -> [Char]
    forall a. Show a => a -> [Char]
    show Hash
    cachedIfaceHash
            [Char] -> Int -> [Char] -> ExceptT [Char] (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface" Int
    50 ([Char] -> ExceptT [Char] (TCMT IO) ())
    -> [Char] -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  stored hash = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Hash -> [Char]
    forall a. Show a => a -> [Char]
    show Hash
    fileIfaceHash
            [Char] -> Int -> [Char] -> ExceptT [Char] (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface" Int
    5 ([Char] -> ExceptT [Char] (TCMT IO) ())
    -> [Char] -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  file is newer, re-reading " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ifp
            [Char] -> ExceptT [Char] (TCMT IO) ()
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError ([Char] -> ExceptT [Char] (TCMT IO) ())
    -> [Char] -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
              [ [Char]
    "the cached interface hash (", Hash -> [Char]
    forall a. Show a => a -> [Char]
    show Hash
    cachedIfaceHash, [Char]
    ")"
              , [Char]
    " does not match interface file (", Hash -> [Char]
    forall a. Show a => a -> [Char]
    show Hash
    fileIfaceHash, [Char]
    ")"
              ]

          Account (BenchPhase (ExceptT [Char] (TCMT IO)))
    -> ExceptT [Char] (TCMT IO) ModuleInfo
    -> ExceptT [Char] (TCMT IO) ModuleInfo
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (ExceptT [Char] (TCMT IO))
    Phase
    Bench.Deserialization] (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
            Hash -> ExceptT [Char] (TCMT IO) ()
    checkSourceHashET (Interface -> Hash
    iSourceHash Interface
    i)

            [Char] -> Int -> [Char] -> ExceptT [Char] (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface" Int
    5 ([Char] -> ExceptT [Char] (TCMT IO) ())
    -> [Char] -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  using stored version of " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ (AbsolutePath -> [Char]
    filePath (AbsolutePath -> [Char]) -> AbsolutePath -> [Char]
    forall a b. (a -> b) -> a -> b
    $ InterfaceFile -> AbsolutePath
    intFilePath InterfaceFile
    ifile)
            SourceFile -> ModuleInfo -> ExceptT [Char] (TCMT IO) ModuleInfo
    loadDecodedModule SourceFile
    file ModuleInfo
    mi

        Left [Char]
    whyNotCached -> ([Char] -> [Char])
    -> 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 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) Bool
    -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (TCM Bool -> ExceptT [Char] (TCMT IO) Bool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM Bool -> ExceptT [Char] (TCMT IO) Bool)
    -> TCM Bool -> ExceptT [Char] (TCMT IO) Bool
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCM Bool
    forall (m :: * -> *). MonadIO m => [Char] -> m Bool
    Lens.isBuiltinModule (AbsolutePath -> [Char]
    filePath (AbsolutePath -> [Char]) -> AbsolutePath -> [Char]
    forall a b. (a -> b) -> a -> b
    $ SourceFile -> AbsolutePath
    srcFilePath SourceFile
    file)) (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 e (m :: * -> *) a. MonadError e m => e -> m a
    throwError [Char]
    "we're ignoring non-builtin interface files"

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

          let ifp :: [Char]
    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)

          Account (BenchPhase (ExceptT [Char] (TCMT IO)))
    -> ExceptT [Char] (TCMT IO) ModuleInfo
    -> ExceptT [Char] (TCMT IO) ModuleInfo
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (ExceptT [Char] (TCMT IO))
    Phase
    Bench.Deserialization] (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
            Hash -> ExceptT [Char] (TCMT IO) ()
    checkSourceHashET ((Hash, Hash) -> Hash
    forall a b. (a, b) -> a
    fst (Hash, Hash)
    hashes)

            [Char] -> Int -> [Char] -> ExceptT [Char] (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface" Int
    5 ([Char] -> ExceptT [Char] (TCMT IO) ())
    -> [Char] -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  no stored version, reading " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ifp

            Interface
    i <- [Char]
    -> MaybeT (TCMT IO) Interface -> ExceptT [Char] (TCMT IO) Interface
    forall (m :: * -> *) e a.
    Functor m =>
    e -> MaybeT m a -> ExceptT e m a
    maybeToExceptT [Char]
    "bad interface, re-type checking" (MaybeT (TCMT IO) Interface -> ExceptT [Char] (TCMT IO) Interface)
    -> MaybeT (TCMT IO) Interface -> ExceptT [Char] (TCMT IO) Interface
    forall a b. (a -> b) -> a -> b
    $ TCMT IO (Maybe Interface) -> MaybeT (TCMT IO) Interface
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (TCMT IO (Maybe Interface) -> MaybeT (TCMT IO) Interface)
    -> TCMT IO (Maybe Interface) -> MaybeT (TCMT IO) Interface
    forall a b. (a -> b) -> a -> b
    $
              InterfaceFile -> TCMT IO (Maybe Interface)
    readInterface InterfaceFile
    ifile

            -- Ensure that the given module name matches the one in the file.
            let topLevelName :: TopLevelModuleName
    topLevelName = ModuleName -> TopLevelModuleName
    toTopLevelModuleName (ModuleName -> TopLevelModuleName)
    -> ModuleName -> TopLevelModuleName
    forall a b. (a -> b) -> a -> b
    $ Interface -> ModuleName
    iModuleName Interface
    i
            Bool -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (TopLevelModuleName
    topLevelName TopLevelModuleName -> TopLevelModuleName -> Bool
    forall a. Eq a => a -> a -> Bool
    == TopLevelModuleName
    x) (ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ())
    -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $
              -- Andreas, 2014-03-27 This check is now done in the scope checker.
              -- checkModuleName topLevelName file
              TCM () -> ExceptT [Char] (TCMT IO) ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM () -> ExceptT [Char] (TCMT IO) ())
    -> TCM () -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath
    -> TopLevelModuleName -> TopLevelModuleName -> TypeError
    OverlappingProjects (SourceFile -> AbsolutePath
    srcFilePath SourceFile
    file) TopLevelModuleName
    topLevelName TopLevelModuleName
    x

            Bool
    isPrimitiveModule <- TCM Bool -> ExceptT [Char] (TCMT IO) Bool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM Bool -> ExceptT [Char] (TCMT IO) Bool)
    -> TCM Bool -> ExceptT [Char] (TCMT IO) Bool
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCM Bool
    forall (m :: * -> *). MonadIO m => [Char] -> m Bool
    Lens.isPrimitiveModule (AbsolutePath -> [Char]
    filePath (AbsolutePath -> [Char]) -> AbsolutePath -> [Char]
    forall a b. (a -> b) -> a -> b
    $ SourceFile -> AbsolutePath
    srcFilePath SourceFile
    file)

            TCM () -> ExceptT [Char] (TCMT IO) ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM () -> ExceptT [Char] (TCMT IO) ())
    -> TCM () -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TopLevelModuleName -> Maybe [Char] -> TCM ()
    chaseMsg [Char]
    "Loading " TopLevelModuleName
    x (Maybe [Char] -> TCM ()) -> Maybe [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    ifp
            -- print imported warnings
            let ws :: [TCWarning]
    ws = (TCWarning -> Bool) -> [TCWarning] -> [TCWarning]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((AbsolutePath -> Maybe AbsolutePath
    forall a. a -> Maybe a
    Strict.Just (SourceFile -> AbsolutePath
    srcFilePath SourceFile
    file) Maybe AbsolutePath -> Maybe AbsolutePath -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Maybe AbsolutePath -> Bool)
    -> (TCWarning -> Maybe AbsolutePath) -> TCWarning -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCWarning -> Maybe AbsolutePath
    tcWarningOrigin) (Interface -> [TCWarning]
    iWarnings Interface
    i)
            Bool -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([TCWarning] -> Bool
    forall a. Null a => a -> Bool
    null [TCWarning]
    ws) (ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ())
    -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Int -> TCMT IO Doc -> ExceptT [Char] (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "warning" Int
    1 (TCMT IO Doc -> ExceptT [Char] (TCMT IO) ())
    -> TCMT IO Doc -> ExceptT [Char] (TCMT IO) ()
    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
    $ TCWarning -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    P.prettyTCM (TCWarning -> TCMT IO Doc) -> [TCWarning] -> [TCMT IO Doc]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [TCWarning]
    ws

            SourceFile -> ModuleInfo -> ExceptT [Char] (TCMT IO) ModuleInfo
    loadDecodedModule SourceFile
    file (ModuleInfo -> ExceptT [Char] (TCMT IO) ModuleInfo)
    -> ModuleInfo -> ExceptT [Char] (TCMT IO) ModuleInfo
    forall a b. (a -> b) -> a -> b
    $ ModuleInfo :: Interface -> [TCWarning] -> Bool -> ModuleCheckMode -> ModuleInfo
    ModuleInfo
              { miInterface :: Interface
    miInterface = Interface
    i
              , miWarnings :: [TCWarning]
    miWarnings = []
              , miPrimitive :: Bool
    miPrimitive = Bool
    isPrimitiveModule
              , miMode :: ModuleCheckMode
    miMode = ModuleCheckMode
    ModuleTypeChecked
              }

    loadDecodedModule
      :: SourceFile
         -- ^ File we process.
      -> ModuleInfo
      -> ExceptT String TCM ModuleInfo
    loadDecodedModule :: SourceFile -> ModuleInfo -> ExceptT [Char] (TCMT IO) ModuleInfo
    loadDecodedModule SourceFile
    file ModuleInfo
    mi = do
      let fp :: [Char]
    fp = AbsolutePath -> [Char]
    filePath (AbsolutePath -> [Char]) -> AbsolutePath -> [Char]
    forall a b. (a -> b) -> a -> b
    $ SourceFile -> AbsolutePath
    srcFilePath SourceFile
    file
      let i :: Interface
    i = ModuleInfo -> Interface
    miInterface ModuleInfo
    mi

      -- Check that it's the right version
      [Char] -> Int -> [Char] -> ExceptT [Char] (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface" Int
    5 ([Char] -> ExceptT [Char] (TCMT IO) ())
    -> [Char] -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  imports: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [(ModuleName, Hash)] -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow (Interface -> [(ModuleName, Hash)]
    iImportedModules Interface
    i)

      -- 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)
      [[[Char]]]
    libOptions <- TCMT IO [[[Char]]] -> ExceptT [Char] (TCMT IO) [[[Char]]]
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO [[[Char]]] -> ExceptT [Char] (TCMT IO) [[[Char]]])
    -> TCMT IO [[[Char]]] -> ExceptT [Char] (TCMT IO) [[[Char]]]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO [[[Char]]]
    getLibraryOptions ([Char] -> TCMT IO [[[Char]]]) -> [Char] -> TCMT IO [[[Char]]]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Char]
    takeDirectory [Char]
    fp
      TCM () -> ExceptT [Char] (TCMT IO) ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM () -> ExceptT [Char] (TCMT IO) ())
    -> TCM () -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ ([[Char]] -> TCM ()) -> [[[Char]]] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ [[Char]] -> TCM ()
    setOptionsFromPragma ([[[Char]]]
    libOptions [[[Char]]] -> [[[Char]]] -> [[[Char]]]
    forall a. [a] -> [a] -> [a]
    ++ Interface -> [[[Char]]]
    iFilePragmaOptions Interface
    i)

      -- Check that options that matter haven't changed compared to
      -- current options (issue #2487)
      ExceptT [Char] (TCMT IO) Bool
    -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (TCM Bool -> ExceptT [Char] (TCMT IO) Bool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM Bool -> ExceptT [Char] (TCMT IO) Bool)
    -> TCM Bool -> ExceptT [Char] (TCMT IO) Bool
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCM Bool
    forall (m :: * -> *). MonadIO m => [Char] -> m Bool
    Lens.isBuiltinModule [Char]
    fp) (ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ())
    -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ do
        PragmaOptions
    currentOptions <- Lens' PragmaOptions TCState
    -> ExceptT [Char] (TCMT IO) PragmaOptions
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' PragmaOptions TCState
    stPragmaOptions
        let disagreements :: [[Char]]
    disagreements =
              [ [Char]
    optName | (PragmaOptions -> RestartCodomain
    opt, [Char]
    optName) <- [(PragmaOptions -> RestartCodomain, [Char])]
    restartOptions,
                          PragmaOptions -> RestartCodomain
    opt PragmaOptions
    currentOptions RestartCodomain -> RestartCodomain -> Bool
    forall a. Eq a => a -> a -> Bool
    /= PragmaOptions -> RestartCodomain
    opt (Interface -> PragmaOptions
    iOptionsUsed Interface
    i) ]
        Bool -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([[Char]] -> Bool
    forall a. Null a => a -> Bool
    null [[Char]]
    disagreements) (ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ())
    -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ do
          [Char] -> Int -> [Char] -> ExceptT [Char] (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.options" Int
    4 ([Char] -> ExceptT [Char] (TCMT IO) ())
    -> [Char] -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
            [ [Char]
    "  Changes in the following options in "
            , [Char] -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow [Char]
    fp
            , [Char]
    ", re-typechecking: "
            , [[Char]] -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow [[Char]]
    disagreements
            ]
          [Char] -> ExceptT [Char] (TCMT IO) ()
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError [Char]
    "options changed"

      -- If any of the imports are newer we need to retype check
      [[Char]]
    badHashMessages <- ([Either [Char] ()] -> [[Char]])
    -> ExceptT [Char] (TCMT IO) [Either [Char] ()]
    -> ExceptT [Char] (TCMT IO) [[Char]]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap [Either [Char] ()] -> [[Char]]
    forall a b. [Either a b] -> [a]
    lefts (ExceptT [Char] (TCMT IO) [Either [Char] ()]
     -> ExceptT [Char] (TCMT IO) [[Char]])
    -> ExceptT [Char] (TCMT IO) [Either [Char] ()]
    -> ExceptT [Char] (TCMT IO) [[Char]]
    forall a b. (a -> b) -> a -> b
    $ [(ModuleName, Hash)]
    -> ((ModuleName, Hash)
        -> ExceptT [Char] (TCMT IO) (Either [Char] ()))
    -> ExceptT [Char] (TCMT IO) [Either [Char] ()]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM (Interface -> [(ModuleName, Hash)]
    iImportedModules Interface
    i) (((ModuleName, Hash)
      -> ExceptT [Char] (TCMT IO) (Either [Char] ()))
     -> ExceptT [Char] (TCMT IO) [Either [Char] ()])
    -> ((ModuleName, Hash)
        -> ExceptT [Char] (TCMT IO) (Either [Char] ()))
    -> ExceptT [Char] (TCMT IO) [Either [Char] ()]
    forall a b. (a -> b) -> a -> b
    $ \(ModuleName
    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 (ExceptT [Char] (ExceptT [Char] (TCMT IO)) ()
     -> ExceptT [Char] (TCMT IO) (Either [Char] ()))
    -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ()
    -> ExceptT [Char] (TCMT IO) (Either [Char] ())
    forall a b. (a -> b) -> a -> b
    $ 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 ", ModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow ModuleName
    impName, [Char]
    " matches ", Hash -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Hash
    impHash ]
        Hash
    latestImpHash <- ExceptT [Char] (TCMT IO) Hash
    -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) Hash
    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
    $ TCMT IO Hash -> ExceptT [Char] (TCMT IO) Hash
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO Hash -> ExceptT [Char] (TCMT IO) Hash)
    -> TCMT IO Hash -> ExceptT [Char] (TCMT IO) Hash
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> TCMT IO Hash -> TCMT IO Hash
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange ModuleName
    impName (TCMT IO Hash -> TCMT IO Hash) -> TCMT IO Hash -> TCMT IO Hash
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> TCMT IO Hash
    moduleHash ModuleName
    impName
        [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]
    "Done checking module hash of import ", ModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow ModuleName
    impName]
        Bool
    -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ()
    -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Hash
    impHash Hash -> Hash -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Hash
    latestImpHash) (ExceptT [Char] (ExceptT [Char] (TCMT IO)) ()
     -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ())
    -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ()
    -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ()
    forall a b. (a -> b) -> a -> b
    $
          [Char] -> ExceptT [Char] (ExceptT [Char] (TCMT IO)) ()
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError ([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]
    "module hash for imported module ", ModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow ModuleName
    impName, [Char]
    " is out of date"
            , [Char]
    " (import cached=", Hash -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Hash
    impHash, [Char]
    ", latest=", Hash -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Hash
    latestImpHash, [Char]
    ")"
            ]

      [[Char]]
    -> ([[Char]] -> ExceptT [Char] (TCMT IO) ())
    -> ExceptT [Char] (TCMT IO) ()
    forall (m :: * -> *) a.
    (Monad m, Null a) =>
    a -> (a -> m ()) -> m ()
    unlessNull [[Char]]
    badHashMessages ([Char] -> ExceptT [Char] (TCMT IO) ()
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError ([Char] -> ExceptT [Char] (TCMT IO) ())
    -> ([[Char]] -> [Char]) -> [[Char]] -> ExceptT [Char] (TCMT IO) ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [[Char]] -> [Char]
    unlines)

      [Char] -> Int -> [Char] -> ExceptT [Char] (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface" Int
    5 [Char]
    "  New module. Let's check it out."
      TCM () -> ExceptT [Char] (TCMT IO) ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM () -> ExceptT [Char] (TCMT IO) ())
    -> TCM () -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ Interface -> TCM ()
    mergeInterface Interface
    i
      Account (BenchPhase (ExceptT [Char] (TCMT IO)))
    -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (ExceptT [Char] (TCMT IO))
    Phase
    Bench.Highlighting] (ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ())
    -> ExceptT [Char] (TCMT IO) () -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $
        TCM () -> ExceptT [Char] (TCMT IO) ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM () -> ExceptT [Char] (TCMT IO) ())
    -> TCM () -> ExceptT [Char] (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ HighlightingLevel -> TCM () -> TCM ()
    forall (tcm :: * -> *).
    MonadTCEnv tcm =>
    HighlightingLevel -> tcm () -> tcm ()
    ifTopLevelAndHighlightingLevelIs HighlightingLevel
    NonInteractive (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          Interface -> SourceFile -> TCM ()
    highlightFromInterface Interface
    i SourceFile
    file

      ModuleInfo -> ExceptT [Char] (TCMT IO) ModuleInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return ModuleInfo
    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
      :: C.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

          [TopLevelModuleName]
    ms          <- TCM [TopLevelModuleName]
    getImportPath
          Range
    range       <- (TCEnv -> Range) -> TCMT IO Range
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Range
    envRange
          Maybe (Closure Call)
    call        <- (TCEnv -> Maybe (Closure Call)) -> TCMT IO (Maybe (Closure Call))
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Maybe (Closure Call)
    envCall
          Map TopLevelModuleName AbsolutePath
    mf          <- Lens' (Map TopLevelModuleName AbsolutePath) TCState
    -> TCMT IO (Map TopLevelModuleName AbsolutePath)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Map TopLevelModuleName AbsolutePath) TCState
    stModuleToSource
          VisitedModules
    vs          <- TCMT IO VisitedModules
    forall (m :: * -> *). ReadTCState m => m VisitedModules
    getVisitedModules
          VisitedModules
    ds          <- TCMT IO VisitedModules
    getDecodedModules
          CommandLineOptions
    opts        <- PersistentTCState -> CommandLineOptions
    stPersistentOptions (PersistentTCState -> CommandLineOptions)
    -> (TCState -> PersistentTCState) -> TCState -> CommandLineOptions
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCState -> PersistentTCState
    stPersistentState (TCState -> CommandLineOptions)
    -> TCMT IO TCState -> TCMT IO CommandLineOptions
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC
          Signature
    isig        <- Lens' Signature TCState -> TCMT IO Signature
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' Signature TCState
    stImports
          Map [Char] (Builtin PrimFun)
    ibuiltin    <- Lens' (Map [Char] (Builtin PrimFun)) TCState
    -> TCMT IO (Map [Char] (Builtin PrimFun))
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Map [Char] (Builtin PrimFun)) TCState
    stImportedBuiltins
          DisplayForms
    display     <- Lens' DisplayForms TCState -> TCMT IO DisplayForms
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' DisplayForms TCState
    stImportsDisplayForms
          Map QName Text
    userwarn    <- Lens' (Map QName Text) TCState -> TCMT IO (Map QName Text)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Map QName Text) TCState
    stImportedUserWarnings
          Set QName
    partialdefs <- Lens' (Set QName) TCState -> TCMT IO (Set QName)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Set QName) TCState
    stImportedPartialDefs
          PatternSynDefns
    ipatsyns <- TCMT IO PatternSynDefns
    forall (m :: * -> *). ReadTCState m => m PatternSynDefns
    getPatternSynImports
          InteractionOutputCallback
    ho       <- TCMT IO InteractionOutputCallback
    forall (m :: * -> *). ReadTCState m => m InteractionOutputCallback
    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.
          (ModuleInfo
    mi, Map TopLevelModuleName AbsolutePath
    newModToSource, VisitedModules
    newDecodedModules) <- ((TCErr
     -> TCMT
          IO
          (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
    -> ((ModuleInfo, Map TopLevelModuleName AbsolutePath,
         VisitedModules)
        -> TCMT
             IO
             (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
    -> Either
         TCErr
         (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
    -> TCMT
         IO
         (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either TCErr
    -> TCMT
         IO
         (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
    -> TCMT
         IO
         (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Either
       TCErr
       (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
     -> TCMT
          IO
          (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
    -> TCMT
         IO
         (Either
            TCErr
            (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
    -> TCMT
         IO
         (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<) (TCMT
       IO
       (Either
          TCErr
          (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
     -> TCMT
          IO
          (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
    -> TCMT
         IO
         (Either
            TCErr
            (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
    -> TCMT
         IO
         (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
    forall a b. (a -> b) -> a -> b
    $
               TCMT
      IO
      (Either
         TCErr
         (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
    -> TCMT
         IO
         (Either
            TCErr
            (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
    forall (m :: * -> *) a.
    (MonadTCState m, ReadTCState m) =>
    m a -> m a
    withoutCache (TCMT
       IO
       (Either
          TCErr
          (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
     -> TCMT
          IO
          (Either
             TCErr
             (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)))
    -> TCMT
         IO
         (Either
            TCErr
            (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
    -> TCMT
         IO
         (Either
            TCErr
            (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
    forall a b. (a -> b) -> a -> b
    $
               -- The cache should not be used for an imported module, and it
               -- should be restored after the module has been type-checked
               TCMT
      IO
      (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
    -> TCMT
         IO
         (Either
            TCErr
            (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
    forall a. TCM a -> TCM (Either TCErr a)
    freshTCM (TCMT
       IO
       (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
     -> TCMT
          IO
          (Either
             TCErr
             (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)))
    -> TCMT
         IO
         (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
    -> TCMT
         IO
         (Either
            TCErr
            (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
    forall a b. (a -> b) -> a -> b
    $
                 [TopLevelModuleName]
    -> TCMT
         IO
         (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
    -> TCMT
         IO
         (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
    forall a. [TopLevelModuleName] -> TCM a -> TCM a
    withImportPath [TopLevelModuleName]
    ms (TCMT
       IO
       (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
     -> TCMT
          IO
          (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
    -> TCMT
         IO
         (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
    -> TCMT
         IO
         (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
    forall a b. (a -> b) -> a -> b
    $
                 (TCEnv -> TCEnv)
    -> TCMT
         IO
         (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
    -> TCMT
         IO
         (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (\TCEnv
    e -> TCEnv
    e
                                  -- Andreas, 2014-08-18:
                                  -- Preserve the range of import statement
                                  -- for reporting termination errors in
                                  -- imported modules:
                                { envRange :: Range
    envRange              = Range
    range
                                , envCall :: Maybe (Closure Call)
    envCall               = Maybe (Closure Call)
    call
                                }) (TCMT
       IO
       (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
     -> TCMT
          IO
          (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules))
    -> TCMT
         IO
         (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
    -> TCMT
         IO
         (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
    forall a b. (a -> b) -> a -> b
    $ do
                   VisitedModules -> TCM ()
    setDecodedModules VisitedModules
    ds
                   CommandLineOptions -> TCM ()
    setCommandLineOptions CommandLineOptions
    opts
                   InteractionOutputCallback -> TCM ()
    setInteractionOutputCallback InteractionOutputCallback
    ho
                   Lens' (Map TopLevelModuleName AbsolutePath) TCState
    stModuleToSource Lens' (Map TopLevelModuleName AbsolutePath) TCState
    -> Map TopLevelModuleName AbsolutePath -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    `setTCLens` Map TopLevelModuleName AbsolutePath
    mf
                   VisitedModules -> TCM ()
    setVisitedModules VisitedModules
    vs
                   Signature
    -> Map [Char] (Builtin PrimFun)
    -> PatternSynDefns
    -> DisplayForms
    -> Map QName Text
    -> Set QName
    -> [TCWarning]
    -> TCM ()
    addImportedThings Signature
    isig Map [Char] (Builtin PrimFun)
    ibuiltin PatternSynDefns
    ipatsyns DisplayForms
    display Map QName Text
    userwarn Set QName
    partialdefs []

                   ModuleInfo
    r  <- TopLevelModuleName
    -> SourceFile -> MainInterface -> Maybe Source -> TCM ModuleInfo
    createInterface TopLevelModuleName
    x SourceFile
    file MainInterface
    NotMainInterface Maybe Source
    msrc
                   Map TopLevelModuleName AbsolutePath
    mf' <- Lens' (Map TopLevelModuleName AbsolutePath) TCState
    -> TCMT IO (Map TopLevelModuleName AbsolutePath)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Map TopLevelModuleName AbsolutePath) TCState
    stModuleToSource
                   VisitedModules
    ds' <- TCMT IO VisitedModules
    getDecodedModules
                   (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
    -> TCMT
         IO
         (ModuleInfo, Map TopLevelModuleName AbsolutePath, VisitedModules)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ModuleInfo
    r, Map TopLevelModuleName AbsolutePath
    mf', VisitedModules
    ds')

          Lens' (Map TopLevelModuleName AbsolutePath) TCState
    stModuleToSource Lens' (Map TopLevelModuleName AbsolutePath) TCState
    -> Map TopLevelModuleName AbsolutePath -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    `setTCLens` Map TopLevelModuleName AbsolutePath
    newModToSource
          VisitedModules -> TCM ()
    setDecodedModules VisitedModules
    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.)
          Either [Char] ModuleInfo
    validated <- ExceptT [Char] (TCMT IO) ModuleInfo
    -> TCM (Either [Char] ModuleInfo)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (ExceptT [Char] (TCMT IO) ModuleInfo
     -> TCM (Either [Char] ModuleInfo))
    -> ExceptT [Char] (TCMT IO) ModuleInfo
    -> TCM (Either [Char] ModuleInfo)
    forall a b. (a -> b) -> a -> b
    $ SourceFile -> ModuleInfo -> ExceptT [Char] (TCMT IO) ModuleInfo
    loadDecodedModule SourceFile
    file ModuleInfo
    mi

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

          ([Char] -> TCM ModuleInfo)
    -> (ModuleInfo -> TCM ModuleInfo)
    -> Either [Char] ModuleInfo
    -> TCM ModuleInfo
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either [Char] -> TCM ModuleInfo
    recheckOnError ModuleInfo -> TCM ModuleInfo
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Either [Char] ModuleInfo
    validated

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

    chaseMsg
      :: String               -- ^ The prefix, like @Checking@, @Finished@, @Loading @.
      -> C.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
      [Char]
    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 (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)
      let maybeFile :: [Char]
    maybeFile = Maybe [Char] -> [Char] -> ([Char] -> [Char]) -> [Char]
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe [Char]
    file [Char]
    "." (([Char] -> [Char]) -> [Char]) -> ([Char] -> [Char]) -> [Char]
    forall a b. (a -> b) -> a -> b
    $ \ [Char]
    f -> [Char]
    " (" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    f [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ")."
          vLvl :: Int
    vLvl | [Char]
    kind [Char] -> [Char] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Char]
    "Checking" = Int
    1
               | Bool
    otherwise          = Int
    2
      [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.chase" Int
    vLvl ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
        [ [Char]
    indentation, [Char]
    kind, [Char]
    " ", TopLevelModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow TopLevelModuleName
    x, [Char]
    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
    file = 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]
    "Generating syntax info for " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ AbsolutePath -> [Char]
    filePath (SourceFile -> AbsolutePath
    srcFilePath SourceFile
    file) [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
        [Char]
    " (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
        (ByteString
    s, IO ()
    close) <- IO (ByteString, IO ()) -> TCMT IO (ByteString, IO ())
    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  Maybe Interface
    mi <- IO (Maybe Interface) -> TCMT IO (Maybe Interface)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (Maybe Interface) -> TCMT IO (Maybe Interface))
    -> (Maybe Interface -> IO (Maybe Interface))
    -> Maybe Interface
    -> TCMT IO (Maybe Interface)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe Interface -> IO (Maybe Interface)
    forall a. a -> IO a
    E.evaluate (Maybe Interface -> TCMT IO (Maybe Interface))
    -> TCMT IO (Maybe Interface) -> TCMT IO (Maybe Interface)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ByteString -> TCMT IO (Maybe Interface)
    decodeInterface ByteString
    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.
            IO () -> TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO IO ()
    close

            Maybe Interface -> TCMT IO (Maybe Interface)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Interface -> TCMT IO (Maybe Interface))
    -> Maybe Interface -> TCMT IO (Maybe Interface)
    forall a b. (a -> b) -> a -> b
    $ Interface -> Interface
    constructIScope (Interface -> Interface) -> Maybe Interface -> Maybe Interface
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe Interface
    mi
          -- Catch exceptions and close
          TCMT IO (Maybe Interface)
    -> (TCErr -> TCMT IO (Maybe Interface))
    -> TCMT IO (Maybe Interface)
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \TCErr
    e -> IO () -> TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO IO ()
    close TCM () -> TCMT IO (Maybe Interface) -> TCMT IO (Maybe Interface)
    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 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 TCState
    _ Range
    _ IOException
    e -> do
            [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "" Int
    0 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "IO exception: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ IOException -> [Char]
    forall a. Show a => a -> [Char]
    show IOException
    e
            Maybe a -> TCMT IO (Maybe 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 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] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    fp [Char] -> [Char] -> [Char]
    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 :: ScopeInfo
    iInsideScope  = ScopeInfo -> ScopeInfo
    withoutPrivates (ScopeInfo -> ScopeInfo) -> ScopeInfo -> ScopeInfo
    forall a b. (a -> b) -> a -> b
    $ Interface -> ScopeInfo
    iInsideScope Interface
    i }
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.write" Int
    50 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          [Char]
    "Writing interface file with hash " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Hash -> [Char]
    forall a. Show a => a -> [Char]
    show (Interface -> Hash
    iFullHash Interface
    filteredIface) [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "."
        ByteString
    encodedIface <- [Char] -> Interface -> TCM ByteString
    encodeFile [Char]
    fp Interface
    filteredIface
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.write" Int
    5 [Char]
    "Wrote interface file."
    #if __GLASGOW_HASKELL__ >= 804
        Interface -> Maybe Interface -> Interface
    forall a. a -> Maybe a -> a
    fromMaybe Interface
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Interface -> Interface)
    -> TCMT IO (Maybe Interface) -> TCMT IO Interface
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Account (BenchPhase (TCMT IO))
    -> TCMT IO (Maybe Interface) -> TCMT IO (Maybe Interface)
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (TCMT IO)
    Phase
    Bench.Deserialization] (ByteString -> TCMT IO (Maybe Interface)
    forall a. EmbPrj a => ByteString -> TCM (Maybe a)
    decode ByteString
    encodedIface))
    #else
        return filteredIface
    #endif
      TCMT IO Interface
    -> (TCErr -> TCMT IO Interface) -> TCMT IO Interface
    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 ()
    reportSLn [Char]
    "" Int
    1 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          [Char]
    "Failed to write interface " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    fp [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "."
        IO () -> TCM ()
    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 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
      :: C.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 SourceFile
    file MainInterface
    isMain Maybe Source
    msrc = do
      let x :: TopLevelModuleName
    x = TopLevelModuleName
    mname
      let fp :: [Char]
    fp = AbsolutePath -> [Char]
    filePath (AbsolutePath -> [Char]) -> AbsolutePath -> [Char]
    forall a b. (a -> b) -> a -> b
    $ SourceFile -> AbsolutePath
    srcFilePath SourceFile
    file
      let checkMsg :: [Char]
    checkMsg = case MainInterface
    isMain of
                       MainInterface Mode
    ScopeCheck -> [Char]
    "Reading "
                       MainInterface
    _                        -> [Char]
    "Checking"
          withMsgs :: TCM ModuleInfo -> TCM ModuleInfo
    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
    x (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 [TCWarning]
    ws <- WhichWarnings -> TCMT IO [TCWarning]
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m, MonadWarning m) =>
    WhichWarnings -> m [TCWarning]
    getAllWarnings WhichWarnings
    AllWarnings
                       let classified :: WarningsAndNonFatalErrors
    classified = [TCWarning] -> WarningsAndNonFatalErrors
    classifyWarnings [TCWarning]
    ws
                       let wa' :: [TCWarning]
    wa' = (TCWarning -> Bool) -> [TCWarning] -> [TCWarning]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((AbsolutePath -> Maybe AbsolutePath
    forall a. a -> Maybe a
    Strict.Just (SourceFile -> AbsolutePath
    srcFilePath SourceFile
    file) Maybe AbsolutePath -> Maybe AbsolutePath -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Maybe AbsolutePath -> Bool)
    -> (TCWarning -> Maybe AbsolutePath) -> TCWarning -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCWarning -> Maybe AbsolutePath
    tcWarningOrigin) (WarningsAndNonFatalErrors -> [TCWarning]
    tcWarnings WarningsAndNonFatalErrors
    classified)
                       Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([TCWarning] -> Bool
    forall a. Null a => a -> Bool
    null [TCWarning]
    wa') (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                         [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "warning" 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
    $ TCWarning -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    P.prettyTCM (TCWarning -> TCMT IO Doc) -> [TCWarning] -> [TCMT IO Doc]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [TCWarning]
    wa'
                       Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when ([TCWarning] -> Bool
    forall a. Null a => a -> Bool
    null (WarningsAndNonFatalErrors -> [TCWarning]
    nonFatalErrors WarningsAndNonFatalErrors
    classified)) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TopLevelModuleName -> Maybe [Char] -> TCM ()
    chaseMsg [Char]
    "Finished" TopLevelModuleName
    x Maybe [Char]
    forall a. Maybe a
    Nothing)

      TCM ModuleInfo -> TCM ModuleInfo
    withMsgs (TCM ModuleInfo -> TCM ModuleInfo)
    -> TCM ModuleInfo -> TCM ModuleInfo
    forall a b. (a -> b) -> a -> b
    $
        Account (BenchPhase (TCMT IO)) -> TCM ModuleInfo -> TCM ModuleInfo
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [TopLevelModuleName -> Phase
    Bench.TopModule TopLevelModuleName
    mname] (TCM ModuleInfo -> TCM ModuleInfo)
    -> TCM ModuleInfo -> TCM ModuleInfo
    forall a b. (a -> b) -> a -> b
    $
        (TCEnv -> TCEnv) -> TCM ModuleInfo -> TCM ModuleInfo
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (\TCEnv
    e -> TCEnv
    e { envCurrentPath :: Maybe AbsolutePath
    envCurrentPath = AbsolutePath -> Maybe AbsolutePath
    forall a. a -> Maybe a
    Just (SourceFile -> AbsolutePath
    srcFilePath SourceFile
    file) }) (TCM ModuleInfo -> TCM ModuleInfo)
    -> TCM ModuleInfo -> TCM ModuleInfo
    forall a b. (a -> b) -> a -> b
    $ do

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

        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.create" Int
    5 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          [Char]
    "Creating interface for " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ TopLevelModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow TopLevelModuleName
    mname [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "."
        [Char] -> Int -> TCM () -> TCM ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
    verboseS [Char]
    "import.iface.create" Int
    10 (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          [Char]
    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
          [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.create" Int
    10 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  visited: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    visited

        Source
    src <- TCM Source -> (Source -> TCM Source) -> Maybe Source -> TCM Source
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (SourceFile -> TCM Source
    parseSource SourceFile
    file) Source -> TCM Source
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe Source
    msrc

        let srcPath :: AbsolutePath
    srcPath = SourceFile -> AbsolutePath
    srcFilePath (SourceFile -> AbsolutePath) -> SourceFile -> AbsolutePath
    forall a b. (a -> b) -> a -> b
    $ Source -> SourceFile
    srcOrigin Source
    src

        HighlightingInfo
    fileTokenInfo <- Account (BenchPhase (TCMT IO))
    -> TCMT IO HighlightingInfo -> TCMT IO HighlightingInfo
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (TCMT IO)
    Phase
    Bench.Highlighting] (TCMT IO HighlightingInfo -> TCMT IO HighlightingInfo)
    -> TCMT IO HighlightingInfo -> TCMT IO HighlightingInfo
    forall a b. (a -> b) -> a -> b
    $
          AbsolutePath -> [Char] -> TCMT IO HighlightingInfo
    generateTokenInfoFromSource AbsolutePath
    srcPath (Text -> [Char]
    TL.unpack (Text -> [Char]) -> Text -> [Char]
    forall a b. (a -> b) -> a -> b
    $ Source -> Text
    srcText Source
    src)
        Lens' HighlightingInfo TCState
    stTokens Lens' HighlightingInfo TCState
    -> (HighlightingInfo -> HighlightingInfo) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    `modifyTCLens` (HighlightingInfo
    fileTokenInfo HighlightingInfo -> HighlightingInfo -> HighlightingInfo
    forall a. Semigroup a => a -> a -> a
    <>)

        Source -> TCM ()
    setOptionsFromSourcePragmas Source
    src

        [Char] -> Int -> TCM () -> TCM ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
    verboseS [Char]
    "import.iface.create" Int
    15 (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          Int
    nestingLevel      <- (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 (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)
          HighlightingLevel
    highlightingLevel <- (TCEnv -> HighlightingLevel) -> TCMT IO HighlightingLevel
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> HighlightingLevel
    envHighlightingLevel
          [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.create" Int
    15 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines
            [ [Char]
    "  nesting      level: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    nestingLevel
            , [Char]
    "  highlighting level: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ HighlightingLevel -> [Char]
    forall a. Show a => a -> [Char]
    show HighlightingLevel
    highlightingLevel
            ]

        -- Scope checking.
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.create" Int
    7 [Char]
    "Starting scope checking."
        TopLevelInfo
    topLevel <- Account (BenchPhase (TCMT IO))
    -> TCMT IO TopLevelInfo -> TCMT IO TopLevelInfo
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (TCMT IO)
    Phase
    Bench.Scoping] (TCMT IO TopLevelInfo -> TCMT IO TopLevelInfo)
    -> TCMT IO TopLevelInfo -> TCMT IO TopLevelInfo
    forall a b. (a -> b) -> a -> b
    $ do
          let topDecls :: [Declaration]
    topDecls = Module -> [Declaration]
    C.modDecls (Module -> [Declaration]) -> Module -> [Declaration]
    forall a b. (a -> b) -> a -> b
    $ Source -> Module
    srcModule Source
    src
          TopLevel [Declaration]
    -> ScopeM (AbsOfCon (TopLevel [Declaration]))
    forall c. ToAbstract c => c -> ScopeM (AbsOfCon c)
    concreteToAbstract_ (AbsolutePath
    -> TopLevelModuleName -> [Declaration] -> TopLevel [Declaration]
    forall a. AbsolutePath -> TopLevelModuleName -> a -> TopLevel a
    TopLevel AbsolutePath
    srcPath TopLevelModuleName
    mname [Declaration]
    topDecls)
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.create" Int
    7 [Char]
    "Finished scope checking."

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

        -- Highlighting from scope checker.
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.create" Int
    7 [Char]
    "Starting highlighting from scope."
        Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (TCMT IO)
    Phase
    Bench.Highlighting] (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          -- Generate and print approximate syntax highlighting info.
          HighlightingLevel -> TCM () -> TCM ()
    forall (tcm :: * -> *).
    MonadTCEnv tcm =>
    HighlightingLevel -> tcm () -> tcm ()
    ifTopLevelAndHighlightingLevelIs HighlightingLevel
    NonInteractive (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
    forall (m :: * -> *).
    MonadTrace m =>
    RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
    printHighlightingInfo RemoveTokenBasedHighlighting
    KeepHighlighting HighlightingInfo
    fileTokenInfo
          HighlightingLevel -> Bool -> TCM () -> TCM ()
    forall (tcm :: * -> *).
    MonadTCEnv tcm =>
    HighlightingLevel -> Bool -> tcm () -> tcm ()
    ifTopLevelAndHighlightingLevelIsOr HighlightingLevel
    NonInteractive Bool
    onlyScope (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            (Declaration -> TCM ()) -> [Declaration] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (\ Declaration
    d -> Declaration -> Level -> Bool -> TCM ()
    generateAndPrintSyntaxInfo Declaration
    d Level
    Partial Bool
    onlyScope) [Declaration]
    ds
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.create" Int
    7 [Char]
    "Finished highlighting from scope."

        -- Type checking.

        -- Now that all the options are in we can check if caching should
        -- be on.
        TCM ()
    forall (m :: * -> *).
    (HasOptions m, MonadDebug m, MonadTCState m) =>
    m ()
    activateLoadedFileCache

        -- invalidate cache if pragmas change, TODO move
        TCM ()
    forall (m :: * -> *).
    (MonadDebug m, MonadTCState m, ReadTCState m) =>
    m ()
    cachingStarts
        PragmaOptions
    opts <- Lens' PragmaOptions TCState -> TCMT IO PragmaOptions
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' PragmaOptions TCState
    stPragmaOptions
        Maybe (TypeCheckAction, PostScopeState)
    me <- TCMT IO (Maybe (TypeCheckAction, PostScopeState))
    forall (m :: * -> *).
    (MonadDebug m, MonadTCState m, ReadTCState m) =>
    m (Maybe (TypeCheckAction, PostScopeState))
    readFromCachedLog
        case Maybe (TypeCheckAction, PostScopeState)
    me of
          Just (Pragmas PragmaOptions
    opts', PostScopeState
    _) | PragmaOptions
    opts PragmaOptions -> PragmaOptions -> Bool
    forall a. Eq a => a -> a -> Bool
    == PragmaOptions
    opts'
            -> () -> TCM ()
    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] -> [Char] -> [Char]
    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
        TypeCheckAction -> TCM ()
    forall (m :: * -> *).
    (MonadDebug m, MonadTCState m, ReadTCState m) =>
    TypeCheckAction -> m ()
    writeToCurrentLog (TypeCheckAction -> TCM ()) -> TypeCheckAction -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions -> TypeCheckAction
    Pragmas PragmaOptions
    opts

        if Bool
    onlyScope
          then do
            [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.create" Int
    7 [Char]
    "Skipping type checking."
            TCM ()
    forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
    cacheCurrentLog
          else do
            [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.create" Int
    7 [Char]
    "Starting type checking."
            Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (TCMT IO)
    Phase
    Bench.Typing] (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (Declaration -> TCM ()) -> [Declaration] -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Declaration -> TCM ()
    checkDeclCached [Declaration]
    ds TCM () -> TCM () -> TCM ()
    forall a b. TCM a -> TCM b -> TCM a
    `finally_` TCM ()
    forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
    cacheCurrentLog
            [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.create" Int
    7 [Char]
    "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

        TCM ()
    unfreezeMetas

        -- Profiling: Count number of metas.
        [Char] -> Int -> TCM () -> TCM ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
    verboseS [Char]
    "profile.metas" Int
    10 (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          MetaId Int
    n <- TCMT IO MetaId
    forall i (m :: * -> *). MonadFresh i m => m i
    fresh
          [Char] -> Integer -> TCM ()
    forall (m :: * -> *).
    MonadStatistics m =>
    [Char] -> Integer -> m ()
    tickN [Char]
    "metas" (Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    n)

        -- Highlighting from type checker.
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.create" Int
    7 [Char]
    "Starting highlighting from type info."
        Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase (TCMT IO)
    Phase
    Bench.Highlighting] (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do

          -- Move any remaining token highlighting to stSyntaxInfo.
          HighlightingInfo
    toks <- Lens' HighlightingInfo TCState -> TCMT IO HighlightingInfo
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' HighlightingInfo TCState
    stTokens
          HighlightingLevel -> TCM () -> TCM ()
    forall (tcm :: * -> *).
    MonadTCEnv tcm =>
    HighlightingLevel -> tcm () -> tcm ()
    ifTopLevelAndHighlightingLevelIs HighlightingLevel
    NonInteractive (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
    forall (m :: * -> *).
    MonadTrace m =>
    RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
    printHighlightingInfo RemoveTokenBasedHighlighting
    KeepHighlighting HighlightingInfo
    toks
          Lens' HighlightingInfo TCState
    stTokens Lens' HighlightingInfo TCState -> HighlightingInfo -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    `setTCLens` HighlightingInfo
    forall a. Monoid a => a
    mempty

          -- Grabbing warnings and unsolved metas to highlight them
          [TCWarning]
    warnings <- WhichWarnings -> TCMT IO [TCWarning]
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m, MonadWarning m) =>
    WhichWarnings -> m [TCWarning]
    getAllWarnings WhichWarnings
    AllWarnings
          Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([TCWarning] -> Bool
    forall a. Null a => a -> Bool
    null [TCWarning]
    warnings) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "import.iface.create" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            TCMT IO Doc
    "collected warnings: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> [TCWarning] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [TCWarning]
    warnings
          [TCWarning]
    unsolved <- TCMT IO [TCWarning]
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m, MonadWarning m) =>
    m [TCWarning]
    getAllUnsolvedWarnings
          Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([TCWarning] -> Bool
    forall a. Null a => a -> Bool
    null [TCWarning]
    unsolved) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "import.iface.create" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            TCMT IO Doc
    "collected unsolved: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> [TCWarning] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [TCWarning]
    unsolved
          let warningInfo :: HighlightingInfo
    warningInfo =
                HighlightingInfoBuilder -> HighlightingInfo
    forall a b. Convert a b => a -> b
    convert (HighlightingInfoBuilder -> HighlightingInfo)
    -> HighlightingInfoBuilder -> HighlightingInfo
    forall a b. (a -> b) -> a -> b
    $ (TCWarning -> HighlightingInfoBuilder)
    -> [TCWarning] -> HighlightingInfoBuilder
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap TCWarning -> HighlightingInfoBuilder
    warningHighlighting ([TCWarning] -> HighlightingInfoBuilder)
    -> [TCWarning] -> HighlightingInfoBuilder
    forall a b. (a -> b) -> a -> b
    $ [TCWarning]
    unsolved [TCWarning] -> [TCWarning] -> [TCWarning]
    forall a. [a] -> [a] -> [a]
    ++ [TCWarning]
    warnings

          Lens' HighlightingInfo TCState
    stSyntaxInfo Lens' HighlightingInfo TCState
    -> (HighlightingInfo -> HighlightingInfo) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    `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

          TCM Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (CommandLineOptions -> Bool
    optGenerateVimFile (CommandLineOptions -> Bool)
    -> TCMT IO CommandLineOptions -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            -- Generate Vim file.
            ScopeInfo -> TCM () -> TCM ()
    forall (m :: * -> *) a. ReadTCState m => ScopeInfo -> m a -> m a
    withScope_ ScopeInfo
    scope (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCM ()
    generateVimFile ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath -> [Char]
    filePath (AbsolutePath -> [Char]) -> AbsolutePath -> [Char]
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath
    srcPath
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.create" Int
    7 [Char]
    "Finished highlighting from type info."

        ScopeInfo -> TCM ()
    setScope ScopeInfo
    scope
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "scope.top" Int
    50 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "SCOPE " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ ScopeInfo -> [Char]
    forall a. Show a => a -> [Char]
    show ScopeInfo
    scope

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

        [MetaId]
    openMetas           <- TCMT IO [MetaId]
    forall (m :: * -> *). ReadTCState m => m [MetaId]
    getOpenMetas
        Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([MetaId] -> Bool
    forall a. Null a => a -> Bool
    null [MetaId]
    openMetas) (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.metas" Int
    10 [Char]
    "We have unsolved metas."
          [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.metas" Int
    10 ([Char] -> TCM ()) -> TCMT IO [Char] -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Goals -> TCMT IO [Char]
    showGoals (Goals -> TCMT IO [Char]) -> TCMT IO Goals -> TCMT IO [Char]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Goals
    getGoals

        HighlightingLevel -> TCM () -> TCM ()
    forall (tcm :: * -> *).
    MonadTCEnv tcm =>
    HighlightingLevel -> tcm () -> tcm ()
    ifTopLevelAndHighlightingLevelIs HighlightingLevel
    NonInteractive TCM ()
    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
        Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (MainInterface -> Bool
    includeStateChanges MainInterface
    isMain) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          -- Andreas, 2018-11-15, re issue #3393:
          -- We do not get here when checking the main module
          -- (then includeStateChanges is True).
          TCM Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (PragmaOptions -> Bool
    optAllowUnsolved (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCM 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.iface.create" Int
    7 [Char]
    "Turning unsolved metas (if any) into postulates."
            ModuleName -> TCM () -> TCM ()
    forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
    withCurrentModule (ScopeInfo
    scope ScopeInfo -> Lens' ModuleName ScopeInfo -> ModuleName
    forall o i. o -> Lens' i o -> i
    ^. Lens' ModuleName ScopeInfo
    scopeCurrent) TCM ()
    openMetasToPostulates
            -- Clear constraints as they might refer to what
            -- they think are open metas.
            Lens' Constraints TCState
    stAwakeConstraints    Lens' Constraints TCState -> Constraints -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    `setTCLens` []
            Lens' Constraints TCState
    stSleepingConstraints Lens' Constraints TCState -> Constraints -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    `setTCLens` []

        -- Serialization.
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.create" Int
    7 [Char]
    "Starting serialization."
        Interface
    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 [BenchPhase (TCMT IO)
    Phase
    Bench.Serialization, BenchPhase (TCMT IO)
    Phase
    Bench.BuildInterface] (TCMT IO Interface -> TCMT IO Interface)
    -> TCMT IO Interface -> TCMT IO Interface
    forall a b. (a -> b) -> a -> b
    $
          Source -> TopLevelInfo -> TCMT IO Interface
    buildInterface Source
    src TopLevelInfo
    topLevel

        [Char] -> Int -> [[Char]] -> TCM ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    [Char] -> Int -> a -> m ()
    reportS [Char]
    "tc.top" Int
    101 ([[Char]] -> TCM ()) -> [[Char]] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          [Char]
    "Signature:" [Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    :
          [ [[Char]] -> [Char]
    unlines
              [ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    q
              , [Char]
    "  type: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Type -> [Char]
    forall a. Show a => a -> [Char]
    show (Definition -> Type
    defType Definition
    def)
              , [Char]
    "  def:  " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Maybe CompiledClauses -> [Char]
    forall a. Show a => a -> [Char]
    show Maybe CompiledClauses
    cc
              ]
          | (QName
    q, Definition
    def) <- HashMap QName Definition -> [(QName, Definition)]
    forall k v. HashMap k v -> [(k, v)]
    HMap.toList (HashMap QName Definition -> [(QName, Definition)])
    -> HashMap QName Definition -> [(QName, Definition)]
    forall a b. (a -> b) -> a -> b
    $ Interface -> Signature
    iSignature Interface
    i Signature
    -> Lens' (HashMap QName Definition) Signature
    -> HashMap QName Definition
    forall o i. o -> Lens' i o -> i
    ^. Lens' (HashMap QName Definition) Signature
    sigDefinitions,
            Function{ funCompiled :: Defn -> Maybe CompiledClauses
    funCompiled = Maybe CompiledClauses
    cc } <- [Definition -> Defn
    theDef Definition
    def]
          ]
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.create" Int
    7 [Char]
    "Finished serialization."

        [TCWarning]
    mallWarnings <- MainInterface -> WhichWarnings -> TCMT IO [TCWarning]
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m, MonadWarning m) =>
    MainInterface -> WhichWarnings -> m [TCWarning]
    getAllWarnings' MainInterface
    isMain WhichWarnings
    ErrorWarnings

        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.create" Int
    7 [Char]
    "Considering writing to interface file."
        Interface
    finalIface <- Interface -> Interface
    constructIScope (Interface -> Interface) -> TCMT IO Interface -> TCMT IO Interface
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> case ([TCWarning]
    mallWarnings, MainInterface
    isMain) of
          (TCWarning
    _:[TCWarning]
    _, 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]
    "We have warnings, skipping writing interface file."
            Interface -> TCMT IO Interface
    forall (m :: * -> *) a. Monad m => a -> m a
    return Interface
    i
          ([], MainInterface Mode
    ScopeCheck) -> do
            [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.create" Int
    7 [Char]
    "We are just scope-checking, skipping writing interface file."
            Interface -> TCMT IO Interface
    forall (m :: * -> *) a. Monad m => a -> m a
    return Interface
    i
          ([], 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]
    "Actually calling writeInterface."
            -- The file was successfully type-checked (and no warnings were
            -- encountered), so the interface should be written out.
            AbsolutePath
    ifile <- SourceFile -> TCM AbsolutePath
    toIFile SourceFile
    file
            Interface
    serializedIface <- AbsolutePath -> Interface -> TCMT IO Interface
    writeInterface AbsolutePath
    ifile Interface
    i
            [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface.create" Int
    7 [Char]
    "Finished writing to interface file."
            Interface -> TCMT IO Interface
    forall (m :: * -> *) a. Monad m => a -> m a
    return Interface
    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.
        Int -> Maybe TopLevelModuleName -> Statistics -> TCM ()
    forall (m :: * -> *).
    (MonadDebug m, MonadTCEnv m, HasOptions m) =>
    Int -> Maybe TopLevelModuleName -> Statistics -> m ()
    printStatistics Int
    30 (TopLevelModuleName -> Maybe TopLevelModuleName
    forall a. a -> Maybe a
    Just TopLevelModuleName
    mname) (Statistics -> TCM ()) -> TCMT IO Statistics -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Statistics
    forall (m :: * -> *). ReadTCState m => m Statistics
    getStatistics

        -- Get the statistics of the current module
        -- and add it to the accumulated statistics.
        Statistics
    localStatistics <- TCMT IO Statistics
    forall (m :: * -> *). ReadTCState m => m Statistics
    getStatistics
        Lens' Statistics TCState
    lensAccumStatistics Lens' Statistics TCState -> (Statistics -> Statistics) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    `modifyTCLens` (Integer -> Integer -> Integer)
    -> Statistics -> Statistics -> Statistics
    forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
    Map.unionWith Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    (+) Statistics
    localStatistics
        [Char] -> Int -> TCM () -> TCM ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
    verboseS [Char]
    "profile" Int
    1 (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface" Int
    5 [Char]
    "Accumulated statistics."

        Bool
    isPrimitiveModule <- [Char] -> TCM Bool
    forall (m :: * -> *). MonadIO m => [Char] -> m Bool
    Lens.isPrimitiveModule (AbsolutePath -> [Char]
    filePath AbsolutePath
    srcPath)

        ModuleInfo -> TCM ModuleInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return ModuleInfo :: Interface -> [TCWarning] -> Bool -> ModuleCheckMode -> ModuleInfo
    ModuleInfo
          { miInterface :: Interface
    miInterface = Interface
    finalIface
          , miWarnings :: [TCWarning]
    miWarnings = [TCWarning]
    mallWarnings
          , miPrimitive :: Bool
    miPrimitive = Bool
    isPrimitiveModule
          , miMode :: ModuleCheckMode
    miMode = MainInterface -> ModuleCheckMode
    moduleCheckMode MainInterface
    isMain
          }

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

    getAllWarnings' :: (MonadFail m, ReadTCState m, MonadWarning m) => MainInterface -> WhichWarnings -> m [TCWarning]
    getAllWarnings' :: forall (m :: * -> *).
    (MonadFail m, ReadTCState m, MonadWarning m) =>
    MainInterface -> WhichWarnings -> m [TCWarning]
    getAllWarnings' (MainInterface Mode
    _) = Set WarningName -> WhichWarnings -> m [TCWarning]
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m, MonadWarning m) =>
    Set WarningName -> WhichWarnings -> m [TCWarning]
    getAllWarningsPreserving Set WarningName
    unsolvedWarnings
    getAllWarnings' MainInterface
    NotMainInterface  = Set WarningName -> WhichWarnings -> m [TCWarning]
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m, MonadWarning m) =>
    Set WarningName -> WhichWarnings -> m [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 = Account -> Interface -> Interface
    forall a. Account -> a -> a
    billToPure [ Phase
    Deserialization ] (Interface -> Interface) -> Interface -> Interface
    forall a b. (a -> b) -> a -> b
    $
      Interface
    i{ iScope :: Map ModuleName Scope
    iScope = ScopeInfo -> Map ModuleName Scope
    publicModules (ScopeInfo -> Map ModuleName Scope)
    -> ScopeInfo -> Map ModuleName Scope
    forall a b. (a -> b) -> a -> b
    $ Interface -> ScopeInfo
    iInsideScope Interface
    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
    topLevelModuleName TopLevelInfo
    topLevel
            source :: Text
    source   = Source -> Text
    srcText Source
    src
            fileType :: FileType
    fileType = Source -> FileType
    srcFileType Source
    src
            defPragmas :: [[[Char]]]
    defPragmas = Source -> [[[Char]]]
    srcDefaultPragmas Source
    src
            filePragmas :: [[[Char]]]
    filePragmas  = Source -> [[[Char]]]
    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).
        Map [Char] (Builtin PrimFun)
    builtin     <- Lens' (Map [Char] (Builtin PrimFun)) TCState
    -> TCMT IO (Map [Char] (Builtin PrimFun))
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Map [Char] (Builtin PrimFun)) TCState
    stLocalBuiltins
        Set ModuleName
    ms          <- TCM (Set ModuleName)
    getImports
        [(ModuleName, Hash)]
    mhs         <- (ModuleName -> TCMT IO (ModuleName, Hash))
    -> [ModuleName] -> TCMT IO [(ModuleName, Hash)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (\ ModuleName
    m -> (ModuleName
    m,) (Hash -> (ModuleName, Hash))
    -> TCMT IO Hash -> TCMT IO (ModuleName, Hash)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModuleName -> TCMT IO Hash
    moduleHash ModuleName
    m) ([ModuleName] -> TCMT IO [(ModuleName, Hash)])
    -> [ModuleName] -> TCMT IO [(ModuleName, Hash)]
    forall a b. (a -> b) -> a -> b
    $ Set ModuleName -> [ModuleName]
    forall a. Set a -> [a]
    Set.toList Set ModuleName
    ms
        Map [Char] [ForeignCode]
    foreignCode <- Lens' (Map [Char] [ForeignCode]) TCState
    -> TCMT IO (Map [Char] [ForeignCode])
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Map [Char] [ForeignCode]) TCState
    stForeignCode
        -- Ulf, 2016-04-12:
        -- Non-closed display forms are not applicable outside the module anyway,
        -- and should be dead-code eliminated (#1928).
        DisplayForms
    origDisplayForms <- ([Open DisplayForm] -> Bool) -> DisplayForms -> DisplayForms
    forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
    HMap.filter (Bool -> Bool
    not (Bool -> Bool)
    -> ([Open DisplayForm] -> Bool) -> [Open DisplayForm] -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Open DisplayForm] -> Bool
    forall a. Null a => a -> Bool
    null) (DisplayForms -> DisplayForms)
    -> (DisplayForms -> DisplayForms) -> DisplayForms -> DisplayForms
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Open DisplayForm] -> [Open DisplayForm])
    -> DisplayForms -> DisplayForms
    forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
    HMap.map ((Open DisplayForm -> Bool)
    -> [Open DisplayForm] -> [Open DisplayForm]
    forall a. (a -> Bool) -> [a] -> [a]
    filter Open DisplayForm -> Bool
    forall a. Open a -> Bool
    isClosed) (DisplayForms -> DisplayForms)
    -> TCMT IO DisplayForms -> TCMT IO DisplayForms
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' DisplayForms TCState -> TCMT IO DisplayForms
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' DisplayForms TCState
    stImportsDisplayForms
        -- TODO: Kill some ranges?
        (DisplayForms
    display, Signature
    sig) <- DisplayForms -> Signature -> TCM (DisplayForms, Signature)
    eliminateDeadCode DisplayForms
    origDisplayForms (Signature -> TCM (DisplayForms, Signature))
    -> TCMT IO Signature -> TCM (DisplayForms, Signature)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Signature
    forall (m :: * -> *). ReadTCState m => m Signature
    getSignature
        Map QName Text
    userwarns      <- Lens' (Map QName Text) TCState -> TCMT IO (Map QName Text)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Map QName Text) TCState
    stLocalUserWarnings
        Maybe Text
    importwarn     <- Lens' (Maybe Text) TCState -> TCMT IO (Maybe Text)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Maybe Text) TCState
    stWarningOnImport
        HighlightingInfo
    syntaxInfo     <- Lens' HighlightingInfo TCState -> TCMT IO HighlightingInfo
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' HighlightingInfo TCState
    stSyntaxInfo
        PragmaOptions
    optionsUsed    <- Lens' PragmaOptions TCState -> TCMT IO PragmaOptions
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' PragmaOptions TCState
    stPragmaOptions
        Set QName
    partialDefs    <- Lens' (Set QName) TCState -> TCMT IO (Set QName)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Set QName) TCState
    stLocalPartialDefs

        -- Andreas, 2015-02-09 kill ranges in pattern synonyms before
        -- serialization to avoid error locations pointing to external files
        -- when expanding a pattern synonym.
        PatternSynDefns
    patsyns <- PatternSynDefns -> PatternSynDefns
    forall a. KillRange a => KillRangeT a
    killRange (PatternSynDefns -> PatternSynDefns)
    -> TCMT IO PatternSynDefns -> TCMT IO PatternSynDefns
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PatternSynDefns
    forall (m :: * -> *). ReadTCState m => m PatternSynDefns
    getPatternSyns
        let builtin' :: Map [Char] (Builtin ([Char], QName))
    builtin' = ([Char] -> Builtin PrimFun -> Builtin ([Char], QName))
    -> Map [Char] (Builtin PrimFun)
    -> Map [Char] (Builtin ([Char], QName))
    forall k a b. (k -> a -> b) -> Map k a -> Map k b
    Map.mapWithKey (\ [Char]
    x Builtin PrimFun
    b -> ([Char]
    x,) (QName -> ([Char], QName))
    -> (PrimFun -> QName) -> PrimFun -> ([Char], QName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PrimFun -> QName
    primFunName (PrimFun -> ([Char], QName))
    -> Builtin PrimFun -> Builtin ([Char], QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Builtin PrimFun
    b) Map [Char] (Builtin PrimFun)
    builtin
        [TCWarning]
    warnings <- WhichWarnings -> TCMT IO [TCWarning]
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m, MonadWarning m) =>
    WhichWarnings -> m [TCWarning]
    getAllWarnings WhichWarnings
    AllWarnings
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface" Int
    7 [Char]
    "  instantiating all meta variables"
        -- Note that the meta-variables in the definitions in "sig" have
        -- already been instantiated (by eliminateDeadCode).
        Interface
    i <- Interface -> TCMT IO Interface
    forall (m :: * -> *). MonadReduce m => Interface -> m Interface
    instantiateFullExceptForDefinitions Interface :: Hash
    -> Text
    -> FileType
    -> [(ModuleName, Hash)]
    -> ModuleName
    -> Map ModuleName Scope
    -> ScopeInfo
    -> Signature
    -> DisplayForms
    -> Map QName Text
    -> Maybe Text
    -> Map [Char] (Builtin ([Char], QName))
    -> Map [Char] [ForeignCode]
    -> HighlightingInfo
    -> [[[Char]]]
    -> [[[Char]]]
    -> PragmaOptions
    -> PatternSynDefns
    -> [TCWarning]
    -> Set QName
    -> Interface
    Interface
          { iSourceHash :: Hash
    iSourceHash      = Text -> Hash
    hashText Text
    source
          , iSource :: Text
    iSource          = Text
    source
          , iFileType :: FileType
    iFileType        = FileType
    fileType
          , iImportedModules :: [(ModuleName, Hash)]
    iImportedModules = [(ModuleName, Hash)]
    mhs
          , iModuleName :: ModuleName
    iModuleName      = ModuleName
    mname
          , iScope :: Map ModuleName Scope
    iScope           = Map ModuleName Scope
    forall a. Null a => a
    empty -- publicModules scope
          , iInsideScope :: ScopeInfo
    iInsideScope     = TopLevelInfo -> ScopeInfo
    topLevelScope TopLevelInfo
    topLevel
          , iSignature :: Signature
    iSignature       = Signature
    sig
          , iDisplayForms :: DisplayForms
    iDisplayForms    = DisplayForms
    display
          , iUserWarnings :: Map QName Text
    iUserWarnings    = Map QName Text
    userwarns
          , iImportWarning :: Maybe Text
    iImportWarning   = Maybe Text
    importwarn
          , iBuiltin :: Map [Char] (Builtin ([Char], QName))
    iBuiltin         = Map [Char] (Builtin ([Char], QName))
    builtin'
          , iForeignCode :: Map [Char] [ForeignCode]
    iForeignCode     = Map [Char] [ForeignCode]
    foreignCode
          , iHighlighting :: HighlightingInfo
    iHighlighting    = HighlightingInfo
    syntaxInfo
          , iDefaultPragmaOptions :: [[[Char]]]
    iDefaultPragmaOptions = [[[Char]]]
    defPragmas
          , iFilePragmaOptions :: [[[Char]]]
    iFilePragmaOptions    = [[[Char]]]
    filePragmas
          , iOptionsUsed :: PragmaOptions
    iOptionsUsed     = PragmaOptions
    optionsUsed
          , iPatternSyns :: PatternSynDefns
    iPatternSyns     = PatternSynDefns
    patsyns
          , iWarnings :: [TCWarning]
    iWarnings        = [TCWarning]
    warnings
          , iPartialDefs :: Set QName
    iPartialDefs     = Set QName
    partialDefs
          }
        [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "import.iface" Int
    7 [Char]
    "  interface complete"
        Interface -> TCMT IO Interface
    forall (m :: * -> *) a. Monad m => a -> m a
    return Interface
    i

    -- | 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
      (ByteString
    s, IO ()
    close) <- [Char] -> IO (ByteString, IO ())
    readBinaryFile' [Char]
    ifile
      let hs :: Maybe (Hash, Hash)
    hs = ByteString -> Maybe (Hash, Hash)
    decodeHashes ByteString
    s
      Hash -> ((Hash, Hash) -> Hash) -> Maybe (Hash, Hash) -> Hash
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Hash
    0 ((Hash -> Hash -> Hash) -> (Hash, Hash) -> Hash
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Hash -> Hash -> Hash
    forall a. Num a => a -> a -> a
    (+)) Maybe (Hash, Hash)
    hs Hash -> IO () -> IO ()
    `seq` IO ()
    close
      Maybe (Hash, Hash) -> IO (Maybe (Hash, Hash))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Hash, Hash)
    hs

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