    {-# LANGUAGE NondecreasingIndentation #-}

    {-| The scope monad with operations.
    -}

    module Agda.Syntax.Scope.Monad where

    import Prelude hiding (null)

    import Control.Arrow ((***))
    import Control.Monad
    import Control.Monad.Except
    import Control.Monad.State

    import Data.Either ( partitionEithers )
    import Data.Foldable (all, traverse_)
    import qualified Data.List as List
    import Data.Map (Map)
    import qualified Data.Map as Map
    import Data.Maybe
    import Data.Set (Set)
    import qualified Data.Set as Set
    import Data.Traversable hiding (for)

    import Agda.Interaction.Options
    import Agda.Interaction.Options.Warnings

    import Agda.Syntax.Common
    import Agda.Syntax.Position
    import Agda.Syntax.Fixity
    import Agda.Syntax.Notation
    import Agda.Syntax.Abstract.Name as A
    import qualified Agda.Syntax.Abstract as A
    import Agda.Syntax.Abstract (ScopeCopyInfo(..))
    import Agda.Syntax.Concrete as C
    import Agda.Syntax.Concrete.Fixity
    import Agda.Syntax.Concrete.Definitions ( DeclarationWarning(..) ,DeclarationWarning'(..) )
      -- TODO: move the relevant warnings out of there
    import Agda.Syntax.Scope.Base as A

    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Monad.Builtin ( HasBuiltins , getBuiltinName' , builtinSet , builtinProp , builtinSetOmega, builtinSSetOmega )
    import Agda.TypeChecking.Monad.Debug
    import Agda.TypeChecking.Monad.State
    import Agda.TypeChecking.Monad.Trace
    import Agda.TypeChecking.Positivity.Occurrence (Occurrence)
    import Agda.TypeChecking.Warnings ( warning, warning' )

    import qualified Agda.Utils.AssocList as AssocList
    import Agda.Utils.CallStack ( CallStack, HasCallStack, withCallerCallStack )
    import Agda.Utils.Functor
    import Agda.Utils.Lens
    import Agda.Utils.List
    import Agda.Utils.List1 (List1, pattern (:|), nonEmpty)
    import Agda.Utils.List2 (List2(List2))
    import qualified Agda.Utils.List1 as List1
    import qualified Agda.Utils.List2 as List2
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Pretty
    import Agda.Utils.Singleton
    import Agda.Utils.Suffix as C

    import Agda.Utils.Impossible

    ---------------------------------------------------------------------------
    -- * The scope checking monad
    ---------------------------------------------------------------------------

    -- | To simplify interaction between scope checking and type checking (in
    --   particular when chasing imports), we use the same monad.
    type ScopeM = TCM

    -- Debugging

    printLocals :: Int -> String -> ScopeM ()
    printLocals :: Int -> [Char] -> TCMT IO ()
    printLocals Int
    v [Char]
    s = [Char] -> Int -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
    verboseS [Char]
    "scope.top" Int
    v (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do
      LocalVars
    locals <- TCMT IO LocalVars
    forall (m :: * -> *). ReadTCState m => m LocalVars
    getLocalVars
      [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "scope.top" Int
    v ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    s [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ LocalVars -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow LocalVars
    locals

    scopeWarning' :: CallStack -> DeclarationWarning' -> ScopeM ()
    scopeWarning' :: CallStack -> DeclarationWarning' -> TCMT IO ()
    scopeWarning' CallStack
    loc = CallStack -> Warning -> TCMT IO ()
    forall (m :: * -> *).
    MonadWarning m =>
    CallStack -> Warning -> m ()
    warning' CallStack
    loc (Warning -> TCMT IO ())
    -> (DeclarationWarning' -> Warning)
    -> DeclarationWarning'
    -> TCMT IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DeclarationWarning -> Warning
    NicifierIssue (DeclarationWarning -> Warning)
    -> (DeclarationWarning' -> DeclarationWarning)
    -> DeclarationWarning'
    -> Warning
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CallStack -> DeclarationWarning' -> DeclarationWarning
    DeclarationWarning CallStack
    loc

    scopeWarning :: HasCallStack => DeclarationWarning' -> ScopeM ()
    scopeWarning :: HasCallStack => DeclarationWarning' -> TCMT IO ()
    scopeWarning = (CallStack -> DeclarationWarning' -> TCMT IO ())
    -> DeclarationWarning' -> TCMT IO ()
    forall b. HasCallStack => (CallStack -> b) -> b
    withCallerCallStack CallStack -> DeclarationWarning' -> TCMT IO ()
    scopeWarning'

    ---------------------------------------------------------------------------
    -- * General operations
    ---------------------------------------------------------------------------

    isDatatypeModule :: ReadTCState m => A.ModuleName -> m (Maybe DataOrRecordModule)
    isDatatypeModule :: forall (m :: * -> *).
    ReadTCState m =>
    ModuleName -> m (Maybe DataOrRecordModule)
    isDatatypeModule ModuleName
    m = do
       Scope -> Maybe DataOrRecordModule
    scopeDatatypeModule (Scope -> Maybe DataOrRecordModule)
    -> (Map ModuleName Scope -> Scope)
    -> Map ModuleName Scope
    -> Maybe DataOrRecordModule
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Scope -> ModuleName -> Map ModuleName Scope -> Scope
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault Scope
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ModuleName
    m (Map ModuleName Scope -> Maybe DataOrRecordModule)
    -> m (Map ModuleName Scope) -> m (Maybe DataOrRecordModule)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' (Map ModuleName Scope) ScopeInfo -> m (Map ModuleName Scope)
    forall (m :: * -> *) a. ReadTCState m => Lens' a ScopeInfo -> m a
    useScope Lens' (Map ModuleName Scope) ScopeInfo
    scopeModules

    getCurrentModule :: ReadTCState m => m A.ModuleName
    getCurrentModule :: forall (m :: * -> *). ReadTCState m => m ModuleName
    getCurrentModule = Range -> ModuleName -> ModuleName
    forall a. SetRange a => Range -> a -> a
    setRange Range
    forall a. Range' a
    noRange (ModuleName -> ModuleName) -> m ModuleName -> m ModuleName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' ModuleName ScopeInfo -> m ModuleName
    forall (m :: * -> *) a. ReadTCState m => Lens' a ScopeInfo -> m a
    useScope Lens' ModuleName ScopeInfo
    scopeCurrent

    setCurrentModule :: MonadTCState m => A.ModuleName -> m ()
    setCurrentModule :: forall (m :: * -> *). MonadTCState m => ModuleName -> m ()
    setCurrentModule ModuleName
    m = (ScopeInfo -> ScopeInfo) -> m ()
    forall (m :: * -> *).
    MonadTCState m =>
    (ScopeInfo -> ScopeInfo) -> m ()
    modifyScope ((ScopeInfo -> ScopeInfo) -> m ())
    -> (ScopeInfo -> ScopeInfo) -> m ()
    forall a b. (a -> b) -> a -> b
    $ Lens' ModuleName ScopeInfo -> LensSet ModuleName ScopeInfo
    forall i o. Lens' i o -> LensSet i o
    set Lens' ModuleName ScopeInfo
    scopeCurrent ModuleName
    m

    withCurrentModule :: (ReadTCState m, MonadTCState m) => A.ModuleName -> m a -> m a
    withCurrentModule :: forall (m :: * -> *) a.
    (ReadTCState m, MonadTCState m) =>
    ModuleName -> m a -> m a
    withCurrentModule ModuleName
    new m a
    action = do
      ModuleName
    old <- m ModuleName
    forall (m :: * -> *). ReadTCState m => m ModuleName
    getCurrentModule
      ModuleName -> m ()
    forall (m :: * -> *). MonadTCState m => ModuleName -> m ()
    setCurrentModule ModuleName
    new
      a
    x   <- m a
    action
      ModuleName -> m ()
    forall (m :: * -> *). MonadTCState m => ModuleName -> m ()
    setCurrentModule ModuleName
    old
      a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    x

    withCurrentModule' :: (MonadTrans t, Monad (t ScopeM)) => A.ModuleName -> t ScopeM a -> t ScopeM a
    withCurrentModule' :: forall (t :: (* -> *) -> * -> *) a.
    (MonadTrans t, Monad (t (TCMT IO))) =>
    ModuleName -> t (TCMT IO) a -> t (TCMT IO) a
    withCurrentModule' ModuleName
    new t (TCMT IO) a
    action = do
      ModuleName
    old <- ScopeM ModuleName -> t (TCMT IO) ModuleName
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift ScopeM ModuleName
    forall (m :: * -> *). ReadTCState m => m ModuleName
    getCurrentModule
      TCMT IO () -> t (TCMT IO) ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> t (TCMT IO) ()) -> TCMT IO () -> t (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> TCMT IO ()
    forall (m :: * -> *). MonadTCState m => ModuleName -> m ()
    setCurrentModule ModuleName
    new
      a
    x   <- t (TCMT IO) a
    action
      TCMT IO () -> t (TCMT IO) ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> t (TCMT IO) ()) -> TCMT IO () -> t (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> TCMT IO ()
    forall (m :: * -> *). MonadTCState m => ModuleName -> m ()
    setCurrentModule ModuleName
    old
      a -> t (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    x

    getNamedScope :: A.ModuleName -> ScopeM Scope
    getNamedScope :: ModuleName -> ScopeM Scope
    getNamedScope ModuleName
    m = do
      ScopeInfo
    scope <- TCMT IO ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope
      case ModuleName -> Map ModuleName Scope -> Maybe Scope
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup ModuleName
    m (ScopeInfo
    scope ScopeInfo
    -> Lens' (Map ModuleName Scope) ScopeInfo -> Map ModuleName Scope
    forall o i. o -> Lens' i o -> i
    ^. Lens' (Map ModuleName Scope) ScopeInfo
    scopeModules) of
        Just Scope
    s  -> Scope -> ScopeM Scope
    forall (m :: * -> *) a. Monad m => a -> m a
    return Scope
    s
        Maybe Scope
    Nothing -> do
          [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "" Int
    0 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "ERROR: In scope\n" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ ScopeInfo -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow ScopeInfo
    scope [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "\nNO SUCH SCOPE " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ ModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow ModuleName
    m
          ScopeM Scope
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    getCurrentScope :: ScopeM Scope
    getCurrentScope :: ScopeM Scope
    getCurrentScope = ModuleName -> ScopeM Scope
    getNamedScope (ModuleName -> ScopeM Scope) -> ScopeM ModuleName -> ScopeM Scope
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ScopeM ModuleName
    forall (m :: * -> *). ReadTCState m => m ModuleName
    getCurrentModule

    -- | Create a new module with an empty scope.
    --   If the module is not new (e.g. duplicate @import@),
    --   don't erase its contents.
    --   (@Just@ if it is a datatype or record module.)
    createModule :: Maybe DataOrRecordModule -> A.ModuleName -> ScopeM ()
    createModule :: Maybe DataOrRecordModule -> ModuleName -> TCMT IO ()
    createModule Maybe DataOrRecordModule
    b ModuleName
    m = do
      [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "scope.createModule" Int
    10 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "createModule " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ ModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow ModuleName
    m
      Scope
    s <- ScopeM Scope
    getCurrentScope
      let parents :: [ModuleName]
    parents = Scope -> ModuleName
    scopeName Scope
    s ModuleName -> [ModuleName] -> [ModuleName]
    forall a. a -> [a] -> [a]
    : Scope -> [ModuleName]
    scopeParents Scope
    s
          sm :: Scope
    sm = Scope
    emptyScope { scopeName :: ModuleName
    scopeName           = ModuleName
    m
                          , scopeParents :: [ModuleName]
    scopeParents        = [ModuleName]
    parents
                          , scopeDatatypeModule :: Maybe DataOrRecordModule
    scopeDatatypeModule = Maybe DataOrRecordModule
    b }
      -- Andreas, 2015-07-02: internal error if module is not new.
      -- Ulf, 2016-02-15: It's not new if multiple imports (#1770).
      -- Andreas, 2020-05-18, issue #3933:
      -- If it is not new (but apparently did not clash),
      -- we do not erase its contents for reasons of monotonicity.
      (Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ()
    modifyScopes ((Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ())
    -> (Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ (Scope -> Scope -> Scope)
    -> ModuleName
    -> Scope
    -> Map ModuleName Scope
    -> Map ModuleName Scope
    forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
    Map.insertWith Scope -> Scope -> Scope
    mergeScope ModuleName
    m Scope
    sm

    -- | Apply a function to the scope map.
    modifyScopes :: (Map A.ModuleName Scope -> Map A.ModuleName Scope) -> ScopeM ()
    modifyScopes :: (Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ()
    modifyScopes = (ScopeInfo -> ScopeInfo) -> TCMT IO ()
    forall (m :: * -> *).
    MonadTCState m =>
    (ScopeInfo -> ScopeInfo) -> m ()
    modifyScope ((ScopeInfo -> ScopeInfo) -> TCMT IO ())
    -> ((Map ModuleName Scope -> Map ModuleName Scope)
        -> ScopeInfo -> ScopeInfo)
    -> (Map ModuleName Scope -> Map ModuleName Scope)
    -> TCMT IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Lens' (Map ModuleName Scope) ScopeInfo
    -> (Map ModuleName Scope -> Map ModuleName Scope)
    -> ScopeInfo
    -> ScopeInfo
    forall i o. Lens' i o -> LensMap i o
    over Lens' (Map ModuleName Scope) ScopeInfo
    scopeModules

    -- | Apply a function to the given scope.
    modifyNamedScope :: A.ModuleName -> (Scope -> Scope) -> ScopeM ()
    modifyNamedScope :: ModuleName -> (Scope -> Scope) -> TCMT IO ()
    modifyNamedScope ModuleName
    m Scope -> Scope
    f = (Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ()
    modifyScopes ((Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ())
    -> (Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ (Scope -> Scope)
    -> ModuleName -> Map ModuleName Scope -> Map ModuleName Scope
    forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
    Map.adjust Scope -> Scope
    f ModuleName
    m

    setNamedScope :: A.ModuleName -> Scope -> ScopeM ()
    setNamedScope :: ModuleName -> Scope -> TCMT IO ()
    setNamedScope ModuleName
    m Scope
    s = ModuleName -> (Scope -> Scope) -> TCMT IO ()
    modifyNamedScope ModuleName
    m ((Scope -> Scope) -> TCMT IO ()) -> (Scope -> Scope) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Scope -> Scope -> Scope
    forall a b. a -> b -> a
    const Scope
    s

    -- | Apply a monadic function to the top scope.
    modifyNamedScopeM :: A.ModuleName -> (Scope -> ScopeM (a, Scope)) -> ScopeM a
    modifyNamedScopeM :: forall a. ModuleName -> (Scope -> ScopeM (a, Scope)) -> ScopeM a
    modifyNamedScopeM ModuleName
    m Scope -> ScopeM (a, Scope)
    f = do
      (a
    a, Scope
    s) <- Scope -> ScopeM (a, Scope)
    f (Scope -> ScopeM (a, Scope)) -> ScopeM Scope -> ScopeM (a, Scope)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ModuleName -> ScopeM Scope
    getNamedScope ModuleName
    m
      ModuleName -> Scope -> TCMT IO ()
    setNamedScope ModuleName
    m Scope
    s
      a -> ScopeM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a

    -- | Apply a function to the current scope.
    modifyCurrentScope :: (Scope -> Scope) -> ScopeM ()
    modifyCurrentScope :: (Scope -> Scope) -> TCMT IO ()
    modifyCurrentScope Scope -> Scope
    f = ScopeM ModuleName
    forall (m :: * -> *). ReadTCState m => m ModuleName
    getCurrentModule ScopeM ModuleName -> (ModuleName -> TCMT IO ()) -> TCMT IO ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= (ModuleName -> (Scope -> Scope) -> TCMT IO ()
    `modifyNamedScope` Scope -> Scope
    f)

    modifyCurrentScopeM :: (Scope -> ScopeM (a, Scope)) -> ScopeM a
    modifyCurrentScopeM :: forall a. (Scope -> ScopeM (a, Scope)) -> ScopeM a
    modifyCurrentScopeM Scope -> ScopeM (a, Scope)
    f = ScopeM ModuleName
    forall (m :: * -> *). ReadTCState m => m ModuleName
    getCurrentModule ScopeM ModuleName -> (ModuleName -> TCMT IO a) -> TCMT IO a
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= (ModuleName -> (Scope -> ScopeM (a, Scope)) -> TCMT IO a
    forall a. ModuleName -> (Scope -> ScopeM (a, Scope)) -> ScopeM a
    `modifyNamedScopeM` Scope -> ScopeM (a, Scope)
    f)

    -- | Apply a function to the public or private name space.
    modifyCurrentNameSpace :: NameSpaceId -> (NameSpace -> NameSpace) -> ScopeM ()
    modifyCurrentNameSpace :: NameSpaceId -> (NameSpace -> NameSpace) -> TCMT IO ()
    modifyCurrentNameSpace NameSpaceId
    acc NameSpace -> NameSpace
    f = (Scope -> Scope) -> TCMT IO ()
    modifyCurrentScope ((Scope -> Scope) -> TCMT IO ()) -> (Scope -> Scope) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ (ScopeNameSpaces -> ScopeNameSpaces) -> Scope -> Scope
    updateScopeNameSpaces ((ScopeNameSpaces -> ScopeNameSpaces) -> Scope -> Scope)
    -> (ScopeNameSpaces -> ScopeNameSpaces) -> Scope -> Scope
    forall a b. (a -> b) -> a -> b
    $
      NameSpaceId
    -> (NameSpace -> NameSpace) -> ScopeNameSpaces -> ScopeNameSpaces
    forall k v. Eq k => k -> (v -> v) -> AssocList k v -> AssocList k v
    AssocList.updateAt NameSpaceId
    acc NameSpace -> NameSpace
    f

    setContextPrecedence :: PrecedenceStack -> ScopeM ()
    setContextPrecedence :: PrecedenceStack -> TCMT IO ()
    setContextPrecedence = (ScopeInfo -> ScopeInfo) -> TCMT IO ()
    forall (m :: * -> *).
    MonadTCState m =>
    (ScopeInfo -> ScopeInfo) -> m ()
    modifyScope_ ((ScopeInfo -> ScopeInfo) -> TCMT IO ())
    -> (PrecedenceStack -> ScopeInfo -> ScopeInfo)
    -> PrecedenceStack
    -> TCMT IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Lens' PrecedenceStack ScopeInfo
    -> PrecedenceStack -> ScopeInfo -> ScopeInfo
    forall i o. Lens' i o -> LensSet i o
    set Lens' PrecedenceStack ScopeInfo
    scopePrecedence

    withContextPrecedence :: ReadTCState m => Precedence -> m a -> m a
    withContextPrecedence :: forall (m :: * -> *) a. ReadTCState m => Precedence -> m a -> m a
    withContextPrecedence Precedence
    p =
      Lens' PrecedenceStack TCState
    -> (PrecedenceStack -> PrecedenceStack) -> m a -> m a
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' a TCState -> (a -> a) -> m b -> m b
    locallyTCState ((ScopeInfo -> f ScopeInfo) -> TCState -> f TCState
    Lens' ScopeInfo TCState
    stScope ((ScopeInfo -> f ScopeInfo) -> TCState -> f TCState)
    -> ((PrecedenceStack -> f PrecedenceStack)
        -> ScopeInfo -> f ScopeInfo)
    -> (PrecedenceStack -> f PrecedenceStack)
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (PrecedenceStack -> f PrecedenceStack) -> ScopeInfo -> f ScopeInfo
    Lens' PrecedenceStack ScopeInfo
    scopePrecedence) ((PrecedenceStack -> PrecedenceStack) -> m a -> m a)
    -> (PrecedenceStack -> PrecedenceStack) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ Precedence -> PrecedenceStack -> PrecedenceStack
    pushPrecedence Precedence
    p

    getLocalVars :: ReadTCState m => m LocalVars
    getLocalVars :: forall (m :: * -> *). ReadTCState m => m LocalVars
    getLocalVars = Lens' LocalVars ScopeInfo -> m LocalVars
    forall (m :: * -> *) a. ReadTCState m => Lens' a ScopeInfo -> m a
    useScope Lens' LocalVars ScopeInfo
    scopeLocals

    modifyLocalVars :: (LocalVars -> LocalVars) -> ScopeM ()
    modifyLocalVars :: (LocalVars -> LocalVars) -> TCMT IO ()
    modifyLocalVars = (ScopeInfo -> ScopeInfo) -> TCMT IO ()
    forall (m :: * -> *).
    MonadTCState m =>
    (ScopeInfo -> ScopeInfo) -> m ()
    modifyScope_ ((ScopeInfo -> ScopeInfo) -> TCMT IO ())
    -> ((LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo)
    -> (LocalVars -> LocalVars)
    -> TCMT IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo
    updateScopeLocals

    setLocalVars :: LocalVars -> ScopeM ()
    setLocalVars :: LocalVars -> TCMT IO ()
    setLocalVars LocalVars
    vars = (LocalVars -> LocalVars) -> TCMT IO ()
    modifyLocalVars ((LocalVars -> LocalVars) -> TCMT IO ())
    -> (LocalVars -> LocalVars) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ LocalVars -> LocalVars -> LocalVars
    forall a b. a -> b -> a
    const LocalVars
    vars

    -- | Run a computation without changing the local variables.
    withLocalVars :: ScopeM a -> ScopeM a
    withLocalVars :: forall a. ScopeM a -> ScopeM a
    withLocalVars = TCMT IO LocalVars
    -> (LocalVars -> TCMT IO ()) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a b.
    Monad m =>
    m a -> (a -> m ()) -> m b -> m b
    bracket_ TCMT IO LocalVars
    forall (m :: * -> *). ReadTCState m => m LocalVars
    getLocalVars LocalVars -> TCMT IO ()
    setLocalVars

    -- | Run a computation outside some number of local variables and add them back afterwards. This
    --   lets you bind variables in the middle of the context and is used when binding generalizable
    --   variables (#3735).
    outsideLocalVars :: Int -> ScopeM a -> ScopeM a
    outsideLocalVars :: forall a. Int -> ScopeM a -> ScopeM a
    outsideLocalVars Int
    n ScopeM a
    m = do
      LocalVars
    inner <- Int -> LocalVars -> LocalVars
    forall a. Int -> [a] -> [a]
    take Int
    n (LocalVars -> LocalVars) -> TCMT IO LocalVars -> TCMT IO LocalVars
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO LocalVars
    forall (m :: * -> *). ReadTCState m => m LocalVars
    getLocalVars
      (LocalVars -> LocalVars) -> TCMT IO ()
    modifyLocalVars (Int -> LocalVars -> LocalVars
    forall a. Int -> [a] -> [a]
    drop Int
    n)
      a
    x <- ScopeM a
    m
      (LocalVars -> LocalVars) -> TCMT IO ()
    modifyLocalVars (LocalVars
    inner LocalVars -> LocalVars -> LocalVars
    forall a. [a] -> [a] -> [a]
    ++)
      a -> ScopeM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    x

    -- | Check that the newly added variable have unique names.

    withCheckNoShadowing :: ScopeM a -> ScopeM a
    withCheckNoShadowing :: forall a. ScopeM a -> ScopeM a
    withCheckNoShadowing = TCMT IO LocalVars
    -> (LocalVars -> TCMT IO ()) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a b.
    Monad m =>
    m a -> (a -> m ()) -> m b -> m b
    bracket_ TCMT IO LocalVars
    forall (m :: * -> *). ReadTCState m => m LocalVars
    getLocalVars ((LocalVars -> TCMT IO ()) -> TCMT IO a -> TCMT IO a)
    -> (LocalVars -> TCMT IO ()) -> TCMT IO a -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ \ LocalVars
    lvarsOld ->
      LocalVars -> LocalVars -> TCMT IO ()
    checkNoShadowing LocalVars
    lvarsOld (LocalVars -> TCMT IO ()) -> TCMT IO LocalVars -> TCMT IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO LocalVars
    forall (m :: * -> *). ReadTCState m => m LocalVars
    getLocalVars

    checkNoShadowing :: LocalVars  -- ^ Old local scope
                     -> LocalVars  -- ^ New local scope
                     -> ScopeM ()
    checkNoShadowing :: LocalVars -> LocalVars -> TCMT IO ()
    checkNoShadowing LocalVars
    old LocalVars
    new = do
      PragmaOptions
    opts <- TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
      Bool -> TCMT IO () -> TCMT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (WarningName
    ShadowingInTelescope_ WarningName -> Set WarningName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member`
              (PragmaOptions -> WarningMode
    optWarningMode PragmaOptions
    opts WarningMode
    -> Lens' (Set WarningName) WarningMode -> Set WarningName
    forall o i. o -> Lens' i o -> i
    ^. Lens' (Set WarningName) WarningMode
    warningSet)) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do
        -- LocalVars is currnently an AssocList so the difference between
        -- two local scope is the left part of the new one.
        let diff :: LocalVars
    diff = Int -> LocalVars -> LocalVars
    forall a. Int -> [a] -> [a]
    dropEnd (LocalVars -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length LocalVars
    old) LocalVars
    new
        -- Filter out the underscores.
        let newNames :: [Name]
    newNames = (Name -> Bool) -> [Name] -> [Name]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool) -> (Name -> Bool) -> Name -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName) ([Name] -> [Name]) -> [Name] -> [Name]
    forall a b. (a -> b) -> a -> b
    $ LocalVars -> [Name]
    forall k v. AssocList k v -> [k]
    AssocList.keys LocalVars
    diff
        -- Associate each name to its occurrences.
        let nameOccs1 :: [(C.Name, List1 Range)]
            nameOccs1 :: [(Name, NonEmpty Range)]
    nameOccs1 = Map Name (NonEmpty Range) -> [(Name, NonEmpty Range)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (Map Name (NonEmpty Range) -> [(Name, NonEmpty Range)])
    -> Map Name (NonEmpty Range) -> [(Name, NonEmpty Range)]
    forall a b. (a -> b) -> a -> b
    $ (NonEmpty Range -> NonEmpty Range -> NonEmpty Range)
    -> [(Name, NonEmpty Range)] -> Map Name (NonEmpty Range)
    forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
    Map.fromListWith NonEmpty Range -> NonEmpty Range -> NonEmpty Range
    forall a. Semigroup a => a -> a -> a
    (<>) ([(Name, NonEmpty Range)] -> Map Name (NonEmpty Range))
    -> [(Name, NonEmpty Range)] -> Map Name (NonEmpty Range)
    forall a b. (a -> b) -> a -> b
    $ (Name -> (Name, NonEmpty Range))
    -> [Name] -> [(Name, NonEmpty Range)]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> (Name, NonEmpty Range)
    pairWithRange [Name]
    newNames
        -- Warn if we have two or more occurrences of the same name.
        let nameOccs2 :: [(C.Name, List2 Range)]
            nameOccs2 :: [(Name, List2 Range)]
    nameOccs2 = ((Name, NonEmpty Range) -> Maybe (Name, List2 Range))
    -> [(Name, NonEmpty Range)] -> [(Name, List2 Range)]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe ((NonEmpty Range -> Maybe (List2 Range))
    -> (Name, NonEmpty Range) -> Maybe (Name, List2 Range)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Decoration t, Functor m) =>
    (a -> m b) -> t a -> m (t b)
    traverseF NonEmpty Range -> Maybe (List2 Range)
    forall a. List1 a -> Maybe (List2 a)
    List2.fromList1Maybe) [(Name, NonEmpty Range)]
    nameOccs1
        [(Name, List2 Range)]
    -> TCMT IO ()
    -> ((Name, List2 Range) -> [(Name, List2 Range)] -> TCMT IO ())
    -> TCMT IO ()
    forall a b. [a] -> b -> (a -> [a] -> b) -> b
    caseList [(Name, List2 Range)]
    nameOccs2 (() -> TCMT IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()) (((Name, List2 Range) -> [(Name, List2 Range)] -> TCMT IO ())
     -> TCMT IO ())
    -> ((Name, List2 Range) -> [(Name, List2 Range)] -> TCMT IO ())
    -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ \ (Name, List2 Range)
    c [(Name, List2 Range)]
    conflicts -> do
          HasCallStack => DeclarationWarning' -> TCMT IO ()
    DeclarationWarning' -> TCMT IO ()
    scopeWarning (DeclarationWarning' -> TCMT IO ())
    -> DeclarationWarning' -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ List1 (Name, List2 Range) -> DeclarationWarning'
    ShadowingInTelescope (List1 (Name, List2 Range) -> DeclarationWarning')
    -> List1 (Name, List2 Range) -> DeclarationWarning'
    forall a b. (a -> b) -> a -> b
    $ (Name, List2 Range)
    c (Name, List2 Range)
    -> [(Name, List2 Range)] -> List1 (Name, List2 Range)
    forall a. a -> [a] -> NonEmpty a
    :| [(Name, List2 Range)]
    conflicts
      where
        pairWithRange :: C.Name -> (C.Name, List1 Range)
        pairWithRange :: Name -> (Name, NonEmpty Range)
    pairWithRange Name
    n = (Name
    n, Range -> NonEmpty Range
    forall el coll. Singleton el coll => el -> coll
    singleton (Range -> NonEmpty Range) -> Range -> NonEmpty Range
    forall a b. (a -> b) -> a -> b
    $ Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    n)

    getVarsToBind :: ScopeM LocalVars
    getVarsToBind :: TCMT IO LocalVars
    getVarsToBind = Lens' LocalVars ScopeInfo -> TCMT IO LocalVars
    forall (m :: * -> *) a. ReadTCState m => Lens' a ScopeInfo -> m a
    useScope Lens' LocalVars ScopeInfo
    scopeVarsToBind

    addVarToBind :: C.Name -> LocalVar -> ScopeM ()
    addVarToBind :: Name -> LocalVar -> TCMT IO ()
    addVarToBind Name
    x LocalVar
    y = (ScopeInfo -> ScopeInfo) -> TCMT IO ()
    forall (m :: * -> *).
    MonadTCState m =>
    (ScopeInfo -> ScopeInfo) -> m ()
    modifyScope_ ((ScopeInfo -> ScopeInfo) -> TCMT IO ())
    -> (ScopeInfo -> ScopeInfo) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ (LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo
    updateVarsToBind ((LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo)
    -> (LocalVars -> LocalVars) -> ScopeInfo -> ScopeInfo
    forall a b. (a -> b) -> a -> b
    $ Name -> LocalVar -> LocalVars -> LocalVars
    forall k v. k -> v -> AssocList k v -> AssocList k v
    AssocList.insert Name
    x LocalVar
    y

    -- | After collecting some variable names in the scopeVarsToBind,
    --   bind them all simultaneously.
    bindVarsToBind :: ScopeM ()
    bindVarsToBind :: TCMT IO ()
    bindVarsToBind = do
      LocalVars
    vars <- TCMT IO LocalVars
    getVarsToBind
      (LocalVars -> LocalVars) -> TCMT IO ()
    modifyLocalVars (LocalVars
    varsLocalVars -> LocalVars -> LocalVars
    forall a. [a] -> [a] -> [a]
    ++)
      Int -> [Char] -> TCMT IO ()
    printLocals Int
    10 [Char]
    "bound variables:"
      (ScopeInfo -> ScopeInfo) -> TCMT IO ()
    forall (m :: * -> *).
    MonadTCState m =>
    (ScopeInfo -> ScopeInfo) -> m ()
    modifyScope_ ((ScopeInfo -> ScopeInfo) -> TCMT IO ())
    -> (ScopeInfo -> ScopeInfo) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ LocalVars -> ScopeInfo -> ScopeInfo
    setVarsToBind []

    annotateDecls :: ReadTCState m => m [A.Declaration] -> m A.Declaration
    annotateDecls :: forall (m :: * -> *).
    ReadTCState m =>
    m [Declaration] -> m Declaration
    annotateDecls m [Declaration]
    m = do
      [Declaration]
    ds <- m [Declaration]
    m
      ScopeInfo
    s  <- m ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope
      Declaration -> m Declaration
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Declaration -> m Declaration) -> Declaration -> m Declaration
    forall a b. (a -> b) -> a -> b
    $ ScopeInfo -> [Declaration] -> Declaration
    A.ScopedDecl ScopeInfo
    s [Declaration]
    ds

    annotateExpr :: ReadTCState m => m A.Expr -> m A.Expr
    annotateExpr :: forall (m :: * -> *). ReadTCState m => m Expr -> m Expr
    annotateExpr m Expr
    m = do
      Expr
    e <- m Expr
    m
      ScopeInfo
    s <- m ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope
      Expr -> m Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> m Expr) -> Expr -> m Expr
    forall a b. (a -> b) -> a -> b
    $ ScopeInfo -> Expr -> Expr
    A.ScopedExpr ScopeInfo
    s Expr
    e

    ---------------------------------------------------------------------------
    -- * Names
    ---------------------------------------------------------------------------

    -- | Create a fresh abstract name from a concrete name.
    --
    --   This function is used when we translate a concrete name
    --   in a binder.  The 'Range' of the concrete name is
    --   saved as the 'nameBindingSite' of the abstract name.
    freshAbstractName :: Fixity' -> C.Name -> ScopeM A.Name
    freshAbstractName :: Fixity' -> Name -> ScopeM Name
    freshAbstractName Fixity'
    fx Name
    x = do
      NameId
    i <- TCMT IO NameId
    forall i (m :: * -> *). MonadFresh i m => m i
    fresh
      Name -> ScopeM Name
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Name -> ScopeM Name) -> Name -> ScopeM Name
    forall a b. (a -> b) -> a -> b
    $ Name :: NameId -> Name -> Name -> Range -> Fixity' -> Bool -> Name
    A.Name
        { nameId :: NameId
    nameId          = NameId
    i
        , nameConcrete :: Name
    nameConcrete    = Name
    x
        , nameCanonical :: Name
    nameCanonical   = Name
    x
        , nameBindingSite :: Range
    nameBindingSite = Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    x
        , nameFixity :: Fixity'
    nameFixity      = Fixity'
    fx
        , nameIsRecordName :: Bool
    nameIsRecordName = Bool
    False
        }

    -- | @freshAbstractName_ = freshAbstractName noFixity'@
    freshAbstractName_ :: C.Name -> ScopeM A.Name
    freshAbstractName_ :: Name -> ScopeM Name
    freshAbstractName_ = Fixity' -> Name -> ScopeM Name
    freshAbstractName Fixity'
    noFixity'

    -- | Create a fresh abstract qualified name.
    freshAbstractQName :: Fixity' -> C.Name -> ScopeM A.QName
    freshAbstractQName :: Fixity' -> Name -> ScopeM QName
    freshAbstractQName Fixity'
    fx Name
    x = do
      Name
    y <- Fixity' -> Name -> ScopeM Name
    freshAbstractName Fixity'
    fx Name
    x
      ModuleName
    m <- ScopeM ModuleName
    forall (m :: * -> *). ReadTCState m => m ModuleName
    getCurrentModule
      QName -> ScopeM QName
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName -> ScopeM QName) -> QName -> ScopeM QName
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> Name -> QName
    A.qualify ModuleName
    m Name
    y

    freshAbstractQName' :: C.Name -> ScopeM A.QName
    freshAbstractQName' :: Name -> ScopeM QName
    freshAbstractQName' Name
    x = do
      Fixity'
    fx <- Name -> ScopeM Fixity'
    getConcreteFixity Name
    x
      Fixity' -> Name -> ScopeM QName
    freshAbstractQName Fixity'
    fx Name
    x

    -- | Create a concrete name that is not yet in scope.
    -- | NOTE: See @chooseName@ in @Agda.Syntax.Translation.AbstractToConcrete@ for similar logic.
    -- | NOTE: See @withName@ in @Agda.Syntax.Translation.ReflectedToAbstract@ for similar logic.
    freshConcreteName :: Range -> Int -> String -> ScopeM C.Name
    freshConcreteName :: Range -> Int -> [Char] -> ScopeM Name
    freshConcreteName Range
    r Int
    i [Char]
    s = do
      let cname :: Name
    cname = Range -> NameInScope -> NameParts -> Name
    C.Name Range
    r NameInScope
    C.NotInScope (NameParts -> Name) -> NameParts -> Name
    forall a b. (a -> b) -> a -> b
    $ NamePart -> NameParts
    forall el coll. Singleton el coll => el -> coll
    singleton (NamePart -> NameParts) -> NamePart -> NameParts
    forall a b. (a -> b) -> a -> b
    $ [Char] -> NamePart
    Id ([Char] -> NamePart) -> [Char] -> NamePart
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Char]
    stringToRawName ([Char] -> [Char]) -> [Char] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char]
    s [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    i
      QName -> ScopeM ResolvedName
    resolveName (Name -> QName
    C.QName Name
    cname) ScopeM ResolvedName -> (ResolvedName -> ScopeM Name) -> ScopeM Name
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        ResolvedName
    UnknownName -> Name -> ScopeM Name
    forall (m :: * -> *) a. Monad m => a -> m a
    return Name
    cname
        ResolvedName
    _           -> Range -> Int -> [Char] -> ScopeM Name
    freshConcreteName Range
    r (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) [Char]
    s

    ---------------------------------------------------------------------------
    -- * Resolving names
    ---------------------------------------------------------------------------

    -- | Look up the abstract name referred to by a given concrete name.
    resolveName :: C.QName -> ScopeM ResolvedName
    resolveName :: QName -> ScopeM ResolvedName
    resolveName = KindsOfNames -> Maybe (Set Name) -> QName -> ScopeM ResolvedName
    resolveName' KindsOfNames
    allKindsOfNames Maybe (Set Name)
    forall a. Maybe a
    Nothing

    -- | Look up the abstract name corresponding to a concrete name of
    --   a certain kind and/or from a given set of names.
    --   Sometimes we know already that we are dealing with a constructor
    --   or pattern synonym (e.g. when we have parsed a pattern).
    --   Then, we can ignore conflicting definitions of that name
    --   of a different kind. (See issue 822.)
    resolveName' ::
      KindsOfNames -> Maybe (Set A.Name) -> C.QName -> ScopeM ResolvedName
    resolveName' :: KindsOfNames -> Maybe (Set Name) -> QName -> ScopeM ResolvedName
    resolveName' KindsOfNames
    kinds Maybe (Set Name)
    names QName
    x = ExceptT (List1 QName) (TCMT IO) ResolvedName
    -> TCMT IO (Either (List1 QName) ResolvedName)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (KindsOfNames
    -> Maybe (Set Name)
    -> QName
    -> ExceptT (List1 QName) (TCMT IO) ResolvedName
    forall (m :: * -> *).
    (ReadTCState m, HasBuiltins m, MonadError (List1 QName) m) =>
    KindsOfNames -> Maybe (Set Name) -> QName -> m ResolvedName
    tryResolveName KindsOfNames
    kinds Maybe (Set Name)
    names QName
    x) TCMT IO (Either (List1 QName) ResolvedName)
    -> (Either (List1 QName) ResolvedName -> ScopeM ResolvedName)
    -> ScopeM ResolvedName
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      Left List1 QName
    ys  -> Call -> ScopeM ResolvedName -> ScopeM ResolvedName
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall (Range -> Call
    SetRange (Range -> Call) -> Range -> Call
    forall a b. (a -> b) -> a -> b
    $ QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    x) (ScopeM ResolvedName -> ScopeM ResolvedName)
    -> ScopeM ResolvedName -> ScopeM ResolvedName
    forall a b. (a -> b) -> a -> b
    $ TypeError -> ScopeM ResolvedName
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> ScopeM ResolvedName)
    -> TypeError -> ScopeM ResolvedName
    forall a b. (a -> b) -> a -> b
    $ QName -> List1 QName -> TypeError
    AmbiguousName QName
    x List1 QName
    ys
      Right ResolvedName
    x' -> ResolvedName -> ScopeM ResolvedName
    forall (m :: * -> *) a. Monad m => a -> m a
    return ResolvedName
    x'

    tryResolveName
      :: (ReadTCState m, HasBuiltins m, MonadError (List1 A.QName) m)
      => KindsOfNames       -- ^ Restrict search to these kinds of names.
      -> Maybe (Set A.Name) -- ^ Unless 'Nothing', restrict search to match any of these names.
      -> C.QName            -- ^ Name to be resolved
      -> m ResolvedName     -- ^ If illegally ambiguous, throw error with the ambiguous name.
    tryResolveName :: forall (m :: * -> *).
    (ReadTCState m, HasBuiltins m, MonadError (List1 QName) m) =>
    KindsOfNames -> Maybe (Set Name) -> QName -> m ResolvedName
    tryResolveName KindsOfNames
    kinds Maybe (Set Name)
    names QName
    x = do
      ScopeInfo
    scope <- m ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope
      let vars :: AssocList QName LocalVar
    vars     = (Name -> QName) -> LocalVars -> AssocList QName LocalVar
    forall k k' v. (k -> k') -> AssocList k v -> AssocList k' v
    AssocList.mapKeysMonotonic Name -> QName
    C.QName (LocalVars -> AssocList QName LocalVar)
    -> LocalVars -> AssocList QName LocalVar
    forall a b. (a -> b) -> a -> b
    $ ScopeInfo
    scope ScopeInfo -> Lens' LocalVars ScopeInfo -> LocalVars
    forall o i. o -> Lens' i o -> i
    ^. Lens' LocalVars ScopeInfo
    scopeLocals
      case QName -> AssocList QName LocalVar -> Maybe LocalVar
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup QName
    x AssocList QName LocalVar
    vars of
        -- Case: we have a local variable x, but is (perhaps) shadowed by some imports ys.
        Just (LocalVar Name
    y BindingSource
    b [AbstractName]
    ys) ->
          -- We may ignore the imports filtered out by the @names@ filter.
          [AbstractName]
    -> m ResolvedName
    -> ([AbstractName] -> m ResolvedName)
    -> m ResolvedName
    forall a b. Null a => a -> b -> (a -> b) -> b
    ifNull ((AbstractName -> AbstractName) -> [AbstractName] -> [AbstractName]
    forall a. (a -> AbstractName) -> [a] -> [a]
    filterNames AbstractName -> AbstractName
    forall a. a -> a
    id [AbstractName]
    ys)
            {-then-} (ResolvedName -> m ResolvedName
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ResolvedName -> m ResolvedName) -> ResolvedName -> m ResolvedName
    forall a b. (a -> b) -> a -> b
    $ Name -> BindingSource -> ResolvedName
    VarName Name
    y{ nameConcrete :: Name
    nameConcrete = QName -> Name
    unqualify QName
    x } BindingSource
    b)
            {-else-} (([AbstractName] -> m ResolvedName) -> m ResolvedName)
    -> ([AbstractName] -> m ResolvedName) -> m ResolvedName
    forall a b. (a -> b) -> a -> b
    $ \ [AbstractName]
    ys' ->
              List1 QName -> m ResolvedName
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (List1 QName -> m ResolvedName) -> List1 QName -> m ResolvedName
    forall a b. (a -> b) -> a -> b
    $ Name -> QName
    A.qualify_ Name
    y QName -> [QName] -> List1 QName
    forall a. a -> [a] -> NonEmpty a
    :| (AbstractName -> QName) -> [AbstractName] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map AbstractName -> QName
    anameName [AbstractName]
    ys'
        -- Case: we do not have a local variable x.
        Maybe LocalVar
    Nothing -> do
          -- Consider only names that are in the given set of names and
          -- are of one of the given kinds
          let filtKind :: [(AbstractName, Access)] -> [(AbstractName, Access)]
    filtKind = ((AbstractName, Access) -> Bool)
    -> [(AbstractName, Access)] -> [(AbstractName, Access)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (((AbstractName, Access) -> Bool)
     -> [(AbstractName, Access)] -> [(AbstractName, Access)])
    -> ((AbstractName, Access) -> Bool)
    -> [(AbstractName, Access)]
    -> [(AbstractName, Access)]
    forall a b. (a -> b) -> a -> b
    $ (KindOfName -> KindsOfNames -> Bool
    `elemKindsOfNames` KindsOfNames
    kinds) (KindOfName -> Bool)
    -> ((AbstractName, Access) -> KindOfName)
    -> (AbstractName, Access)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbstractName -> KindOfName
    anameKind (AbstractName -> KindOfName)
    -> ((AbstractName, Access) -> AbstractName)
    -> (AbstractName, Access)
    -> KindOfName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (AbstractName, Access) -> AbstractName
    forall a b. (a, b) -> a
    fst
              possibleNames :: QName -> [(AbstractName, Access)]
    possibleNames QName
    z = [(AbstractName, Access)] -> [(AbstractName, Access)]
    filtKind ([(AbstractName, Access)] -> [(AbstractName, Access)])
    -> [(AbstractName, Access)] -> [(AbstractName, Access)]
    forall a b. (a -> b) -> a -> b
    $ ((AbstractName, Access) -> AbstractName)
    -> [(AbstractName, Access)] -> [(AbstractName, Access)]
    forall a. (a -> AbstractName) -> [a] -> [a]
    filterNames (AbstractName, Access) -> AbstractName
    forall a b. (a, b) -> a
    fst ([(AbstractName, Access)] -> [(AbstractName, Access)])
    -> [(AbstractName, Access)] -> [(AbstractName, Access)]
    forall a b. (a -> b) -> a -> b
    $ QName -> ScopeInfo -> [(AbstractName, Access)]
    forall a. InScope a => QName -> ScopeInfo -> [(a, Access)]
    scopeLookup' QName
    z ScopeInfo
    scope
          -- If the name has a suffix, also consider the possibility that
          -- the base name is in scope (e.g. the builtin sorts `Set` and `Prop`).
          QName -> Bool
    canHaveSuffix <- m (QName -> Bool)
    forall (m :: * -> *). HasBuiltins m => m (QName -> Bool)
    canHaveSuffixTest
          let (Maybe Suffix
    xsuffix, QName
    xbase) = ((Name -> (Maybe Suffix, Name)) -> QName -> (Maybe Suffix, QName)
    Lens' Name QName
    C.lensQNameName ((Name -> (Maybe Suffix, Name)) -> QName -> (Maybe Suffix, QName))
    -> ((Maybe Suffix -> (Maybe Suffix, Maybe Suffix))
        -> Name -> (Maybe Suffix, Name))
    -> (Maybe Suffix -> (Maybe Suffix, Maybe Suffix))
    -> QName
    -> (Maybe Suffix, QName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Maybe Suffix -> (Maybe Suffix, Maybe Suffix))
    -> Name -> (Maybe Suffix, Name)
    Lens' (Maybe Suffix) Name
    nameSuffix) (,Maybe Suffix
    forall a. Maybe a
    Nothing) QName
    x
              possibleBaseNames :: [(AbstractName, Access)]
    possibleBaseNames = ((AbstractName, Access) -> Bool)
    -> [(AbstractName, Access)] -> [(AbstractName, Access)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (QName -> Bool
    canHaveSuffix (QName -> Bool)
    -> ((AbstractName, Access) -> QName)
    -> (AbstractName, Access)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbstractName -> QName
    anameName (AbstractName -> QName)
    -> ((AbstractName, Access) -> AbstractName)
    -> (AbstractName, Access)
    -> QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (AbstractName, Access) -> AbstractName
    forall a b. (a, b) -> a
    fst) ([(AbstractName, Access)] -> [(AbstractName, Access)])
    -> [(AbstractName, Access)] -> [(AbstractName, Access)]
    forall a b. (a -> b) -> a -> b
    $ QName -> [(AbstractName, Access)]
    possibleNames QName
    xbase
              suffixedNames :: Maybe (Suffix, NonEmpty (AbstractName, Access))
    suffixedNames = (,) (Suffix
     -> NonEmpty (AbstractName, Access)
     -> (Suffix, NonEmpty (AbstractName, Access)))
    -> Maybe Suffix
    -> Maybe
         (NonEmpty (AbstractName, Access)
          -> (Suffix, NonEmpty (AbstractName, Access)))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe Suffix -> Maybe Suffix
    fromConcreteSuffix Maybe Suffix
    xsuffix Maybe
      (NonEmpty (AbstractName, Access)
       -> (Suffix, NonEmpty (AbstractName, Access)))
    -> Maybe (NonEmpty (AbstractName, Access))
    -> Maybe (Suffix, NonEmpty (AbstractName, Access))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [(AbstractName, Access)] -> Maybe (NonEmpty (AbstractName, Access))
    forall a. [a] -> Maybe (NonEmpty a)
    nonEmpty [(AbstractName, Access)]
    possibleBaseNames
          case ([(AbstractName, Access)] -> Maybe (NonEmpty (AbstractName, Access))
    forall a. [a] -> Maybe (NonEmpty a)
    nonEmpty ([(AbstractName, Access)]
     -> Maybe (NonEmpty (AbstractName, Access)))
    -> [(AbstractName, Access)]
    -> Maybe (NonEmpty (AbstractName, Access))
    forall a b. (a -> b) -> a -> b
    $ QName -> [(AbstractName, Access)]
    possibleNames QName
    x) of
            Just NonEmpty (AbstractName, Access)
    ds  | let ks :: NonEmpty (Maybe Induction)
    ks = ((AbstractName, Access) -> Maybe Induction)
    -> NonEmpty (AbstractName, Access) -> NonEmpty (Maybe Induction)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (KindOfName -> Maybe Induction
    isConName (KindOfName -> Maybe Induction)
    -> ((AbstractName, Access) -> KindOfName)
    -> (AbstractName, Access)
    -> Maybe Induction
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbstractName -> KindOfName
    anameKind (AbstractName -> KindOfName)
    -> ((AbstractName, Access) -> AbstractName)
    -> (AbstractName, Access)
    -> KindOfName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (AbstractName, Access) -> AbstractName
    forall a b. (a, b) -> a
    fst) NonEmpty (AbstractName, Access)
    ds
                     , (Maybe Induction -> Bool) -> NonEmpty (Maybe Induction) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Maybe Induction -> Bool
    forall a. Maybe a -> Bool
    isJust NonEmpty (Maybe Induction)
    ks
                     , Maybe (Suffix, NonEmpty (AbstractName, Access)) -> Bool
    forall a. Maybe a -> Bool
    isNothing Maybe (Suffix, NonEmpty (AbstractName, Access))
    suffixedNames ->
              ResolvedName -> m ResolvedName
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ResolvedName -> m ResolvedName) -> ResolvedName -> m ResolvedName
    forall a b. (a -> b) -> a -> b
    $ Set Induction -> List1 AbstractName -> ResolvedName
    ConstructorName ([Induction] -> Set Induction
    forall a. Ord a => [a] -> Set a
    Set.fromList ([Induction] -> Set Induction) -> [Induction] -> Set Induction
    forall a b. (a -> b) -> a -> b
    $ NonEmpty (Maybe Induction) -> [Induction]
    forall a. List1 (Maybe a) -> [a]
    List1.catMaybes NonEmpty (Maybe Induction)
    ks) (List1 AbstractName -> ResolvedName)
    -> List1 AbstractName -> ResolvedName
    forall a b. (a -> b) -> a -> b
    $ ((AbstractName, Access) -> AbstractName)
    -> NonEmpty (AbstractName, Access) -> List1 AbstractName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (AbstractName -> AbstractName
    upd (AbstractName -> AbstractName)
    -> ((AbstractName, Access) -> AbstractName)
    -> (AbstractName, Access)
    -> AbstractName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (AbstractName, Access) -> AbstractName
    forall a b. (a, b) -> a
    fst) NonEmpty (AbstractName, Access)
    ds

            Just NonEmpty (AbstractName, Access)
    ds  | ((AbstractName, Access) -> Bool)
    -> NonEmpty (AbstractName, Access) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all ((KindOfName
    FldName KindOfName -> KindOfName -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (KindOfName -> Bool)
    -> ((AbstractName, Access) -> KindOfName)
    -> (AbstractName, Access)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbstractName -> KindOfName
    anameKind (AbstractName -> KindOfName)
    -> ((AbstractName, Access) -> AbstractName)
    -> (AbstractName, Access)
    -> KindOfName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (AbstractName, Access) -> AbstractName
    forall a b. (a, b) -> a
    fst) NonEmpty (AbstractName, Access)
    ds , Maybe (Suffix, NonEmpty (AbstractName, Access)) -> Bool
    forall a. Maybe a -> Bool
    isNothing Maybe (Suffix, NonEmpty (AbstractName, Access))
    suffixedNames ->
              ResolvedName -> m ResolvedName
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ResolvedName -> m ResolvedName) -> ResolvedName -> m ResolvedName
    forall a b. (a -> b) -> a -> b
    $ List1 AbstractName -> ResolvedName
    FieldName (List1 AbstractName -> ResolvedName)
    -> List1 AbstractName -> ResolvedName
    forall a b. (a -> b) -> a -> b
    $ ((AbstractName, Access) -> AbstractName)
    -> NonEmpty (AbstractName, Access) -> List1 AbstractName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (AbstractName -> AbstractName
    upd (AbstractName -> AbstractName)
    -> ((AbstractName, Access) -> AbstractName)
    -> (AbstractName, Access)
    -> AbstractName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (AbstractName, Access) -> AbstractName
    forall a b. (a, b) -> a
    fst) NonEmpty (AbstractName, Access)
    ds

            Just NonEmpty (AbstractName, Access)
    ds  | ((AbstractName, Access) -> Bool)
    -> NonEmpty (AbstractName, Access) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all ((KindOfName
    PatternSynName KindOfName -> KindOfName -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (KindOfName -> Bool)
    -> ((AbstractName, Access) -> KindOfName)
    -> (AbstractName, Access)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbstractName -> KindOfName
    anameKind (AbstractName -> KindOfName)
    -> ((AbstractName, Access) -> AbstractName)
    -> (AbstractName, Access)
    -> KindOfName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (AbstractName, Access) -> AbstractName
    forall a b. (a, b) -> a
    fst) NonEmpty (AbstractName, Access)
    ds , Maybe (Suffix, NonEmpty (AbstractName, Access)) -> Bool
    forall a. Maybe a -> Bool
    isNothing Maybe (Suffix, NonEmpty (AbstractName, Access))
    suffixedNames ->
              ResolvedName -> m ResolvedName
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ResolvedName -> m ResolvedName) -> ResolvedName -> m ResolvedName
    forall a b. (a -> b) -> a -> b
    $ List1 AbstractName -> ResolvedName
    PatternSynResName (List1 AbstractName -> ResolvedName)
    -> List1 AbstractName -> ResolvedName
    forall a b. (a -> b) -> a -> b
    $ ((AbstractName, Access) -> AbstractName)
    -> NonEmpty (AbstractName, Access) -> List1 AbstractName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (AbstractName -> AbstractName
    upd (AbstractName -> AbstractName)
    -> ((AbstractName, Access) -> AbstractName)
    -> (AbstractName, Access)
    -> AbstractName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (AbstractName, Access) -> AbstractName
    forall a b. (a, b) -> a
    fst) NonEmpty (AbstractName, Access)
    ds

            Just ((AbstractName
    d, Access
    a) :| []) | Maybe (Suffix, NonEmpty (AbstractName, Access)) -> Bool
    forall a. Maybe a -> Bool
    isNothing Maybe (Suffix, NonEmpty (AbstractName, Access))
    suffixedNames ->
              ResolvedName -> m ResolvedName
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ResolvedName -> m ResolvedName) -> ResolvedName -> m ResolvedName
    forall a b. (a -> b) -> a -> b
    $ Access -> AbstractName -> Suffix -> ResolvedName
    DefinedName Access
    a (AbstractName -> AbstractName
    upd AbstractName
    d) Suffix
    A.NoSuffix

            Just NonEmpty (AbstractName, Access)
    ds -> List1 QName -> m ResolvedName
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (List1 QName -> m ResolvedName) -> List1 QName -> m ResolvedName
    forall a b. (a -> b) -> a -> b
    $ ((AbstractName, Access) -> QName)
    -> NonEmpty (AbstractName, Access) -> List1 QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (AbstractName -> QName
    anameName (AbstractName -> QName)
    -> ((AbstractName, Access) -> AbstractName)
    -> (AbstractName, Access)
    -> QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (AbstractName, Access) -> AbstractName
    forall a b. (a, b) -> a
    fst) (NonEmpty (AbstractName, Access) -> List1 QName)
    -> NonEmpty (AbstractName, Access) -> List1 QName
    forall a b. (a -> b) -> a -> b
    $ Maybe (Suffix, NonEmpty (AbstractName, Access))
    -> (NonEmpty (AbstractName, Access)
        -> NonEmpty (AbstractName, Access))
    -> ((Suffix, NonEmpty (AbstractName, Access))
        -> NonEmpty (AbstractName, Access)
        -> NonEmpty (AbstractName, Access))
    -> NonEmpty (AbstractName, Access)
    -> NonEmpty (AbstractName, Access)
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe (Suffix, NonEmpty (AbstractName, Access))
    suffixedNames NonEmpty (AbstractName, Access) -> NonEmpty (AbstractName, Access)
    forall a. a -> a
    id (NonEmpty (AbstractName, Access)
    -> NonEmpty (AbstractName, Access)
    -> NonEmpty (AbstractName, Access)
    forall a. Semigroup a => a -> a -> a
    (<>) (NonEmpty (AbstractName, Access)
     -> NonEmpty (AbstractName, Access)
     -> NonEmpty (AbstractName, Access))
    -> ((Suffix, NonEmpty (AbstractName, Access))
        -> NonEmpty (AbstractName, Access))
    -> (Suffix, NonEmpty (AbstractName, Access))
    -> NonEmpty (AbstractName, Access)
    -> NonEmpty (AbstractName, Access)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Suffix, NonEmpty (AbstractName, Access))
    -> NonEmpty (AbstractName, Access)
    forall a b. (a, b) -> b
    snd) NonEmpty (AbstractName, Access)
    ds

            Maybe (NonEmpty (AbstractName, Access))
    Nothing -> case Maybe (Suffix, NonEmpty (AbstractName, Access))
    suffixedNames of
              Maybe (Suffix, NonEmpty (AbstractName, Access))
    Nothing -> ResolvedName -> m ResolvedName
    forall (m :: * -> *) a. Monad m => a -> m a
    return ResolvedName
    UnknownName
              Just (Suffix
    suffix , (AbstractName
    d, Access
    a) :| []) -> ResolvedName -> m ResolvedName
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ResolvedName -> m ResolvedName) -> ResolvedName -> m ResolvedName
    forall a b. (a -> b) -> a -> b
    $ Access -> AbstractName -> Suffix -> ResolvedName
    DefinedName Access
    a (AbstractName -> AbstractName
    upd AbstractName
    d) Suffix
    suffix
              Just (Suffix
    suffix , NonEmpty (AbstractName, Access)
    sds) -> List1 QName -> m ResolvedName
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (List1 QName -> m ResolvedName) -> List1 QName -> m ResolvedName
    forall a b. (a -> b) -> a -> b
    $ ((AbstractName, Access) -> QName)
    -> NonEmpty (AbstractName, Access) -> List1 QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (AbstractName -> QName
    anameName (AbstractName -> QName)
    -> ((AbstractName, Access) -> AbstractName)
    -> (AbstractName, Access)
    -> QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (AbstractName, Access) -> AbstractName
    forall a b. (a, b) -> a
    fst) NonEmpty (AbstractName, Access)
    sds

      where
      -- @names@ intended semantics: a filter on names.
      -- @Nothing@: don't filter out anything.
      -- @Just ns@: filter by membership in @ns@.
      filterNames :: forall a. (a -> AbstractName) -> [a] -> [a]
      filterNames :: forall a. (a -> AbstractName) -> [a] -> [a]
    filterNames = case Maybe (Set Name)
    names of
        Maybe (Set Name)
    Nothing -> \ a -> AbstractName
    f -> [a] -> [a]
    forall a. a -> a
    id
        Just Set Name
    ns -> \ a -> AbstractName
    f -> (a -> Bool) -> [a] -> [a]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((a -> Bool) -> [a] -> [a]) -> (a -> Bool) -> [a] -> [a]
    forall a b. (a -> b) -> a -> b
    $ (Name -> Set Name -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Name
    ns) (Name -> Bool) -> (a -> Name) -> a -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Name
    A.qnameName (QName -> Name) -> (a -> QName) -> a -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbstractName -> QName
    anameName (AbstractName -> QName) -> (a -> AbstractName) -> a -> QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> AbstractName
    f
        -- lambda-dropped style by intention
      upd :: AbstractName -> AbstractName
    upd AbstractName
    d = AbstractName -> Name -> AbstractName
    updateConcreteName AbstractName
    d (Name -> AbstractName) -> Name -> AbstractName
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    unqualify QName
    x
      updateConcreteName :: AbstractName -> C.Name -> AbstractName
      updateConcreteName :: AbstractName -> Name -> AbstractName
    updateConcreteName d :: AbstractName
    d@(AbsName { anameName :: AbstractName -> QName
    anameName = A.QName ModuleName
    qm Name
    qn }) Name
    x =
        AbstractName
    d { anameName :: QName
    anameName = ModuleName -> Name -> QName
    A.QName (Range -> ModuleName -> ModuleName
    forall a. SetRange a => Range -> a -> a
    setRange (Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    x) ModuleName
    qm) (Name
    qn { nameConcrete :: Name
    nameConcrete = Name
    x }) }
      fromConcreteSuffix :: Maybe Suffix -> Maybe Suffix
    fromConcreteSuffix = \case
        Maybe Suffix
    Nothing              -> Maybe Suffix
    forall a. Maybe a
    Nothing
        Just C.Prime{}       -> Maybe Suffix
    forall a. Maybe a
    Nothing
        Just (C.Index Integer
    i)     -> Suffix -> Maybe Suffix
    forall a. a -> Maybe a
    Just (Suffix -> Maybe Suffix) -> Suffix -> Maybe Suffix
    forall a b. (a -> b) -> a -> b
    $ Integer -> Suffix
    A.Suffix Integer
    i
        Just (C.Subscript Integer
    i) -> Suffix -> Maybe Suffix
    forall a. a -> Maybe a
    Just (Suffix -> Maybe Suffix) -> Suffix -> Maybe Suffix
    forall a b. (a -> b) -> a -> b
    $ Integer -> Suffix
    A.Suffix Integer
    i

    -- | Test if a given abstract name can appear with a suffix. Currently
    --   only true for the names of builtin sorts @Set@ and @Prop@.
    canHaveSuffixTest :: HasBuiltins m => m (A.QName -> Bool)
    canHaveSuffixTest :: forall (m :: * -> *). HasBuiltins m => m (QName -> Bool)
    canHaveSuffixTest = do
      Maybe QName
    builtinSet  <- [Char] -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
    getBuiltinName' [Char]
    builtinSet
      Maybe QName
    builtinProp <- [Char] -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
    getBuiltinName' [Char]
    builtinProp
      Maybe QName
    builtinSetOmega <- [Char] -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
    getBuiltinName' [Char]
    builtinSetOmega
      Maybe QName
    builtinSSetOmega <- [Char] -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
    getBuiltinName' [Char]
    builtinSSetOmega
      (QName -> Bool) -> m (QName -> Bool)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((QName -> Bool) -> m (QName -> Bool))
    -> (QName -> Bool) -> m (QName -> Bool)
    forall a b. (a -> b) -> a -> b
    $ \QName
    x -> QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    x Maybe QName -> [Maybe QName] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Maybe QName
    builtinSet, Maybe QName
    builtinProp, Maybe QName
    builtinSetOmega, Maybe QName
    builtinSSetOmega]

    -- | Look up a module in the scope.
    resolveModule :: C.QName -> ScopeM AbstractModule
    resolveModule :: QName -> ScopeM AbstractModule
    resolveModule QName
    x = do
      [AbstractModule]
    ms <- QName -> ScopeInfo -> [AbstractModule]
    forall a. InScope a => QName -> ScopeInfo -> [a]
    scopeLookup QName
    x (ScopeInfo -> [AbstractModule])
    -> TCMT IO ScopeInfo -> TCMT IO [AbstractModule]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope
      Maybe (NonEmpty AbstractModule)
    -> ScopeM AbstractModule
    -> (NonEmpty AbstractModule -> ScopeM AbstractModule)
    -> ScopeM AbstractModule
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe ([AbstractModule] -> Maybe (NonEmpty AbstractModule)
    forall a. [a] -> Maybe (NonEmpty a)
    nonEmpty [AbstractModule]
    ms) (TypeError -> ScopeM AbstractModule
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> ScopeM AbstractModule)
    -> TypeError -> ScopeM AbstractModule
    forall a b. (a -> b) -> a -> b
    $ QName -> TypeError
    NoSuchModule QName
    x) ((NonEmpty AbstractModule -> ScopeM AbstractModule)
     -> ScopeM AbstractModule)
    -> (NonEmpty AbstractModule -> ScopeM AbstractModule)
    -> ScopeM AbstractModule
    forall a b. (a -> b) -> a -> b
    $ \ case
        AbsModule ModuleName
    m WhyInScope
    why :| [] -> AbstractModule -> ScopeM AbstractModule
    forall (m :: * -> *) a. Monad m => a -> m a
    return (AbstractModule -> ScopeM AbstractModule)
    -> AbstractModule -> ScopeM AbstractModule
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> WhyInScope -> AbstractModule
    AbsModule (ModuleName
    m ModuleName -> QName -> ModuleName
    forall t u. (SetRange t, HasRange u) => t -> u -> t
    `withRangeOf` QName
    x) WhyInScope
    why
        NonEmpty AbstractModule
    ms                    -> TypeError -> ScopeM AbstractModule
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> ScopeM AbstractModule)
    -> TypeError -> ScopeM AbstractModule
    forall a b. (a -> b) -> a -> b
    $ QName -> List1 ModuleName -> TypeError
    AmbiguousModule QName
    x ((AbstractModule -> ModuleName)
    -> NonEmpty AbstractModule -> List1 ModuleName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap AbstractModule -> ModuleName
    amodName NonEmpty AbstractModule
    ms)

    -- | Get the fixity of a not yet bound name.
    getConcreteFixity :: C.Name -> ScopeM Fixity'
    getConcreteFixity :: Name -> ScopeM Fixity'
    getConcreteFixity Name
    x = Fixity' -> Name -> Map Name Fixity' -> Fixity'
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault Fixity'
    noFixity' Name
    x (Map Name Fixity' -> Fixity')
    -> TCMT IO (Map Name Fixity') -> ScopeM Fixity'
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' (Map Name Fixity') ScopeInfo -> TCMT IO (Map Name Fixity')
    forall (m :: * -> *) a. ReadTCState m => Lens' a ScopeInfo -> m a
    useScope Lens' (Map Name Fixity') ScopeInfo
    scopeFixities

    -- | Get the polarities of a not yet bound name.
    getConcretePolarity :: C.Name -> ScopeM (Maybe [Occurrence])
    getConcretePolarity :: Name -> ScopeM (Maybe [Occurrence])
    getConcretePolarity Name
    x = Name -> Map Name [Occurrence] -> Maybe [Occurrence]
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x (Map Name [Occurrence] -> Maybe [Occurrence])
    -> TCMT IO (Map Name [Occurrence]) -> ScopeM (Maybe [Occurrence])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' (Map Name [Occurrence]) ScopeInfo
    -> TCMT IO (Map Name [Occurrence])
    forall (m :: * -> *) a. ReadTCState m => Lens' a ScopeInfo -> m a
    useScope Lens' (Map Name [Occurrence]) ScopeInfo
    scopePolarities

    instance MonadFixityError ScopeM where
      throwMultipleFixityDecls :: forall a. [(Name, [Fixity'])] -> ScopeM a
    throwMultipleFixityDecls [(Name, [Fixity'])]
    xs         = case [(Name, [Fixity'])]
    xs of
        (Name
    x, [Fixity']
    _) : [(Name, [Fixity'])]
    _ -> Range -> ScopeM a -> ScopeM a
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange (Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    x) (ScopeM a -> ScopeM a) -> ScopeM a -> ScopeM a
    forall a b. (a -> b) -> a -> b
    $ TypeError -> ScopeM a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> ScopeM a) -> TypeError -> ScopeM a
    forall a b. (a -> b) -> a -> b
    $ [(Name, [Fixity'])] -> TypeError
    MultipleFixityDecls [(Name, [Fixity'])]
    xs
        []         -> ScopeM a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      throwMultiplePolarityPragmas :: forall a. [Name] -> ScopeM a
    throwMultiplePolarityPragmas [Name]
    xs     = case [Name]
    xs of
        Name
    x : [Name]
    _ -> Range -> ScopeM a -> ScopeM a
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange (Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    x) (ScopeM a -> ScopeM a) -> ScopeM a -> ScopeM a
    forall a b. (a -> b) -> a -> b
    $ TypeError -> ScopeM a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> ScopeM a) -> TypeError -> ScopeM a
    forall a b. (a -> b) -> a -> b
    $ [Name] -> TypeError
    MultiplePolarityPragmas [Name]
    xs
        []    -> ScopeM a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      warnUnknownNamesInFixityDecl :: HasCallStack => [Name] -> TCMT IO ()
    warnUnknownNamesInFixityDecl        = HasCallStack => DeclarationWarning' -> TCMT IO ()
    DeclarationWarning' -> TCMT IO ()
    scopeWarning (DeclarationWarning' -> TCMT IO ())
    -> ([Name] -> DeclarationWarning') -> [Name] -> TCMT IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Name] -> DeclarationWarning'
    UnknownNamesInFixityDecl
      warnUnknownNamesInPolarityPragmas :: HasCallStack => [Name] -> TCMT IO ()
    warnUnknownNamesInPolarityPragmas   = HasCallStack => DeclarationWarning' -> TCMT IO ()
    DeclarationWarning' -> TCMT IO ()
    scopeWarning (DeclarationWarning' -> TCMT IO ())
    -> ([Name] -> DeclarationWarning') -> [Name] -> TCMT IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Name] -> DeclarationWarning'
    UnknownNamesInPolarityPragmas
      warnUnknownFixityInMixfixDecl :: HasCallStack => [Name] -> TCMT IO ()
    warnUnknownFixityInMixfixDecl       = HasCallStack => DeclarationWarning' -> TCMT IO ()
    DeclarationWarning' -> TCMT IO ()
    scopeWarning (DeclarationWarning' -> TCMT IO ())
    -> ([Name] -> DeclarationWarning') -> [Name] -> TCMT IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Name] -> DeclarationWarning'
    UnknownFixityInMixfixDecl
      warnPolarityPragmasButNotPostulates :: HasCallStack => [Name] -> TCMT IO ()
    warnPolarityPragmasButNotPostulates = HasCallStack => DeclarationWarning' -> TCMT IO ()
    DeclarationWarning' -> TCMT IO ()
    scopeWarning (DeclarationWarning' -> TCMT IO ())
    -> ([Name] -> DeclarationWarning') -> [Name] -> TCMT IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Name] -> DeclarationWarning'
    PolarityPragmasButNotPostulates

    -- | Collect the fixity/syntax declarations and polarity pragmas from the list
    --   of declarations and store them in the scope.
    computeFixitiesAndPolarities :: DoWarn -> [C.Declaration] -> ScopeM a -> ScopeM a
    computeFixitiesAndPolarities :: forall a. DoWarn -> [Declaration] -> ScopeM a -> ScopeM a
    computeFixitiesAndPolarities DoWarn
    warn [Declaration]
    ds ScopeM a
    cont = do
      (Map Name Fixity', Map Name [Occurrence])
    fp <- DoWarn
    -> [Declaration]
    -> TCMT IO (Map Name Fixity', Map Name [Occurrence])
    forall (m :: * -> *).
    MonadFixityError m =>
    DoWarn
    -> [Declaration] -> m (Map Name Fixity', Map Name [Occurrence])
    fixitiesAndPolarities DoWarn
    warn [Declaration]
    ds
      -- Andreas, 2019-08-16:
      -- Since changing fixities and polarities does not affect the name sets,
      -- we do not need to invoke @modifyScope@ here
      -- (which does @recomputeInverseScopeMaps@).
      -- A simple @locallyScope@ is sufficient.
      Lens' (Map Name Fixity', Map Name [Occurrence]) ScopeInfo
    -> ((Map Name Fixity', Map Name [Occurrence])
        -> (Map Name Fixity', Map Name [Occurrence]))
    -> ScopeM a
    -> ScopeM a
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' a ScopeInfo -> (a -> a) -> m b -> m b
    locallyScope Lens' (Map Name Fixity', Map Name [Occurrence]) ScopeInfo
    scopeFixitiesAndPolarities ((Map Name Fixity', Map Name [Occurrence])
    -> (Map Name Fixity', Map Name [Occurrence])
    -> (Map Name Fixity', Map Name [Occurrence])
    forall a b. a -> b -> a
    const (Map Name Fixity', Map Name [Occurrence])
    fp) ScopeM a
    cont

    -- | Get the notation of a name. The name is assumed to be in scope.
    getNotation
      :: C.QName
      -> Set A.Name
         -- ^ The name must correspond to one of the names in this set.
      -> ScopeM NewNotation
    getNotation :: QName -> Set Name -> ScopeM NewNotation
    getNotation QName
    x Set Name
    ns = do
      ResolvedName
    r <- KindsOfNames -> Maybe (Set Name) -> QName -> ScopeM ResolvedName
    resolveName' KindsOfNames
    allKindsOfNames (Set Name -> Maybe (Set Name)
    forall a. a -> Maybe a
    Just Set Name
    ns) QName
    x
      case ResolvedName
    r of
        VarName Name
    y BindingSource
    _         -> NewNotation -> ScopeM NewNotation
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NewNotation -> ScopeM NewNotation)
    -> NewNotation -> ScopeM NewNotation
    forall a b. (a -> b) -> a -> b
    $ QName -> Name -> NewNotation
    namesToNotation QName
    x Name
    y
        DefinedName Access
    _ AbstractName
    d Suffix
    _   -> NewNotation -> ScopeM NewNotation
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NewNotation -> ScopeM NewNotation)
    -> NewNotation -> ScopeM NewNotation
    forall a b. (a -> b) -> a -> b
    $ AbstractName -> NewNotation
    notation AbstractName
    d
        FieldName List1 AbstractName
    ds        -> NewNotation -> ScopeM NewNotation
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NewNotation -> ScopeM NewNotation)
    -> NewNotation -> ScopeM NewNotation
    forall a b. (a -> b) -> a -> b
    $ List1 AbstractName -> NewNotation
    oneNotation List1 AbstractName
    ds
        ConstructorName Set Induction
    _ List1 AbstractName
    ds-> NewNotation -> ScopeM NewNotation
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NewNotation -> ScopeM NewNotation)
    -> NewNotation -> ScopeM NewNotation
    forall a b. (a -> b) -> a -> b
    $ List1 AbstractName -> NewNotation
    oneNotation List1 AbstractName
    ds
        PatternSynResName List1 AbstractName
    n -> NewNotation -> ScopeM NewNotation
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NewNotation -> ScopeM NewNotation)
    -> NewNotation -> ScopeM NewNotation
    forall a b. (a -> b) -> a -> b
    $ List1 AbstractName -> NewNotation
    oneNotation List1 AbstractName
    n
        ResolvedName
    UnknownName         -> ScopeM NewNotation
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      where
        notation :: AbstractName -> NewNotation
    notation = QName -> Name -> NewNotation
    namesToNotation QName
    x (Name -> NewNotation)
    -> (AbstractName -> Name) -> AbstractName -> NewNotation
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Name
    qnameName (QName -> Name) -> (AbstractName -> QName) -> AbstractName -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbstractName -> QName
    anameName
        oneNotation :: List1 AbstractName -> NewNotation
    oneNotation List1 AbstractName
    ds =
          case [NewNotation] -> [NewNotation]
    mergeNotations ([NewNotation] -> [NewNotation]) -> [NewNotation] -> [NewNotation]
    forall a b. (a -> b) -> a -> b
    $ (AbstractName -> NewNotation) -> [AbstractName] -> [NewNotation]
    forall a b. (a -> b) -> [a] -> [b]
    map AbstractName -> NewNotation
    notation ([AbstractName] -> [NewNotation])
    -> [AbstractName] -> [NewNotation]
    forall a b. (a -> b) -> a -> b
    $ List1 AbstractName -> [AbstractName]
    forall a. NonEmpty a -> [a]
    List1.toList List1 AbstractName
    ds of
            [NewNotation
    n] -> NewNotation
    n
            [NewNotation]
    _   -> NewNotation
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    ---------------------------------------------------------------------------
    -- * Binding names
    ---------------------------------------------------------------------------

    -- | Bind a variable.
    bindVariable
      :: A.BindingSource -- ^ @λ@, @Π@, @let@, ...?
      -> C.Name          -- ^ Concrete name.
      -> A.Name          -- ^ Abstract name.
      -> ScopeM ()
    bindVariable :: BindingSource -> Name -> Name -> TCMT IO ()
    bindVariable BindingSource
    b Name
    x Name
    y = (LocalVars -> LocalVars) -> TCMT IO ()
    modifyLocalVars ((LocalVars -> LocalVars) -> TCMT IO ())
    -> (LocalVars -> LocalVars) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Name -> LocalVar -> LocalVars -> LocalVars
    forall k v. k -> v -> AssocList k v -> AssocList k v
    AssocList.insert Name
    x (LocalVar -> LocalVars -> LocalVars)
    -> LocalVar -> LocalVars -> LocalVars
    forall a b. (a -> b) -> a -> b
    $ Name -> BindingSource -> [AbstractName] -> LocalVar
    LocalVar Name
    y BindingSource
    b []

    -- | Temporarily unbind a variable. Used for non-recursive lets.
    unbindVariable :: C.Name -> ScopeM a -> ScopeM a
    unbindVariable :: forall a. Name -> ScopeM a -> ScopeM a
    unbindVariable Name
    x = TCMT IO LocalVars
    -> (LocalVars -> TCMT IO ()) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a b.
    Monad m =>
    m a -> (a -> m ()) -> m b -> m b
    bracket_ (TCMT IO LocalVars
    forall (m :: * -> *). ReadTCState m => m LocalVars
    getLocalVars TCMT IO LocalVars -> TCMT IO () -> TCMT IO LocalVars
    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
    <* (LocalVars -> LocalVars) -> TCMT IO ()
    modifyLocalVars (Name -> LocalVars -> LocalVars
    forall k v. Eq k => k -> AssocList k v -> AssocList k v
    AssocList.delete Name
    x)) ((LocalVars -> LocalVars) -> TCMT IO ()
    modifyLocalVars ((LocalVars -> LocalVars) -> TCMT IO ())
    -> (LocalVars -> LocalVars -> LocalVars) -> LocalVars -> TCMT IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LocalVars -> LocalVars -> LocalVars
    forall a b. a -> b -> a
    const)

    -- | Bind a defined name. Must not shadow anything.
    bindName :: Access -> KindOfName -> C.Name -> A.QName -> ScopeM ()
    bindName :: Access -> KindOfName -> Name -> QName -> TCMT IO ()
    bindName Access
    acc KindOfName
    kind Name
    x QName
    y = Access -> KindOfName -> NameMetadata -> Name -> QName -> TCMT IO ()
    bindName' Access
    acc KindOfName
    kind NameMetadata
    NoMetadata Name
    x QName
    y

    bindName' :: Access -> KindOfName -> NameMetadata -> C.Name -> A.QName -> ScopeM ()
    bindName' :: Access -> KindOfName -> NameMetadata -> Name -> QName -> TCMT IO ()
    bindName' Access
    acc KindOfName
    kind NameMetadata
    meta Name
    x QName
    y = TCMT IO (Maybe TypeError)
    -> (TypeError -> TCMT IO ()) -> TCMT IO ()
    forall (m :: * -> *) a.
    Monad m =>
    m (Maybe a) -> (a -> m ()) -> m ()
    whenJustM (Access
    -> KindOfName
    -> NameMetadata
    -> Name
    -> QName
    -> TCMT IO (Maybe TypeError)
    bindName'' Access
    acc KindOfName
    kind NameMetadata
    meta Name
    x QName
    y) TypeError -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError

    -- | Bind a name. Returns the 'TypeError' if exists, but does not throw it.
    bindName'' :: Access -> KindOfName -> NameMetadata -> C.Name -> A.QName -> ScopeM (Maybe TypeError)
    bindName'' :: Access
    -> KindOfName
    -> NameMetadata
    -> Name
    -> QName
    -> TCMT IO (Maybe TypeError)
    bindName'' Access
    acc KindOfName
    kind NameMetadata
    meta Name
    x QName
    y = do
      Bool -> TCMT IO () -> TCMT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Name -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName Name
    x) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ (Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ()
    modifyScopes ((Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ())
    -> (Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ (Scope -> Scope) -> Map ModuleName Scope -> Map ModuleName Scope
    forall a b k. (a -> b) -> Map k a -> Map k b
    Map.map ((Scope -> Scope) -> Map ModuleName Scope -> Map ModuleName Scope)
    -> (Scope -> Scope) -> Map ModuleName Scope -> Map ModuleName Scope
    forall a b. (a -> b) -> a -> b
    $ NameSpaceId -> Name -> Scope -> Scope
    removeNameFromScope NameSpaceId
    PrivateNS Name
    x
      ResolvedName
    r  <- QName -> ScopeM ResolvedName
    resolveName (Name -> QName
    C.QName Name
    x)
      let y' :: Either TypeError AbstractName
          y' :: Either TypeError AbstractName
    y' = case ResolvedName
    r of
            -- Binding an anonymous declaration always succeeds.
            -- In case it's not the first one, we simply remove the one that came before
            ResolvedName
    _ | Name -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName Name
    x      -> Either TypeError AbstractName
    success
            DefinedName Access
    _ AbstractName
    d Suffix
    _   -> QName -> Either TypeError AbstractName
    clash (QName -> Either TypeError AbstractName)
    -> QName -> Either TypeError AbstractName
    forall a b. (a -> b) -> a -> b
    $ AbstractName -> QName
    anameName AbstractName
    d
            VarName Name
    z BindingSource
    _         -> QName -> Either TypeError AbstractName
    clash (QName -> Either TypeError AbstractName)
    -> QName -> Either TypeError AbstractName
    forall a b. (a -> b) -> a -> b
    $ Name -> QName
    A.qualify_ Name
    z
            FieldName       List1 AbstractName
    ds  -> (KindOfName -> Bool)
    -> List1 AbstractName -> Either TypeError AbstractName
    ambiguous (KindOfName -> KindOfName -> Bool
    forall a. Eq a => a -> a -> Bool
    == KindOfName
    FldName) List1 AbstractName
    ds
            ConstructorName Set Induction
    i List1 AbstractName
    ds-> (KindOfName -> Bool)
    -> List1 AbstractName -> Either TypeError AbstractName
    ambiguous (Maybe Induction -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe Induction -> Bool)
    -> (KindOfName -> Maybe Induction) -> KindOfName -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . KindOfName -> Maybe Induction
    isConName) List1 AbstractName
    ds
            PatternSynResName List1 AbstractName
    n -> (KindOfName -> Bool)
    -> List1 AbstractName -> Either TypeError AbstractName
    ambiguous (KindOfName -> KindOfName -> Bool
    forall a. Eq a => a -> a -> Bool
    == KindOfName
    PatternSynName) List1 AbstractName
    n
            ResolvedName
    UnknownName         -> Either TypeError AbstractName
    success
      let ns :: NameSpaceId
    ns = if Name -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName Name
    x then NameSpaceId
    PrivateNS else Access -> NameSpaceId
    localNameSpace Access
    acc
      (AbstractName -> TCMT IO ())
    -> Either TypeError AbstractName -> TCMT IO ()
    forall (t :: * -> *) (f :: * -> *) a b.
    (Foldable t, Applicative f) =>
    (a -> f b) -> t a -> f ()
    traverse_ ((Scope -> Scope) -> TCMT IO ()
    modifyCurrentScope ((Scope -> Scope) -> TCMT IO ())
    -> (AbstractName -> Scope -> Scope) -> AbstractName -> TCMT IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NameSpaceId -> Name -> AbstractName -> Scope -> Scope
    addNameToScope NameSpaceId
    ns Name
    x) Either TypeError AbstractName
    y'
      Maybe TypeError -> TCMT IO (Maybe TypeError)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Maybe TypeError -> TCMT IO (Maybe TypeError))
    -> Maybe TypeError -> TCMT IO (Maybe TypeError)
    forall a b. (a -> b) -> a -> b
    $ (TypeError -> Maybe TypeError)
    -> (AbstractName -> Maybe TypeError)
    -> Either TypeError AbstractName
    -> Maybe TypeError
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either TypeError -> Maybe TypeError
    forall a. a -> Maybe a
    Just (Maybe TypeError -> AbstractName -> Maybe TypeError
    forall a b. a -> b -> a
    const Maybe TypeError
    forall a. Maybe a
    Nothing) Either TypeError AbstractName
    y'
      where
        success :: Either TypeError AbstractName
    success = AbstractName -> Either TypeError AbstractName
    forall a b. b -> Either a b
    Right (AbstractName -> Either TypeError AbstractName)
    -> AbstractName -> Either TypeError AbstractName
    forall a b. (a -> b) -> a -> b
    $ QName -> KindOfName -> WhyInScope -> NameMetadata -> AbstractName
    AbsName QName
    y KindOfName
    kind WhyInScope
    Defined NameMetadata
    meta
        clash :: QName -> Either TypeError AbstractName
    clash QName
    n = TypeError -> Either TypeError AbstractName
    forall a b. a -> Either a b
    Left (TypeError -> Either TypeError AbstractName)
    -> TypeError -> Either TypeError AbstractName
    forall a b. (a -> b) -> a -> b
    $ QName -> QName -> Maybe NiceDeclaration -> TypeError
    ClashingDefinition (Name -> QName
    C.QName Name
    x) QName
    n Maybe NiceDeclaration
    forall a. Maybe a
    Nothing

        ambiguous :: (KindOfName -> Bool)
    -> List1 AbstractName -> Either TypeError AbstractName
    ambiguous KindOfName -> Bool
    f List1 AbstractName
    ds =
          if KindOfName -> Bool
    f KindOfName
    kind Bool -> Bool -> Bool
    && (AbstractName -> Bool) -> List1 AbstractName -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (KindOfName -> Bool
    f (KindOfName -> Bool)
    -> (AbstractName -> KindOfName) -> AbstractName -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbstractName -> KindOfName
    anameKind) List1 AbstractName
    ds
          then Either TypeError AbstractName
    success else QName -> Either TypeError AbstractName
    clash (QName -> Either TypeError AbstractName)
    -> QName -> Either TypeError AbstractName
    forall a b. (a -> b) -> a -> b
    $ AbstractName -> QName
    anameName (List1 AbstractName -> AbstractName
    forall a. NonEmpty a -> a
    List1.head List1 AbstractName
    ds)

    -- | Rebind a name. Use with care!
    --   Ulf, 2014-06-29: Currently used to rebind the name defined by an
    --   unquoteDecl, which is a 'QuotableName' in the body, but a 'DefinedName'
    --   later on.
    rebindName :: Access -> KindOfName -> C.Name -> A.QName -> ScopeM ()
    rebindName :: Access -> KindOfName -> Name -> QName -> TCMT IO ()
    rebindName Access
    acc KindOfName
    kind Name
    x QName
    y = do
      (Scope -> Scope) -> TCMT IO ()
    modifyCurrentScope ((Scope -> Scope) -> TCMT IO ()) -> (Scope -> Scope) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ NameSpaceId -> Name -> Scope -> Scope
    removeNameFromScope (Access -> NameSpaceId
    localNameSpace Access
    acc) Name
    x
      Access -> KindOfName -> Name -> QName -> TCMT IO ()
    bindName Access
    acc KindOfName
    kind Name
    x QName
    y

    -- | Bind a module name.
    bindModule :: Access -> C.Name -> A.ModuleName -> ScopeM ()
    bindModule :: Access -> Name -> ModuleName -> TCMT IO ()
    bindModule Access
    acc Name
    x ModuleName
    m = (Scope -> Scope) -> TCMT IO ()
    modifyCurrentScope ((Scope -> Scope) -> TCMT IO ()) -> (Scope -> Scope) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
      NameSpaceId -> Name -> AbstractModule -> Scope -> Scope
    addModuleToScope (Access -> NameSpaceId
    localNameSpace Access
    acc) Name
    x (ModuleName -> WhyInScope -> AbstractModule
    AbsModule ModuleName
    m WhyInScope
    Defined)

    -- | Bind a qualified module name. Adds it to the imports field of the scope.
    bindQModule :: Access -> C.QName -> A.ModuleName -> ScopeM ()
    bindQModule :: Access -> QName -> ModuleName -> TCMT IO ()
    bindQModule Access
    acc QName
    q ModuleName
    m = (Scope -> Scope) -> TCMT IO ()
    modifyCurrentScope ((Scope -> Scope) -> TCMT IO ()) -> (Scope -> Scope) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ \Scope
    s ->
      Scope
    s { scopeImports :: Map QName ModuleName
    scopeImports = QName -> ModuleName -> Map QName ModuleName -> Map QName ModuleName
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert QName
    q ModuleName
    m (Scope -> Map QName ModuleName
    scopeImports Scope
    s) }

    ---------------------------------------------------------------------------
    -- * Module manipulation operations
    ---------------------------------------------------------------------------

    -- | Clear the scope of any no names.
    stripNoNames :: ScopeM ()
    stripNoNames :: TCMT IO ()
    stripNoNames = (Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ()
    modifyScopes ((Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ())
    -> (Map ModuleName Scope -> Map ModuleName Scope) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ (Scope -> Scope) -> Map ModuleName Scope -> Map ModuleName Scope
    forall a b k. (a -> b) -> Map k a -> Map k b
    Map.map ((Scope -> Scope) -> Map ModuleName Scope -> Map ModuleName Scope)
    -> (Scope -> Scope) -> Map ModuleName Scope -> Map ModuleName Scope
    forall a b. (a -> b) -> a -> b
    $ (NamesInScope -> NamesInScope)
    -> (ModulesInScope -> ModulesInScope)
    -> (InScopeSet -> InScopeSet)
    -> Scope
    -> Scope
    mapScope_ NamesInScope -> NamesInScope
    forall {a}. Map Name a -> Map Name a
    stripN ModulesInScope -> ModulesInScope
    forall {a}. Map Name a -> Map Name a
    stripN InScopeSet -> InScopeSet
    forall a. a -> a
    id
      where
        stripN :: Map Name a -> Map Name a
    stripN = (Name -> a -> Bool) -> Map Name a -> Map Name a
    forall k a. (k -> a -> Bool) -> Map k a -> Map k a
    Map.filterWithKey ((Name -> a -> Bool) -> Map Name a -> Map Name a)
    -> (Name -> a -> Bool) -> Map Name a -> Map Name a
    forall a b. (a -> b) -> a -> b
    $ Bool -> a -> Bool
    forall a b. a -> b -> a
    const (Bool -> a -> Bool) -> (Name -> Bool) -> Name -> a -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Bool -> Bool
    not (Bool -> Bool) -> (Name -> Bool) -> Name -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName

    type WSM = StateT ScopeMemo ScopeM

    data ScopeMemo = ScopeMemo
      { ScopeMemo -> Ren QName
    memoNames   :: A.Ren A.QName
      , ScopeMemo -> Map ModuleName (ModuleName, Bool)
    memoModules :: Map ModuleName (ModuleName, Bool)
        -- ^ Bool: did we copy recursively? We need to track this because we don't
        --   copy recursively when creating new modules for reexported functions
        --   (issue1985), but we might need to copy recursively later.
      }

    memoToScopeInfo :: ScopeMemo -> ScopeCopyInfo
    memoToScopeInfo :: ScopeMemo -> ScopeCopyInfo
    memoToScopeInfo (ScopeMemo Ren QName
    names Map ModuleName (ModuleName, Bool)
    mods) =
      ScopeCopyInfo :: Ren ModuleName -> Ren QName -> ScopeCopyInfo
    ScopeCopyInfo { renNames :: Ren QName
    renNames   = Ren QName
    names
                    , renModules :: Ren ModuleName
    renModules = ((ModuleName, Bool) -> List1 ModuleName)
    -> Map ModuleName (ModuleName, Bool) -> Ren ModuleName
    forall a b k. (a -> b) -> Map k a -> Map k b
    Map.map (ModuleName -> List1 ModuleName
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (ModuleName -> List1 ModuleName)
    -> ((ModuleName, Bool) -> ModuleName)
    -> (ModuleName, Bool)
    -> List1 ModuleName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ModuleName, Bool) -> ModuleName
    forall a b. (a, b) -> a
    fst) Map ModuleName (ModuleName, Bool)
    mods }

    -- | Create a new scope with the given name from an old scope. Renames
    --   public names in the old scope to match the new name and returns the
    --   renamings.
    copyScope :: C.QName -> A.ModuleName -> Scope -> ScopeM (Scope, ScopeCopyInfo)
    copyScope :: QName -> ModuleName -> Scope -> ScopeM (Scope, ScopeCopyInfo)
    copyScope QName
    oldc ModuleName
    new0 Scope
    s = ((WhyInScope -> WhyInScope) -> Scope -> Scope
    inScopeBecause (QName -> WhyInScope -> WhyInScope
    Applied QName
    oldc) (Scope -> Scope)
    -> (ScopeMemo -> ScopeCopyInfo)
    -> (Scope, ScopeMemo)
    -> (Scope, ScopeCopyInfo)
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** ScopeMemo -> ScopeCopyInfo
    memoToScopeInfo) ((Scope, ScopeMemo) -> (Scope, ScopeCopyInfo))
    -> ScopeM (Scope, ScopeMemo) -> ScopeM (Scope, ScopeCopyInfo)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> StateT ScopeMemo (TCMT IO) Scope
    -> ScopeMemo -> ScopeM (Scope, ScopeMemo)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT (ModuleName -> Scope -> StateT ScopeMemo (TCMT IO) Scope
    copy ModuleName
    new0 Scope
    s) (Ren QName -> Map ModuleName (ModuleName, Bool) -> ScopeMemo
    ScopeMemo Ren QName
    forall a. Monoid a => a
    mempty Map ModuleName (ModuleName, Bool)
    forall a. Monoid a => a
    mempty)
      where
        copy :: A.ModuleName -> Scope -> WSM Scope
        copy :: ModuleName -> Scope -> StateT ScopeMemo (TCMT IO) Scope
    copy ModuleName
    new Scope
    s = do
          TCMT IO () -> StateT ScopeMemo (TCMT IO) ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> StateT ScopeMemo (TCMT IO) ())
    -> TCMT IO () -> StateT ScopeMemo (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "scope.copy" Int
    20 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Copying scope " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ ModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow ModuleName
    old [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " to " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ ModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow ModuleName
    new
          TCMT IO () -> StateT ScopeMemo (TCMT IO) ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> StateT ScopeMemo (TCMT IO) ())
    -> TCMT IO () -> StateT ScopeMemo (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "scope.copy" Int
    50 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Scope -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Scope
    s
          Scope
    s0 <- ScopeM Scope -> StateT ScopeMemo (TCMT IO) Scope
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (ScopeM Scope -> StateT ScopeMemo (TCMT IO) Scope)
    -> ScopeM Scope -> StateT ScopeMemo (TCMT IO) Scope
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> ScopeM Scope
    getNamedScope ModuleName
    new
          -- Delete private names, then copy names and modules. Recompute inScope
          -- set rather than trying to copy it.
          Scope
    s' <- Scope -> Scope
    recomputeInScopeSets (Scope -> Scope)
    -> StateT ScopeMemo (TCMT IO) Scope
    -> StateT ScopeMemo (TCMT IO) Scope
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (NamesInScope -> StateT ScopeMemo (TCMT IO) NamesInScope)
    -> (ModulesInScope -> StateT ScopeMemo (TCMT IO) ModulesInScope)
    -> (InScopeSet -> StateT ScopeMemo (TCMT IO) InScopeSet)
    -> Scope
    -> StateT ScopeMemo (TCMT IO) Scope
    forall (m :: * -> *).
    Applicative m =>
    (NamesInScope -> m NamesInScope)
    -> (ModulesInScope -> m ModulesInScope)
    -> (InScopeSet -> m InScopeSet)
    -> Scope
    -> m Scope
    mapScopeM_ NamesInScope -> StateT ScopeMemo (TCMT IO) NamesInScope
    copyD ModulesInScope -> StateT ScopeMemo (TCMT IO) ModulesInScope
    copyM InScopeSet -> StateT ScopeMemo (TCMT IO) InScopeSet
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NameSpaceId -> NameSpace -> Scope -> Scope
    setNameSpace NameSpaceId
    PrivateNS NameSpace
    emptyNameSpace Scope
    s)
          -- Fix name and parent.
          Scope -> StateT ScopeMemo (TCMT IO) Scope
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Scope -> StateT ScopeMemo (TCMT IO) Scope)
    -> Scope -> StateT ScopeMemo (TCMT IO) Scope
    forall a b. (a -> b) -> a -> b
    $ Scope
    s' { scopeName :: ModuleName
    scopeName    = Scope -> ModuleName
    scopeName Scope
    s0
                      , scopeParents :: [ModuleName]
    scopeParents = Scope -> [ModuleName]
    scopeParents Scope
    s0
                      }
          where
            rnew :: Range
    rnew = ModuleName -> Range
    forall a. HasRange a => a -> Range
    getRange ModuleName
    new
            new' :: ModuleName
    new' = ModuleName -> ModuleName
    forall a. KillRange a => KillRangeT a
    killRange ModuleName
    new
            newL :: [Name]
    newL = ModuleName -> [Name]
    A.mnameToList ModuleName
    new'
            old :: ModuleName
    old  = Scope -> ModuleName
    scopeName Scope
    s

            copyD :: NamesInScope -> WSM NamesInScope
            copyD :: NamesInScope -> StateT ScopeMemo (TCMT IO) NamesInScope
    copyD = ([AbstractName] -> StateT ScopeMemo (TCMT IO) [AbstractName])
    -> NamesInScope -> StateT ScopeMemo (TCMT IO) NamesInScope
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse (([AbstractName] -> StateT ScopeMemo (TCMT IO) [AbstractName])
     -> NamesInScope -> StateT ScopeMemo (TCMT IO) NamesInScope)
    -> ([AbstractName] -> StateT ScopeMemo (TCMT IO) [AbstractName])
    -> NamesInScope
    -> StateT ScopeMemo (TCMT IO) NamesInScope
    forall a b. (a -> b) -> a -> b
    $ (AbstractName -> StateT ScopeMemo (TCMT IO) AbstractName)
    -> [AbstractName] -> StateT ScopeMemo (TCMT IO) [AbstractName]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((AbstractName -> StateT ScopeMemo (TCMT IO) AbstractName)
     -> [AbstractName] -> StateT ScopeMemo (TCMT IO) [AbstractName])
    -> (AbstractName -> StateT ScopeMemo (TCMT IO) AbstractName)
    -> [AbstractName]
    -> StateT ScopeMemo (TCMT IO) [AbstractName]
    forall a b. (a -> b) -> a -> b
    $ (QName -> WSM QName)
    -> AbstractName -> StateT ScopeMemo (TCMT IO) AbstractName
    onName QName -> WSM QName
    renName

            copyM :: ModulesInScope -> WSM ModulesInScope
            copyM :: ModulesInScope -> StateT ScopeMemo (TCMT IO) ModulesInScope
    copyM = ([AbstractModule] -> StateT ScopeMemo (TCMT IO) [AbstractModule])
    -> ModulesInScope -> StateT ScopeMemo (TCMT IO) ModulesInScope
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse (([AbstractModule] -> StateT ScopeMemo (TCMT IO) [AbstractModule])
     -> ModulesInScope -> StateT ScopeMemo (TCMT IO) ModulesInScope)
    -> ([AbstractModule]
        -> StateT ScopeMemo (TCMT IO) [AbstractModule])
    -> ModulesInScope
    -> StateT ScopeMemo (TCMT IO) ModulesInScope
    forall a b. (a -> b) -> a -> b
    $ (AbstractModule -> StateT ScopeMemo (TCMT IO) AbstractModule)
    -> [AbstractModule] -> StateT ScopeMemo (TCMT IO) [AbstractModule]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((AbstractModule -> StateT ScopeMemo (TCMT IO) AbstractModule)
     -> [AbstractModule] -> StateT ScopeMemo (TCMT IO) [AbstractModule])
    -> (AbstractModule -> StateT ScopeMemo (TCMT IO) AbstractModule)
    -> [AbstractModule]
    -> StateT ScopeMemo (TCMT IO) [AbstractModule]
    forall a b. (a -> b) -> a -> b
    $ (ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName)
    -> AbstractModule -> StateT ScopeMemo (TCMT IO) AbstractModule
    Lens' ModuleName AbstractModule
    lensAmodName ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
    renMod

            onName :: (A.QName -> WSM A.QName) -> AbstractName -> WSM AbstractName
            onName :: (QName -> WSM QName)
    -> AbstractName -> StateT ScopeMemo (TCMT IO) AbstractName
    onName QName -> WSM QName
    f AbstractName
    d =
              case AbstractName -> KindOfName
    anameKind AbstractName
    d of
                KindOfName
    PatternSynName -> AbstractName -> StateT ScopeMemo (TCMT IO) AbstractName
    forall (m :: * -> *) a. Monad m => a -> m a
    return AbstractName
    d  -- Pattern synonyms are simply aliased, not renamed
                KindOfName
    _ -> (QName -> WSM QName)
    -> AbstractName -> StateT ScopeMemo (TCMT IO) AbstractName
    Lens' QName AbstractName
    lensAnameName QName -> WSM QName
    f AbstractName
    d

            -- Adding to memo structure.
            addName :: QName -> QName -> m ()
    addName QName
    x QName
    y     = (ScopeMemo -> ScopeMemo) -> m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((ScopeMemo -> ScopeMemo) -> m ())
    -> (ScopeMemo -> ScopeMemo) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \ ScopeMemo
    i -> ScopeMemo
    i { memoNames :: Ren QName
    memoNames   = (List1 QName -> List1 QName -> List1 QName)
    -> QName -> List1 QName -> Ren QName -> Ren QName
    forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
    Map.insertWith List1 QName -> List1 QName -> List1 QName
    forall a. Semigroup a => a -> a -> a
    (<>) QName
    x (QName -> List1 QName
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure QName
    y) (ScopeMemo -> Ren QName
    memoNames ScopeMemo
    i) }
            addMod :: ModuleName -> ModuleName -> Bool -> m ()
    addMod  ModuleName
    x ModuleName
    y Bool
    rec = (ScopeMemo -> ScopeMemo) -> m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((ScopeMemo -> ScopeMemo) -> m ())
    -> (ScopeMemo -> ScopeMemo) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \ ScopeMemo
    i -> ScopeMemo
    i { memoModules :: Map ModuleName (ModuleName, Bool)
    memoModules = ModuleName
    -> (ModuleName, Bool)
    -> Map ModuleName (ModuleName, Bool)
    -> Map ModuleName (ModuleName, Bool)
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert ModuleName
    x (ModuleName
    y, Bool
    rec) (ScopeMemo -> Map ModuleName (ModuleName, Bool)
    memoModules ScopeMemo
    i) }

            -- Querying the memo structure.
            findName :: QName -> m (Maybe (List1 QName))
    findName QName
    x = (ScopeMemo -> Maybe (List1 QName)) -> m (Maybe (List1 QName))
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets (QName -> Ren QName -> Maybe (List1 QName)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup QName
    x (Ren QName -> Maybe (List1 QName))
    -> (ScopeMemo -> Ren QName) -> ScopeMemo -> Maybe (List1 QName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ScopeMemo -> Ren QName
    memoNames) -- NB:: Defined but not used
            findMod :: ModuleName -> m (Maybe (ModuleName, Bool))
    findMod  ModuleName
    x = (ScopeMemo -> Maybe (ModuleName, Bool))
    -> m (Maybe (ModuleName, Bool))
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets (ModuleName
    -> Map ModuleName (ModuleName, Bool) -> Maybe (ModuleName, Bool)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup ModuleName
    x (Map ModuleName (ModuleName, Bool) -> Maybe (ModuleName, Bool))
    -> (ScopeMemo -> Map ModuleName (ModuleName, Bool))
    -> ScopeMemo
    -> Maybe (ModuleName, Bool)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ScopeMemo -> Map ModuleName (ModuleName, Bool)
    memoModules)

            refresh :: A.Name -> WSM A.Name
            refresh :: Name -> WSM Name
    refresh Name
    x = do
              NameId
    i <- TCMT IO NameId -> StateT ScopeMemo (TCMT IO) NameId
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TCMT IO NameId
    forall i (m :: * -> *). MonadFresh i m => m i
    fresh
              Name -> WSM Name
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Name -> WSM Name) -> Name -> WSM Name
    forall a b. (a -> b) -> a -> b
    $ Name
    x { nameId :: NameId
    A.nameId = NameId
    i }

            -- Change a binding M.x -> old.M'.y to M.x -> new.M'.y
            renName :: A.QName -> WSM A.QName
            renName :: QName -> WSM QName
    renName QName
    x = do
              -- Issue 1985: For re-exported names we can't use new' as the
              -- module, since it has the wrong telescope. Example:
              --
              --    module M1 (A : Set) where
              --      module M2 (B : Set) where
              --        postulate X : Set
              --      module M3 (C : Set) where
              --        module M4 (D E : Set) where
              --          open M2 public
              --
              --    module M = M1.M3 A C
              --
              -- Here we can't copy M1.M2.X to M.M4.X since we need
              -- X : (B : Set) → Set, but M.M4 has telescope (D E : Set). Thus, we
              -- would break the invariant that all functions in a module share the
              -- module telescope. Instead we copy M1.M2.X to M.M2.X for a fresh
              -- module M2 that gets the right telescope.
              ModuleName
    m <- if QName
    x QName -> ModuleName -> Bool
    `isInModule` ModuleName
    old
                     then ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
    forall (m :: * -> *) a. Monad m => a -> m a
    return ModuleName
    new'
                     else Bool -> ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
    renMod' Bool
    False (QName -> ModuleName
    qnameModule QName
    x)
                              -- Don't copy recursively here, we only know that the
                              -- current name x should be copied.
              -- Generate a fresh name for the target.
              -- Andreas, 2015-08-11 Issue 1619:
              -- Names copied by a module macro should get the module macro's
              -- range as declaration range
              -- (maybe rather the one of the open statement).
              -- For now, we just set their range
              -- to the new module name's one, which fixes issue 1619.
              QName
    y <- Range -> QName -> QName
    forall a. SetRange a => Range -> a -> a
    setRange Range
    rnew (QName -> QName) -> (Name -> QName) -> Name -> QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ModuleName -> Name -> QName
    A.qualify ModuleName
    m (Name -> QName) -> WSM Name -> WSM QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Name -> WSM Name
    refresh (QName -> Name
    qnameName QName
    x)
              TCMT IO () -> StateT ScopeMemo (TCMT IO) ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> StateT ScopeMemo (TCMT IO) ())
    -> TCMT IO () -> StateT ScopeMemo (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "scope.copy" Int
    50 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  Copying " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    x [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " to " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    y
              QName -> QName -> StateT ScopeMemo (TCMT IO) ()
    forall {m :: * -> *}.
    MonadState ScopeMemo m =>
    QName -> QName -> m ()
    addName QName
    x QName
    y
              QName -> WSM QName
    forall (m :: * -> *) a. Monad m => a -> m a
    return QName
    y

            -- Change a binding M.x -> old.M'.y to M.x -> new.M'.y
            renMod :: A.ModuleName -> WSM A.ModuleName
            renMod :: ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
    renMod = Bool -> ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
    renMod' Bool
    True

            renMod' :: Bool -> ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
    renMod' Bool
    rec ModuleName
    x = do
              -- Andreas, issue 1607:
              -- If we have already copied this module, return the copy.
              Maybe (ModuleName, Bool)
    z <- ModuleName -> StateT ScopeMemo (TCMT IO) (Maybe (ModuleName, Bool))
    forall {m :: * -> *}.
    MonadState ScopeMemo m =>
    ModuleName -> m (Maybe (ModuleName, Bool))
    findMod ModuleName
    x
              case Maybe (ModuleName, Bool)
    z of
                Just (ModuleName
    y, Bool
    False) | Bool
    rec -> ModuleName
    y ModuleName
    -> StateT ScopeMemo (TCMT IO) ()
    -> StateT ScopeMemo (TCMT IO) ModuleName
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ ModuleName -> ModuleName -> StateT ScopeMemo (TCMT IO) ()
    copyRec ModuleName
    x ModuleName
    y
                Just (ModuleName
    y, Bool
    _)           -> ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
    forall (m :: * -> *) a. Monad m => a -> m a
    return ModuleName
    y
                Maybe (ModuleName, Bool)
    Nothing -> do
                -- Ulf (issue 1985): If copying a reexported module we put it at the
                -- top-level, to make sure we don't mess up the invariant that all
                -- (abstract) names M.f share the argument telescope of M.
                let newM :: [Name]
    newM = if ModuleName
    x ModuleName -> ModuleName -> Bool
    `isLtChildModuleOf` ModuleName
    old then [Name]
    newL else ModuleName -> [Name]
    mnameToList ModuleName
    new0

                ModuleName
    y <- do
                   -- Andreas, Jesper, 2015-07-02: Issue 1597
                   -- Don't blindly drop a prefix of length of the old qualifier.
                   -- If things are imported by open public they do not have the old qualifier
                   -- as prefix.  Those need just to be linked, not copied.
                   -- return $ A.mnameFromList $ (newL ++) $ drop (size old) $ A.mnameToList x
                   -- caseMaybe (stripPrefix (A.mnameToList old) (A.mnameToList x)) (return x) $ \ suffix -> do
                   --   return $ A.mnameFromList $ newL ++ suffix
                   -- Ulf, 2016-02-22: #1726
                   -- We still need to copy modules from 'open public'. Same as in renName.
                   Name
    y <- Name -> WSM Name
    refresh (Name -> WSM Name) -> Name -> WSM Name
    forall a b. (a -> b) -> a -> b
    $ Name -> [Name] -> Name
    forall a. a -> [a] -> a
    lastWithDefault Name
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([Name] -> Name) -> [Name] -> Name
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> [Name]
    A.mnameToList ModuleName
    x
                   ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName)
    -> ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
    forall a b. (a -> b) -> a -> b
    $ [Name] -> ModuleName
    A.mnameFromList ([Name] -> ModuleName) -> [Name] -> ModuleName
    forall a b. (a -> b) -> a -> b
    $ [Name]
    newM [Name] -> [Name] -> [Name]
    forall a. [a] -> [a] -> [a]
    ++ [Name
    y]
                -- Andreas, Jesper, 2015-07-02: Issue 1597
                -- Don't copy a module over itself, it will just be emptied of its contents.
                if (ModuleName
    x ModuleName -> ModuleName -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModuleName
    y) then ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
    forall (m :: * -> *) a. Monad m => a -> m a
    return ModuleName
    x else do
                TCMT IO () -> StateT ScopeMemo (TCMT IO) ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> StateT ScopeMemo (TCMT IO) ())
    -> TCMT IO () -> StateT ScopeMemo (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "scope.copy" Int
    50 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  Copying module " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ ModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow ModuleName
    x [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " to " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ ModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow ModuleName
    y
                ModuleName -> ModuleName -> Bool -> StateT ScopeMemo (TCMT IO) ()
    forall {m :: * -> *}.
    MonadState ScopeMemo m =>
    ModuleName -> ModuleName -> Bool -> m ()
    addMod ModuleName
    x ModuleName
    y Bool
    rec
                TCMT IO () -> StateT ScopeMemo (TCMT IO) ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> StateT ScopeMemo (TCMT IO) ())
    -> TCMT IO () -> StateT ScopeMemo (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ Maybe DataOrRecordModule -> ModuleName -> TCMT IO ()
    createModule Maybe DataOrRecordModule
    forall a. Maybe a
    Nothing ModuleName
    y
                -- We need to copy the contents of included modules recursively (only when 'rec')
                Bool
    -> StateT ScopeMemo (TCMT IO) () -> StateT ScopeMemo (TCMT IO) ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    rec (StateT ScopeMemo (TCMT IO) () -> StateT ScopeMemo (TCMT IO) ())
    -> StateT ScopeMemo (TCMT IO) () -> StateT ScopeMemo (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> ModuleName -> StateT ScopeMemo (TCMT IO) ()
    copyRec ModuleName
    x ModuleName
    y
                ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
    forall (m :: * -> *) a. Monad m => a -> m a
    return ModuleName
    y
              where
                copyRec :: ModuleName -> ModuleName -> StateT ScopeMemo (TCMT IO) ()
    copyRec ModuleName
    x ModuleName
    y = do
                  Scope
    s0 <- ScopeM Scope -> StateT ScopeMemo (TCMT IO) Scope
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (ScopeM Scope -> StateT ScopeMemo (TCMT IO) Scope)
    -> ScopeM Scope -> StateT ScopeMemo (TCMT IO) Scope
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> ScopeM Scope
    getNamedScope ModuleName
    x
                  Scope
    s  <- ModuleName
    -> StateT ScopeMemo (TCMT IO) Scope
    -> StateT ScopeMemo (TCMT IO) Scope
    forall (t :: (* -> *) -> * -> *) a.
    (MonadTrans t, Monad (t (TCMT IO))) =>
    ModuleName -> t (TCMT IO) a -> t (TCMT IO) a
    withCurrentModule' ModuleName
    y (StateT ScopeMemo (TCMT IO) Scope
     -> StateT ScopeMemo (TCMT IO) Scope)
    -> StateT ScopeMemo (TCMT IO) Scope
    -> StateT ScopeMemo (TCMT IO) Scope
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> Scope -> StateT ScopeMemo (TCMT IO) Scope
    copy ModuleName
    y Scope
    s0
                  TCMT IO () -> StateT ScopeMemo (TCMT IO) ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO () -> StateT ScopeMemo (TCMT IO) ())
    -> TCMT IO () -> StateT ScopeMemo (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> (Scope -> Scope) -> TCMT IO ()
    modifyNamedScope ModuleName
    y (Scope -> Scope -> Scope
    forall a b. a -> b -> a
    const Scope
    s)

    ---------------------------------------------------------------------------
    -- * Import directives
    ---------------------------------------------------------------------------

    -- | Warn about useless fixity declarations in @renaming@ directives.
    --   Monadic for the sake of error reporting.
    checkNoFixityInRenamingModule :: [C.Renaming] -> ScopeM ()
    checkNoFixityInRenamingModule :: [Renaming] -> TCMT IO ()
    checkNoFixityInRenamingModule [Renaming]
    ren = do
      Maybe (NonEmpty Range)
    -> (NonEmpty Range -> TCMT IO ()) -> TCMT IO ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust ([Range] -> Maybe (NonEmpty Range)
    forall a. [a] -> Maybe (NonEmpty a)
    nonEmpty ([Range] -> Maybe (NonEmpty Range))
    -> [Range] -> Maybe (NonEmpty Range)
    forall a b. (a -> b) -> a -> b
    $ (Renaming -> Maybe Range) -> [Renaming] -> [Range]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe Renaming -> Maybe Range
    rangeOfUselessInfix [Renaming]
    ren) ((NonEmpty Range -> TCMT IO ()) -> TCMT IO ())
    -> (NonEmpty Range -> TCMT IO ()) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ \ NonEmpty Range
    rs -> do
        NonEmpty Range -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange NonEmpty Range
    rs (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do
          Warning -> TCMT IO ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCMT IO ()) -> Warning -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ NonEmpty Range -> Warning
    FixityInRenamingModule NonEmpty Range
    rs
      where
      rangeOfUselessInfix :: C.Renaming -> Maybe Range
      rangeOfUselessInfix :: Renaming -> Maybe Range
    rangeOfUselessInfix = \case
        Renaming ImportedModule{} ImportedName
    _ Maybe Fixity
    mfx Range
    _ -> Fixity -> Range
    forall a. HasRange a => a -> Range
    getRange (Fixity -> Range) -> Maybe Fixity -> Maybe Range
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe Fixity
    mfx
        Renaming
    _ -> Maybe Range
    forall a. Maybe a
    Nothing

    -- Moved here carefully from Parser.y to preserve the archaeological artefact
    -- dating from Oct 2005 (5ba14b647b9bd175733f9563e744176425c39126).
    -- | Check that an import directive doesn't contain repeated names.
    verifyImportDirective :: [C.ImportedName] -> C.HidingDirective -> C.RenamingDirective -> ScopeM ()
    verifyImportDirective :: [ImportedName] -> [ImportedName] -> [Renaming] -> TCMT IO ()
    verifyImportDirective [ImportedName]
    usn [ImportedName]
    hdn [Renaming]
    ren =
        case ([ImportedName] -> Bool) -> [[ImportedName]] -> [[ImportedName]]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >Int
    1) (Int -> Bool) -> ([ImportedName] -> Int) -> [ImportedName] -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [ImportedName] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length)
             ([[ImportedName]] -> [[ImportedName]])
    -> [[ImportedName]] -> [[ImportedName]]
    forall a b. (a -> b) -> a -> b
    $ [ImportedName] -> [[ImportedName]]
    forall a. Eq a => [a] -> [[a]]
    List.group
             ([ImportedName] -> [[ImportedName]])
    -> [ImportedName] -> [[ImportedName]]
    forall a b. (a -> b) -> a -> b
    $ [ImportedName] -> [ImportedName]
    forall a. Ord a => [a] -> [a]
    List.sort [ImportedName]
    xs
        of
            []  -> () -> TCMT IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            [[ImportedName]]
    yss -> [[ImportedName]] -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange [[ImportedName]]
    yss (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    [Char] -> m a
    genericError ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
                    [Char]
    "Repeated name" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    s [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " in import directive: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
                    [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    List.intersperse [Char]
    ", " ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> a -> b
    $ ([ImportedName] -> [Char]) -> [[ImportedName]] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map (ImportedName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow (ImportedName -> [Char])
    -> ([ImportedName] -> ImportedName) -> [ImportedName] -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [ImportedName] -> ImportedName
    forall a. [a] -> a
    head) [[ImportedName]]
    yss)
                where
                    s :: [Char]
    s = case [[ImportedName]]
    yss of
                            [[ImportedName]
    _] -> [Char]
    ""
                            [[ImportedName]]
    _   -> [Char]
    "s"
        where
            xs :: [ImportedName]
    xs = [ImportedName]
    usn [ImportedName] -> [ImportedName] -> [ImportedName]
    forall a. [a] -> [a] -> [a]
    ++ [ImportedName]
    hdn [ImportedName] -> [ImportedName] -> [ImportedName]
    forall a. [a] -> [a] -> [a]
    ++ (Renaming -> ImportedName) -> [Renaming] -> [ImportedName]
    forall a b. (a -> b) -> [a] -> [b]
    map Renaming -> ImportedName
    forall n m. Renaming' n m -> ImportedName' n m
    renFrom [Renaming]
    ren

    -- | Apply an import directive and check that all the names mentioned actually
    --   exist.
    --
    --   Monadic for the sake of error reporting.
    applyImportDirectiveM
      :: C.QName                           -- ^ Name of the scope, only for error reporting.
      -> C.ImportDirective                 -- ^ Description of how scope is to be modified.
      -> Scope                             -- ^ Input scope.
      -> ScopeM (A.ImportDirective, Scope) -- ^ Scope-checked description, output scope.
    applyImportDirectiveM :: QName
    -> ImportDirective -> Scope -> ScopeM (ImportDirective, Scope)
    applyImportDirectiveM QName
    m (ImportDirective Range
    rng Using' Name Name
    usn' [ImportedName]
    hdn' [Renaming]
    ren' Maybe Range
    public) Scope
    scope0 = do

        -- Module names do not come with fixities, thus, we should complain if the
        -- user has supplied fixity annotations to @renaming module@ clauses.
        [Renaming] -> TCMT IO ()
    checkNoFixityInRenamingModule [Renaming]
    ren'

        -- Andreas, 2020-06-06, issue #4707
        -- Duplicates in @using@ directive are dropped with a warning.
        [ImportedName]
    usingList <- Using' Name Name -> ScopeM [ImportedName]
    discardDuplicatesInUsing Using' Name Name
    usn'

        -- The following check was originally performed by the parser.
        -- The Great Ulf Himself added the check back in the dawn of time
        -- (5ba14b647b9bd175733f9563e744176425c39126)
        -- when Agda 2 wasn't even believed to exist yet.
        [ImportedName] -> [ImportedName] -> [Renaming] -> TCMT IO ()
    verifyImportDirective [ImportedName]
    usingList [ImportedName]
    hdn' [Renaming]
    ren'

        -- We start by checking that all of the names talked about in the import
        -- directive do exist.  If some do not then we remove them and raise a warning.
        let ([ImportedName]
    missingExports, [ImportedName' (Name, QName) (Name, ModuleName)]
    namesA) = [ImportedName]
    -> ([ImportedName],
        [ImportedName' (Name, QName) (Name, ModuleName)])
    checkExist ([ImportedName]
     -> ([ImportedName],
         [ImportedName' (Name, QName) (Name, ModuleName)]))
    -> [ImportedName]
    -> ([ImportedName],
        [ImportedName' (Name, QName) (Name, ModuleName)])
    forall a b. (a -> b) -> a -> b
    $ [ImportedName]
    usingList [ImportedName] -> [ImportedName] -> [ImportedName]
    forall a. [a] -> [a] -> [a]
    ++ [ImportedName]
    hdn' [ImportedName] -> [ImportedName] -> [ImportedName]
    forall a. [a] -> [a] -> [a]
    ++ (Renaming -> ImportedName) -> [Renaming] -> [ImportedName]
    forall a b. (a -> b) -> [a] -> [b]
    map Renaming -> ImportedName
    forall n m. Renaming' n m -> ImportedName' n m
    renFrom [Renaming]
    ren'
        Bool -> TCMT IO () -> TCMT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([ImportedName] -> Bool
    forall a. Null a => a -> Bool
    null [ImportedName]
    missingExports) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Range -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange Range
    rng (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do
          [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "scope.import.apply" Int
    20 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "non existing names: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [ImportedName] -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow [ImportedName]
    missingExports
          Warning -> TCMT IO ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCMT IO ()) -> Warning -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ QName -> [Name] -> [Name] -> [ImportedName] -> Warning
    ModuleDoesntExport QName
    m (NamesInScope -> [Name]
    forall k a. Map k a -> [k]
    Map.keys NamesInScope
    namesInScope) (ModulesInScope -> [Name]
    forall k a. Map k a -> [k]
    Map.keys ModulesInScope
    modulesInScope) [ImportedName]
    missingExports

        -- We can now define a cleaned-up version of the import directive.
        let notMissing :: ImportedName -> Bool
    notMissing = Bool -> Bool
    not (Bool -> Bool) -> (ImportedName -> Bool) -> ImportedName -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([ImportedName]
    missingExports [ImportedName] -> ImportedName -> Bool
    forall a. Ord a => [a] -> a -> Bool
    `hasElem`)  -- #3997, efficient lookup in missingExports
        let usn :: [ImportedName]
    usn = (ImportedName -> Bool) -> [ImportedName] -> [ImportedName]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ImportedName -> Bool
    notMissing [ImportedName]
    usingList        -- remove missingExports from usn'
        let hdn :: [ImportedName]
    hdn = (ImportedName -> Bool) -> [ImportedName] -> [ImportedName]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ImportedName -> Bool
    notMissing [ImportedName]
    hdn'             -- remove missingExports from hdn'
        let ren :: [Renaming]
    ren = (Renaming -> Bool) -> [Renaming] -> [Renaming]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (ImportedName -> Bool
    notMissing (ImportedName -> Bool)
    -> (Renaming -> ImportedName) -> Renaming -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Renaming -> ImportedName
    forall n m. Renaming' n m -> ImportedName' n m
    renFrom) [Renaming]
    ren'                   -- and from ren'
        let dir :: ImportDirective
    dir = Range
    -> Using' Name Name
    -> [ImportedName]
    -> [Renaming]
    -> Maybe Range
    -> ImportDirective
    forall n m.
    Range
    -> Using' n m
    -> HidingDirective' n m
    -> RenamingDirective' n m
    -> Maybe Range
    -> ImportDirective' n m
    ImportDirective Range
    rng (([ImportedName] -> [ImportedName])
    -> Using' Name Name -> Using' Name Name
    forall n1 m1 n2 m2.
    ([ImportedName' n1 m1] -> [ImportedName' n2 m2])
    -> Using' n1 m1 -> Using' n2 m2
    mapUsing ([ImportedName] -> [ImportedName] -> [ImportedName]
    forall a b. a -> b -> a
    const [ImportedName]
    usn) Using' Name Name
    usn') [ImportedName]
    hdn [Renaming]
    ren Maybe Range
    public

        -- Convenient shorthands for defined names and names brought into scope:
        let names :: [ImportedName]
    names        = (Renaming -> ImportedName) -> [Renaming] -> [ImportedName]
    forall a b. (a -> b) -> [a] -> [b]
    map Renaming -> ImportedName
    forall n m. Renaming' n m -> ImportedName' n m
    renFrom [Renaming]
    ren [ImportedName] -> [ImportedName] -> [ImportedName]
    forall a. [a] -> [a] -> [a]
    ++ [ImportedName]
    hdn [ImportedName] -> [ImportedName] -> [ImportedName]
    forall a. [a] -> [a] -> [a]
    ++ [ImportedName]
    usn
        let definedNames :: [ImportedName]
    definedNames = (Renaming -> ImportedName) -> [Renaming] -> [ImportedName]
    forall a b. (a -> b) -> [a] -> [b]
    map Renaming -> ImportedName
    forall n m. Renaming' n m -> ImportedName' n m
    renTo [Renaming]
    ren
        let targetNames :: [ImportedName]
    targetNames  = [ImportedName]
    usn [ImportedName] -> [ImportedName] -> [ImportedName]
    forall a. [a] -> [a] -> [a]
    ++ [ImportedName]
    definedNames

        -- Efficient test of (`elem` names):
        let inNames :: ImportedName -> Bool
    inNames      = ([ImportedName]
    names [ImportedName] -> ImportedName -> Bool
    forall a. Ord a => [a] -> a -> Bool
    `hasElem`)

        -- Efficient test of whether a module import should be added to the import
        -- of a definition (like a data or record definition).
        let extra :: Name -> Bool
    extra Name
    x = ImportedName -> Bool
    inNames (Name -> ImportedName
    forall n m. n -> ImportedName' n m
    ImportedName   Name
    x)
                   Bool -> Bool -> Bool
    && ImportedName -> Bool
    notMissing (Name -> ImportedName
    forall n m. m -> ImportedName' n m
    ImportedModule Name
    x)
                   Bool -> Bool -> Bool
    && (Bool -> Bool
    not (Bool -> Bool) -> (ImportedName -> Bool) -> ImportedName -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ImportedName -> Bool
    inNames (ImportedName -> Bool) -> ImportedName -> Bool
    forall a b. (a -> b) -> a -> b
    $ Name -> ImportedName
    forall n m. m -> ImportedName' n m
    ImportedModule Name
    x)
                      -- The last test implies that @hiding (module M)@ prevents @module M@
                      -- from entering the @using@ list in @addExtraModule@.

        ImportDirective
    dir' <- (ImportedName -> Bool)
    -> ImportDirective -> TCMT IO ImportDirective
    forall {m :: * -> *} {m}.
    MonadWarning m =>
    (ImportedName' Name m -> Bool)
    -> ImportDirective -> m ImportDirective
    sanityCheck (Bool -> Bool
    not (Bool -> Bool) -> (ImportedName -> Bool) -> ImportedName -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ImportedName -> Bool
    inNames) (ImportDirective -> TCMT IO ImportDirective)
    -> ImportDirective -> TCMT IO ImportDirective
    forall a b. (a -> b) -> a -> b
    $ (Name -> Bool) -> ImportDirective -> ImportDirective
    addExtraModules Name -> Bool
    extra ImportDirective
    dir

        -- Check for duplicate imports in a single import directive.
        -- @dup@ : To be imported names that are mentioned more than once.
        [ImportedName] -> ([ImportedName] -> TCMT IO ()) -> TCMT IO ()
    forall (m :: * -> *) a.
    (Monad m, Null a) =>
    a -> (a -> m ()) -> m ()
    unlessNull ([ImportedName] -> [ImportedName]
    forall a. Ord a => [a] -> [a]
    allDuplicates [ImportedName]
    targetNames) (([ImportedName] -> TCMT IO ()) -> TCMT IO ())
    -> ([ImportedName] -> TCMT IO ()) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ \ [ImportedName]
    dup ->
          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
    $ QName -> [ImportedName] -> TypeError
    DuplicateImports QName
    m [ImportedName]
    dup

        -- Apply the import directive.
        let (Scope
    scope', (Set Name
    nameClashes, Set Name
    moduleClashes)) = ImportDirective -> Scope -> (Scope, (Set Name, Set Name))
    applyImportDirective_ ImportDirective
    dir' Scope
    scope

        -- Andreas, 2019-11-08, issue #4154, report clashes
        -- introduced by the @renaming@.
        Bool -> TCMT IO () -> TCMT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Set Name -> Bool
    forall a. Null a => a -> Bool
    null Set Name
    nameClashes) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
          Warning -> TCMT IO ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCMT IO ()) -> Warning -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ NameOrModule -> [Name] -> Warning
    ClashesViaRenaming NameOrModule
    NameNotModule ([Name] -> Warning) -> [Name] -> Warning
    forall a b. (a -> b) -> a -> b
    $ Set Name -> [Name]
    forall a. Set a -> [a]
    Set.toList Set Name
    nameClashes
        Bool -> TCMT IO () -> TCMT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Set Name -> Bool
    forall a. Null a => a -> Bool
    null Set Name
    moduleClashes) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
          Warning -> TCMT IO ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCMT IO ()) -> Warning -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ NameOrModule -> [Name] -> Warning
    ClashesViaRenaming NameOrModule
    ModuleNotName ([Name] -> Warning) -> [Name] -> Warning
    forall a b. (a -> b) -> a -> b
    $ Set Name -> [Name]
    forall a. Set a -> [a]
    Set.toList Set Name
    moduleClashes

        -- Look up the defined names in the new scope.
        let namesInScope' :: NamesInScope
    namesInScope'   = (Scope -> NamesInScope
    forall a. InScope a => Scope -> ThingsInScope a
    allNamesInScope Scope
    scope' :: ThingsInScope AbstractName)
        let modulesInScope' :: ModulesInScope
    modulesInScope' = (Scope -> ModulesInScope
    forall a. InScope a => Scope -> ThingsInScope a
    allNamesInScope Scope
    scope' :: ThingsInScope AbstractModule)
        let look :: k -> Map k [c] -> c
    look k
    x = c -> [c] -> c
    forall a. a -> [a] -> a
    headWithDefault c
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([c] -> c) -> (Map k [c] -> [c]) -> Map k [c] -> c
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [c] -> k -> Map k [c] -> [c]
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault [c]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ k
    x
        -- We set the ranges to the ranges of the concrete names in order to get
        -- highlighting for the names in the import directive.
        let definedA :: [ImportedName' (Name, QName) (Name, ModuleName)]
    definedA = [ImportedName]
    -> (ImportedName -> ImportedName' (Name, QName) (Name, ModuleName))
    -> [ImportedName' (Name, QName) (Name, ModuleName)]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for [ImportedName]
    definedNames ((ImportedName -> ImportedName' (Name, QName) (Name, ModuleName))
     -> [ImportedName' (Name, QName) (Name, ModuleName)])
    -> (ImportedName -> ImportedName' (Name, QName) (Name, ModuleName))
    -> [ImportedName' (Name, QName) (Name, ModuleName)]
    forall a b. (a -> b) -> a -> b
    $ \case
              ImportedName   Name
    x -> (Name, QName) -> ImportedName' (Name, QName) (Name, ModuleName)
    forall n m. n -> ImportedName' n m
    ImportedName   ((Name, QName) -> ImportedName' (Name, QName) (Name, ModuleName))
    -> (AbstractName -> (Name, QName))
    -> AbstractName
    -> ImportedName' (Name, QName) (Name, ModuleName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name
    x,) (QName -> (Name, QName))
    -> (AbstractName -> QName) -> AbstractName -> (Name, QName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Range -> QName -> QName
    forall a. SetRange a => Range -> a -> a
    setRange (Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    x) (QName -> QName)
    -> (AbstractName -> QName) -> AbstractName -> QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbstractName -> QName
    anameName (AbstractName -> ImportedName' (Name, QName) (Name, ModuleName))
    -> AbstractName -> ImportedName' (Name, QName) (Name, ModuleName)
    forall a b. (a -> b) -> a -> b
    $ Name -> NamesInScope -> AbstractName
    forall {k} {c}. Ord k => k -> Map k [c] -> c
    look Name
    x NamesInScope
    namesInScope'
              ImportedModule Name
    x -> (Name, ModuleName)
    -> ImportedName' (Name, QName) (Name, ModuleName)
    forall n m. m -> ImportedName' n m
    ImportedModule ((Name, ModuleName)
     -> ImportedName' (Name, QName) (Name, ModuleName))
    -> (AbstractModule -> (Name, ModuleName))
    -> AbstractModule
    -> ImportedName' (Name, QName) (Name, ModuleName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name
    x,) (ModuleName -> (Name, ModuleName))
    -> (AbstractModule -> ModuleName)
    -> AbstractModule
    -> (Name, ModuleName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Range -> ModuleName -> ModuleName
    forall a. SetRange a => Range -> a -> a
    setRange (Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    x) (ModuleName -> ModuleName)
    -> (AbstractModule -> ModuleName) -> AbstractModule -> ModuleName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbstractModule -> ModuleName
    amodName  (AbstractModule -> ImportedName' (Name, QName) (Name, ModuleName))
    -> AbstractModule -> ImportedName' (Name, QName) (Name, ModuleName)
    forall a b. (a -> b) -> a -> b
    $ Name -> ModulesInScope -> AbstractModule
    forall {k} {c}. Ord k => k -> Map k [c] -> c
    look Name
    x ModulesInScope
    modulesInScope'

        let adir :: ImportDirective
    adir = [ImportedName' (Name, QName) (Name, ModuleName)]
    -> [ImportedName' (Name, QName) (Name, ModuleName)]
    -> ImportDirective
    -> ImportDirective
    forall n1 m1 n2 m2.
    (Ord n1, Ord m1) =>
    [ImportedName' (n1, n2) (m1, m2)]
    -> [ImportedName' (n1, n2) (m1, m2)]
    -> ImportDirective' n1 m1
    -> ImportDirective' n2 m2
    mapImportDir [ImportedName' (Name, QName) (Name, ModuleName)]
    namesA [ImportedName' (Name, QName) (Name, ModuleName)]
    definedA ImportDirective
    dir
        (ImportDirective, Scope) -> ScopeM (ImportDirective, Scope)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ImportDirective
    adir, Scope
    scope') -- TODO Issue 1714: adir

      where
        -- Andreas, 2020-06-23, issue #4773, fixing regression in 2.5.1.
        -- Import directive may not mention private things.
        -- ```agda
        --   module M where private X = Set
        --   module N = M using (X)
        -- ```
        -- Further, modules (N) need not copy private things (X) from other
        -- modules (M) ever, since they cannot legally referred to
        -- (neither through qualification (N.X) nor open N).
        -- Thus, we can unconditionally remove private definitions
        -- before we apply the import directive.
        scope :: Scope
    scope = Scope -> Scope
    restrictPrivate Scope
    scope0

        -- Return names in the @using@ directive, discarding duplicates.
        -- Monadic for the sake of throwing warnings.
        discardDuplicatesInUsing :: C.Using -> ScopeM [C.ImportedName]
        discardDuplicatesInUsing :: Using' Name Name -> ScopeM [ImportedName]
    discardDuplicatesInUsing = \case
          Using' Name Name
    UseEverything -> [ImportedName] -> ScopeM [ImportedName]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
          Using  [ImportedName]
    xs     -> do
            let ([ImportedName]
    ys, [ImportedName]
    dups) = (ImportedName -> ImportedName)
    -> [ImportedName] -> ([ImportedName], [ImportedName])
    forall b a. Ord b => (a -> b) -> [a] -> ([a], [a])
    nubAndDuplicatesOn ImportedName -> ImportedName
    forall a. a -> a
    id [ImportedName]
    xs
            [ImportedName] -> (List1 ImportedName -> TCMT IO ()) -> TCMT IO ()
    forall m a. Null m => [a] -> (List1 a -> m) -> m
    List1.unlessNull [ImportedName]
    dups ((List1 ImportedName -> TCMT IO ()) -> TCMT IO ())
    -> (List1 ImportedName -> TCMT IO ()) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Warning -> TCMT IO ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCMT IO ())
    -> (List1 ImportedName -> Warning)
    -> List1 ImportedName
    -> TCMT IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 ImportedName -> Warning
    DuplicateUsing
            [ImportedName] -> ScopeM [ImportedName]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ImportedName]
    ys

        -- If both @using@ and @hiding@ directive are present,
        -- the hiding directive may only contain modules whose twins are mentioned.
        -- Monadic for the sake of error reporting.
        sanityCheck :: (ImportedName' Name m -> Bool)
    -> ImportDirective -> m ImportDirective
    sanityCheck ImportedName' Name m -> Bool
    notMentioned = \case
          dir :: ImportDirective
    dir@(ImportDirective{ using :: forall n m. ImportDirective' n m -> Using' n m
    using = Using{}, hiding :: forall n m. ImportDirective' n m -> HidingDirective' n m
    hiding = [ImportedName]
    ys }) -> do
              let useless :: ImportedName -> Bool
    useless = \case
                    ImportedName{}   -> Bool
    True
                    ImportedModule Name
    y -> ImportedName' Name m -> Bool
    notMentioned (Name -> ImportedName' Name m
    forall n m. n -> ImportedName' n m
    ImportedName Name
    y)
              [ImportedName] -> ([ImportedName] -> m ()) -> m ()
    forall (m :: * -> *) a.
    (Monad m, Null a) =>
    a -> (a -> m ()) -> m ()
    unlessNull ((ImportedName -> Bool) -> [ImportedName] -> [ImportedName]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ImportedName -> Bool
    useless [ImportedName]
    ys) (([ImportedName] -> m ()) -> m ())
    -> ([ImportedName] -> m ()) -> m ()
    forall a b. (a -> b) -> a -> b
    $ Warning -> m ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> m ())
    -> ([ImportedName] -> Warning) -> [ImportedName] -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [ImportedName] -> Warning
    UselessHiding
              -- We can empty @hiding@ now, since there is an explicit @using@ directive
              -- and @hiding@ served its purpose to prevent modules to enter the @Using@ list.
              ImportDirective -> m ImportDirective
    forall (m :: * -> *) a. Monad m => a -> m a
    return ImportDirective
    dir{ hiding :: [ImportedName]
    hiding = [] }
          ImportDirective
    dir -> ImportDirective -> m ImportDirective
    forall (m :: * -> *) a. Monad m => a -> m a
    return ImportDirective
    dir

        addExtraModules :: (C.Name -> Bool) -> C.ImportDirective -> C.ImportDirective
        addExtraModules :: (Name -> Bool) -> ImportDirective -> ImportDirective
    addExtraModules Name -> Bool
    extra ImportDirective
    dir =
          ImportDirective
    dir{ using :: Using' Name Name
    using       = ([ImportedName] -> [ImportedName])
    -> Using' Name Name -> Using' Name Name
    forall n1 m1 n2 m2.
    ([ImportedName' n1 m1] -> [ImportedName' n2 m2])
    -> Using' n1 m1 -> Using' n2 m2
    mapUsing ((ImportedName -> [ImportedName])
    -> [ImportedName] -> [ImportedName]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap ImportedName -> [ImportedName]
    addExtra) (Using' Name Name -> Using' Name Name)
    -> Using' Name Name -> Using' Name Name
    forall a b. (a -> b) -> a -> b
    $ ImportDirective -> Using' Name Name
    forall n m. ImportDirective' n m -> Using' n m
    using ImportDirective
    dir
             , hiding :: [ImportedName]
    hiding      = (ImportedName -> [ImportedName])
    -> [ImportedName] -> [ImportedName]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap ImportedName -> [ImportedName]
    addExtra            ([ImportedName] -> [ImportedName])
    -> [ImportedName] -> [ImportedName]
    forall a b. (a -> b) -> a -> b
    $ ImportDirective -> [ImportedName]
    forall n m. ImportDirective' n m -> HidingDirective' n m
    hiding ImportDirective
    dir
             , impRenaming :: [Renaming]
    impRenaming = (Renaming -> [Renaming]) -> [Renaming] -> [Renaming]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Renaming -> [Renaming]
    extraRenaming       ([Renaming] -> [Renaming]) -> [Renaming] -> [Renaming]
    forall a b. (a -> b) -> a -> b
    $ ImportDirective -> [Renaming]
    forall n m. ImportDirective' n m -> RenamingDirective' n m
    impRenaming ImportDirective
    dir
             }
          where
            addExtra :: ImportedName -> [ImportedName]
    addExtra f :: ImportedName
    f@(ImportedName Name
    y) | Name -> Bool
    extra Name
    y = [ImportedName
    f, Name -> ImportedName
    forall n m. m -> ImportedName' n m
    ImportedModule Name
    y]
            addExtra ImportedName
    m = [ImportedName
    m]

            extraRenaming :: Renaming -> [Renaming]
    extraRenaming = \case
              r :: Renaming
    r@(Renaming (ImportedName Name
    y) (ImportedName Name
    z) Maybe Fixity
    _fixity Range
    rng) | Name -> Bool
    extra Name
    y ->
                 [ Renaming
    r , ImportedName -> ImportedName -> Maybe Fixity -> Range -> Renaming
    forall n m.
    ImportedName' n m
    -> ImportedName' n m -> Maybe Fixity -> Range -> Renaming' n m
    Renaming (Name -> ImportedName
    forall n m. m -> ImportedName' n m
    ImportedModule Name
    y) (Name -> ImportedName
    forall n m. m -> ImportedName' n m
    ImportedModule Name
    z) Maybe Fixity
    forall a. Maybe a
    Nothing Range
    rng ]
              Renaming
    r -> [Renaming
    r]

        -- Names and modules (abstract) in scope before the import.
        namesInScope :: NamesInScope
    namesInScope   = (Scope -> NamesInScope
    forall a. InScope a => Scope -> ThingsInScope a
    allNamesInScope Scope
    scope :: ThingsInScope AbstractName)
        modulesInScope :: ModulesInScope
    modulesInScope = (Scope -> ModulesInScope
    forall a. InScope a => Scope -> ThingsInScope a
    allNamesInScope Scope
    scope :: ThingsInScope AbstractModule)
        concreteNamesInScope :: [Name]
    concreteNamesInScope = (NamesInScope -> [Name]
    forall k a. Map k a -> [k]
    Map.keys NamesInScope
    namesInScope [Name] -> [Name] -> [Name]
    forall a. [a] -> [a] -> [a]
    ++ ModulesInScope -> [Name]
    forall k a. Map k a -> [k]
    Map.keys ModulesInScope
    modulesInScope :: [C.Name])

        -- AST versions of the concrete names passed as an argument.
        -- We get back a pair consisting of a list of missing exports first,
        -- and a list of successful imports second.
        checkExist :: [ImportedName] -> ([ImportedName], [ImportedName' (C.Name, A.QName) (C.Name, A.ModuleName)])
        checkExist :: [ImportedName]
    -> ([ImportedName],
        [ImportedName' (Name, QName) (Name, ModuleName)])
    checkExist [ImportedName]
    xs = [Either
       ImportedName (ImportedName' (Name, QName) (Name, ModuleName))]
    -> ([ImportedName],
        [ImportedName' (Name, QName) (Name, ModuleName)])
    forall a b. [Either a b] -> ([a], [b])
    partitionEithers ([Either
        ImportedName (ImportedName' (Name, QName) (Name, ModuleName))]
     -> ([ImportedName],
         [ImportedName' (Name, QName) (Name, ModuleName)]))
    -> [Either
          ImportedName (ImportedName' (Name, QName) (Name, ModuleName))]
    -> ([ImportedName],
        [ImportedName' (Name, QName) (Name, ModuleName)])
    forall a b. (a -> b) -> a -> b
    $ [ImportedName]
    -> (ImportedName
        -> Either
             ImportedName (ImportedName' (Name, QName) (Name, ModuleName)))
    -> [Either
          ImportedName (ImportedName' (Name, QName) (Name, ModuleName))]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for [ImportedName]
    xs ((ImportedName
      -> Either
           ImportedName (ImportedName' (Name, QName) (Name, ModuleName)))
     -> [Either
           ImportedName (ImportedName' (Name, QName) (Name, ModuleName))])
    -> (ImportedName
        -> Either
             ImportedName (ImportedName' (Name, QName) (Name, ModuleName)))
    -> [Either
          ImportedName (ImportedName' (Name, QName) (Name, ModuleName))]
    forall a b. (a -> b) -> a -> b
    $ \ ImportedName
    name -> case ImportedName
    name of
          ImportedName Name
    x   -> (Name, QName) -> ImportedName' (Name, QName) (Name, ModuleName)
    forall n m. n -> ImportedName' n m
    ImportedName   ((Name, QName) -> ImportedName' (Name, QName) (Name, ModuleName))
    -> (AbstractName -> (Name, QName))
    -> AbstractName
    -> ImportedName' (Name, QName) (Name, ModuleName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name
    x,) (QName -> (Name, QName))
    -> (AbstractName -> QName) -> AbstractName -> (Name, QName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Range -> QName -> QName
    forall a. SetRange a => Range -> a -> a
    setRange (Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    x) (QName -> QName)
    -> (AbstractName -> QName) -> AbstractName -> QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbstractName -> QName
    anameName (AbstractName -> ImportedName' (Name, QName) (Name, ModuleName))
    -> Either ImportedName AbstractName
    -> Either
         ImportedName (ImportedName' (Name, QName) (Name, ModuleName))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ImportedName
    -> Name -> NamesInScope -> Either ImportedName AbstractName
    forall a err b. Ord a => err -> a -> Map a [b] -> Either err b
    resolve ImportedName
    name Name
    x NamesInScope
    namesInScope
          ImportedModule Name
    x -> (Name, ModuleName)
    -> ImportedName' (Name, QName) (Name, ModuleName)
    forall n m. m -> ImportedName' n m
    ImportedModule ((Name, ModuleName)
     -> ImportedName' (Name, QName) (Name, ModuleName))
    -> (AbstractModule -> (Name, ModuleName))
    -> AbstractModule
    -> ImportedName' (Name, QName) (Name, ModuleName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name
    x,) (ModuleName -> (Name, ModuleName))
    -> (AbstractModule -> ModuleName)
    -> AbstractModule
    -> (Name, ModuleName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Range -> ModuleName -> ModuleName
    forall a. SetRange a => Range -> a -> a
    setRange (Name -> Range
    forall a. HasRange a => a -> Range
    getRange Name
    x) (ModuleName -> ModuleName)
    -> (AbstractModule -> ModuleName) -> AbstractModule -> ModuleName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbstractModule -> ModuleName
    amodName  (AbstractModule -> ImportedName' (Name, QName) (Name, ModuleName))
    -> Either ImportedName AbstractModule
    -> Either
         ImportedName (ImportedName' (Name, QName) (Name, ModuleName))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ImportedName
    -> Name -> ModulesInScope -> Either ImportedName AbstractModule
    forall a err b. Ord a => err -> a -> Map a [b] -> Either err b
    resolve ImportedName
    name Name
    x ModulesInScope
    modulesInScope

          where resolve :: Ord a => err -> a -> Map a [b] -> Either err b
                resolve :: forall a err b. Ord a => err -> a -> Map a [b] -> Either err b
    resolve err
    err a
    x Map a [b]
    m = Either err b -> ([b] -> Either err b) -> Maybe [b] -> Either err b
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (err -> Either err b
    forall a b. a -> Either a b
    Left err
    err) (b -> Either err b
    forall a b. b -> Either a b
    Right (b -> Either err b) -> ([b] -> b) -> [b] -> Either err b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [b] -> b
    forall a. [a] -> a
    head) (Maybe [b] -> Either err b) -> Maybe [b] -> Either err b
    forall a b. (a -> b) -> a -> b
    $ a -> Map a [b] -> Maybe [b]
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup a
    x Map a [b]
    m

    -- | Translation of @ImportDirective@.
    mapImportDir
      :: (Ord n1, Ord m1)
      => [ImportedName' (n1,n2) (m1,m2)]  -- ^ Translation of imported names.
      -> [ImportedName' (n1,n2) (m1,m2)]  -- ^ Translation of names defined by this import.
      -> ImportDirective' n1 m1
      -> ImportDirective' n2 m2
    mapImportDir :: forall n1 m1 n2 m2.
    (Ord n1, Ord m1) =>
    [ImportedName' (n1, n2) (m1, m2)]
    -> [ImportedName' (n1, n2) (m1, m2)]
    -> ImportDirective' n1 m1
    -> ImportDirective' n2 m2
    mapImportDir [ImportedName' (n1, n2) (m1, m2)]
    src0 [ImportedName' (n1, n2) (m1, m2)]
    tgt0 (ImportDirective Range
    r Using' n1 m1
    u HidingDirective' n1 m1
    h RenamingDirective' n1 m1
    ren Maybe Range
    open) =
      Range
    -> Using' n2 m2
    -> HidingDirective' n2 m2
    -> RenamingDirective' n2 m2
    -> Maybe Range
    -> ImportDirective' n2 m2
    forall n m.
    Range
    -> Using' n m
    -> HidingDirective' n m
    -> RenamingDirective' n m
    -> Maybe Range
    -> ImportDirective' n m
    ImportDirective Range
    r
        ((HidingDirective' n1 m1 -> HidingDirective' n2 m2)
    -> Using' n1 m1 -> Using' n2 m2
    forall n1 m1 n2 m2.
    ([ImportedName' n1 m1] -> [ImportedName' n2 m2])
    -> Using' n1 m1 -> Using' n2 m2
    mapUsing ((ImportedName' n1 m1 -> ImportedName' n2 m2)
    -> HidingDirective' n1 m1 -> HidingDirective' n2 m2
    forall a b. (a -> b) -> [a] -> [b]
    map (ImportedNameMap n1 n2 m1 m2
    -> ImportedName' n1 m1 -> ImportedName' n2 m2
    forall n1 m1 n2 m2.
    (Ord n1, Ord m1) =>
    ImportedNameMap n1 n2 m1 m2
    -> ImportedName' n1 m1 -> ImportedName' n2 m2
    lookupImportedName ImportedNameMap n1 n2 m1 m2
    src)) Using' n1 m1
    u)
        ((ImportedName' n1 m1 -> ImportedName' n2 m2)
    -> HidingDirective' n1 m1 -> HidingDirective' n2 m2
    forall a b. (a -> b) -> [a] -> [b]
    map (ImportedNameMap n1 n2 m1 m2
    -> ImportedName' n1 m1 -> ImportedName' n2 m2
    forall n1 m1 n2 m2.
    (Ord n1, Ord m1) =>
    ImportedNameMap n1 n2 m1 m2
    -> ImportedName' n1 m1 -> ImportedName' n2 m2
    lookupImportedName ImportedNameMap n1 n2 m1 m2
    src) HidingDirective' n1 m1
    h)
        ((Renaming' n1 m1 -> Renaming' n2 m2)
    -> RenamingDirective' n1 m1 -> RenamingDirective' n2 m2
    forall a b. (a -> b) -> [a] -> [b]
    map (ImportedNameMap n1 n2 m1 m2
    -> ImportedNameMap n1 n2 m1 m2
    -> Renaming' n1 m1
    -> Renaming' n2 m2
    forall n1 m1 n2 m2.
    (Ord n1, Ord m1) =>
    ImportedNameMap n1 n2 m1 m2
    -> ImportedNameMap n1 n2 m1 m2
    -> Renaming' n1 m1
    -> Renaming' n2 m2
    mapRenaming ImportedNameMap n1 n2 m1 m2
    src ImportedNameMap n1 n2 m1 m2
    tgt) RenamingDirective' n1 m1
    ren)
        Maybe Range
    open
      where
      src :: ImportedNameMap n1 n2 m1 m2
    src = [ImportedName' (n1, n2) (m1, m2)] -> ImportedNameMap n1 n2 m1 m2
    forall n1 m1 n2 m2.
    (Ord n1, Ord m1) =>
    [ImportedName' (n1, n2) (m1, m2)] -> ImportedNameMap n1 n2 m1 m2
    importedNameMapFromList [ImportedName' (n1, n2) (m1, m2)]
    src0
      tgt :: ImportedNameMap n1 n2 m1 m2
    tgt = [ImportedName' (n1, n2) (m1, m2)] -> ImportedNameMap n1 n2 m1 m2
    forall n1 m1 n2 m2.
    (Ord n1, Ord m1) =>
    [ImportedName' (n1, n2) (m1, m2)] -> ImportedNameMap n1 n2 m1 m2
    importedNameMapFromList [ImportedName' (n1, n2) (m1, m2)]
    tgt0

    -- | A finite map for @ImportedName@s.

    data ImportedNameMap n1 n2 m1 m2 = ImportedNameMap
      { forall n1 n2 m1 m2. ImportedNameMap n1 n2 m1 m2 -> Map n1 n2
    inameMap   :: Map n1 n2
      , forall n1 n2 m1 m2. ImportedNameMap n1 n2 m1 m2 -> Map m1 m2
    imoduleMap :: Map m1 m2
      }

    -- | Create a 'ImportedNameMap'.
    importedNameMapFromList
      :: (Ord n1, Ord m1)
      => [ImportedName' (n1,n2) (m1,m2)]
      -> ImportedNameMap n1 n2 m1 m2
    importedNameMapFromList :: forall n1 m1 n2 m2.
    (Ord n1, Ord m1) =>
    [ImportedName' (n1, n2) (m1, m2)] -> ImportedNameMap n1 n2 m1 m2
    importedNameMapFromList = (ImportedName' (n1, n2) (m1, m2)
     -> ImportedNameMap n1 n2 m1 m2 -> ImportedNameMap n1 n2 m1 m2)
    -> ImportedNameMap n1 n2 m1 m2
    -> [ImportedName' (n1, n2) (m1, m2)]
    -> ImportedNameMap n1 n2 m1 m2
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr ((ImportedNameMap n1 n2 m1 m2
     -> ImportedName' (n1, n2) (m1, m2) -> ImportedNameMap n1 n2 m1 m2)
    -> ImportedName' (n1, n2) (m1, m2)
    -> ImportedNameMap n1 n2 m1 m2
    -> ImportedNameMap n1 n2 m1 m2
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip ImportedNameMap n1 n2 m1 m2
    -> ImportedName' (n1, n2) (m1, m2) -> ImportedNameMap n1 n2 m1 m2
    forall {n1} {m1} {n2} {m2}.
    (Ord n1, Ord m1) =>
    ImportedNameMap n1 n2 m1 m2
    -> ImportedName' (n1, n2) (m1, m2) -> ImportedNameMap n1 n2 m1 m2
    add) (ImportedNameMap n1 n2 m1 m2
     -> [ImportedName' (n1, n2) (m1, m2)]
     -> ImportedNameMap n1 n2 m1 m2)
    -> ImportedNameMap n1 n2 m1 m2
    -> [ImportedName' (n1, n2) (m1, m2)]
    -> ImportedNameMap n1 n2 m1 m2
    forall a b. (a -> b) -> a -> b
    $ Map n1 n2 -> Map m1 m2 -> ImportedNameMap n1 n2 m1 m2
    forall n1 n2 m1 m2.
    Map n1 n2 -> Map m1 m2 -> ImportedNameMap n1 n2 m1 m2
    ImportedNameMap Map n1 n2
    forall k a. Map k a
    Map.empty Map m1 m2
    forall k a. Map k a
    Map.empty
      where
      add :: ImportedNameMap n1 n2 m1 m2
    -> ImportedName' (n1, n2) (m1, m2) -> ImportedNameMap n1 n2 m1 m2
    add (ImportedNameMap Map n1 n2
    nm Map m1 m2
    mm) = \case
        ImportedName   (n1
    x,n2
    y) -> Map n1 n2 -> Map m1 m2 -> ImportedNameMap n1 n2 m1 m2
    forall n1 n2 m1 m2.
    Map n1 n2 -> Map m1 m2 -> ImportedNameMap n1 n2 m1 m2
    ImportedNameMap (n1 -> n2 -> Map n1 n2 -> Map n1 n2
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert n1
    x n2
    y Map n1 n2
    nm) Map m1 m2
    mm
        ImportedModule (m1
    x,m2
    y) -> Map n1 n2 -> Map m1 m2 -> ImportedNameMap n1 n2 m1 m2
    forall n1 n2 m1 m2.
    Map n1 n2 -> Map m1 m2 -> ImportedNameMap n1 n2 m1 m2
    ImportedNameMap Map n1 n2
    nm (m1 -> m2 -> Map m1 m2 -> Map m1 m2
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert m1
    x m2
    y Map m1 m2
    mm)

    -- | Apply a 'ImportedNameMap'.
    lookupImportedName
      :: (Ord n1, Ord m1)
      => ImportedNameMap n1 n2 m1 m2
      -> ImportedName' n1 m1
      -> ImportedName' n2 m2
    lookupImportedName :: forall n1 m1 n2 m2.
    (Ord n1, Ord m1) =>
    ImportedNameMap n1 n2 m1 m2
    -> ImportedName' n1 m1 -> ImportedName' n2 m2
    lookupImportedName (ImportedNameMap Map n1 n2
    nm Map m1 m2
    mm) = \case
        ImportedName   n1
    x -> n2 -> ImportedName' n2 m2
    forall n m. n -> ImportedName' n m
    ImportedName   (n2 -> ImportedName' n2 m2) -> n2 -> ImportedName' n2 m2
    forall a b. (a -> b) -> a -> b
    $ n2 -> n1 -> Map n1 n2 -> n2
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault n2
    forall a. HasCallStack => a
    __IMPOSSIBLE__ n1
    x Map n1 n2
    nm
        ImportedModule m1
    x -> m2 -> ImportedName' n2 m2
    forall n m. m -> ImportedName' n m
    ImportedModule (m2 -> ImportedName' n2 m2) -> m2 -> ImportedName' n2 m2
    forall a b. (a -> b) -> a -> b
    $ m2 -> m1 -> Map m1 m2 -> m2
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault m2
    forall a. HasCallStack => a
    __IMPOSSIBLE__ m1
    x Map m1 m2
    mm

    -- | Translation of @Renaming@.
    mapRenaming
      ::  (Ord n1, Ord m1)
      => ImportedNameMap n1 n2 m1 m2  -- ^ Translation of 'renFrom' names and module names.
      -> ImportedNameMap n1 n2 m1 m2  -- ^ Translation of 'rento'   names and module names.
      -> Renaming' n1 m1  -- ^ Renaming before translation (1).
      -> Renaming' n2 m2  -- ^ Renaming after  translation (2).
    mapRenaming :: forall n1 m1 n2 m2.
    (Ord n1, Ord m1) =>
    ImportedNameMap n1 n2 m1 m2
    -> ImportedNameMap n1 n2 m1 m2
    -> Renaming' n1 m1
    -> Renaming' n2 m2
    mapRenaming ImportedNameMap n1 n2 m1 m2
    src ImportedNameMap n1 n2 m1 m2
    tgt (Renaming ImportedName' n1 m1
    from ImportedName' n1 m1
    to Maybe Fixity
    fixity Range
    r) =
      ImportedName' n2 m2
    -> ImportedName' n2 m2 -> Maybe Fixity -> Range -> Renaming' n2 m2
    forall n m.
    ImportedName' n m
    -> ImportedName' n m -> Maybe Fixity -> Range -> Renaming' n m
    Renaming (ImportedNameMap n1 n2 m1 m2
    -> ImportedName' n1 m1 -> ImportedName' n2 m2
    forall n1 m1 n2 m2.
    (Ord n1, Ord m1) =>
    ImportedNameMap n1 n2 m1 m2
    -> ImportedName' n1 m1 -> ImportedName' n2 m2
    lookupImportedName ImportedNameMap n1 n2 m1 m2
    src ImportedName' n1 m1
    from) (ImportedNameMap n1 n2 m1 m2
    -> ImportedName' n1 m1 -> ImportedName' n2 m2
    forall n1 m1 n2 m2.
    (Ord n1, Ord m1) =>
    ImportedNameMap n1 n2 m1 m2
    -> ImportedName' n1 m1 -> ImportedName' n2 m2
    lookupImportedName ImportedNameMap n1 n2 m1 m2
    tgt ImportedName' n1 m1
    to) Maybe Fixity
    fixity Range
    r

    ---------------------------------------------------------------------------
    -- * Opening a module
    ---------------------------------------------------------------------------

    data OpenKind = LetOpenModule | TopOpenModule

    noGeneralizedVarsIfLetOpen :: OpenKind -> Scope -> Scope
    noGeneralizedVarsIfLetOpen :: OpenKind -> Scope -> Scope
    noGeneralizedVarsIfLetOpen OpenKind
    TopOpenModule = Scope -> Scope
    forall a. a -> a
    id
    noGeneralizedVarsIfLetOpen OpenKind
    LetOpenModule = Scope -> Scope
    disallowGeneralizedVars

    -- | Open a module.
    openModule_ :: OpenKind -> C.QName -> C.ImportDirective -> ScopeM A.ImportDirective
    openModule_ :: OpenKind -> QName -> ImportDirective -> ScopeM ImportDirective
    openModule_ OpenKind
    kind QName
    cm ImportDirective
    dir = OpenKind
    -> Maybe ModuleName
    -> QName
    -> ImportDirective
    -> ScopeM ImportDirective
    openModule OpenKind
    kind Maybe ModuleName
    forall a. Maybe a
    Nothing QName
    cm ImportDirective
    dir

    -- | Open a module, possibly given an already resolved module name.
    openModule :: OpenKind -> Maybe A.ModuleName  -> C.QName -> C.ImportDirective -> ScopeM A.ImportDirective
    openModule :: OpenKind
    -> Maybe ModuleName
    -> QName
    -> ImportDirective
    -> ScopeM ImportDirective
    openModule OpenKind
    kind Maybe ModuleName
    mam QName
    cm ImportDirective
    dir = do
      ModuleName
    current <- ScopeM ModuleName
    forall (m :: * -> *). ReadTCState m => m ModuleName
    getCurrentModule
      ModuleName
    m <- Maybe ModuleName
    -> ScopeM ModuleName
    -> (ModuleName -> ScopeM ModuleName)
    -> ScopeM ModuleName
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe ModuleName
    mam (AbstractModule -> ModuleName
    amodName (AbstractModule -> ModuleName)
    -> ScopeM AbstractModule -> ScopeM ModuleName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> ScopeM AbstractModule
    resolveModule QName
    cm) ModuleName -> ScopeM ModuleName
    forall (m :: * -> *) a. Monad m => a -> m a
    return
      let acc :: NameSpaceId
    acc | Maybe Range
    Nothing <- ImportDirective -> Maybe Range
    forall n m. ImportDirective' n m -> Maybe Range
    publicOpen ImportDirective
    dir     = NameSpaceId
    PrivateNS
              | ModuleName
    m ModuleName -> ModuleName -> Bool
    `isLtChildModuleOf` ModuleName
    current = NameSpaceId
    PublicNS
              | Bool
    otherwise                     = NameSpaceId
    ImportedNS

      -- Get the scope exported by module to be opened.
      (ImportDirective
    adir, Scope
    s') <- QName
    -> ImportDirective -> Scope -> ScopeM (ImportDirective, Scope)
    applyImportDirectiveM QName
    cm ImportDirective
    dir (Scope -> ScopeM (ImportDirective, Scope))
    -> (Scope -> Scope) -> Scope -> ScopeM (ImportDirective, Scope)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (WhyInScope -> WhyInScope) -> Scope -> Scope
    inScopeBecause (QName -> WhyInScope -> WhyInScope
    Opened QName
    cm) (Scope -> Scope) -> (Scope -> Scope) -> Scope -> Scope
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
                    OpenKind -> Scope -> Scope
    noGeneralizedVarsIfLetOpen OpenKind
    kind (Scope -> ScopeM (ImportDirective, Scope))
    -> ScopeM Scope -> ScopeM (ImportDirective, Scope)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ModuleName -> ScopeM Scope
    getNamedScope ModuleName
    m
      let s :: Scope
    s  = NameSpaceId -> Scope -> Scope
    setScopeAccess NameSpaceId
    acc Scope
    s'
      let ns :: NameSpace
    ns = NameSpaceId -> Scope -> NameSpace
    scopeNameSpace NameSpaceId
    acc Scope
    s
      (Scope -> Scope) -> TCMT IO ()
    modifyCurrentScope (Scope -> Scope -> Scope
    `mergeScope` Scope
    s)
      -- Andreas, 2018-06-03, issue #3057:
      -- If we simply check for ambiguous exported identifiers _after_
      -- importing the new identifiers into the current scope, we also
      -- catch the case of importing an ambiguous identifier.
      TCMT IO ()
    checkForClashes

      -- Importing names might shadow existing locals.
      [Char] -> Int -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
    verboseS [Char]
    "scope.locals" Int
    10 (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do
        [Name]
    locals <- ((Name, LocalVar) -> Maybe Name) -> LocalVars -> [Name]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (\ (Name
    c,LocalVar
    x) -> Name
    c Name -> Maybe Name -> Maybe Name
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ LocalVar -> Maybe Name
    notShadowedLocal LocalVar
    x) (LocalVars -> [Name]) -> TCMT IO LocalVars -> TCMT IO [Name]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO LocalVars
    forall (m :: * -> *). ReadTCState m => m LocalVars
    getLocalVars
        let newdefs :: [Name]
    newdefs = NamesInScope -> [Name]
    forall k a. Map k a -> [k]
    Map.keys (NamesInScope -> [Name]) -> NamesInScope -> [Name]
    forall a b. (a -> b) -> a -> b
    $ NameSpace -> NamesInScope
    nsNames NameSpace
    ns
            shadowed :: [Name]
    shadowed = [Name]
    locals [Name] -> [Name] -> [Name]
    forall a. Eq a => [a] -> [a] -> [a]
    `List.intersect` [Name]
    newdefs
        [Char] -> Int -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "scope.locals" Int
    10 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "opening module shadows the following locals vars: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Name] -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow [Name]
    shadowed
      -- Andreas, 2014-09-03, issue 1266: shadow local variables by imported defs.
      (LocalVars -> LocalVars) -> TCMT IO ()
    modifyLocalVars ((LocalVars -> LocalVars) -> TCMT IO ())
    -> (LocalVars -> LocalVars) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ (Name -> LocalVar -> LocalVar) -> LocalVars -> LocalVars
    forall k v. (k -> v -> v) -> AssocList k v -> AssocList k v
    AssocList.mapWithKey ((Name -> LocalVar -> LocalVar) -> LocalVars -> LocalVars)
    -> (Name -> LocalVar -> LocalVar) -> LocalVars -> LocalVars
    forall a b. (a -> b) -> a -> b
    $ \ Name
    c LocalVar
    x ->
        case Name -> NamesInScope -> Maybe [AbstractName]
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    c (NamesInScope -> Maybe [AbstractName])
    -> NamesInScope -> Maybe [AbstractName]
    forall a b. (a -> b) -> a -> b
    $ NameSpace -> NamesInScope
    nsNames NameSpace
    ns of
          Maybe [AbstractName]
    Nothing -> LocalVar
    x
          Just [AbstractName]
    ys -> [AbstractName] -> LocalVar -> LocalVar
    shadowLocal [AbstractName]
    ys LocalVar
    x

      ImportDirective -> ScopeM ImportDirective
    forall (m :: * -> *) a. Monad m => a -> m a
    return ImportDirective
    adir

      where
        -- Only checks for clashes that would lead to the same
        -- name being exported twice from the module.
        checkForClashes :: TCMT IO ()
    checkForClashes = Bool -> TCMT IO () -> TCMT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Maybe Range -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe Range -> Bool) -> Maybe Range -> Bool
    forall a b. (a -> b) -> a -> b
    $ ImportDirective -> Maybe Range
    forall n m. ImportDirective' n m -> Maybe Range
    publicOpen ImportDirective
    dir) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do

            NameSpace
    exported <- Scope -> NameSpace
    allThingsInScope (Scope -> NameSpace) -> (Scope -> Scope) -> Scope -> NameSpace
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Scope -> Scope
    restrictPrivate (Scope -> NameSpace) -> ScopeM Scope -> TCMT IO NameSpace
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (ModuleName -> ScopeM Scope
    getNamedScope (ModuleName -> ScopeM Scope) -> ScopeM ModuleName -> ScopeM Scope
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ScopeM ModuleName
    forall (m :: * -> *). ReadTCState m => m ModuleName
    getCurrentModule)

            -- Get all exported concrete names that are mapped to at least 2 abstract names
            let defClashes :: [(Name, [AbstractName])]
    defClashes = ((Name, [AbstractName]) -> Bool)
    -> [(Name, [AbstractName])] -> [(Name, [AbstractName])]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (\ (Name
    _c, [AbstractName]
    as) -> [AbstractName] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [AbstractName]
    as Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    2) ([(Name, [AbstractName])] -> [(Name, [AbstractName])])
    -> [(Name, [AbstractName])] -> [(Name, [AbstractName])]
    forall a b. (a -> b) -> a -> b
    $ NamesInScope -> [(Name, [AbstractName])]
    forall k a. Map k a -> [(k, a)]
    Map.toList (NamesInScope -> [(Name, [AbstractName])])
    -> NamesInScope -> [(Name, [AbstractName])]
    forall a b. (a -> b) -> a -> b
    $ NameSpace -> NamesInScope
    nsNames NameSpace
    exported
                modClashes :: [(Name, [AbstractModule])]
    modClashes = ((Name, [AbstractModule]) -> Bool)
    -> [(Name, [AbstractModule])] -> [(Name, [AbstractModule])]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (\ (Name
    _c, [AbstractModule]
    as) -> [AbstractModule] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [AbstractModule]
    as Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    2) ([(Name, [AbstractModule])] -> [(Name, [AbstractModule])])
    -> [(Name, [AbstractModule])] -> [(Name, [AbstractModule])]
    forall a b. (a -> b) -> a -> b
    $ ModulesInScope -> [(Name, [AbstractModule])]
    forall k a. Map k a -> [(k, a)]
    Map.toList (ModulesInScope -> [(Name, [AbstractModule])])
    -> ModulesInScope -> [(Name, [AbstractModule])]
    forall a b. (a -> b) -> a -> b
    $ NameSpace -> ModulesInScope
    nsModules NameSpace
    exported

                -- No ambiguity if concrete identifier is only mapped to
                -- constructor names or only to projection names.
                defClash :: (a, [AbstractName]) -> Bool
    defClash (a
    _, [AbstractName]
    qs) = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ (KindOfName -> Bool) -> [KindOfName] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Maybe Induction -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe Induction -> Bool)
    -> (KindOfName -> Maybe Induction) -> KindOfName -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . KindOfName -> Maybe Induction
    isConName) [KindOfName]
    ks Bool -> Bool -> Bool
    || (KindOfName -> Bool) -> [KindOfName] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (KindOfName -> KindOfName -> Bool
    forall a. Eq a => a -> a -> Bool
    ==KindOfName
    FldName) [KindOfName]
    ks
                  where ks :: [KindOfName]
    ks = (AbstractName -> KindOfName) -> [AbstractName] -> [KindOfName]
    forall a b. (a -> b) -> [a] -> [b]
    map AbstractName -> KindOfName
    anameKind [AbstractName]
    qs
            -- We report the first clashing exported identifier.
            [(Name, [AbstractName])]
    -> ([(Name, [AbstractName])] -> TCMT IO ()) -> TCMT IO ()
    forall (m :: * -> *) a.
    (Monad m, Null a) =>
    a -> (a -> m ()) -> m ()
    unlessNull (((Name, [AbstractName]) -> Bool)
    -> [(Name, [AbstractName])] -> [(Name, [AbstractName])]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (\ (Name, [AbstractName])
    x -> (Name, [AbstractName]) -> Bool
    forall {a}. (a, [AbstractName]) -> Bool
    defClash (Name, [AbstractName])
    x) [(Name, [AbstractName])]
    defClashes) (([(Name, [AbstractName])] -> TCMT IO ()) -> TCMT IO ())
    -> ([(Name, [AbstractName])] -> TCMT IO ()) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
              \ ((Name
    x, AbstractName
    q:[AbstractName]
    _) : [(Name, [AbstractName])]
    _) -> 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
    $ QName -> QName -> Maybe NiceDeclaration -> TypeError
    ClashingDefinition (Name -> QName
    C.QName Name
    x) (AbstractName -> QName
    anameName AbstractName
    q) Maybe NiceDeclaration
    forall a. Maybe a
    Nothing

            [(Name, [AbstractModule])]
    -> ([(Name, [AbstractModule])] -> TCMT IO ()) -> TCMT IO ()
    forall (m :: * -> *) a.
    (Monad m, Null a) =>
    a -> (a -> m ()) -> m ()
    unlessNull [(Name, [AbstractModule])]
    modClashes (([(Name, [AbstractModule])] -> TCMT IO ()) -> TCMT IO ())
    -> ([(Name, [AbstractModule])] -> TCMT IO ()) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ \ ((Name
    _, [AbstractModule]
    ms) : [(Name, [AbstractModule])]
    _) -> do
              Maybe (AbstractModule, AbstractModule)
    -> TCMT IO ()
    -> ((AbstractModule, AbstractModule) -> TCMT IO ())
    -> TCMT IO ()
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe ([AbstractModule] -> Maybe (AbstractModule, AbstractModule)
    forall a. [a] -> Maybe (a, a)
    last2 [AbstractModule]
    ms) TCMT IO ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (((AbstractModule, AbstractModule) -> TCMT IO ()) -> TCMT IO ())
    -> ((AbstractModule, AbstractModule) -> TCMT IO ()) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ \ (AbstractModule
    m0, AbstractModule
    m1) -> do
                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
    $ ModuleName -> ModuleName -> TypeError
    ClashingModule (AbstractModule -> ModuleName
    amodName AbstractModule
    m0) (AbstractModule -> ModuleName
    amodName AbstractModule
    m1)