    {-# OPTIONS_GHC -Wunused-imports #-}

    module Agda.TypeChecking.Monad.Imports
      ( addImport
      , addImportCycleCheck
      , checkForImportCycle
      , dropDecodedModule
      , getDecodedModule
      , getDecodedModules
      , getImportPath
      , getPrettyVisitedModules
      , getVisitedModule
      , getVisitedModules
      , setDecodedModules
      , setVisitedModules
      , storeDecodedModule
      , visitModule
      , withImportPath
      ) where

    import Control.Arrow   ( (***) )
    import Control.Monad   ( when )

    import Data.Maybe (catMaybes)
    import qualified Data.Map as Map
    import Data.Set (Set)
    import qualified Data.Set as Set

    import Agda.Syntax.Common.Pretty
    import Agda.Syntax.TopLevelModuleName
    import Agda.TypeChecking.Monad.Base

    import Agda.Utils.List ( caseListM )
    import qualified Agda.Utils.List1 as List1
    import qualified Agda.Utils.List2 as List2
    import Agda.Utils.Singleton (singleton)

    import Agda.Utils.Impossible

    -- | Register the given module as imported in the current state.
    --   Also recursively add its imports to the cumulative imports.
    addImport :: TopLevelModuleName -> TCM ()
    addImport :: TopLevelModuleName -> TCM ()
    addImport TopLevelModuleName
    top = do
      Lens' TCState (Set TopLevelModuleName)
    -> (Set TopLevelModuleName -> Set TopLevelModuleName) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    modifyTCLens' (Set TopLevelModuleName -> f (Set TopLevelModuleName))
    -> TCState -> f TCState
    Lens' TCState (Set TopLevelModuleName)
    stImportedModules ((Set TopLevelModuleName -> Set TopLevelModuleName) -> TCM ())
    -> (Set TopLevelModuleName -> Set TopLevelModuleName) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleName
    -> Set TopLevelModuleName -> Set TopLevelModuleName
    forall a. Ord a => a -> Set a -> Set a
    Set.insert TopLevelModuleName
    top
      Lens' TCState (Set TopLevelModuleName)
    -> (Set TopLevelModuleName -> TCMT IO (Set TopLevelModuleName))
    -> TCM ()
    forall (m :: * -> *) a.
    (MonadTCState m, ReadTCState m) =>
    Lens' TCState a -> (a -> m a) -> m ()
    modifyTCLensM (Set TopLevelModuleName -> f (Set TopLevelModuleName))
    -> TCState -> f TCState
    Lens' TCState (Set TopLevelModuleName)
    stImportedModulesTransitive ((Set TopLevelModuleName -> TCMT IO (Set TopLevelModuleName))
     -> TCM ())
    -> (Set TopLevelModuleName -> TCMT IO (Set TopLevelModuleName))
    -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Set TopLevelModuleName
    -> Set TopLevelModuleName -> TCMT IO (Set TopLevelModuleName)
    forall (m :: * -> *).
    ReadTCState m =>
    Set TopLevelModuleName
    -> Set TopLevelModuleName -> m (Set TopLevelModuleName)
    completeTransitiveImports (Set TopLevelModuleName
     -> Set TopLevelModuleName -> TCMT IO (Set TopLevelModuleName))
    -> Set TopLevelModuleName
    -> Set TopLevelModuleName
    -> TCMT IO (Set TopLevelModuleName)
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleName -> Set TopLevelModuleName
    forall el coll. Singleton el coll => el -> coll
    singleton TopLevelModuleName
    top

    -- | @completeTransitiveImports ms ms'@.
    --   Precondition: @ms@ disjoint from @ms'@.
    completeTransitiveImports :: ReadTCState m => Set TopLevelModuleName -> ImportedModules -> m ImportedModules
    completeTransitiveImports :: forall (m :: * -> *).
    ReadTCState m =>
    Set TopLevelModuleName
    -> Set TopLevelModuleName -> m (Set TopLevelModuleName)
    completeTransitiveImports Set TopLevelModuleName
    ms Set TopLevelModuleName
    old = if Set TopLevelModuleName -> Bool
    forall a. Set a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Set TopLevelModuleName
    ms then Set TopLevelModuleName -> m (Set TopLevelModuleName)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Set TopLevelModuleName
    old else do

      -- Add the given imports to the current set.
      let next :: Set TopLevelModuleName
    next = Set TopLevelModuleName
    old Set TopLevelModuleName
    -> Set TopLevelModuleName -> Set TopLevelModuleName
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.union` Set TopLevelModuleName
    ms

      -- The interfaces for the modules we added to the transitive imports.
      is <- [Maybe ModuleInfo] -> [ModuleInfo]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe ModuleInfo] -> [ModuleInfo])
    -> m [Maybe ModuleInfo] -> m [ModuleInfo]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TopLevelModuleName -> m (Maybe ModuleInfo))
    -> [TopLevelModuleName] -> m [Maybe ModuleInfo]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM TopLevelModuleName -> m (Maybe ModuleInfo)
    forall (m :: * -> *).
    ReadTCState m =>
    TopLevelModuleName -> m (Maybe ModuleInfo)
    getVisitedModule (Set TopLevelModuleName -> [TopLevelModuleName]
    forall a. Set a -> [a]
    Set.toList Set TopLevelModuleName
    ms)

      -- The imports of these modules.
      let imps = [Set TopLevelModuleName] -> Set TopLevelModuleName
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ([Set TopLevelModuleName] -> Set TopLevelModuleName)
    -> [Set TopLevelModuleName] -> Set TopLevelModuleName
    forall a b. (a -> b) -> a -> b
    $ (ModuleInfo -> Set TopLevelModuleName)
    -> [ModuleInfo] -> [Set TopLevelModuleName]
    forall a b. (a -> b) -> [a] -> [b]
    map ([TopLevelModuleName] -> Set TopLevelModuleName
    forall a. Ord a => [a] -> Set a
    Set.fromList ([TopLevelModuleName] -> Set TopLevelModuleName)
    -> (ModuleInfo -> [TopLevelModuleName])
    -> ModuleInfo
    -> Set TopLevelModuleName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((TopLevelModuleName, Hash) -> TopLevelModuleName)
    -> [(TopLevelModuleName, Hash)] -> [TopLevelModuleName]
    forall a b. (a -> b) -> [a] -> [b]
    map (TopLevelModuleName, Hash) -> TopLevelModuleName
    forall a b. (a, b) -> a
    fst ([(TopLevelModuleName, Hash)] -> [TopLevelModuleName])
    -> (ModuleInfo -> [(TopLevelModuleName, Hash)])
    -> ModuleInfo
    -> [TopLevelModuleName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Interface -> [(TopLevelModuleName, Hash)]
    iImportedModules (Interface -> [(TopLevelModuleName, Hash)])
    -> (ModuleInfo -> Interface)
    -> ModuleInfo
    -> [(TopLevelModuleName, Hash)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ModuleInfo -> Interface
    miInterface) [ModuleInfo]
    is

      -- Recurse on the new imports.
      completeTransitiveImports (imps `Set.difference` next) next

    addImportCycleCheck :: TopLevelModuleName -> TCM a -> TCM a
    addImportCycleCheck :: forall a. TopLevelModuleName -> TCM a -> TCM a
    addImportCycleCheck TopLevelModuleName
    m =
        (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a)
    -> (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ \TCEnv
    e -> TCEnv
    e { envImportPath = m : envImportPath e }

    getImportPath :: TCM [TopLevelModuleName]
    getImportPath :: TCM [TopLevelModuleName]
    getImportPath = (TCEnv -> [TopLevelModuleName]) -> TCM [TopLevelModuleName]
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> [TopLevelModuleName]
    envImportPath

    visitModule :: ModuleInfo -> TCM ()
    visitModule :: ModuleInfo -> TCM ()
    visitModule ModuleInfo
    mi =
      Lens' TCState (Map TopLevelModuleName ModuleInfo)
    -> (Map TopLevelModuleName ModuleInfo
        -> Map TopLevelModuleName ModuleInfo)
    -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> (a -> a) -> m ()
    modifyTCLens (Map TopLevelModuleName ModuleInfo
     -> f (Map TopLevelModuleName ModuleInfo))
    -> TCState -> f TCState
    Lens' TCState (Map TopLevelModuleName ModuleInfo)
    stVisitedModules ((Map TopLevelModuleName ModuleInfo
      -> Map TopLevelModuleName ModuleInfo)
     -> TCM ())
    -> (Map TopLevelModuleName ModuleInfo
        -> Map TopLevelModuleName ModuleInfo)
    -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        TopLevelModuleName
    -> ModuleInfo
    -> Map TopLevelModuleName ModuleInfo
    -> Map TopLevelModuleName ModuleInfo
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert (Interface -> TopLevelModuleName
    iTopLevelModuleName (Interface -> TopLevelModuleName)
    -> Interface -> TopLevelModuleName
    forall a b. (a -> b) -> a -> b
    $ ModuleInfo -> Interface
    miInterface ModuleInfo
    mi) ModuleInfo
    mi

    setVisitedModules :: VisitedModules -> TCM ()
    setVisitedModules :: Map TopLevelModuleName ModuleInfo -> TCM ()
    setVisitedModules Map TopLevelModuleName ModuleInfo
    ms = Lens' TCState (Map TopLevelModuleName ModuleInfo)
    -> Map TopLevelModuleName ModuleInfo -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' TCState a -> a -> m ()
    setTCLens (Map TopLevelModuleName ModuleInfo
     -> f (Map TopLevelModuleName ModuleInfo))
    -> TCState -> f TCState
    Lens' TCState (Map TopLevelModuleName ModuleInfo)
    stVisitedModules Map TopLevelModuleName ModuleInfo
    ms

    getVisitedModules :: ReadTCState m => m VisitedModules
    getVisitedModules :: forall (m :: * -> *).
    ReadTCState m =>
    m (Map TopLevelModuleName ModuleInfo)
    getVisitedModules = Lens' TCState (Map TopLevelModuleName ModuleInfo)
    -> m (Map TopLevelModuleName ModuleInfo)
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (Map TopLevelModuleName ModuleInfo
     -> f (Map TopLevelModuleName ModuleInfo))
    -> TCState -> f TCState
    Lens' TCState (Map TopLevelModuleName ModuleInfo)
    stVisitedModules

    getPrettyVisitedModules :: ReadTCState m => m Doc
    getPrettyVisitedModules :: forall (m :: * -> *). ReadTCState m => m Doc
    getPrettyVisitedModules = do
      visited <-  ((TopLevelModuleName, ModuleInfo) -> Doc)
    -> [(TopLevelModuleName, ModuleInfo)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Doc -> Doc -> Doc) -> (Doc, Doc) -> Doc
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    (<>) ((Doc, Doc) -> Doc)
    -> ((TopLevelModuleName, ModuleInfo) -> (Doc, Doc))
    -> (TopLevelModuleName, ModuleInfo)
    -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (TopLevelModuleName -> Doc
    forall a. Pretty a => a -> Doc
    pretty (TopLevelModuleName -> Doc)
    -> (ModuleInfo -> Doc)
    -> (TopLevelModuleName, ModuleInfo)
    -> (Doc, Doc)
    forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** (ModuleCheckMode -> Doc
    prettyCheckMode (ModuleCheckMode -> Doc)
    -> (ModuleInfo -> ModuleCheckMode) -> ModuleInfo -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ModuleInfo -> ModuleCheckMode
    miMode))) ([(TopLevelModuleName, ModuleInfo)] -> [Doc])
    -> (Map TopLevelModuleName ModuleInfo
        -> [(TopLevelModuleName, ModuleInfo)])
    -> Map TopLevelModuleName ModuleInfo
    -> [Doc]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map TopLevelModuleName ModuleInfo
    -> [(TopLevelModuleName, ModuleInfo)]
    forall k a. Map k a -> [(k, a)]
    Map.toList
              (Map TopLevelModuleName ModuleInfo -> [Doc])
    -> m (Map TopLevelModuleName ModuleInfo) -> m [Doc]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Map TopLevelModuleName ModuleInfo)
    forall (m :: * -> *).
    ReadTCState m =>
    m (Map TopLevelModuleName ModuleInfo)
    getVisitedModules
      return $ hcat $ punctuate ", " visited
      where
      prettyCheckMode :: ModuleCheckMode -> Doc
      prettyCheckMode :: ModuleCheckMode -> Doc
    prettyCheckMode ModuleCheckMode
    ModuleTypeChecked                  = Doc
    ""
      prettyCheckMode ModuleCheckMode
    ModuleScopeChecked                 = Doc
    " (scope only)"

    getVisitedModule :: ReadTCState m
                     => TopLevelModuleName
                     -> m (Maybe ModuleInfo)
    getVisitedModule :: forall (m :: * -> *).
    ReadTCState m =>
    TopLevelModuleName -> m (Maybe ModuleInfo)
    getVisitedModule TopLevelModuleName
    x = TopLevelModuleName
    -> Map TopLevelModuleName ModuleInfo -> Maybe ModuleInfo
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup TopLevelModuleName
    x (Map TopLevelModuleName ModuleInfo -> Maybe ModuleInfo)
    -> m (Map TopLevelModuleName ModuleInfo) -> m (Maybe ModuleInfo)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCState (Map TopLevelModuleName ModuleInfo)
    -> m (Map TopLevelModuleName ModuleInfo)
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (Map TopLevelModuleName ModuleInfo
     -> f (Map TopLevelModuleName ModuleInfo))
    -> TCState -> f TCState
    Lens' TCState (Map TopLevelModuleName ModuleInfo)
    stVisitedModules

    getDecodedModules :: TCM DecodedModules
    getDecodedModules :: TCM (Map TopLevelModuleName ModuleInfo)
    getDecodedModules = PersistentTCState -> Map TopLevelModuleName ModuleInfo
    stDecodedModules (PersistentTCState -> Map TopLevelModuleName ModuleInfo)
    -> (TCState -> PersistentTCState)
    -> TCState
    -> Map TopLevelModuleName ModuleInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCState -> PersistentTCState
    stPersistentState (TCState -> Map TopLevelModuleName ModuleInfo)
    -> TCMT IO TCState -> TCM (Map TopLevelModuleName ModuleInfo)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC

    setDecodedModules :: DecodedModules -> TCM ()
    setDecodedModules :: Map TopLevelModuleName ModuleInfo -> TCM ()
    setDecodedModules Map TopLevelModuleName ModuleInfo
    ms = (TCState -> TCState) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (TCState -> TCState) -> m ()
    modifyTC ((TCState -> TCState) -> TCM ()) -> (TCState -> TCState) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \TCState
    s ->
      TCState
    s { stPersistentState = (stPersistentState s) { stDecodedModules = ms } }

    getDecodedModule :: TopLevelModuleName -> TCM (Maybe ModuleInfo)
    getDecodedModule :: TopLevelModuleName -> TCM (Maybe ModuleInfo)
    getDecodedModule TopLevelModuleName
    x = TopLevelModuleName
    -> Map TopLevelModuleName ModuleInfo -> Maybe ModuleInfo
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup TopLevelModuleName
    x (Map TopLevelModuleName ModuleInfo -> Maybe ModuleInfo)
    -> (TCState -> Map TopLevelModuleName ModuleInfo)
    -> TCState
    -> Maybe ModuleInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PersistentTCState -> Map TopLevelModuleName ModuleInfo
    stDecodedModules (PersistentTCState -> Map TopLevelModuleName ModuleInfo)
    -> (TCState -> PersistentTCState)
    -> TCState
    -> Map TopLevelModuleName ModuleInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCState -> PersistentTCState
    stPersistentState (TCState -> Maybe ModuleInfo)
    -> TCMT IO TCState -> TCM (Maybe ModuleInfo)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC

    storeDecodedModule :: ModuleInfo -> TCM ()
    storeDecodedModule :: ModuleInfo -> TCM ()
    storeDecodedModule ModuleInfo
    mi = (TCState -> TCState) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (TCState -> TCState) -> m ()
    modifyTC ((TCState -> TCState) -> TCM ()) -> (TCState -> TCState) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \TCState
    s ->
      TCState
    s { stPersistentState =
            (stPersistentState s) { stDecodedModules =
              Map.insert (iTopLevelModuleName $ miInterface mi) mi $
                stDecodedModules (stPersistentState s)
            }
      }

    dropDecodedModule :: TopLevelModuleName -> TCM ()
    dropDecodedModule :: TopLevelModuleName -> TCM ()
    dropDecodedModule TopLevelModuleName
    x = (TCState -> TCState) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (TCState -> TCState) -> m ()
    modifyTC ((TCState -> TCState) -> TCM ()) -> (TCState -> TCState) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \TCState
    s ->
      TCState
    s { stPersistentState =
            (stPersistentState s) { stDecodedModules =
                                      Map.delete x $ stDecodedModules $ stPersistentState s
                                  }
      }

    withImportPath :: [TopLevelModuleName] -> TCM a -> TCM a
    withImportPath :: forall a. [TopLevelModuleName] -> TCM a -> TCM a
    withImportPath [TopLevelModuleName]
    path = (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC ((TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a)
    -> (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ \TCEnv
    e -> TCEnv
    e { envImportPath = path }

    -- | Assumes that the first module in the import path is the module we are
    --   worried about.
    checkForImportCycle :: TCM ()
    checkForImportCycle :: TCM ()
    checkForImportCycle = do
      TCM [TopLevelModuleName]
    -> TCM ()
    -> (TopLevelModuleName -> [TopLevelModuleName] -> TCM ())
    -> TCM ()
    forall (m :: * -> *) a b.
    Monad m =>
    m [a] -> m b -> (a -> [a] -> m b) -> m b
    caseListM TCM [TopLevelModuleName]
    getImportPath TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ((TopLevelModuleName -> [TopLevelModuleName] -> TCM ()) -> TCM ())
    -> (TopLevelModuleName -> [TopLevelModuleName] -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ TopLevelModuleName
    m [TopLevelModuleName]
    ms -> do
        Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (TopLevelModuleName
    m TopLevelModuleName -> [TopLevelModuleName] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [TopLevelModuleName]
    ms) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ List2 TopLevelModuleName -> TypeError
    CyclicModuleDependency (List2 TopLevelModuleName -> TypeError)
    -> List2 TopLevelModuleName -> TypeError
    forall a b. (a -> b) -> a -> b
    $
          List1 TopLevelModuleName
    -> TopLevelModuleName -> List2 TopLevelModuleName
    forall a. List1 a -> a -> List2 a
    List2.snoc (List1 TopLevelModuleName
    -> [TopLevelModuleName] -> List1 TopLevelModuleName
    forall a. List1 a -> [a] -> List1 a
    List1.fromListSafe List1 TopLevelModuleName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([TopLevelModuleName] -> List1 TopLevelModuleName)
    -> [TopLevelModuleName] -> List1 TopLevelModuleName
    forall a b. (a -> b) -> a -> b
    $ (TopLevelModuleName -> Bool)
    -> [TopLevelModuleName] -> [TopLevelModuleName]
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile (TopLevelModuleName -> TopLevelModuleName -> Bool
    forall a. Eq a => a -> a -> Bool
    /= TopLevelModuleName
    m) ([TopLevelModuleName] -> [TopLevelModuleName])
    -> [TopLevelModuleName] -> [TopLevelModuleName]
    forall a b. (a -> b) -> a -> b
    $ [TopLevelModuleName] -> [TopLevelModuleName]
    forall a. [a] -> [a]
    reverse [TopLevelModuleName]
    ms) TopLevelModuleName
    m
            -- NB: we know that ms contains m, so even after dropWhile the list is not empty.