    {-# LANGUAGE NondecreasingIndentation #-}

    {-| The scope monad with operations.
    -}

    module Agda.Syntax.Scope.Monad where

    import Prelude hiding (null)

    import Control.Arrow ((***))
    import Control.Monad.Except       ( MonadError, throwError, runExceptT )
    import Control.Monad.State        ( StateT, runStateT, gets, modify )
    import Control.Monad.Trans        ( MonadTrans, lift )
    import Control.Monad.Trans.Maybe  ( MaybeT(MaybeT), runMaybeT )
    import Control.Applicative

    import Data.Either ( partitionEithers )
    import Data.Foldable (all, traverse_)
    import qualified Data.List as List
    import Data.Map (Map)
    import qualified Data.HashMap.Strict as HMap
    import qualified Data.HashSet as HSet
    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.Common.Pretty
    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 as I
    import Agda.TypeChecking.Monad.Builtin
      ( HasBuiltins, getBuiltinName'
      , builtinProp, builtinSet, builtinStrictSet, builtinPropOmega, builtinSetOmega, builtinSSetOmega )
    import Agda.TypeChecking.Monad.Debug
    import Agda.TypeChecking.Monad.State
    import Agda.TypeChecking.Monad.Trace
    import Agda.TypeChecking.Positivity.Occurrence ( PragmaPolarities, 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, toList)
    import Agda.Utils.List2 (List2(List2), toList)
    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.Set1 ( Set1 )
    import qualified Agda.Utils.Set1 as Set1
    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] -> ScopeM ()
    printLocals Int
    v [Char]
    s = [Char] -> Int -> ScopeM () -> ScopeM ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
    verboseS [Char]
    "scope.top" Int
    v (ScopeM () -> ScopeM ()) -> ScopeM () -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $ do
      locals <- TCMT IO LocalVars
    forall (m :: * -> *). ReadTCState m => m LocalVars
    getLocalVars
      reportSLn "scope.top" v $ s ++ " " ++ prettyShow locals

    scopeWarning' :: CallStack -> DeclarationWarning' -> ScopeM ()
    scopeWarning' :: CallStack -> DeclarationWarning' -> ScopeM ()
    scopeWarning' CallStack
    loc = CallStack -> Warning -> ScopeM ()
    forall (m :: * -> *).
    MonadWarning m =>
    CallStack -> Warning -> m ()
    warning' CallStack
    loc (Warning -> ScopeM ())
    -> (DeclarationWarning' -> Warning)
    -> DeclarationWarning'
    -> ScopeM ()
    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' -> ScopeM ()
    scopeWarning = (CallStack -> DeclarationWarning' -> ScopeM ())
    -> DeclarationWarning' -> ScopeM ()
    forall b. HasCallStack => (CallStack -> b) -> b
    withCallerCallStack CallStack -> DeclarationWarning' -> ScopeM ()
    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' ScopeInfo (Map ModuleName Scope) -> m (Map ModuleName Scope)
    forall (m :: * -> *) a. ReadTCState m => Lens' ScopeInfo a -> m a
    useScope (Map ModuleName Scope -> f (Map ModuleName Scope))
    -> ScopeInfo -> f ScopeInfo
    Lens' ScopeInfo (Map ModuleName Scope)
    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' ScopeInfo ModuleName -> m ModuleName
    forall (m :: * -> *) a. ReadTCState m => Lens' ScopeInfo a -> m a
    useScope (ModuleName -> f ModuleName) -> ScopeInfo -> f ScopeInfo
    Lens' ScopeInfo ModuleName
    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' ScopeInfo ModuleName -> LensSet ScopeInfo ModuleName
    forall o i. Lens' o i -> LensSet o i
    set (ModuleName -> f ModuleName) -> ScopeInfo -> f ScopeInfo
    Lens' ScopeInfo ModuleName
    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
      old <- m ModuleName
    forall (m :: * -> *). ReadTCState m => m ModuleName
    getCurrentModule
      setCurrentModule new
      x   <- action
      setCurrentModule old
      return 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
      old <- ScopeM ModuleName -> t (TCMT IO) ModuleName
    forall (m :: * -> *) a. Monad m => m a -> t m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift ScopeM ModuleName
    forall (m :: * -> *). ReadTCState m => m ModuleName
    getCurrentModule
      lift $ setCurrentModule new
      x   <- action
      lift $ setCurrentModule old
      return x

    getNamedScope :: A.ModuleName -> ScopeM Scope
    getNamedScope :: ModuleName -> ScopeM Scope
    getNamedScope ModuleName
    m = do
      scope <- TCMT IO ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope
      case Map.lookup m (scope ^. scopeModules) of
        Just Scope
    s  -> Scope -> ScopeM Scope
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Scope
    s
        Maybe Scope
    Nothing -> do
          [Char] -> Int -> [Char] -> ScopeM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "" Int
    0 ([Char] -> ScopeM ()) -> [Char] -> ScopeM ()
    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 -> ScopeM ()
    createModule Maybe DataOrRecordModule
    b ModuleName
    m = do
      [Char] -> Int -> [Char] -> ScopeM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "scope.createModule" Int
    30 ([Char] -> ScopeM ()) -> [Char] -> ScopeM ()
    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
      s <- ScopeM Scope
    getCurrentScope
      let parents = Scope -> ModuleName
    scopeName Scope
    s ModuleName -> [ModuleName] -> [ModuleName]
    forall a. a -> [a] -> [a]
    : Scope -> [ModuleName]
    scopeParents Scope
    s
          sm = Scope
    emptyScope { scopeName           = m
                          , scopeParents        = parents
                          , scopeDatatypeModule = 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.
      modifyScopes $ Map.insertWith mergeScope m 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) -> ScopeM ()
    modifyScopes = (ScopeInfo -> ScopeInfo) -> ScopeM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (ScopeInfo -> ScopeInfo) -> m ()
    modifyScope ((ScopeInfo -> ScopeInfo) -> ScopeM ())
    -> ((Map ModuleName Scope -> Map ModuleName Scope)
        -> ScopeInfo -> ScopeInfo)
    -> (Map ModuleName Scope -> Map ModuleName Scope)
    -> ScopeM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Lens' ScopeInfo (Map ModuleName Scope)
    -> (Map ModuleName Scope -> Map ModuleName Scope)
    -> ScopeInfo
    -> ScopeInfo
    forall o i. Lens' o i -> LensMap o i
    over (Map ModuleName Scope -> f (Map ModuleName Scope))
    -> ScopeInfo -> f ScopeInfo
    Lens' ScopeInfo (Map ModuleName Scope)
    scopeModules

    -- | Apply a function to the given scope.
    modifyNamedScope :: A.ModuleName -> (Scope -> Scope) -> ScopeM ()
    modifyNamedScope :: ModuleName -> (Scope -> Scope) -> ScopeM ()
    modifyNamedScope ModuleName
    m Scope -> Scope
    f = (Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ()
    modifyScopes ((Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ())
    -> (Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ()
    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 -> ScopeM ()
    setNamedScope ModuleName
    m Scope
    s = ModuleName -> (Scope -> Scope) -> ScopeM ()
    modifyNamedScope ModuleName
    m ((Scope -> Scope) -> ScopeM ()) -> (Scope -> Scope) -> ScopeM ()
    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, 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
      setNamedScope m s
      return a

    -- | Apply a function to the current scope.
    modifyCurrentScope :: (Scope -> Scope) -> ScopeM ()
    modifyCurrentScope :: (Scope -> Scope) -> ScopeM ()
    modifyCurrentScope Scope -> Scope
    f = ScopeM ModuleName
    forall (m :: * -> *). ReadTCState m => m ModuleName
    getCurrentModule ScopeM ModuleName -> (ModuleName -> ScopeM ()) -> ScopeM ()
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= (ModuleName -> (Scope -> Scope) -> ScopeM ()
    `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 a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    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) -> ScopeM ()
    modifyCurrentNameSpace NameSpaceId
    acc NameSpace -> NameSpace
    f = (Scope -> Scope) -> ScopeM ()
    modifyCurrentScope ((Scope -> Scope) -> ScopeM ()) -> (Scope -> Scope) -> ScopeM ()
    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 -> ScopeM ()
    setContextPrecedence = (ScopeInfo -> ScopeInfo) -> ScopeM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (ScopeInfo -> ScopeInfo) -> m ()
    modifyScope_ ((ScopeInfo -> ScopeInfo) -> ScopeM ())
    -> (PrecedenceStack -> ScopeInfo -> ScopeInfo)
    -> PrecedenceStack
    -> ScopeM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Lens' ScopeInfo PrecedenceStack
    -> PrecedenceStack -> ScopeInfo -> ScopeInfo
    forall o i. Lens' o i -> LensSet o i
    set (PrecedenceStack -> f PrecedenceStack) -> ScopeInfo -> f ScopeInfo
    Lens' ScopeInfo PrecedenceStack
    scopePrecedence

    withContextPrecedence :: ReadTCState m => Precedence -> m a -> m a
    withContextPrecedence :: forall (m :: * -> *) a. ReadTCState m => Precedence -> m a -> m a
    withContextPrecedence Precedence
    p =
      Lens' TCState PrecedenceStack
    -> (PrecedenceStack -> PrecedenceStack) -> m a -> m a
    forall a b. Lens' TCState a -> (a -> a) -> m b -> m b
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' TCState a -> (a -> a) -> m b -> m b
    locallyTCState ((ScopeInfo -> f ScopeInfo) -> TCState -> f TCState
    Lens' TCState ScopeInfo
    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' ScopeInfo PrecedenceStack
    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' ScopeInfo LocalVars -> m LocalVars
    forall (m :: * -> *) a. ReadTCState m => Lens' ScopeInfo a -> m a
    useScope (LocalVars -> f LocalVars) -> ScopeInfo -> f ScopeInfo
    Lens' ScopeInfo LocalVars
    scopeLocals

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

    setLocalVars :: LocalVars -> ScopeM ()
    setLocalVars :: LocalVars -> ScopeM ()
    setLocalVars LocalVars
    vars = (LocalVars -> LocalVars) -> ScopeM ()
    modifyLocalVars ((LocalVars -> LocalVars) -> ScopeM ())
    -> (LocalVars -> LocalVars) -> ScopeM ()
    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 -> ScopeM ()) -> 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 -> ScopeM ()
    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
      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
      modifyLocalVars (drop n)
      x <- m
      modifyLocalVars (inner ++)
      return 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 -> ScopeM ()) -> 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 -> ScopeM ()) -> TCMT IO a -> TCMT IO a)
    -> (LocalVars -> ScopeM ()) -> TCMT IO a -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ \ LocalVars
    lvarsOld ->
      LocalVars -> LocalVars -> ScopeM ()
    checkNoShadowing LocalVars
    lvarsOld (LocalVars -> ScopeM ()) -> TCMT IO LocalVars -> ScopeM ()
    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 -> ScopeM ()
    checkNoShadowing LocalVars
    old LocalVars
    new = do
      opts <- TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
      when (ShadowingInTelescope_ `Set.member`
              (optWarningMode opts ^. warningSet)) $ do
        -- LocalVars is currnently an AssocList so the difference between
        -- two local scope is the left part of the new one.
        let diff = Int -> LocalVars -> LocalVars
    forall a. Int -> [a] -> [a]
    dropEnd (LocalVars -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length LocalVars
    old) LocalVars
    new
        -- Filter out the underscores.
        let 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 = 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, 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)
    forall (m :: * -> *) a b.
    Functor m =>
    (a -> m b) -> (Name, a) -> m (Name, b)
    traverseF NonEmpty Range -> Maybe (List2 Range)
    forall a. List1 a -> Maybe (List2 a)
    List2.fromList1Maybe) [(Name, NonEmpty Range)]
    nameOccs1
        caseList nameOccs2 (return ()) $ \ (Name, List2 Range)
    c [(Name, List2 Range)]
    conflicts -> do
          HasCallStack => DeclarationWarning' -> ScopeM ()
    DeclarationWarning' -> ScopeM ()
    scopeWarning (DeclarationWarning' -> ScopeM ())
    -> DeclarationWarning' -> ScopeM ()
    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' ScopeInfo LocalVars -> TCMT IO LocalVars
    forall (m :: * -> *) a. ReadTCState m => Lens' ScopeInfo a -> m a
    useScope (LocalVars -> f LocalVars) -> ScopeInfo -> f ScopeInfo
    Lens' ScopeInfo LocalVars
    scopeVarsToBind

    addVarToBind :: C.Name -> LocalVar -> ScopeM ()
    addVarToBind :: Name -> LocalVar -> ScopeM ()
    addVarToBind Name
    x LocalVar
    y = (ScopeInfo -> ScopeInfo) -> ScopeM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (ScopeInfo -> ScopeInfo) -> m ()
    modifyScope_ ((ScopeInfo -> ScopeInfo) -> ScopeM ())
    -> (ScopeInfo -> ScopeInfo) -> ScopeM ()
    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 :: ScopeM ()
    bindVarsToBind = do
      vars <- TCMT IO LocalVars
    getVarsToBind
      modifyLocalVars (vars ++)
      printLocals 30 "bound variables:"
      modifyScope_ $ setVarsToBind []

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

    annotateExpr :: ReadTCState m => m A.Expr -> m A.Expr
    annotateExpr :: forall (m :: * -> *). ReadTCState m => m Expr -> m Expr
    annotateExpr m Expr
    m = do
      e <- m Expr
    m
      s <- getScope
      return $ A.ScopedExpr s 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
      i <- TCMT IO NameId
    forall i (m :: * -> *). MonadFresh i m => m i
    fresh
      return $ A.Name
        { nameId          = i
        , nameConcrete    = x
        , nameCanonical   = x
        , nameBindingSite = getRange x
        , nameFixity      = fx
        , nameIsRecordName = 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
      y <- Fixity' -> Name -> ScopeM Name
    freshAbstractName Fixity'
    fx Name
    x
      m <- getCurrentModule
      return $ A.qualify m y

    freshAbstractQName' :: C.Name -> ScopeM A.QName
    freshAbstractQName' :: Name -> ScopeM QName
    freshAbstractQName' Name
    x = do
      fx <- Name -> ScopeM Fixity'
    getConcreteFixity Name
    x
      freshAbstractQName fx 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 a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        ResolvedName
    UnknownName -> Name -> ScopeM Name
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Name
    cname
        ResolvedName
    _           -> Range -> Int -> [Char] -> ScopeM Name
    freshConcreteName Range
    r (Int
    i Int -> 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 (Set1 Name) -> QName -> ScopeM ResolvedName
    resolveName' KindsOfNames
    allKindsOfNames Maybe (Set1 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 (Set1 A.Name) -> C.QName -> ScopeM ResolvedName
    resolveName' :: KindsOfNames -> Maybe (Set1 Name) -> QName -> ScopeM ResolvedName
    resolveName' KindsOfNames
    kinds Maybe (Set1 Name)
    names QName
    x = ExceptT NameResolutionError (TCMT IO) ResolvedName
    -> TCMT IO (Either NameResolutionError ResolvedName)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (KindsOfNames
    -> Maybe (Set1 Name)
    -> QName
    -> ExceptT NameResolutionError (TCMT IO) ResolvedName
    forall (m :: * -> *).
    (ReadTCState m, HasBuiltins m, MonadError NameResolutionError m) =>
    KindsOfNames -> Maybe (Set1 Name) -> QName -> m ResolvedName
    tryResolveName KindsOfNames
    kinds Maybe (Set1 Name)
    names QName
    x) TCMT IO (Either NameResolutionError ResolvedName)
    -> (Either NameResolutionError ResolvedName -> ScopeM ResolvedName)
    -> ScopeM ResolvedName
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      Left (IllegalAmbiguity AmbiguousNameReason
    reason)  -> do
        [Char] -> Int -> [Char] -> ScopeM ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    [Char] -> Int -> a -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportS [Char]
    "scope.resolve" Int
    60 ([Char] -> ScopeM ()) -> [Char] -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $
          [Char]
    "resolveName': ambiguous name" [Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    :
          (QName -> [Char]) -> [QName] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name -> [Char]
    forall a. Show a => a -> [Char]
    show (Name -> [Char]) -> (QName -> Name) -> QName -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Name
    qnameName) (List2 QName -> [Item (List2 QName)]
    forall l. IsList l => l -> [Item l]
    toList (List2 QName -> [Item (List2 QName)])
    -> List2 QName -> [Item (List2 QName)]
    forall a b. (a -> b) -> a -> b
    $ AmbiguousNameReason -> List2 QName
    ambiguousNamesInReason AmbiguousNameReason
    reason)
        QName -> ScopeM ResolvedName -> ScopeM ResolvedName
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange 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 -> AmbiguousNameReason -> TypeError
    AmbiguousName QName
    x AmbiguousNameReason
    reason

      Left (ConstrOfNonRecord QName
    q ResolvedName
    r) -> case ResolvedName
    r of
        ResolvedName
    UnknownName -> QName -> ScopeM ResolvedName -> ScopeM ResolvedName
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange 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 -> TypeError
    I.NotInScope QName
    q
        ResolvedName
    _ -> QName -> ScopeM ResolvedName -> ScopeM ResolvedName
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange 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
    $ ResolvedName -> TypeError
    ConstructorNameOfNonRecord ResolvedName
    r

      Right ResolvedName
    x' -> ResolvedName -> ScopeM ResolvedName
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ResolvedName
    x'

    tryResolveName :: forall m. (ReadTCState m, HasBuiltins m, MonadError NameResolutionError m)
      => KindsOfNames
           -- ^ Restrict search to these kinds of names.
      -> Maybe (Set1 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 NameResolutionError m) =>
    KindsOfNames -> Maybe (Set1 Name) -> QName -> m ResolvedName
    tryResolveName KindsOfNames
    kinds Maybe (Set1 Name)
    names QName
    x = do
      scope <- m ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope
      let
        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' ScopeInfo LocalVars -> LocalVars
    forall o i. o -> Lens' o i -> i
    ^. (LocalVars -> f LocalVars) -> ScopeInfo -> f ScopeInfo
    Lens' ScopeInfo LocalVars
    scopeLocals
        throwAmb = NameResolutionError -> m a
    forall a. NameResolutionError -> m a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (NameResolutionError -> m a)
    -> (AmbiguousNameReason -> NameResolutionError)
    -> AmbiguousNameReason
    -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AmbiguousNameReason -> NameResolutionError
    IllegalAmbiguity
      case lookup x vars of

        -- Case: we have a local variable x, but is (perhaps) shadowed by some imports ys.
        Just var :: LocalVar
    var@(LocalVar Name
    y BindingSource
    b [AbstractName]
    ys) ->
          -- We may ignore the imports filtered out by the @names@ filter.
          case [AbstractName] -> Maybe (NonEmpty AbstractName)
    forall a. [a] -> Maybe (NonEmpty a)
    nonEmpty ([AbstractName] -> Maybe (NonEmpty AbstractName))
    -> [AbstractName] -> Maybe (NonEmpty AbstractName)
    forall a b. (a -> b) -> a -> b
    $ (AbstractName -> AbstractName) -> [AbstractName] -> [AbstractName]
    forall a. (a -> AbstractName) -> [a] -> [a]
    filterNames AbstractName -> AbstractName
    forall a. a -> a
    id [AbstractName]
    ys of
            Maybe (NonEmpty AbstractName)
    Nothing  -> ResolvedName -> m ResolvedName
    forall a. a -> m a
    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 = unqualify x } BindingSource
    b
            Just NonEmpty AbstractName
    ys' -> AmbiguousNameReason -> m ResolvedName
    forall {a}. AmbiguousNameReason -> m a
    throwAmb (AmbiguousNameReason -> m ResolvedName)
    -> AmbiguousNameReason -> m ResolvedName
    forall a b. (a -> b) -> a -> b
    $ LocalVar -> NonEmpty AbstractName -> AmbiguousNameReason
    AmbiguousLocalVar LocalVar
    var NonEmpty 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`).
          canHaveSuffix <- m (QName -> Bool)
    forall (m :: * -> *). HasBuiltins m => m (QName -> Bool)
    canHaveSuffixTest
          let (xsuffix, xbase) = (C.lensQNameName . nameSuffix) (,Nothing) x
              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 = (,) (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 a b. Maybe (a -> b) -> Maybe a -> Maybe b
    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 (nonEmpty $ possibleNames x) of
            Just NonEmpty (AbstractName, Access)
    ds  | Just NonEmpty Induction
    ks <- ((AbstractName, Access) -> Maybe Induction)
    -> NonEmpty (AbstractName, Access) -> Maybe (NonEmpty Induction)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> NonEmpty a -> f (NonEmpty b)
    traverse (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
                         -- all names resolve to a constructor name
                     , Maybe (Suffix, NonEmpty (AbstractName, Access)) -> Bool
    forall a. Maybe a -> Bool
    isNothing Maybe (Suffix, NonEmpty (AbstractName, Access))
    suffixedNames ->
              ResolvedName -> m ResolvedName
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ResolvedName -> m ResolvedName) -> ResolvedName -> m ResolvedName
    forall a b. (a -> b) -> a -> b
    $ Set1 Induction -> NonEmpty AbstractName -> ResolvedName
    ConstructorName (NonEmpty Induction -> Set1 Induction
    forall a. Ord a => NonEmpty a -> NESet a
    Set1.fromList NonEmpty Induction
    ks) (NonEmpty AbstractName -> ResolvedName)
    -> NonEmpty AbstractName -> ResolvedName
    forall a b. (a -> b) -> a -> b
    $ ((AbstractName, Access) -> AbstractName)
    -> NonEmpty (AbstractName, Access) -> NonEmpty AbstractName
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    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 a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ResolvedName -> m ResolvedName) -> ResolvedName -> m ResolvedName
    forall a b. (a -> b) -> a -> b
    $ NonEmpty AbstractName -> ResolvedName
    FieldName (NonEmpty AbstractName -> ResolvedName)
    -> NonEmpty AbstractName -> ResolvedName
    forall a b. (a -> b) -> a -> b
    $ ((AbstractName, Access) -> AbstractName)
    -> NonEmpty (AbstractName, Access) -> NonEmpty AbstractName
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    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 a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ResolvedName -> m ResolvedName) -> ResolvedName -> m ResolvedName
    forall a b. (a -> b) -> a -> b
    $ NonEmpty AbstractName -> ResolvedName
    PatternSynResName (NonEmpty AbstractName -> ResolvedName)
    -> NonEmpty AbstractName -> ResolvedName
    forall a b. (a -> b) -> a -> b
    $ ((AbstractName, Access) -> AbstractName)
    -> NonEmpty (AbstractName, Access) -> NonEmpty AbstractName
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    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) :| [(AbstractName, Access)]
    ds) -> case (Maybe (Suffix, NonEmpty (AbstractName, Access))
    suffixedNames, [(AbstractName, Access)]
    ds) of
              (Maybe (Suffix, NonEmpty (AbstractName, Access))
    Nothing, []) ->
                ResolvedName -> m ResolvedName
    forall a. a -> m a
    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
              (Maybe (Suffix, NonEmpty (AbstractName, Access))
    Nothing, (AbstractName
    d',Access
    _) : [(AbstractName, Access)]
    ds') ->
                AmbiguousNameReason -> m ResolvedName
    forall {a}. AmbiguousNameReason -> m a
    throwAmb (AmbiguousNameReason -> m ResolvedName)
    -> AmbiguousNameReason -> m ResolvedName
    forall a b. (a -> b) -> a -> b
    $ List2 AbstractName -> AmbiguousNameReason
    AmbiguousDeclName (List2 AbstractName -> AmbiguousNameReason)
    -> List2 AbstractName -> AmbiguousNameReason
    forall a b. (a -> b) -> a -> b
    $ AbstractName
    -> AbstractName -> [AbstractName] -> List2 AbstractName
    forall a. a -> a -> [a] -> List2 a
    List2 AbstractName
    d AbstractName
    d' ([AbstractName] -> List2 AbstractName)
    -> [AbstractName] -> List2 AbstractName
    forall a b. (a -> b) -> a -> b
    $ ((AbstractName, Access) -> AbstractName)
    -> [(AbstractName, Access)] -> [AbstractName]
    forall a b. (a -> b) -> [a] -> [b]
    map (AbstractName, Access) -> AbstractName
    forall a b. (a, b) -> a
    fst [(AbstractName, Access)]
    ds'
              (Just (Suffix
    _, NonEmpty (AbstractName, Access)
    ss), [(AbstractName, Access)]
    _) ->
                AmbiguousNameReason -> m ResolvedName
    forall {a}. AmbiguousNameReason -> m a
    throwAmb (AmbiguousNameReason -> m ResolvedName)
    -> AmbiguousNameReason -> m ResolvedName
    forall a b. (a -> b) -> a -> b
    $ List2 AbstractName -> AmbiguousNameReason
    AmbiguousDeclName (List2 AbstractName -> AmbiguousNameReason)
    -> List2 AbstractName -> AmbiguousNameReason
    forall a b. (a -> b) -> a -> b
    $ NonEmpty AbstractName
    -> NonEmpty AbstractName -> List2 AbstractName
    forall a. List1 a -> List1 a -> List2 a
    List2.append (AbstractName
    d AbstractName -> [AbstractName] -> NonEmpty AbstractName
    forall a. a -> [a] -> NonEmpty a
    :| ((AbstractName, Access) -> AbstractName)
    -> [(AbstractName, Access)] -> [AbstractName]
    forall a b. (a -> b) -> [a] -> [b]
    map (AbstractName, Access) -> AbstractName
    forall a b. (a, b) -> a
    fst [(AbstractName, Access)]
    ds) (((AbstractName, Access) -> AbstractName)
    -> NonEmpty (AbstractName, Access) -> NonEmpty AbstractName
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (AbstractName, Access) -> AbstractName
    forall a b. (a, b) -> a
    fst NonEmpty (AbstractName, Access)
    ss)

            -- Name is of the form r.constructor
            Maybe (NonEmpty (AbstractName, Access))
    Nothing | Just QName
    r <- QName -> Maybe QName
    isRecordConstructor QName
    x -> do
              -- We resolve the record name r with no filter, that way we
              -- can know when printing an error message whether r is not in
              -- scope, or whether it's some other type of name, etc.
              recd <- KindsOfNames -> Maybe (Set1 Name) -> QName -> m ResolvedName
    forall (m :: * -> *).
    (ReadTCState m, HasBuiltins m, MonadError NameResolutionError m) =>
    KindsOfNames -> Maybe (Set1 Name) -> QName -> m ResolvedName
    tryResolveName KindsOfNames
    AllKindsOfNames Maybe (Set1 Name)
    forall a. Maybe a
    Nothing QName
    r

              case recd of
                DefinedName Access
    acc AbstractName
    abs Suffix
    suf -> QName -> m (Maybe (QName, Maybe Induction))
    forall (m :: * -> *).
    ReadTCState m =>
    QName -> m (Maybe (QName, Maybe Induction))
    getRecordConstructor (AbstractName -> QName
    anameName AbstractName
    abs) m (Maybe (QName, Maybe Induction))
    -> (Maybe (QName, Maybe Induction) -> m ResolvedName)
    -> m ResolvedName
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
                  Just (QName
    qn, Maybe Induction
    ind) -> ResolvedName -> m ResolvedName
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (ResolvedName -> m ResolvedName) -> ResolvedName -> m ResolvedName
    forall a b. (a -> b) -> a -> b
    $ Set1 Induction -> NonEmpty AbstractName -> ResolvedName
    ConstructorName (Induction -> Set1 Induction
    forall a. a -> NESet a
    Set1.singleton (Induction -> Set1 Induction) -> Induction -> Set1 Induction
    forall a b. (a -> b) -> a -> b
    $ Induction -> Maybe Induction -> Induction
    forall a. a -> Maybe a -> a
    fromMaybe Induction
    Inductive Maybe Induction
    ind) (NonEmpty AbstractName -> ResolvedName)
    -> NonEmpty AbstractName -> ResolvedName
    forall a b. (a -> b) -> a -> b
    $
                    AbstractName -> NonEmpty AbstractName
    forall a. a -> NonEmpty a
    List1.singleton (AbstractName -> NonEmpty AbstractName)
    -> AbstractName -> NonEmpty AbstractName
    forall a b. (a -> b) -> a -> b
    $ AbstractName -> AbstractName
    upd AbstractName
    abs { anameName = qn, anameKind = ConName }
                  Maybe (QName, Maybe Induction)
    Nothing -> NameResolutionError -> m ResolvedName
    forall a. NameResolutionError -> m a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (NameResolutionError -> m ResolvedName)
    -> NameResolutionError -> m ResolvedName
    forall a b. (a -> b) -> a -> b
    $ QName -> ResolvedName -> NameResolutionError
    ConstrOfNonRecord QName
    r ResolvedName
    recd
                ResolvedName
    _ -> NameResolutionError -> m ResolvedName
    forall a. NameResolutionError -> m a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (NameResolutionError -> m ResolvedName)
    -> NameResolutionError -> m ResolvedName
    forall a b. (a -> b) -> a -> b
    $ QName -> ResolvedName -> NameResolutionError
    ConstrOfNonRecord QName
    r ResolvedName
    recd

            Maybe (NonEmpty (AbstractName, Access))
    Nothing -> case Maybe (Suffix, NonEmpty (AbstractName, Access))
    suffixedNames of
              Maybe (Suffix, NonEmpty (AbstractName, Access))
    Nothing -> ResolvedName -> m ResolvedName
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ResolvedName
    UnknownName
              Just (Suffix
    suffix , (AbstractName
    d, Access
    a) :| []) -> ResolvedName -> m ResolvedName
    forall a. a -> m a
    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 , (AbstractName
    d1,Access
    _) :| (AbstractName
    d2,Access
    _) : [(AbstractName, Access)]
    sds) ->
                AmbiguousNameReason -> m ResolvedName
    forall {a}. AmbiguousNameReason -> m a
    throwAmb (AmbiguousNameReason -> m ResolvedName)
    -> AmbiguousNameReason -> m ResolvedName
    forall a b. (a -> b) -> a -> b
    $ List2 AbstractName -> AmbiguousNameReason
    AmbiguousDeclName (List2 AbstractName -> AmbiguousNameReason)
    -> List2 AbstractName -> AmbiguousNameReason
    forall a b. (a -> b) -> a -> b
    $ AbstractName
    -> AbstractName -> [AbstractName] -> List2 AbstractName
    forall a. a -> a -> [a] -> List2 a
    List2 AbstractName
    d1 AbstractName
    d2 ([AbstractName] -> List2 AbstractName)
    -> [AbstractName] -> List2 AbstractName
    forall a b. (a -> b) -> a -> b
    $ ((AbstractName, Access) -> AbstractName)
    -> [(AbstractName, Access)] -> [AbstractName]
    forall a b. (a -> b) -> [a] -> [b]
    map (AbstractName, Access) -> AbstractName
    forall a b. (a, b) -> a
    fst [(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 (Set1 Name)
    names of
        Maybe (Set1 Name)
    Nothing -> \ a -> AbstractName
    f -> [a] -> [a]
    forall a. a -> a
    id
        Just Set1 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 -> Set1 Name -> Bool
    forall a. Ord a => a -> NESet a -> Bool
    `Set1.member` Set1 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 = A.QName (setRange (getRange x) qm) (qn { nameConcrete = 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.
    canHaveSuffixTest :: HasBuiltins m => m (A.QName -> Bool)
    canHaveSuffixTest :: forall (m :: * -> *). HasBuiltins m => m (QName -> Bool)
    canHaveSuffixTest = do
      builtinProp <- BuiltinId -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
    getBuiltinName' BuiltinId
    builtinProp
      builtinSet  <- getBuiltinName' builtinSet
      builtinSSet <- getBuiltinName' builtinStrictSet
      builtinPropOmega <- getBuiltinName' builtinPropOmega
      builtinSetOmega <- getBuiltinName' builtinSetOmega
      builtinSSetOmega <- getBuiltinName' builtinSSetOmega
      return $ \QName
    x -> QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    x Maybe QName -> [Maybe QName] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Maybe QName
    builtinProp, Maybe QName
    builtinSet, Maybe QName
    builtinSSet, Maybe QName
    builtinPropOmega, 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
      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
      caseMaybe (nonEmpty ms) (typeError $ NoSuchModule x) $ \ case
        AbsModule ModuleName
    m WhyInScope
    why :| [] -> AbstractModule -> ScopeM AbstractModule
    forall a. a -> TCMT IO a
    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 a b. (a -> b) -> NonEmpty a -> NonEmpty b
    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' ScopeInfo (Map Name Fixity') -> TCMT IO (Map Name Fixity')
    forall (m :: * -> *) a. ReadTCState m => Lens' ScopeInfo a -> m a
    useScope (Map Name Fixity' -> f (Map Name Fixity'))
    -> ScopeInfo -> f ScopeInfo
    Lens' ScopeInfo (Map Name Fixity')
    scopeFixities

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

    instance MonadFixityError ScopeM where
      throwMultipleFixityDecls :: forall a. List1 (Name, Pair Fixity') -> ScopeM a
    throwMultipleFixityDecls List1 (Name, Pair Fixity')
    xs         = case List1 (Name, Pair Fixity')
    xs of
        (Name
    x, Pair Fixity'
    _) :| [(Name, Pair 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
    $ List1 (Name, Pair Fixity') -> TypeError
    MultipleFixityDecls List1 (Name, Pair Fixity')
    xs
      throwMultiplePolarityPragmas :: forall a. List1 Name -> ScopeM a
    throwMultiplePolarityPragmas List1 Name
    xs     = case List1 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
    $ List1 Name -> TypeError
    MultiplePolarityPragmas List1 Name
    xs
      warnUnknownNamesInFixityDecl :: HasCallStack => Set1 Name -> ScopeM ()
    warnUnknownNamesInFixityDecl        = HasCallStack => DeclarationWarning' -> ScopeM ()
    DeclarationWarning' -> ScopeM ()
    scopeWarning (DeclarationWarning' -> ScopeM ())
    -> (Set1 Name -> DeclarationWarning') -> Set1 Name -> ScopeM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set1 Name -> DeclarationWarning'
    UnknownNamesInFixityDecl
      warnUnknownNamesInPolarityPragmas :: HasCallStack => Set1 Name -> ScopeM ()
    warnUnknownNamesInPolarityPragmas   = HasCallStack => DeclarationWarning' -> ScopeM ()
    DeclarationWarning' -> ScopeM ()
    scopeWarning (DeclarationWarning' -> ScopeM ())
    -> (Set1 Name -> DeclarationWarning') -> Set1 Name -> ScopeM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set1 Name -> DeclarationWarning'
    UnknownNamesInPolarityPragmas
      warnUnknownFixityInMixfixDecl :: HasCallStack => Set1 Name -> ScopeM ()
    warnUnknownFixityInMixfixDecl       = HasCallStack => DeclarationWarning' -> ScopeM ()
    DeclarationWarning' -> ScopeM ()
    scopeWarning (DeclarationWarning' -> ScopeM ())
    -> (Set1 Name -> DeclarationWarning') -> Set1 Name -> ScopeM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set1 Name -> DeclarationWarning'
    UnknownFixityInMixfixDecl
      warnPolarityPragmasButNotPostulates :: HasCallStack => Set1 Name -> ScopeM ()
    warnPolarityPragmasButNotPostulates = HasCallStack => DeclarationWarning' -> ScopeM ()
    DeclarationWarning' -> ScopeM ()
    scopeWarning (DeclarationWarning' -> ScopeM ())
    -> (Set1 Name -> DeclarationWarning') -> Set1 Name -> ScopeM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set1 Name -> DeclarationWarning'
    PolarityPragmasButNotPostulates
      warnEmptyPolarityPragma :: HasCallStack => Range -> ScopeM ()
    warnEmptyPolarityPragma             = HasCallStack => DeclarationWarning' -> ScopeM ()
    DeclarationWarning' -> ScopeM ()
    scopeWarning (DeclarationWarning' -> ScopeM ())
    -> (Range -> DeclarationWarning') -> Range -> ScopeM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Range -> DeclarationWarning'
    EmptyPolarityPragma

    -- | 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
      fp <- DoWarn
    -> [Declaration]
    -> TCMT IO (Map Name Fixity', Map Name PragmaPolarities)
    forall (m :: * -> *).
    MonadFixityError m =>
    DoWarn
    -> [Declaration] -> m (Map Name Fixity', Map Name PragmaPolarities)
    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.
      locallyScope scopeFixitiesAndPolarities (const fp) cont

    -- | Get the notation of a name. The name is assumed to be in scope.
    getNotation
      :: C.QName
      -> Set1 A.Name
         -- ^ The name must correspond to one of the names in this set.
      -> ScopeM NewNotation
    getNotation :: QName -> Set1 Name -> ScopeM NewNotation
    getNotation QName
    x Set1 Name
    ns = do
      r <- KindsOfNames -> Maybe (Set1 Name) -> QName -> ScopeM ResolvedName
    resolveName' KindsOfNames
    allKindsOfNames (Set1 Name -> Maybe (Set1 Name)
    forall a. a -> Maybe a
    Just Set1 Name
    ns) QName
    x
      case r of
        VarName Name
    y BindingSource
    _         -> NewNotation -> ScopeM NewNotation
    forall a. a -> TCMT IO a
    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 a. a -> TCMT IO a
    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 NonEmpty AbstractName
    ds        -> NewNotation -> ScopeM NewNotation
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NewNotation -> ScopeM NewNotation)
    -> NewNotation -> ScopeM NewNotation
    forall a b. (a -> b) -> a -> b
    $ NonEmpty AbstractName -> NewNotation
    oneNotation NonEmpty AbstractName
    ds
        ConstructorName Set1 Induction
    _ NonEmpty AbstractName
    ds-> NewNotation -> ScopeM NewNotation
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NewNotation -> ScopeM NewNotation)
    -> NewNotation -> ScopeM NewNotation
    forall a b. (a -> b) -> a -> b
    $ NonEmpty AbstractName -> NewNotation
    oneNotation NonEmpty AbstractName
    ds
        PatternSynResName NonEmpty AbstractName
    n -> NewNotation -> ScopeM NewNotation
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NewNotation -> ScopeM NewNotation)
    -> NewNotation -> ScopeM NewNotation
    forall a b. (a -> b) -> a -> b
    $ NonEmpty AbstractName -> NewNotation
    oneNotation NonEmpty 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 :: NonEmpty AbstractName -> NewNotation
    oneNotation = NonEmpty NewNotation -> NewNotation
    forall a. NonEmpty a -> a
    List1.head (NonEmpty NewNotation -> NewNotation)
    -> (NonEmpty AbstractName -> NonEmpty NewNotation)
    -> NonEmpty AbstractName
    -> NewNotation
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NonEmpty NewNotation -> NonEmpty NewNotation
    mergeNotations (NonEmpty NewNotation -> NonEmpty NewNotation)
    -> (NonEmpty AbstractName -> NonEmpty NewNotation)
    -> NonEmpty AbstractName
    -> NonEmpty NewNotation
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (AbstractName -> NewNotation)
    -> NonEmpty AbstractName -> NonEmpty NewNotation
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap AbstractName -> NewNotation
    notation

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

    -- | Bind a variable.
    bindVariable
      :: A.BindingSource -- ^ @λ@, @Π@, @let@, ...?
      -> C.Name          -- ^ Concrete name.
      -> A.Name          -- ^ Abstract name.
      -> ScopeM ()
    bindVariable :: BindingSource -> Name -> Name -> ScopeM ()
    bindVariable BindingSource
    b Name
    x Name
    y = (LocalVars -> LocalVars) -> ScopeM ()
    modifyLocalVars ((LocalVars -> LocalVars) -> ScopeM ())
    -> (LocalVars -> LocalVars) -> ScopeM ()
    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 -> ScopeM ()) -> 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 -> ScopeM () -> TCMT IO LocalVars
    forall a b. TCMT IO a -> TCMT IO b -> TCMT IO a
    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
    <* (LocalVars -> LocalVars) -> ScopeM ()
    modifyLocalVars (Name -> LocalVars -> LocalVars
    forall k v. Eq k => k -> AssocList k v -> AssocList k v
    AssocList.delete Name
    x)) ((LocalVars -> LocalVars) -> ScopeM ()
    modifyLocalVars ((LocalVars -> LocalVars) -> ScopeM ())
    -> (LocalVars -> LocalVars -> LocalVars) -> LocalVars -> ScopeM ()
    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 -> ScopeM ()
    bindName Access
    acc KindOfName
    kind Name
    x QName
    y = Access -> KindOfName -> NameMetadata -> Name -> QName -> ScopeM ()
    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 -> ScopeM ()
    bindName' Access
    acc KindOfName
    kind NameMetadata
    meta Name
    x QName
    y = TCMT IO (Maybe TypeError) -> (TypeError -> ScopeM ()) -> ScopeM ()
    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 -> ScopeM ()
    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 -> ScopeM () -> ScopeM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (Name -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName Name
    x) (ScopeM () -> ScopeM ()) -> ScopeM () -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $ (Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ()
    modifyScopes ((Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ())
    -> (Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ()
    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
      r  <- QName -> ScopeM ResolvedName
    resolveName (Name -> QName
    C.QName Name
    x)
      let 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       NonEmpty AbstractName
    ds  -> (KindOfName -> Bool)
    -> NonEmpty AbstractName -> Either TypeError AbstractName
    ambiguous (KindOfName -> KindOfName -> Bool
    forall a. Eq a => a -> a -> Bool
    == KindOfName
    FldName) NonEmpty AbstractName
    ds
            ConstructorName Set1 Induction
    i NonEmpty AbstractName
    ds-> (KindOfName -> Bool)
    -> NonEmpty 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) NonEmpty AbstractName
    ds
            PatternSynResName NonEmpty AbstractName
    n -> (KindOfName -> Bool)
    -> NonEmpty AbstractName -> Either TypeError AbstractName
    ambiguous (KindOfName -> KindOfName -> Bool
    forall a. Eq a => a -> a -> Bool
    == KindOfName
    PatternSynName) NonEmpty AbstractName
    n
            ResolvedName
    UnknownName         -> Either TypeError AbstractName
    success
      let ns = if Name -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName Name
    x then NameSpaceId
    PrivateNS else Access -> NameSpaceId
    localNameSpace Access
    acc
      traverse_ (modifyCurrentScope . addNameToScope ns x) y'
      pure $ either Just (const Nothing) 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)
    -> NonEmpty AbstractName -> Either TypeError AbstractName
    ambiguous KindOfName -> Bool
    f NonEmpty AbstractName
    ds =
          if KindOfName -> Bool
    f KindOfName
    kind Bool -> Bool -> Bool
    && (AbstractName -> Bool) -> NonEmpty 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) NonEmpty 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 (NonEmpty AbstractName -> AbstractName
    forall a. NonEmpty a -> a
    List1.head NonEmpty 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 -> ScopeM ()
    rebindName Access
    acc KindOfName
    kind Name
    x QName
    y = do
      if KindOfName
    kind KindOfName -> KindOfName -> Bool
    forall a. Eq a => a -> a -> Bool
    == KindOfName
    ConName
        then (Scope -> Scope) -> ScopeM ()
    modifyCurrentScope ((Scope -> Scope) -> ScopeM ()) -> (Scope -> Scope) -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $
               NameSpaceId
    -> (NamesInScope -> NamesInScope)
    -> (ModulesInScope -> ModulesInScope)
    -> (InScopeSet -> InScopeSet)
    -> Scope
    -> Scope
    mapScopeNS (Access -> NameSpaceId
    localNameSpace Access
    acc)
                          ((NonEmpty AbstractName -> Maybe (NonEmpty AbstractName))
    -> Name -> NamesInScope -> NamesInScope
    forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
    Map.update ([AbstractName] -> Maybe (NonEmpty AbstractName)
    forall a. [a] -> Maybe (NonEmpty a)
    nonEmpty ([AbstractName] -> Maybe (NonEmpty AbstractName))
    -> (NonEmpty AbstractName -> [AbstractName])
    -> NonEmpty AbstractName
    -> Maybe (NonEmpty AbstractName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (AbstractName -> Bool) -> NonEmpty AbstractName -> [AbstractName]
    forall a. (a -> Bool) -> NonEmpty a -> [a]
    List1.filter ((KindOfName
    ConName KindOfName -> KindOfName -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (KindOfName -> Bool)
    -> (AbstractName -> KindOfName) -> AbstractName -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbstractName -> KindOfName
    anameKind)) Name
    x)
                          ModulesInScope -> ModulesInScope
    forall a. a -> a
    id
                          InScopeSet -> InScopeSet
    forall a. a -> a
    id
        else (Scope -> Scope) -> ScopeM ()
    modifyCurrentScope ((Scope -> Scope) -> ScopeM ()) -> (Scope -> Scope) -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $ NameSpaceId -> Name -> Scope -> Scope
    removeNameFromScope (Access -> NameSpaceId
    localNameSpace Access
    acc) Name
    x
      Access -> KindOfName -> Name -> QName -> ScopeM ()
    bindName Access
    acc KindOfName
    kind Name
    x QName
    y

    -- | Bind a module name.
    bindModule :: Access -> C.Name -> A.ModuleName -> ScopeM ()
    bindModule :: Access -> Name -> ModuleName -> ScopeM ()
    bindModule Access
    acc Name
    x ModuleName
    m = (Scope -> Scope) -> ScopeM ()
    modifyCurrentScope ((Scope -> Scope) -> ScopeM ()) -> (Scope -> Scope) -> ScopeM ()
    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 -> ScopeM ()
    bindQModule Access
    acc QName
    q ModuleName
    m = (Scope -> Scope) -> ScopeM ()
    modifyCurrentScope ((Scope -> Scope) -> ScopeM ()) -> (Scope -> Scope) -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $ \Scope
    s ->
      Scope
    s { scopeImports = Map.insert q m (scopeImports s) }

    ---------------------------------------------------
    -- * Operations to do with record constructor names
    ---------------------------------------------------

    -- | Record (ha) that a given record has the specified constructor name.
    setRecordConstructor :: A.QName -> (A.QName, Maybe Induction) -> ScopeM ()
    setRecordConstructor :: QName -> (QName, Maybe Induction) -> ScopeM ()
    setRecordConstructor QName
    recr (QName, Maybe Induction)
    con = (ScopeInfo -> ScopeInfo) -> ScopeM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (ScopeInfo -> ScopeInfo) -> m ()
    modifyScope_ ((ScopeInfo -> ScopeInfo) -> ScopeM ())
    -> (ScopeInfo -> ScopeInfo) -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $ Lens' ScopeInfo (Map QName (QName, Maybe Induction))
    -> LensMap ScopeInfo (Map QName (QName, Maybe Induction))
    forall o i. Lens' o i -> LensMap o i
    over (Map QName (QName, Maybe Induction)
     -> f (Map QName (QName, Maybe Induction)))
    -> ScopeInfo -> f ScopeInfo
    Lens' ScopeInfo (Map QName (QName, Maybe Induction))
    scopeRecords LensMap ScopeInfo (Map QName (QName, Maybe Induction))
    -> LensMap ScopeInfo (Map QName (QName, Maybe Induction))
    forall a b. (a -> b) -> a -> b
    $ QName
    -> (QName, Maybe Induction)
    -> Map QName (QName, Maybe Induction)
    -> Map QName (QName, Maybe Induction)
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert QName
    recr (QName, Maybe Induction)
    con

    -- | Get the internal 'QName' for the  name of a record constructor. If
    -- the name does not refer to a record type, 'Nothing' is returned.
    getRecordConstructor :: ReadTCState m => A.QName -> m (Maybe (A.QName, Maybe Induction))
    getRecordConstructor :: forall (m :: * -> *).
    ReadTCState m =>
    QName -> m (Maybe (QName, Maybe Induction))
    getRecordConstructor QName
    recr = MaybeT m (QName, Maybe Induction)
    -> m (Maybe (QName, Maybe Induction))
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT m (QName, Maybe Induction)
     -> m (Maybe (QName, Maybe Induction)))
    -> MaybeT m (QName, Maybe Induction)
    -> m (Maybe (QName, Maybe Induction))
    forall a b. (a -> b) -> a -> b
    $ MaybeT m (QName, Maybe Induction)
    local MaybeT m (QName, Maybe Induction)
    -> MaybeT m (QName, Maybe Induction)
    -> MaybeT m (QName, Maybe Induction)
    forall a. MaybeT m a -> MaybeT m a -> MaybeT m a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> MaybeT m (QName, Maybe Induction)
    imported where
      local :: MaybeT m (QName, Maybe Induction)
    local = do
        recs <- Lens' ScopeInfo (Map QName (QName, Maybe Induction))
    -> MaybeT m (Map QName (QName, Maybe Induction))
    forall (m :: * -> *) a. ReadTCState m => Lens' ScopeInfo a -> m a
    useScope (Map QName (QName, Maybe Induction)
     -> f (Map QName (QName, Maybe Induction)))
    -> ScopeInfo -> f ScopeInfo
    Lens' ScopeInfo (Map QName (QName, Maybe Induction))
    scopeRecords
        MaybeT $ pure $ Map.lookup recr recs
      imported :: MaybeT m (QName, Maybe Induction)
    imported = do
        idefs <- Lens' TCState (HashMap QName Definition)
    -> MaybeT m (HashMap QName Definition)
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC ((Signature -> f Signature) -> TCState -> f TCState
    Lens' TCState Signature
    stImports ((Signature -> f Signature) -> TCState -> f TCState)
    -> ((HashMap QName Definition -> f (HashMap QName Definition))
        -> Signature -> f Signature)
    -> (HashMap QName Definition -> f (HashMap QName Definition))
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (HashMap QName Definition -> f (HashMap QName Definition))
    -> Signature -> f Signature
    Lens' Signature (HashMap QName Definition)
    sigDefinitions)
        case theDef <$> HMap.lookup recr idefs of
          Just def :: Defn
    def@I.Record{} -> (QName, Maybe Induction) -> MaybeT m (QName, Maybe Induction)
    forall a. a -> MaybeT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Defn -> QName
    I.recCon Defn
    def, Defn -> Maybe Induction
    I.recInduction Defn
    def)
          Maybe Defn
    _ -> m (Maybe (QName, Maybe Induction))
    -> MaybeT m (QName, Maybe Induction)
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (m (Maybe (QName, Maybe Induction))
     -> MaybeT m (QName, Maybe Induction))
    -> m (Maybe (QName, Maybe Induction))
    -> MaybeT m (QName, Maybe Induction)
    forall a b. (a -> b) -> a -> b
    $ Maybe (QName, Maybe Induction)
    -> m (Maybe (QName, Maybe Induction))
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe (QName, Maybe Induction)
    forall a. Maybe a
    Nothing

    -- | Is this the qualified name which refers to the constructor of an
    -- anonymous record (like @Foo.constructor@)?
    --
    -- If so, return the part of the name referring to the record (@Foo@).
    isRecordConstructor :: C.QName -> Maybe C.QName
    isRecordConstructor :: QName -> Maybe QName
    isRecordConstructor = ([Name] -> QName) -> Maybe [Name] -> Maybe QName
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap [Name] -> QName
    to (Maybe [Name] -> Maybe QName)
    -> (QName -> Maybe [Name]) -> QName -> Maybe QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Maybe [Name]
    toplevel where
      toplevel, is :: C.QName -> Maybe [C.Name]
      toplevel :: QName -> Maybe [Name]
    toplevel (Qual Name
    r QName
    n) = (Name
    rName -> [Name] -> [Name]
    forall a. a -> [a] -> [a]
    :) ([Name] -> [Name]) -> Maybe [Name] -> Maybe [Name]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> Maybe [Name]
    is QName
    n
      toplevel QName
    _          = Maybe [Name]
    forall a. Maybe a
    Nothing

      is :: QName -> Maybe [Name]
    is (C.Qual Name
    r QName
    n) = (Name
    rName -> [Name] -> [Name]
    forall a. a -> [a] -> [a]
    :) ([Name] -> [Name]) -> Maybe [Name] -> Maybe [Name]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> Maybe [Name]
    is QName
    n
      is (C.QName Name
    n)  = case Name
    n of
        C.Name Range
    _ NameInScope
    _ (Id [Char]
    w :| [])
          | [Char]
    w [Char] -> [Char] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Char]
    "constructor" -> [Name] -> Maybe [Name]
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []
        Name
    _ -> Maybe [Name]
    forall a. Maybe a
    Nothing

      to :: [Name] -> QName
    to []     = QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      to [Name
    x]    = Name -> QName
    C.QName Name
    x
      to (Name
    x:[Name]
    xs) = Name -> QName -> QName
    C.Qual Name
    x ([Name] -> QName
    to [Name]
    xs)

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

    -- | Clear the scope of any no names.
    stripNoNames :: ScopeM ()
    stripNoNames :: ScopeM ()
    stripNoNames = (Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ()
    modifyScopes ((Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ())
    -> (Map ModuleName Scope -> Map ModuleName Scope) -> ScopeM ()
    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 { 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 a. a -> NonEmpty a
    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 }

    -- | Mark a name as being a copy in the TC state.
    copyName :: A.QName -> A.QName -> ScopeM ()
    copyName :: QName -> QName -> ScopeM ()
    copyName QName
    from QName
    to = do
      from <- QName -> Maybe QName -> QName
    forall a. a -> Maybe a -> a
    fromMaybe QName
    from (Maybe QName -> QName)
    -> (HashMap QName QName -> Maybe QName)
    -> HashMap QName QName
    -> QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> HashMap QName QName -> Maybe QName
    forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
    HMap.lookup QName
    from (HashMap QName QName -> QName)
    -> TCMT IO (HashMap QName QName) -> ScopeM QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' TCState (HashMap QName QName)
    -> TCMT IO (HashMap QName QName)
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (HashMap QName QName -> f (HashMap QName QName))
    -> TCState -> f TCState
    Lens' TCState (HashMap QName QName)
    stCopiedNames
      modifyTCLens stCopiedNames $ HMap.insert to from
      let
        k Maybe (HashSet QName)
    Nothing  = HashSet QName -> Maybe (HashSet QName)
    forall a. a -> Maybe a
    Just (QName -> HashSet QName
    forall a. Hashable a => a -> HashSet a
    HSet.singleton QName
    to)
        k (Just HashSet QName
    s) = HashSet QName -> Maybe (HashSet QName)
    forall a. a -> Maybe a
    Just (QName -> HashSet QName -> HashSet QName
    forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
    HSet.insert QName
    to HashSet QName
    s)
      modifyTCLens stNameCopies $ HMap.alter k from

    -- | 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 b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** ScopeMemo -> ScopeCopyInfo
    memoToScopeInfo) ((Scope, ScopeMemo) -> (Scope, ScopeCopyInfo))
    -> TCMT IO (Scope, ScopeMemo) -> ScopeM (Scope, ScopeCopyInfo)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> StateT ScopeMemo (TCMT IO) Scope
    -> ScopeMemo -> TCMT IO (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
          ScopeM () -> StateT ScopeMemo (TCMT IO) ()
    forall (m :: * -> *) a. Monad m => m a -> StateT ScopeMemo m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (ScopeM () -> StateT ScopeMemo (TCMT IO) ())
    -> ScopeM () -> StateT ScopeMemo (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Int -> [Char] -> ScopeM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "scope.copy" Int
    20 ([Char] -> ScopeM ()) -> [Char] -> ScopeM ()
    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
          ScopeM () -> StateT ScopeMemo (TCMT IO) ()
    forall (m :: * -> *) a. Monad m => m a -> StateT ScopeMemo m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (ScopeM () -> StateT ScopeMemo (TCMT IO) ())
    -> ScopeM () -> StateT ScopeMemo (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Int -> [Char] -> ScopeM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "scope.copy" Int
    50 ([Char] -> ScopeM ()) -> [Char] -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $ Scope -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Scope
    s
          s0 <- ScopeM Scope -> StateT ScopeMemo (TCMT IO) Scope
    forall (m :: * -> *) a. Monad m => m a -> StateT ScopeMemo m a
    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.
          s' <- recomputeInScopeSets <$> mapScopeM_ copyD copyM return (setNameSpace PrivateNS emptyNameSpace s)
          -- Fix name and parent.
          return $ s' { scopeName    = scopeName s0
                      , scopeParents = scopeParents 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 = (NonEmpty AbstractName
     -> StateT ScopeMemo (TCMT IO) (NonEmpty AbstractName))
    -> NamesInScope -> StateT ScopeMemo (TCMT IO) NamesInScope
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Map Name a -> f (Map Name b)
    traverse ((NonEmpty AbstractName
      -> StateT ScopeMemo (TCMT IO) (NonEmpty AbstractName))
     -> NamesInScope -> StateT ScopeMemo (TCMT IO) NamesInScope)
    -> (NonEmpty AbstractName
        -> StateT ScopeMemo (TCMT IO) (NonEmpty AbstractName))
    -> NamesInScope
    -> StateT ScopeMemo (TCMT IO) NamesInScope
    forall a b. (a -> b) -> a -> b
    $ (AbstractName -> StateT ScopeMemo (TCMT IO) AbstractName)
    -> NonEmpty AbstractName
    -> StateT ScopeMemo (TCMT IO) (NonEmpty AbstractName)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> NonEmpty a -> m (NonEmpty b)
    mapM ((AbstractName -> StateT ScopeMemo (TCMT IO) AbstractName)
     -> NonEmpty AbstractName
     -> StateT ScopeMemo (TCMT IO) (NonEmpty AbstractName))
    -> (AbstractName -> StateT ScopeMemo (TCMT IO) AbstractName)
    -> NonEmpty AbstractName
    -> StateT ScopeMemo (TCMT IO) (NonEmpty 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 = (NonEmpty AbstractModule
     -> StateT ScopeMemo (TCMT IO) (NonEmpty AbstractModule))
    -> ModulesInScope -> StateT ScopeMemo (TCMT IO) ModulesInScope
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Map Name a -> f (Map Name b)
    traverse ((NonEmpty AbstractModule
      -> StateT ScopeMemo (TCMT IO) (NonEmpty AbstractModule))
     -> ModulesInScope -> StateT ScopeMemo (TCMT IO) ModulesInScope)
    -> (NonEmpty AbstractModule
        -> StateT ScopeMemo (TCMT IO) (NonEmpty AbstractModule))
    -> ModulesInScope
    -> StateT ScopeMemo (TCMT IO) ModulesInScope
    forall a b. (a -> b) -> a -> b
    $ (AbstractModule -> StateT ScopeMemo (TCMT IO) AbstractModule)
    -> NonEmpty AbstractModule
    -> StateT ScopeMemo (TCMT IO) (NonEmpty AbstractModule)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> NonEmpty a -> m (NonEmpty b)
    mapM ((AbstractModule -> StateT ScopeMemo (TCMT IO) AbstractModule)
     -> NonEmpty AbstractModule
     -> StateT ScopeMemo (TCMT IO) (NonEmpty AbstractModule))
    -> (AbstractModule -> StateT ScopeMemo (TCMT IO) AbstractModule)
    -> NonEmpty AbstractModule
    -> StateT ScopeMemo (TCMT IO) (NonEmpty AbstractModule)
    forall a b. (a -> b) -> a -> b
    $ (ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName)
    -> AbstractModule -> StateT ScopeMemo (TCMT IO) AbstractModule
    Lens' AbstractModule ModuleName
    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 a. a -> StateT ScopeMemo (TCMT IO) a
    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' AbstractName QName
    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   = Map.insertWith (<>) x (pure y) (memoNames 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.insert x (y, rec) (memoModules 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
              i <- TCMT IO NameId -> StateT ScopeMemo (TCMT IO) NameId
    forall (m :: * -> *) a. Monad m => m a -> StateT ScopeMemo m a
    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
              return $ x { A.nameId = i }

            copyRecordConstr :: A.QName -> A.QName -> WSM ()
            copyRecordConstr :: QName -> QName -> StateT ScopeMemo (TCMT IO) ()
    copyRecordConstr QName
    from QName
    to = QName
    -> StateT ScopeMemo (TCMT IO) (Maybe (QName, Maybe Induction))
    forall (m :: * -> *).
    ReadTCState m =>
    QName -> m (Maybe (QName, Maybe Induction))
    getRecordConstructor QName
    from StateT ScopeMemo (TCMT IO) (Maybe (QName, Maybe Induction))
    -> (Maybe (QName, Maybe Induction)
        -> StateT ScopeMemo (TCMT IO) ())
    -> StateT ScopeMemo (TCMT IO) ()
    forall a b.
    StateT ScopeMemo (TCMT IO) a
    -> (a -> StateT ScopeMemo (TCMT IO) b)
    -> StateT ScopeMemo (TCMT IO) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
              Just (QName
    con, Maybe Induction
    ind) -> do
                con' <- QName -> WSM QName
    renName QName
    con
                lift $ setRecordConstructor to (con', ind)
              Maybe (QName, Maybe Induction)
    Nothing  -> () -> StateT ScopeMemo (TCMT IO) ()
    forall a. a -> StateT ScopeMemo (TCMT IO) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

            -- 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.
              m <- if QName
    x QName -> ModuleName -> Bool
    `isInModule` ModuleName
    old
                     then ModuleName -> StateT ScopeMemo (TCMT IO) ModuleName
    forall a. a -> StateT ScopeMemo (TCMT IO) a
    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.
              y <- setRange rnew . A.qualify m <$> refresh (qnameName x)
              lift $ reportSLn "scope.copy" 50 $ "  Copying " ++ prettyShow x ++ " to " ++ prettyShow y
              addName x y
              lift (copyName x y)
              copyRecordConstr x y
              return 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.
              z <- ModuleName -> StateT ScopeMemo (TCMT IO) (Maybe (ModuleName, Bool))
    forall {m :: * -> *}.
    MonadState ScopeMemo m =>
    ModuleName -> m (Maybe (ModuleName, Bool))
    findMod ModuleName
    x
              case z of
                Just (ModuleName
    y, Bool
    False) | Bool
    rec -> ModuleName
    y ModuleName
    -> StateT ScopeMemo (TCMT IO) ()
    -> StateT ScopeMemo (TCMT IO) ModuleName
    forall a b.
    a -> StateT ScopeMemo (TCMT IO) b -> StateT ScopeMemo (TCMT IO) a
    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 a. a -> StateT ScopeMemo (TCMT IO) a
    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

                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.
                   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
                   return $ A.mnameFromList $ newM ++ [y]
                -- Andreas, Jesper, 2015-07-02: Issue 1597
                -- Don't copy a module over itself, it will just be emptied of its contents.
                if (x == y) then return x else do
                lift $ reportSLn "scope.copy" 50 $ "  Copying module " ++ prettyShow x ++ " to " ++ prettyShow y
                addMod x y rec
                lift $ createModule Nothing y
                -- We need to copy the contents of included modules recursively (only when 'rec')
                when rec $ copyRec x y
                return y
              where
                copyRec :: ModuleName -> ModuleName -> StateT ScopeMemo (TCMT IO) ()
    copyRec ModuleName
    x ModuleName
    y = do
                  s0 <- ScopeM Scope -> StateT ScopeMemo (TCMT IO) Scope
    forall (m :: * -> *) a. Monad m => m a -> StateT ScopeMemo m a
    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
                  s  <- withCurrentModule' y $ copy y s0
                  lift $ modifyNamedScope y (const s)

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

    -- | Warn about useless fixity declarations in @renaming@ directives.
    --   Monadic for the sake of error reporting.
    checkNoFixityInRenamingModule :: [C.Renaming] -> ScopeM ()
    checkNoFixityInRenamingModule :: [Renaming] -> ScopeM ()
    checkNoFixityInRenamingModule [Renaming]
    ren = do
      Maybe (NonEmpty Range)
    -> (NonEmpty Range -> ScopeM ()) -> ScopeM ()
    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 -> ScopeM ()) -> ScopeM ())
    -> (NonEmpty Range -> ScopeM ()) -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $ \ NonEmpty Range
    rs -> do
        NonEmpty Range -> ScopeM () -> ScopeM ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange NonEmpty Range
    rs (ScopeM () -> ScopeM ()) -> ScopeM () -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $ do
          Warning -> ScopeM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> ScopeM ()) -> Warning -> ScopeM ()
    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

    -- | Check that an import directive doesn't contain repeated names.
    verifyImportDirective :: [C.ImportedName] -> C.HidingDirective -> C.RenamingDirective -> ScopeM ()
    verifyImportDirective :: [ImportedName] -> [ImportedName] -> [Renaming] -> ScopeM ()
    verifyImportDirective [ImportedName]
    usn [ImportedName]
    hdn [Renaming]
    ren =
      [List2 ImportedName]
    -> (List1 (List2 ImportedName) -> ScopeM ()) -> ScopeM ()
    forall (m :: * -> *) a.
    Applicative m =>
    [a] -> (List1 a -> m ()) -> m ()
    List1.unlessNull
        ((List1 ImportedName -> Maybe (List2 ImportedName))
    -> [List1 ImportedName] -> [List2 ImportedName]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe List1 ImportedName -> Maybe (List2 ImportedName)
    forall a. List1 a -> Maybe (List2 a)
    List2.fromList1Maybe ([List1 ImportedName] -> [List2 ImportedName])
    -> ([ImportedName] -> [List1 ImportedName])
    -> [ImportedName]
    -> [List2 ImportedName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [ImportedName] -> [List1 ImportedName]
    forall (f :: * -> *) a. (Foldable f, Eq a) => f a -> [NonEmpty a]
    List1.group ([ImportedName] -> [List1 ImportedName])
    -> ([ImportedName] -> [ImportedName])
    -> [ImportedName]
    -> [List1 ImportedName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [ImportedName] -> [ImportedName]
    forall a. Ord a => [a] -> [a]
    List.sort ([ImportedName] -> [List2 ImportedName])
    -> [ImportedName] -> [List2 ImportedName]
    forall a b. (a -> b) -> a -> b
    $ [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)
        \ List1 (List2 ImportedName)
    yss -> List1 (List2 ImportedName) -> ScopeM () -> ScopeM ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange List1 (List2 ImportedName)
    yss (ScopeM () -> ScopeM ()) -> ScopeM () -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $ TypeError -> ScopeM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> ScopeM ()) -> TypeError -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $ List1 (List2 ImportedName) -> TypeError
    RepeatedNamesInImportDirective List1 (List2 ImportedName)
    yss

    -- | 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 KwRange
    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] -> ScopeM ()
    checkNoFixityInRenamingModule [Renaming]
    ren'

        -- Andreas, 2020-06-06, issue #4707
        -- Duplicates in @using@ directive are dropped with a warning.
        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.
        verifyImportDirective usingList hdn' 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 (missingExports, namesA) = checkExist $ usingList ++ hdn' ++ map renFrom ren'
        () <- List1.unlessNull missingExports \ List1 ImportedName
    missingExports1 -> Range -> ScopeM () -> ScopeM ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange Range
    rng do
          [Char] -> Int -> [Char] -> ScopeM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "scope.import.apply" Int
    30 ([Char] -> ScopeM ()) -> [Char] -> ScopeM ()
    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 -> ScopeM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> ScopeM ()) -> Warning -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> [Name] -> [Name] -> List1 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) List1 ImportedName
    missingExports1

        -- We can now define a cleaned-up version of the import directive.
        let 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 -> Bool) -> [ImportedName] -> [ImportedName]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ImportedName -> Bool
    notMissing [ImportedName]
    usingList        -- remove missingExports from usn'
        let hdn = (ImportedName -> Bool) -> [ImportedName] -> [ImportedName]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ImportedName -> Bool
    notMissing [ImportedName]
    hdn'             -- remove missingExports from hdn'
        let 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 = Range
    -> Using' Name Name
    -> [ImportedName]
    -> [Renaming]
    -> Maybe KwRange
    -> ImportDirective
    forall n m.
    Range
    -> Using' n m
    -> HidingDirective' n m
    -> RenamingDirective' n m
    -> Maybe KwRange
    -> 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 KwRange
    public

        -- Convenient shorthands for defined names and names brought into scope:
        let 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 = (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]
    usn [ImportedName] -> [ImportedName] -> [ImportedName]
    forall a. [a] -> [a] -> [a]
    ++ [ImportedName]
    definedNames

        -- Efficient test of (`elem` names):
        let 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
    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@.

        dir' <- sanityCheck (not . inNames) $ addExtraModules extra dir

        -- Check for duplicate imports in a single import directive.
        -- @dup@ : To be imported names that are mentioned more than once.
        () <- List1.unlessNull (allDuplicates targetNames) $ \ List1 ImportedName
    dup ->
          TypeError -> ScopeM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> ScopeM ()) -> TypeError -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> List1 ImportedName -> TypeError
    DuplicateImports QName
    m List1 ImportedName
    dup

        -- Apply the import directive.
        let (scope', (nameClashes, moduleClashes)) = applyImportDirective_ dir' scope

        -- Andreas, 2019-11-08, issue #4154, report clashes
        -- introduced by the @renaming@.
        Set1.unlessNull nameClashes \ Set1 Name
    nameClashes ->
          Warning -> ScopeM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> ScopeM ()) -> Warning -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $ NameOrModule -> Set1 Name -> Warning
    ClashesViaRenaming NameOrModule
    NameNotModule Set1 Name
    nameClashes
        Set1.unlessNull moduleClashes \ Set1 Name
    moduleClashes ->
          Warning -> ScopeM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> ScopeM ()) -> Warning -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $ NameOrModule -> Set1 Name -> Warning
    ClashesViaRenaming NameOrModule
    ModuleNotName Set1 Name
    moduleClashes

        -- Look up the defined names in the new scope.
        let namesInScope'   = (Scope -> NamesInScope
    forall a. InScope a => Scope -> ThingsInScope a
    allNamesInScope Scope
    scope' :: ThingsInScope AbstractName)
        let modulesInScope' = (Scope -> ModulesInScope
    forall a. InScope a => Scope -> ThingsInScope a
    allNamesInScope Scope
    scope' :: ThingsInScope AbstractModule)
        let look k
    x = NonEmpty c -> c
    forall a. NonEmpty a -> a
    List1.head (NonEmpty c -> c)
    -> (Map k (NonEmpty c) -> NonEmpty c) -> Map k (NonEmpty c) -> c
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NonEmpty c -> k -> Map k (NonEmpty c) -> NonEmpty c
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault NonEmpty 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]
    -> (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 (NonEmpty 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 (NonEmpty c) -> c
    look Name
    x ModulesInScope
    modulesInScope'

        let 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
        return (adir, 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 a. a -> TCMT IO a
    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 -> ScopeM ()) -> ScopeM ()
    forall (m :: * -> *) a.
    Applicative m =>
    [a] -> (List1 a -> m ()) -> m ()
    List1.unlessNull [ImportedName]
    dups ((List1 ImportedName -> ScopeM ()) -> ScopeM ())
    -> (List1 ImportedName -> ScopeM ()) -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $ Warning -> ScopeM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> ScopeM ())
    -> (List1 ImportedName -> Warning)
    -> List1 ImportedName
    -> ScopeM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 ImportedName -> Warning
    DuplicateUsing
            [ImportedName] -> ScopeM [ImportedName]
    forall a. a -> TCMT IO a
    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] -> (List1 ImportedName -> m ()) -> m ()
    forall (m :: * -> *) a.
    Applicative m =>
    [a] -> (List1 a -> m ()) -> m ()
    List1.unlessNull ((ImportedName -> Bool) -> [ImportedName] -> [ImportedName]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ImportedName -> Bool
    useless [ImportedName]
    ys) ((List1 ImportedName -> m ()) -> m ())
    -> (List1 ImportedName -> m ()) -> m ()
    forall a b. (a -> b) -> a -> b
    $ Warning -> m ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> m ())
    -> (List1 ImportedName -> Warning) -> List1 ImportedName -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 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.
              return dir{ hiding = [] }
          ImportDirective
    dir -> ImportDirective -> m ImportDirective
    forall a. a -> m a
    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       = mapUsing (concatMap addExtra) $ using dir
             , hiding      = concatMap addExtra            $ hiding dir
             , impRenaming = concatMap extraRenaming       $ impRenaming 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 (List1 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 (List1 b) -> Either err b
    resolve ImportedName
    name Name
    x ModulesInScope
    modulesInScope
          where
            resolve :: Ord a => err -> a -> Map a (List1 b) -> Either err b
            resolve :: forall a err b.
    Ord a =>
    err -> a -> Map a (List1 b) -> Either err b
    resolve err
    err a
    x Map a (List1 b)
    m = Either err b
    -> (List1 b -> Either err b) -> Maybe (List1 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) -> (List1 b -> b) -> List1 b -> Either err b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 b -> b
    forall a. NonEmpty a -> a
    List1.head) (Maybe (List1 b) -> Either err b)
    -> Maybe (List1 b) -> Either err b
    forall a b. (a -> b) -> a -> b
    $ a -> Map a (List1 b) -> Maybe (List1 b)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup a
    x Map a (List1 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 KwRange
    open) =
      Range
    -> Using' n2 m2
    -> HidingDirective' n2 m2
    -> RenamingDirective' n2 m2
    -> Maybe KwRange
    -> ImportDirective' n2 m2
    forall n m.
    Range
    -> Using' n m
    -> HidingDirective' n m
    -> RenamingDirective' n m
    -> Maybe KwRange
    -> 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 KwRange
    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 a b. (a -> b -> b) -> b -> [a] -> b
    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
      current <- ScopeM ModuleName
    forall (m :: * -> *). ReadTCState m => m ModuleName
    getCurrentModule
      m <- caseMaybe mam (amodName <$> resolveModule cm) return
      let acc | Maybe KwRange
    Nothing <- ImportDirective -> Maybe KwRange
    forall n m. ImportDirective' n m -> Maybe KwRange
    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.
      (adir, s') <- applyImportDirectiveM cm dir . inScopeBecause (Opened cm) .
                    noGeneralizedVarsIfLetOpen kind =<< getNamedScope m
      let s  = NameSpaceId -> Scope -> Scope
    setScopeAccess NameSpaceId
    acc Scope
    s'
      let ns = NameSpaceId -> Scope -> NameSpace
    scopeNameSpace NameSpaceId
    acc Scope
    s
      modifyCurrentScope (`mergeScope` 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.
      checkForClashes

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

      return adir

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

            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, NonEmpty AbstractName) -> Bool)
    -> [(Name, NonEmpty AbstractName)]
    -> [(Name, NonEmpty AbstractName)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (\ (Name
    _c, NonEmpty AbstractName
    as) -> NonEmpty AbstractName -> Int
    forall a. NonEmpty a -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length NonEmpty AbstractName
    as Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    2) ([(Name, NonEmpty AbstractName)]
     -> [(Name, NonEmpty AbstractName)])
    -> [(Name, NonEmpty AbstractName)]
    -> [(Name, NonEmpty AbstractName)]
    forall a b. (a -> b) -> a -> b
    $ NamesInScope -> [(Name, NonEmpty AbstractName)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (NamesInScope -> [(Name, NonEmpty AbstractName)])
    -> NamesInScope -> [(Name, NonEmpty AbstractName)]
    forall a b. (a -> b) -> a -> b
    $ NameSpace -> NamesInScope
    nsNames NameSpace
    exported
                modClashes = ((Name, NonEmpty AbstractModule) -> Bool)
    -> [(Name, NonEmpty AbstractModule)]
    -> [(Name, NonEmpty AbstractModule)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (\ (Name
    _c, NonEmpty AbstractModule
    as) -> NonEmpty AbstractModule -> Int
    forall a. NonEmpty a -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length NonEmpty AbstractModule
    as Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    2) ([(Name, NonEmpty AbstractModule)]
     -> [(Name, NonEmpty AbstractModule)])
    -> [(Name, NonEmpty AbstractModule)]
    -> [(Name, NonEmpty AbstractModule)]
    forall a b. (a -> b) -> a -> b
    $ ModulesInScope -> [(Name, NonEmpty AbstractModule)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (ModulesInScope -> [(Name, NonEmpty AbstractModule)])
    -> ModulesInScope -> [(Name, NonEmpty 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 or only to pattern synonyms.
                defClash (a
    _, t AbstractName
    qs) = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    or
                  [ (KindOfName -> Bool) -> t 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) t KindOfName
    ks
                  , (KindOfName -> Bool) -> t 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)         t KindOfName
    ks
                  , (KindOfName -> Bool) -> t KindOfName -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (KindOfName -> KindOfName -> Bool
    forall a. Eq a => a -> a -> Bool
    == KindOfName
    PatternSynName)  t KindOfName
    ks
                  ]
                  where ks :: t KindOfName
    ks = (AbstractName -> KindOfName) -> t AbstractName -> t KindOfName
    forall a b. (a -> b) -> t a -> t b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap AbstractName -> KindOfName
    anameKind t AbstractName
    qs
            -- We report the first clashing exported identifier.
            () <- List1.unlessNull (filter defClash defClashes) $
              \ ((Name
    x, AbstractName
    q :| [AbstractName]
    _) :| [(Name, NonEmpty AbstractName)]
    _) -> TypeError -> ScopeM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> ScopeM ()) -> TypeError -> ScopeM ()
    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

            List1.unlessNull modClashes $ \ ((Name
    _, NonEmpty AbstractModule
    ms) :| [(Name, NonEmpty AbstractModule)]
    _) -> do
              Maybe (AbstractModule, AbstractModule)
    -> ScopeM ()
    -> ((AbstractModule, AbstractModule) -> ScopeM ())
    -> ScopeM ()
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe (NonEmpty AbstractModule -> Maybe (AbstractModule, AbstractModule)
    forall a. List1 a -> Maybe (a, a)
    List1.last2 NonEmpty AbstractModule
    ms) ScopeM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (((AbstractModule, AbstractModule) -> ScopeM ()) -> ScopeM ())
    -> ((AbstractModule, AbstractModule) -> ScopeM ()) -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $ \ (AbstractModule
    m0, AbstractModule
    m1) -> do
                TypeError -> ScopeM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> ScopeM ()) -> TypeError -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> ModuleName -> TypeError
    ClashingModule (AbstractModule -> ModuleName
    amodName AbstractModule
    m0) (AbstractModule -> ModuleName
    amodName AbstractModule
    m1)