    ------------------------------------------------------------------------
    -- | Functions which map between module names and file names.
    --
    -- Note that file name lookups are cached in the 'TCState'. The code
    -- assumes that no Agda source files are added or removed from the
    -- include directories while the code is being type checked.
    ------------------------------------------------------------------------

    module Agda.Interaction.FindFile
      ( SourceFile(..), InterfaceFile(intFilePath)
      , toIFile, mkInterfaceFile
      , FindError(..), findErrorToTypeError
      , findFile, findFile', findFile'_, findFile''
      , findInterfaceFile', findInterfaceFile
      , checkModuleName
      , rootNameModule
      , replaceModuleExtension
      , dropAgdaExtension, hasAgdaExtension, stripAgdaExtension
      ) where

    import Prelude hiding (null)

    import Control.Monad
    import Control.Monad.Except
    import Control.Monad.State
    import Control.Monad.Trans
    import Data.Maybe (catMaybes, fromMaybe, isJust)
    import qualified Data.Map as Map
    import qualified Data.Text as T
    import System.FilePath

    import Agda.Interaction.Library ( findProjectRoot )

    import Agda.Syntax.Concrete
    import Agda.Syntax.Parser
    import Agda.Syntax.Parser.Literate (literateExtsShortList)
    import Agda.Syntax.Position
    import Agda.Syntax.TopLevelModuleName

    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Monad.Benchmark (billTo)
    import qualified Agda.TypeChecking.Monad.Benchmark as Bench
    import {-# SOURCE #-} Agda.TypeChecking.Monad.Options
      (getIncludeDirs, libToTCM)
    import Agda.TypeChecking.Monad.State ( registerFileIdWithBuiltin, topLevelModuleName )
    import Agda.TypeChecking.Monad.Trace (runPM, setCurrentRange)

    import Agda.Version ( version )

    import Agda.Utils.Applicative ( (?$>) )
    import Agda.Utils.CallStack   ( HasCallStack )
    import Agda.Utils.FileId
    import Agda.Utils.FileName
    import Agda.Utils.List  ( stripSuffix, nubOn )
    import Agda.Utils.List1 ( List1, pattern (:|) )
    import Agda.Utils.List2 ( List2, pattern List2 )
    import qualified Agda.Utils.List1 as List1
    import qualified Agda.Utils.List2 as List2
    import Agda.Utils.Monad ( ifM, unlessM )
    import Agda.Syntax.Common.Pretty ( Pretty(..), prettyShow )
    import qualified Agda.Syntax.Common.Pretty as P
    import Agda.Utils.Singleton

    import Agda.Utils.Impossible

    -- This instance isn't producing something pretty.
    -- instance Pretty SourceFile where
    --   pretty = pretty . srcFileId

    -- | File must exist.
    newtype InterfaceFile = InterfaceFile { InterfaceFile -> AbsolutePath
    intFilePath :: AbsolutePath }

    instance Pretty InterfaceFile where
      pretty :: InterfaceFile -> Doc
    pretty = AbsolutePath -> Doc
    forall a. Pretty a => a -> Doc
    pretty (AbsolutePath -> Doc)
    -> (InterfaceFile -> AbsolutePath) -> InterfaceFile -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . InterfaceFile -> AbsolutePath
    intFilePath

    -- | Makes an interface file from an AbsolutePath candidate.
    --   If the file does not exist, then fail by returning @Nothing@.

    mkInterfaceFile
      :: AbsolutePath             -- ^ Path to the candidate interface file
      -> IO (Maybe InterfaceFile) -- ^ Interface file iff it exists
    mkInterfaceFile :: AbsolutePath -> IO (Maybe InterfaceFile)
    mkInterfaceFile AbsolutePath
    fp = do
      ex <- String -> IO Bool
    doesFileExistCaseSensitive (String -> IO Bool) -> String -> IO Bool
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath -> String
    filePath AbsolutePath
    fp
      pure (ex ?$> InterfaceFile fp)

    -- | Converts an Agda file name to the corresponding interface file
    --   name. Note that we do not guarantee that the file exists.

    toIFile :: HasCallStack => SourceFile -> TCM AbsolutePath
    toIFile :: HasCallStack => SourceFile -> TCM AbsolutePath
    toIFile (SourceFile FileId
    fi) = do
      src <- FileId -> TCM AbsolutePath
    forall (m :: * -> *). MonadFileId m => FileId -> m AbsolutePath
    fileFromId FileId
    fi -- partial function, thus HasCallStack
      let fp = AbsolutePath -> String
    filePath AbsolutePath
    src
      let localIFile = String -> AbsolutePath -> AbsolutePath
    replaceModuleExtension String
    ".agdai" AbsolutePath
    src
      mroot <- libToTCM $ findProjectRoot (takeDirectory fp)
      case mroot of
        Maybe String
    Nothing   -> AbsolutePath -> TCM AbsolutePath
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure AbsolutePath
    localIFile
        Just String
    root -> do
          let buildDir :: String
    buildDir = String
    root String -> String -> String
    </> String
    "_build" String -> String -> String
    </> String
    version String -> String -> String
    </> String
    "agda"
          fileName <- IO String -> TCMT IO String
    forall a. IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO String -> TCMT IO String) -> IO String -> TCMT IO String
    forall a b. (a -> b) -> a -> b
    $ String -> String -> IO String
    makeRelativeCanonical String
    root (AbsolutePath -> String
    filePath AbsolutePath
    localIFile)
          let separatedIFile = String -> AbsolutePath
    mkAbsolute (String -> AbsolutePath) -> String -> AbsolutePath
    forall a b. (a -> b) -> a -> b
    $ String
    buildDir String -> String -> String
    </> String
    fileName
          pure separatedIFile

    replaceModuleExtension :: String -> AbsolutePath -> AbsolutePath
    replaceModuleExtension :: String -> AbsolutePath -> AbsolutePath
    replaceModuleExtension ext :: String
    ext@(Char
    '.':String
    _) = String -> AbsolutePath
    mkAbsolute (String -> AbsolutePath)
    -> (AbsolutePath -> String) -> AbsolutePath -> AbsolutePath
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ext) (String -> String)
    -> (AbsolutePath -> String) -> AbsolutePath -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .  String -> String
    dropAgdaExtension (String -> String)
    -> (AbsolutePath -> String) -> AbsolutePath -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbsolutePath -> String
    filePath
    replaceModuleExtension String
    ext = String -> AbsolutePath -> AbsolutePath
    replaceModuleExtension (Char
    '.'Char -> String -> String
    forall a. a -> [a] -> [a]
    :String
    ext)

    -- | Errors which can arise when trying to find a source file.
    --
    -- Invariant: All paths are absolute.

    data FindError
      = NotFound [AbsolutePath]
          -- ^ The file was not found.
          --   It should have had one of the given file names.
      | Ambiguous (List2 AbsolutePath)
          -- ^ Several matching files were found.
      deriving Int -> FindError -> String -> String
    [FindError] -> String -> String
    FindError -> String
    (Int -> FindError -> String -> String)
    -> (FindError -> String)
    -> ([FindError] -> String -> String)
    -> Show FindError
    forall a.
    (Int -> a -> String -> String)
    -> (a -> String) -> ([a] -> String -> String) -> Show a
    $cshowsPrec :: Int -> FindError -> String -> String
    showsPrec :: Int -> FindError -> String -> String
    $cshow :: FindError -> String
    show :: FindError -> String
    $cshowList :: [FindError] -> String -> String
    showList :: [FindError] -> String -> String
    Show

    -- | Given the module name which the error applies to this function
    -- converts a 'FindError' to a 'TypeError'.

    findErrorToTypeError :: TopLevelModuleName -> FindError -> TypeError
    findErrorToTypeError :: TopLevelModuleName -> FindError -> TypeError
    findErrorToTypeError TopLevelModuleName
    m = \case
      NotFound  [AbsolutePath]
    files -> TopLevelModuleName -> [AbsolutePath] -> TypeError
    FileNotFound TopLevelModuleName
    m [AbsolutePath]
    files
      Ambiguous List2 AbsolutePath
    files -> TopLevelModuleName -> List2 AbsolutePath -> TypeError
    AmbiguousTopLevelModuleName TopLevelModuleName
    m List2 AbsolutePath
    files

    -- findErrorToTypeError :: MonadFileId m => TopLevelModuleName -> FindError -> m TypeError
    -- findErrorToTypeError m = \case
    --   NotFound  files -> FileNotFound m <$> mapM srcFilePath files
    --   Ambiguous files -> AmbiguousTopLevelModuleName m <$> mapM srcFilePath files

    -- | Finds the source file corresponding to a given top-level module
    -- name. The returned paths are absolute.
    --
    -- Raises an error if the file cannot be found.

    findFile :: TopLevelModuleName -> TCM SourceFile
    findFile :: TopLevelModuleName -> TCM SourceFile
    findFile TopLevelModuleName
    m = do
      mf <- TopLevelModuleName -> TCM (Either FindError SourceFile)
    findFile' TopLevelModuleName
    m
      case mf of
        Left FindError
    err -> TypeError -> TCM SourceFile
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM SourceFile) -> TypeError -> TCM SourceFile
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleName -> FindError -> TypeError
    findErrorToTypeError TopLevelModuleName
    m FindError
    err
        Right SourceFile
    f  -> SourceFile -> TCM SourceFile
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SourceFile
    f

    -- | Tries to find the source file corresponding to a given top-level
    --   module name. The returned paths are absolute.
    --
    --   SIDE EFFECT:  Updates 'stModuleToSource'.
    findFile' :: TopLevelModuleName -> TCM (Either FindError SourceFile)
    findFile' :: TopLevelModuleName -> TCM (Either FindError SourceFile)
    findFile' TopLevelModuleName
    m = do
        dirs     <- TCMT IO (List1 AbsolutePath)
    forall (m :: * -> *). HasOptions m => m (List1 AbsolutePath)
    getIncludeDirs
        modToSrc <- useTC stModuleToSource
        (r, modToSrc) <- liftIO $ runStateT (findFile'' dirs m) modToSrc
        stModuleToSource `setTCLens` modToSrc
        return r

    -- | A variant of 'findFile'' which manipulates an extra 'ModuleToSourceId'

    findFile'_ ::
         List1 AbsolutePath
           -- ^ Include paths.
      -> TopLevelModuleName
      -> StateT ModuleToSourceId TCM (Either FindError SourceFile)
    findFile'_ :: List1 AbsolutePath
    -> TopLevelModuleName
    -> StateT ModuleToSourceId TCM (Either FindError SourceFile)
    findFile'_ List1 AbsolutePath
    incs TopLevelModuleName
    m = do
      dict <- Lens' TCState FileDictWithBuiltins
    -> StateT ModuleToSourceId TCM FileDictWithBuiltins
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (FileDictWithBuiltins -> f FileDictWithBuiltins)
    -> TCState -> f TCState
    Lens' TCState FileDictWithBuiltins
    stFileDict
      m2s  <- get
      (r, ModuleToSource dict' m2s') <- liftIO $
        runStateT (findFile'' incs m) $ ModuleToSource dict m2s
      setTCLens stFileDict dict'
      put m2s'
      return r

    -- | A variant of 'findFile'' which does not require 'TCM'.

    findFile'' ::
         List1 AbsolutePath
           -- ^ Include paths.
      -> TopLevelModuleName
      -> StateT ModuleToSource IO (Either FindError SourceFile)
    findFile'' :: List1 AbsolutePath
    -> TopLevelModuleName
    -> StateT ModuleToSource IO (Either FindError SourceFile)
    findFile'' List1 AbsolutePath
    dirs TopLevelModuleName
    m = do
      ModuleToSource dict modToSrc <- StateT ModuleToSource IO ModuleToSource
    forall s (m :: * -> *). MonadState s m => m s
    get
      case Map.lookup m modToSrc of
        Just SourceFile
    sf -> Either FindError SourceFile
    -> StateT ModuleToSource IO (Either FindError SourceFile)
    forall a. a -> StateT ModuleToSource IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either FindError SourceFile
     -> StateT ModuleToSource IO (Either FindError SourceFile))
    -> Either FindError SourceFile
    -> StateT ModuleToSource IO (Either FindError SourceFile)
    forall a b. (a -> b) -> a -> b
    $ SourceFile -> Either FindError SourceFile
    forall a b. b -> Either a b
    Right SourceFile
    sf
        Maybe SourceFile
    Nothing -> do
          files          <- IO [AbsolutePath] -> StateT ModuleToSource IO [AbsolutePath]
    forall a. IO a -> StateT ModuleToSource IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO [AbsolutePath] -> StateT ModuleToSource IO [AbsolutePath])
    -> IO [AbsolutePath] -> StateT ModuleToSource IO [AbsolutePath]
    forall a b. (a -> b) -> a -> b
    $ [String] -> IO [AbsolutePath]
    fileList [String]
    agdaFileExtensions
          existingFiles  <- liftIO $ filterM (doesFileExistCaseSensitive . filePath) files
          case nubOn id existingFiles of
            [AbsolutePath
    file]   -> do
              let (FileId
    i, FileDictWithBuiltins
    dict') = AbsolutePath
    -> FileDictWithBuiltins -> (FileId, FileDictWithBuiltins)
    registerFileIdWithBuiltin AbsolutePath
    file FileDictWithBuiltins
    dict
              let src :: SourceFile
    src = FileId -> SourceFile
    SourceFile FileId
    i
              ModuleToSource -> StateT ModuleToSource IO ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put (ModuleToSource -> StateT ModuleToSource IO ())
    -> ModuleToSource -> StateT ModuleToSource IO ()
    forall a b. (a -> b) -> a -> b
    $ FileDictWithBuiltins -> ModuleToSourceId -> ModuleToSource
    ModuleToSource FileDictWithBuiltins
    dict' (ModuleToSourceId -> ModuleToSource)
    -> ModuleToSourceId -> ModuleToSource
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleName
    -> SourceFile -> ModuleToSourceId -> ModuleToSourceId
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert TopLevelModuleName
    m SourceFile
    src ModuleToSourceId
    modToSrc
              Either FindError SourceFile
    -> StateT ModuleToSource IO (Either FindError SourceFile)
    forall a. a -> StateT ModuleToSource IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SourceFile -> Either FindError SourceFile
    forall a b. b -> Either a b
    Right SourceFile
    src)
            []       -> do
              filesShortList <- IO [AbsolutePath] -> StateT ModuleToSource IO [AbsolutePath]
    forall a. IO a -> StateT ModuleToSource IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO [AbsolutePath] -> StateT ModuleToSource IO [AbsolutePath])
    -> IO [AbsolutePath] -> StateT ModuleToSource IO [AbsolutePath]
    forall a b. (a -> b) -> a -> b
    $ [String] -> IO [AbsolutePath]
    fileList ([String] -> IO [AbsolutePath]) -> [String] -> IO [AbsolutePath]
    forall a b. (a -> b) -> a -> b
    $ List2 String -> [Item (List2 String)]
    forall l. IsList l => l -> [Item l]
    List2.toList List2 String
    parseFileExtsShortList
              return (Left (NotFound filesShortList))
            AbsolutePath
    f0:AbsolutePath
    f1:[AbsolutePath]
    fs -> Either FindError SourceFile
    -> StateT ModuleToSource IO (Either FindError SourceFile)
    forall a. a -> StateT ModuleToSource IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (FindError -> Either FindError SourceFile
    forall a b. a -> Either a b
    Left (List2 AbsolutePath -> FindError
    Ambiguous (List2 AbsolutePath -> FindError)
    -> List2 AbsolutePath -> FindError
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath
    -> AbsolutePath -> [AbsolutePath] -> List2 AbsolutePath
    forall a. a -> a -> [a] -> List2 a
    List2 AbsolutePath
    f0 AbsolutePath
    f1 [AbsolutePath]
    fs))
      where
        fileList :: [String] -> IO [AbsolutePath]
    fileList [String]
    exts = (String -> IO AbsolutePath) -> [String] -> IO [AbsolutePath]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM String -> IO AbsolutePath
    absolute
                        [ AbsolutePath -> String
    filePath AbsolutePath
    dir String -> String -> String
    </> String
    file
                        | AbsolutePath
    dir  <- List1 AbsolutePath -> [Item (List1 AbsolutePath)]
    forall l. IsList l => l -> [Item l]
    List1.toList List1 AbsolutePath
    dirs
                        , String
    file <- (String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (TopLevelModuleName -> String -> String
    moduleNameToFileName TopLevelModuleName
    m) [String]
    exts
                        ]

    -- | Finds the interface file corresponding to a given top-level
    -- module file. The returned paths are absolute.
    --
    -- Raises 'Nothing' if the interface file cannot be found.

    findInterfaceFile' :: HasCallStack  -- We are calling partial function toIFile, thus want a call stack.
      => SourceFile                 -- ^ Path to the source file
      -> TCM (Maybe InterfaceFile)  -- ^ Maybe path to the interface file
    findInterfaceFile' :: HasCallStack => SourceFile -> TCM (Maybe InterfaceFile)
    findInterfaceFile' SourceFile
    fp = IO (Maybe InterfaceFile) -> TCM (Maybe InterfaceFile)
    forall a. IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (Maybe InterfaceFile) -> TCM (Maybe InterfaceFile))
    -> (AbsolutePath -> IO (Maybe InterfaceFile))
    -> AbsolutePath
    -> TCM (Maybe InterfaceFile)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbsolutePath -> IO (Maybe InterfaceFile)
    mkInterfaceFile (AbsolutePath -> TCM (Maybe InterfaceFile))
    -> TCM AbsolutePath -> TCM (Maybe InterfaceFile)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< HasCallStack => SourceFile -> TCM AbsolutePath
    SourceFile -> TCM AbsolutePath
    toIFile SourceFile
    fp

    -- | Finds the interface file corresponding to a given top-level
    -- module file. The returned paths are absolute.
    --
    -- Raises an error if the source file cannot be found, and returns
    -- 'Nothing' if the source file can be found but not the interface
    -- file.

    findInterfaceFile :: HasCallStack  -- because of calling a partial function
      => TopLevelModuleName -> TCM (Maybe InterfaceFile)
    findInterfaceFile :: HasCallStack => TopLevelModuleName -> TCM (Maybe InterfaceFile)
    findInterfaceFile TopLevelModuleName
    m = HasCallStack => SourceFile -> TCM (Maybe InterfaceFile)
    SourceFile -> TCM (Maybe InterfaceFile)
    findInterfaceFile' (SourceFile -> TCM (Maybe InterfaceFile))
    -> TCM SourceFile -> TCM (Maybe InterfaceFile)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TopLevelModuleName -> TCM SourceFile
    findFile TopLevelModuleName
    m

    -- | Ensures that the module name matches the file name. The file
    -- corresponding to the module name (according to the include path)
    -- has to be the same as the given file name.

    checkModuleName ::
         TopLevelModuleName
           -- ^ The name of the module.
      -> SourceFile
           -- ^ The file from which it was loaded.
      -> Maybe TopLevelModuleName
           -- ^ The expected name, coming from an import statement.
      -> TCM ()
    checkModuleName :: TopLevelModuleName
    -> SourceFile -> Maybe TopLevelModuleName -> TCMT IO ()
    checkModuleName TopLevelModuleName
    name SourceFile
    src0 Maybe TopLevelModuleName
    mexpected = do
      file <- SourceFile -> TCM AbsolutePath
    forall (m :: * -> *). MonadFileId m => SourceFile -> m AbsolutePath
    srcFilePath SourceFile
    src0
      findFile' name >>= \case

        Left (NotFound [AbsolutePath]
    files)  -> TypeError -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
          case Maybe TopLevelModuleName
    mexpected of
            Maybe TopLevelModuleName
    Nothing -> TopLevelModuleName -> [AbsolutePath] -> TypeError
    ModuleNameDoesntMatchFileName TopLevelModuleName
    name [AbsolutePath]
    files
            Just TopLevelModuleName
    expected -> TopLevelModuleName -> TopLevelModuleName -> TypeError
    ModuleNameUnexpected TopLevelModuleName
    name TopLevelModuleName
    expected

        Left (Ambiguous List2 AbsolutePath
    files) -> TypeError -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
          TopLevelModuleName -> List2 AbsolutePath -> TypeError
    AmbiguousTopLevelModuleName TopLevelModuleName
    name List2 AbsolutePath
    files

        Right SourceFile
    src -> do
          file' <- SourceFile -> TCM AbsolutePath
    forall (m :: * -> *). MonadFileId m => SourceFile -> m AbsolutePath
    srcFilePath SourceFile
    src
          file  <- liftIO $ absolute $ filePath file
          unlessM (liftIO $ sameFile file file') $
            typeError $ ModuleDefinedInOtherFile name file file'

      -- Andreas, 2020-09-28, issue #4671:  In any case, make sure
      -- that we do not end up with a mismatch between expected
      -- and actual module name.

      forM_ mexpected \ TopLevelModuleName
    expected ->
        Bool -> TCMT IO () -> TCMT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (TopLevelModuleName
    name TopLevelModuleName -> TopLevelModuleName -> Bool
    forall a. Eq a => a -> a -> Bool
    == TopLevelModuleName
    expected) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
          TypeError -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath
    -> TopLevelModuleName -> TopLevelModuleName -> TypeError
    OverlappingProjects AbsolutePath
    file TopLevelModuleName
    name TopLevelModuleName
    expected
          -- OverlappingProjects is the correct error for
          -- test/Fail/customized/NestedProjectRoots
          -- -- typeError $ ModuleNameUnexpected name expected

    parseFileExtsShortList :: List2 String
    parseFileExtsShortList :: List2 String
    parseFileExtsShortList = String -> List1 String -> List2 String
    forall a. a -> List1 a -> List2 a
    List2.cons String
    ".agda" List1 String
    literateExtsShortList

    -- | Remove an Agda file extension from a filepath, if possible.
    stripAgdaExtension :: FilePath -> Maybe FilePath
    stripAgdaExtension :: String -> Maybe String
    stripAgdaExtension = [String] -> String -> Maybe String
    stripAnyOfExtensions [String]
    agdaFileExtensions

    -- | Check if a file path has an Agda extension.
    hasAgdaExtension :: FilePath -> Bool
    hasAgdaExtension :: String -> Bool
    hasAgdaExtension = Maybe String -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe String -> Bool)
    -> (String -> Maybe String) -> String -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Maybe String
    stripAgdaExtension

    -- | Remove an existing Agda file extension from a file path.
    dropAgdaExtension :: FilePath -> FilePath
    dropAgdaExtension :: String -> String
    dropAgdaExtension = String -> Maybe String -> String
    forall a. a -> Maybe a -> a
    fromMaybe String
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe String -> String)
    -> (String -> Maybe String) -> String -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Maybe String
    stripAgdaExtension

    rootNameModule :: AbsolutePath -> String
    rootNameModule :: AbsolutePath -> String
    rootNameModule = String -> String
    dropAgdaExtension (String -> String)
    -> (AbsolutePath -> String) -> AbsolutePath -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String, String) -> String
    forall a b. (a, b) -> b
    snd ((String, String) -> String)
    -> (AbsolutePath -> (String, String)) -> AbsolutePath -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> (String, String)
    splitFileName (String -> (String, String))
    -> (AbsolutePath -> String) -> AbsolutePath -> (String, String)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbsolutePath -> String
    filePath