Agda-2.9.0: src/full/Agda/Syntax/Scope/Monad.hs
{-# LANGUAGE NondecreasingIndentation #-}
{-| The scope monad with operations.
-}
module Agda.Syntax.Scope.Monad (module Agda.Syntax.Scope.Monad, module Agda.Syntax.Scope.State) where
import Prelude hiding (null)
import Control.Monad.Except ( MonadError, throwError, runExceptT )
import Control.Monad.State ( StateT, runStateT, gets, modify )
import Control.Monad.Trans ( MonadTrans, lift )
import Control.Monad.IO.Class
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.IORef
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 Agda.Syntax.Abstract qualified 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.Syntax.Scope.State
import Agda.Syntax.Scope.UnusedImports (lookedupModule, registerModuleOpening)
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.Tuple ((***), pattern Pair)
import Agda.Utils.Impossible
-- Debugging
printLocals :: Int -> String -> ScopeM ()
printLocals v s = verboseS "scope.top" v $ do
locals <- getLocalVars
reportSLn "scope.top" v $ s ++ " " ++ prettyShow locals
scopeWarning' :: CallStack -> DeclarationWarning' -> ScopeM ()
scopeWarning' loc = warning' loc . NicifierIssue . DeclarationWarning loc
scopeWarning :: HasCallStack => DeclarationWarning' -> ScopeM ()
scopeWarning = withCallerCallStack scopeWarning'
---------------------------------------------------------------------------
-- * General operations
---------------------------------------------------------------------------
isDatatypeModule :: ReadTCState m => A.ModuleName -> m (Maybe DataOrRecordModule)
isDatatypeModule m = do
scopeDatatypeModule . Map.findWithDefault __IMPOSSIBLE__ m <$> useScope scopeModules
getNamedScope :: A.ModuleName -> ScopeM Scope
getNamedScope m = do
scope <- getScope
case Map.lookup m (scope ^. scopeModules) of
Just s -> return s
Nothing -> do
reportSLn "" 0 $ "ERROR: In scope\n" ++ prettyShow scope ++ "\nNO SUCH SCOPE " ++ prettyShow m
__IMPOSSIBLE__
getCurrentScope :: ScopeM Scope
getCurrentScope = getNamedScope =<< 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 b m = do
reportSLn "scope.createModule" 30 $ "createModule " ++ prettyShow m
s <- getCurrentScope
let parents = scopeName s : scopeParents s
sm = 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
-- András, 2025-08-30: TODO: only inverse modules need to be recomputed
recomputeInverseScope
-- | Apply a function to the scope map.
modifyScopes :: (Map A.ModuleName Scope -> Map A.ModuleName Scope) -> ScopeM ()
modifyScopes = modifyScope . over scopeModules
-- | Apply a function to the given scope.
modifyNamedScope :: A.ModuleName -> (Scope -> Scope) -> ScopeM ()
modifyNamedScope m f = modifyScopes $ Map.adjust f m
-- | Apply a function to the current scope.
modifyCurrentScope :: (Scope -> Scope) -> ScopeM ()
modifyCurrentScope f = getCurrentModule >>= (`modifyNamedScope` f)
setContextPrecedence :: PrecedenceStack -> ScopeM ()
setContextPrecedence = modifyScope . set scopePrecedence
withContextPrecedence :: ReadTCState m => Precedence -> m a -> m a
withContextPrecedence p =
locallyTCState (stScope . scopePrecedence) $ pushPrecedence p
getLocalVars :: ReadTCState m => m LocalVars
getLocalVars = useScope scopeLocals
modifyLocalVars :: (LocalVars -> LocalVars) -> ScopeM ()
modifyLocalVars = modifyScope . updateScopeLocals
setLocalVars :: LocalVars -> ScopeM ()
setLocalVars vars = modifyLocalVars $ const vars
-- | Run a computation without changing the local variables.
withLocalVars :: ScopeM a -> ScopeM a
withLocalVars = bracket_ getLocalVars 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 n m = do
inner <- take n <$> 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 = bracket_ getLocalVars $ \ lvarsOld ->
checkNoShadowing lvarsOld =<< getLocalVars
checkNoShadowing :: LocalVars -- ^ Old local scope
-> LocalVars -- ^ New local scope
-> ScopeM ()
checkNoShadowing old new = do
opts <- 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 = dropEnd (length old) new
-- Filter out the underscores.
let newNames = filter (not . isNoName) $ AssocList.keys diff
-- Associate each name to its occurrences.
let nameOccs1 :: [(C.Name, List1 Range)]
nameOccs1 = Map.toList $ Map.fromListWith (<>) $ map pairWithRange newNames
-- Warn if we have two or more occurrences of the same name.
let nameOccs2 :: [(C.Name, List2 Range)]
nameOccs2 = mapMaybe (traverseF List2.fromList1Maybe) nameOccs1
caseList nameOccs2 (return ()) $ \ c conflicts -> do
scopeWarning $ ShadowingInTelescope $ c :| conflicts
where
pairWithRange :: C.Name -> (C.Name, List1 Range)
pairWithRange n = (n, singleton $ getRange n)
getVarsToBind :: ScopeM LocalVars
getVarsToBind = useScope scopeVarsToBind
addVarToBind :: C.Name -> LocalVar -> ScopeM ()
addVarToBind x y = modifyScope $ updateVarsToBind $ AssocList.insert x y
-- | After collecting some variable names in the scopeVarsToBind,
-- bind them all simultaneously.
bindVarsToBind :: ScopeM ()
bindVarsToBind = do
vars <- getVarsToBind
modifyLocalVars (vars ++)
printLocals 30 "bound variables:"
modifyScope $ setVarsToBind []
annotateDecls :: ReadTCState m => m [A.Declaration] -> m (Maybe A.Declaration)
annotateDecls m = do
forMM (List1.nonEmpty <$> m) \ ds1 -> do
getScope <&> (`A.ScopedDecl` ds1)
annotateExpr :: ReadTCState m => m A.Expr -> m A.Expr
annotateExpr m = do
e <- 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 fx x = do
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_ = freshAbstractName noFixity'
-- | Create a fresh abstract qualified name.
freshAbstractQName :: Fixity' -> C.Name -> ScopeM A.QName
freshAbstractQName fx x = do
y <- freshAbstractName fx x
m <- getCurrentModule
return $ A.qualify m y
freshAbstractQName' :: C.Name -> ScopeM A.QName
freshAbstractQName' x = do
fx <- getConcreteFixity 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 r i s = do
let cname = C.Name r C.NotInScope $ singleton $ Id $ stringToRawName $ s ++ show i
resolveName (C.QName cname) >>= \case
UnknownName -> return cname
_ -> freshConcreteName r (i + 1) s
---------------------------------------------------------------------------
-- * Resolving names
---------------------------------------------------------------------------
-- | Look up the abstract name referred to by a given concrete name.
resolveName :: C.QName -> ScopeM ResolvedName
resolveName = resolveName' allKindsOfNames 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' kinds names x = runExceptT (tryResolveName kinds names x) >>= \case
Left (IllegalAmbiguity reason) -> do
reportS "scope.resolve" 60 $ unlines $
"resolveName': ambiguous name" :
map (show . qnameName) (toList $ ambiguousNamesInReason reason)
setCurrentRange x $ typeError $ AmbiguousName x reason
Left (ConstrOfNonRecord q r) -> case r of
UnknownName -> setCurrentRange x $ typeError $ I.NotInScope q
_ -> setCurrentRange x $ typeError $ ConstructorNameOfNonRecord r
Right x' -> pure 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 kinds names x = do
scope <- getScope
let
vars = AssocList.mapKeysMonotonic C.QName $ scope ^. scopeLocals
throwAmb = throwError . IllegalAmbiguity
case lookup x vars of
-- Case: we have a local variable x, but is (perhaps) shadowed by some imports ys.
Just var@(LocalVar y b ys) ->
-- We may ignore the imports filtered out by the @names@ filter.
case nonEmpty $ filterNames id ys of
Nothing -> return $ VarName y{ nameConcrete = unqualify x } b
Just ys' -> throwAmb $ AmbiguousLocalVar var ys'
-- Case: we do not have a local variable x.
Nothing -> do
-- Consider only names that are in the given set of names and
-- are of one of the given kinds
let filtKind = filter $ (`elemKindsOfNames` kinds) . anameKind . fst
possibleNames z = filtKind $ filterNames fst $ scopeLookup' z 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 <- canHaveSuffixTest
let (xsuffix, xbase) = (C.lensQNameName . nameSuffix) (,Nothing) x
possibleBaseNames = filter (canHaveSuffix . anameName . fst) $ possibleNames xbase
suffixedNames = (,) <$> fromConcreteSuffix xsuffix <*> nonEmpty possibleBaseNames
case (nonEmpty $ possibleNames x) of
Just ds | Just ks <- traverse (isConName . anameKind . fst) ds
-- all names resolve to a constructor name
, isNothing suffixedNames ->
return $ ConstructorName (Set1.fromList ks) $ fmap (upd . fst) ds
Just ds | all ((FldName ==) . anameKind . fst) ds , isNothing suffixedNames ->
return $ FieldName $ fmap (upd . fst) ds
Just ds | all ((PatternSynName ==) . anameKind . fst) ds , isNothing suffixedNames ->
return $ PatternSynResName $ fmap (upd . fst) ds
Just ((d, a) :| ds) -> case (suffixedNames, ds) of
(Nothing, []) ->
return $ DefinedName a (upd d) A.NoSuffix
(Nothing, (d',_) : ds') ->
throwAmb $ AmbiguousDeclName $ List2 d d' $ map fst ds'
(Just (_, ss), _) ->
throwAmb $ AmbiguousDeclName $ List2.append (d :| map fst ds) (fmap fst ss)
Nothing -> case suffixedNames of
-- Name is of the form R.constructor but did not resolve.
-- Since the record constructor is bound as @constructor@ in the
-- scope of the record module R (see 'bindRecordConstructorPseudoName'),
-- this means that R is not (the module of) a record type.
-- Produce a more informative error than "not in scope".
Nothing | Just r <- isRecordConstructor 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.
tryResolveName AllKindsOfNames Nothing r >>= \case
-- If R does resolve to a record type, its constructor is
-- simply not in scope here; report the plain not-in-scope error.
DefinedName _ d _ | anameKind d == RecName -> return UnknownName
-- If R is not a name but a module (e.g. a copy of a record module),
-- report R.constructor rather than R as not in scope.
UnknownName | not $ null (scopeLookup r scope :: [AbstractModule]) ->
return UnknownName
recd -> throwError $ ConstrOfNonRecord r recd
Nothing -> return UnknownName
Just (suffix , (d, a) :| []) -> return $ DefinedName a (upd d) suffix
Just (suffix , (d1,_) :| (d2,_) : sds) ->
throwAmb $ AmbiguousDeclName $ List2 d1 d2 $ map fst 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 = case names of
Nothing -> \ f -> id
Just ns -> \ f -> filter $ (`Set1.member` ns) . A.qnameName . anameName . f
-- lambda-dropped style by intention
upd d = updateConcreteName d $ unqualify x
updateConcreteName :: AbstractName -> C.Name -> AbstractName
updateConcreteName d@(AbsName { anameName = A.QName qm qn }) x =
d { anameName = A.QName (setRange (getRange x) qm) (qn { nameConcrete = x }) }
fromConcreteSuffix = \case
Nothing -> Nothing
Just C.Prime{} -> Nothing
Just (C.Index i) -> Just $ A.Suffix i
Just (C.Subscript i) -> Just $ A.Suffix 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 = do
builtinProp <- getBuiltinName' builtinProp
builtinSet <- getBuiltinName' builtinSet
builtinSSet <- getBuiltinName' builtinStrictSet
builtinPropOmega <- getBuiltinName' builtinPropOmega
builtinSetOmega <- getBuiltinName' builtinSetOmega
builtinSSetOmega <- getBuiltinName' builtinSSetOmega
return $ \x -> Just x `elem` [builtinProp, builtinSet, builtinSSet, builtinPropOmega, builtinSetOmega, builtinSSetOmega]
-- | Look up a module in the scope.
-- Marks the module as used for the unused-imports analysis.
resolveModule :: C.QName -> ScopeM AbstractModule
resolveModule x = do
ms <- scopeLookup x <$> getScope
caseMaybe (nonEmpty ms) (typeError $ NoSuchModule x) $ \ case
AbsModule m why :| [] -> do
let am = AbsModule (m `withRangeOf` x) why
am <$ lookedupModule x am
ms -> typeError $ AmbiguousModule x (fmap amodName ms)
-- | Get the fixity of a not yet bound name.
getConcreteFixity :: C.Name -> ScopeM Fixity'
getConcreteFixity x = Map.findWithDefault noFixity' x <$> useScope scopeFixities
-- | Get the polarities of a not yet bound name.
getConcretePolarity :: C.Name -> ScopeM (Maybe PragmaPolarities)
getConcretePolarity x = Map.lookup x <$> useScope scopePolarities
instance MonadFixityError ScopeM where
throwMultipleFixityDecls xs = case xs of
(_, Pair _ f2) :| _ -> setCurrentRange (theNameRange f2) $ typeError $ MultipleFixityDecls xs
throwMultiplePolarityPragmas xs = case xs of
x :| _ -> setCurrentRange (getRange x) $ typeError $ MultiplePolarityPragmas xs
warnUnknownNamesInFixityDecl = scopeWarning . UnknownNamesInFixityDecl
warnUnknownNamesInPolarityPragmas = scopeWarning . UnknownNamesInPolarityPragmas
warnUnknownFixityInMixfixDecl = scopeWarning . UnknownFixityInMixfixDecl
warnPolarityPragmasButNotPostulates = scopeWarning . PolarityPragmasButNotPostulates
warnEmptyPolarityPragma = scopeWarning . EmptyPolarityPragma
warnFixityDeclarationForNonOperator r x = scopeWarning $ FixityDeclarationForNonOperator r x
-- | 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 warn ds cont = do
!fp <- fixitiesAndPolarities warn 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 x ns = do
r <- resolveName' allKindsOfNames (Just ns) x
case r of
VarName y _ -> return $ namesToNotation x y
DefinedName _ d _ -> return $ notation d
FieldName ds -> return $ oneNotation ds
ConstructorName _ ds-> return $ oneNotation ds
PatternSynResName n -> return $ oneNotation n
UnknownName -> __IMPOSSIBLE__
where
notation = namesToNotation x . qnameName . anameName
oneNotation = List1.head . mergeNotations . fmap notation
---------------------------------------------------------------------------
-- * Binding names
---------------------------------------------------------------------------
-- | Bind a variable.
bindVariable
:: A.BindingSource -- ^ @λ@, @Π@, @let@, ...?
-> C.Name -- ^ Concrete name.
-> A.Name -- ^ Abstract name.
-> ScopeM ()
bindVariable b x y = modifyLocalVars $ AssocList.insert x $ LocalVar y b []
-- | Temporarily unbind a variable. Used for non-recursive lets.
unbindVariable :: C.Name -> ScopeM a -> ScopeM a
unbindVariable x = bracket_ (getLocalVars <* modifyLocalVars (AssocList.delete x)) (modifyLocalVars . const)
-- | Bind a defined name. Must not shadow anything.
bindName :: Access -> KindOfName -> C.Name -> A.QName -> ScopeM ()
bindName acc kind x y = bindName' acc kind noMetadata x y
bindName' :: Access -> KindOfName -> NameMetadata -> C.Name -> A.QName -> ScopeM ()
bindName' acc kind meta x y = whenJustM (bindName'' acc kind meta x y) typeError
addNameToInverseScope :: KindOfName -> C.Name -> AbstractName -> ScopeInfo -> ScopeInfo
addNameToInverseScope kind x y s =
let !y' = anameName y
in s { _scopeInScope = Set.insert y' (_scopeInScope s)
, _scopeInverseName = HMap.insertWith (<>) (A.nameId y')
(NameMapEntry kind (C.QName x :| [])) (_scopeInverseName s)
}
-- | 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'' acc kind meta x y = do
when (isNoName x) $ do
modifyScopes $ Map.map $ removeNameFromScope PrivateNS x
recomputeInverseScope
r <- resolveName (C.QName x)
let y' :: Either TypeError AbstractName
y' = case r of
-- Binding an anonymous declaration always succeeds.
-- In case it's not the first one, we simply remove the one that came before
_ | isNoName x -> success
DefinedName _ d _ -> clash $ ClashingAbstractName d
VarName z _ -> clash $ ClashingQName $ A.qualify_ z
FieldName ds -> ambiguous (== FldName) ds
ConstructorName i ds-> ambiguous (isJust . isConName) ds
PatternSynResName n -> ambiguous (== PatternSynName) n
UnknownName -> success
let ns = if isNoName x then PrivateNS else localNameSpace acc
forM_ y' \y' -> do
modifyCurrentScope $ addNameToScope ns x y'
modifyScope $ addNameToInverseScope kind x y'
pure $ either Just (const Nothing) y'
where
success = Right $ AbsName y kind Defined meta
clash n = Left $ ClashingDefinition (C.QName x) n Nothing
ambiguous f ds =
if f kind && all (f . anameKind) ds
then success else clash $ ClashingAbstractName $ List1.head 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 -> NameMetadata -> C.Name -> A.QName -> ScopeM ()
rebindName acc kind meta x y = do
if kind == ConName then do
modifyCurrentScope $
mapScopeNS (localNameSpace acc)
(Map.update (nonEmpty . List1.filter ((ConName ==) . anameKind)) x)
id
id
else do
modifyCurrentScope $ removeNameFromScope (localNameSpace acc) x
recomputeInverseScope
bindName' acc kind meta x y
-- András, 2025-08-30: TODO: directly extend inverse scope.
-- | Bind a module name.
bindModule :: Access -> C.Name -> A.ModuleName -> ScopeM ()
bindModule acc x m = do
modifyCurrentScope $ addModuleToScope (localNameSpace acc) x (AbsModule m Defined)
recomputeInverseScope
-- | Bind a qualified module name. Adds it to the imports field of the scope.
bindQModule :: Access -> C.QName -> A.ModuleName -> ScopeM ()
bindQModule acc q m = do
modifyCurrentScope $ \s -> s { scopeImports = Map.insert q m (scopeImports s) }
recomputeInverseScope
---------------------------------------------------
-- * Operations to do with record constructor names
---------------------------------------------------
-- | Bind the pseudo-name @constructor@ in the scope of the record module,
-- mapping it to the (possibly anonymous) constructor of the record.
--
-- This is what makes @R.constructor@ resolve: @R@ is the record /module/
-- and @constructor@ an ordinary name in it, so no special treatment is
-- needed when resolving the qualified name @R.constructor@.
--
-- Note that @constructor@ is a keyword, thus, it can never be parsed
-- as an unqualified name. In particular, @open R@ does not make the
-- record constructor accessible under the name @constructor@, and
-- @constructor@ cannot be mentioned in @using@, @hiding@ or @renaming@.
--
-- This does not put the record constructor itself into the record module
-- (which would be wrong, see issue #4189, since the record module is
-- parameterized over the record value, but the constructor is not);
-- it only adds this alias for it.
bindRecordConstructorPseudoName :: A.ModuleName -> KindOfName -> A.QName -> ScopeM ()
bindRecordConstructorPseudoName m kind y = do
modifyNamedScope m $
addNameToScope PublicNS recordConstructorPseudoName $
AbsName y kind Defined noMetadata
-- Note: we cannot use 'addNameToInverseScope' here, since that would
-- register the unqualified (and thus unparseable) rendering @constructor@.
recomputeInverseScope
-- | Remove the record constructor pseudo-name from the scope of a record module.
--
-- The alias @constructor@ is only meant to be used in the qualified form
-- @R.constructor@, where @R@ is the record module. Thus, it is not brought
-- into scope by @open R@.
--
-- It is also not copied when the record module @R@ itself is applied to
-- arguments (as in @module M = R@): the record module is parameterized over
-- the record value, but the record constructor is not (issue #4189).
-- (When @R@ is only copied as a submodule of the applied module, the
-- constructor is copied correctly, since the arguments are then taken from
-- the enclosing module.)
dropRecordConstructorPseudoName :: Scope -> Scope
dropRecordConstructorPseudoName s
| Just IsRecordModule <- scopeDatatypeModule s =
-- We don't have enough information for an incremental update of the
-- in-scope sets, so recompute them (cheap: record modules are small).
recomputeInScopeSets $ mapScope_ (Map.delete recordConstructorPseudoName) id id s
| otherwise = s
-- | The pseudo-name @constructor@ under which the constructor of a record
-- is bound in the scope of the record module.
--
-- Since @constructor@ is a keyword, this name is only reachable
-- as the tail of a qualified name, e.g., @R.constructor@.
recordConstructorPseudoName :: C.Name
recordConstructorPseudoName = C.simpleName "constructor"
-- | Is this the qualified name which refers to the constructor of a
-- record (like @Foo.constructor@)?
--
-- If so, return the part of the name referring to the record (@Foo@).
--
-- This is only used to produce a good error message when @Foo.constructor@
-- does not resolve; the resolution itself goes through the ordinary
-- scope lookup, see 'bindRecordConstructorPseudoName'.
isRecordConstructor :: C.QName -> Maybe C.QName
isRecordConstructor = fmap to . toplevel where
toplevel, is :: C.QName -> Maybe [C.Name]
toplevel (Qual r n) = (r:) <$> is n
toplevel _ = Nothing
is (C.Qual r n) = (r:) <$> is n
is (C.QName n) = case n of
C.Name _ _ (Id w :| [])
| w == "constructor" -> pure []
_ -> Nothing
to [] = __IMPOSSIBLE__
to [x] = C.QName x
to (x:xs) = C.Qual x (to xs)
---------------------------------------------------------------------------
-- * Module manipulation operations
---------------------------------------------------------------------------
-- | Clear the scope of any no names.
stripNoNames :: ScopeM ()
stripNoNames = do
let stripN = Map.filterWithKey $ const . not . isNoName
modifyScopes $ Map.map $ mapScope_ stripN stripN id
recomputeInverseScope
type WSM = StateT ScopeMemo ScopeM
data ScopeMemo = ScopeMemo
{ memoNames :: A.Ren A.QName
, 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 names mods) =
ScopeCopyInfo
{ renNames = names
, renModules = Map.map (pure . fst) mods
}
-- | Mark a name as being a copy in the TC state, associating it with
-- the given 'A.ScopeCopyRef' for liveness information.
copyName :: A.QName -> A.QName -> ScopeM ()
copyName from to = do
from <- fromMaybe from . HMap.lookup from <$> useTC stCopiedNames
modifyTCLens stCopiedNames $ HMap.insert to from
let
k Nothing = Just (HSet.singleton to)
k (Just s) = Just (HSet.insert to 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 oldc new0 s =
(inScopeBecause (Applied oldc) *** memoToScopeInfo) <$>
runStateT (copy new0 $ dropRecordConstructorPseudoName s) (ScopeMemo mempty mempty)
where
copy :: A.ModuleName -> Scope -> WSM Scope
copy new s = do
lift $ reportSLn "scope.copy" 20 $ "Copying scope " ++ prettyShow old ++ " to " ++ prettyShow new
lift $ reportSLn "scope.copy" 50 $ prettyShow s
s0 <- lift $ getNamedScope new
-- Delete private names, then copy names and modules. Recompute inScope
-- set and name parts rather than trying to copy them.
s' <- recomputeNameParts . recomputeInScopeSets <$>
mapScopeM_ copyD copyM return (setNameSpace PrivateNS emptyNameSpace s)
-- Fix name and parent.
return $ s' { scopeName = scopeName s0
, scopeParents = scopeParents s0
}
where
rnew = getRange new
new' = killRange new
newL = A.mnameToList new'
old = scopeName s
copyD :: NamesInScope -> WSM NamesInScope
copyD = Map.traverseWithKey \ x -> mapM $ onName $ renNameFor x
-- Andreas, 2026-08-23:
-- The pseudo-name @constructor@ bound in a record module
-- (see 'bindRecordConstructorPseudoName') is only an alias for the record
-- constructor. If the record has a named constructor, the latter lives
-- outside the record module, and copying the alias like an ordinary name
-- would produce a second copy of the constructor (plus a spurious copy of
-- the module the constructor lives in). Thus, reuse the existing copy.
renNameFor :: C.Name -> A.QName -> WSM A.QName
renNameFor x y
| x == recordConstructorPseudoName =
maybe (renName y) (return . List1.head) =<< findName y
| otherwise = renName y
copyM :: ModulesInScope -> WSM ModulesInScope
copyM = traverse $ mapM $ lensAmodName renMod
onName :: (A.QName -> WSM A.QName) -> AbstractName -> WSM AbstractName
onName f d =
case anameKind d of
PatternSynName -> return d -- Pattern synonyms are simply aliased, not renamed
_ -> lensAnameName f d
-- Adding to memo structure.
addName x y = modify $ \ i -> i { memoNames = Map.insertWith (<>) x (pure y) (memoNames i) }
addMod x y rec = modify $ \ i -> i { memoModules = Map.insert x (y, rec) (memoModules i) }
-- Querying the memo structure.
findName :: A.QName -> WSM (Maybe (List1 A.QName))
findName x = gets (Map.lookup x . memoNames)
findMod x = gets (Map.lookup x . memoModules)
refresh :: A.Name -> WSM A.Name
refresh x = do
i <- lift fresh
return $ x { A._nameId = i }
-- Change a binding M.x -> old.M'.y to M.x -> new.M'.y
renName :: A.QName -> WSM A.QName
renName 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 x `isInModule` old
then return new'
else renMod' False (qnameModule 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)
return y
-- Change a binding M.x -> old.M'.y to M.x -> new.M'.y
renMod :: A.ModuleName -> WSM A.ModuleName
renMod = renMod' True
renMod' rec x = do
-- Andreas, issue 1607:
-- If we have already copied this module, return the copy.
z <- findMod x
case z of
Just (y, False) | rec -> y <$ copyRec x y
Just (y, _) -> return y
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 = if x `isLtChildModuleOf` old then newL else mnameToList 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 <- refresh $ lastWithDefault __IMPOSSIBLE__ $ A.mnameToList 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 x y = do
s0 <- lift $ getNamedScope x
s <- withCurrentModule' y $ copy y s0
-- András, 2025-08-30: inverse scope will be computed immediately after copyScope returns
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 ren = do
whenJust (nonEmpty $ mapMaybe rangeOfUselessInfix ren) $ \ rs -> do
setCurrentRange rs $ do
warning $ FixityInRenamingModule rs
where
rangeOfUselessInfix :: C.Renaming -> Maybe Range
rangeOfUselessInfix = \case
Renaming ImportedModule{} _ mfx _ -> getRange <$> mfx
_ -> Nothing
-- | Warn about fixity declarations for targets that are non-operators
-- or closed operators:
checkNoFixityForClosedOperator :: [C.Renaming] -> ScopeM ()
checkNoFixityForClosedOperator ren = do
forM_ ren \case
Renaming (ImportedName _) (ImportedName x) mfx r
| Just _ <- mfx, not (isPrePostOrInfixOperator x) -> warnFixityDeclarationForNonOperator r x
| otherwise -> pure ()
Renaming ImportedModule{} ImportedModule{} _ _ -> pure ()
_ -> __IMPOSSIBLE__
-- | 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 m (ImportDirective rng usn' hdn' ren' public) scope0 = do
-- Module names do not come with fixities, thus, we should complain if the
-- user has supplied fixity annotations to @renaming module@ clauses.
checkNoFixityInRenamingModule ren'
-- Andreas, 2026-09-11, issue #1438
-- Warn about fixities declared for non- or closed-operators.
checkNoFixityForClosedOperator ren'
-- TODO (post 2.9.0): purge fixity declarations for closed and non-operators.
-- See also 'fixitiesAndPolarities.
-- Andreas, 2020-06-06, issue #4707
-- Duplicates in @using@ directive are dropped with a warning.
usingList <- discardDuplicatesInUsing usn'
-- Check that an import directive doesn't contain repeated names.
-- Historic note:
-- 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.
let names' = usingList ++ hdn' ++ map renFrom ren' -- all mentioned names from the imported module
-- Report any duplicates in @names'@.
List1.unlessNull (mapMaybe List2.fromList1Maybe $ List1.group $ List.sort names') \ yss ->
setCurrentRange yss $ typeError $ RepeatedNamesInImportDirective yss
-- 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 names'
() <- List1.unlessNull missingExports \ missingExports1 -> setCurrentRange rng do
reportSLn "scope.import.apply" 30 $ "non existing names: " ++ prettyShow missingExports
warning $ ModuleDoesntExport m (Map.keys namesInScope) (Map.keys modulesInScope) missingExports1
-- We can now define a cleaned-up version of the import directive.
let notMissing = not . (missingExports `hasElem`) -- #3997, efficient lookup in missingExports
let usn = filter notMissing usingList -- remove missingExports from usn'
let hdn = filter notMissing hdn' -- remove missingExports from hdn'
let ren = filter (notMissing . renFrom) ren' -- and from ren'
let dir = ImportDirective rng (mapUsing (const usn) usn') hdn ren public
-- Convenient shorthands for defined names and names brought into scope:
let names = map renFrom ren ++ hdn ++ usn
let definedNames = map renTo ren
let targetNames = usn ++ definedNames
-- Efficient test of (`elem` names):
let inNames = (names `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 x = inNames (ImportedName x)
&& notMissing (ImportedModule x)
&& (not . inNames $ ImportedModule 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) $ \ dup ->
typeError $ DuplicateImports m 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 \ nameClashes ->
warning $ ClashesViaRenaming NameNotModule nameClashes
Set1.unlessNull moduleClashes \ moduleClashes ->
warning $ ClashesViaRenaming ModuleNotName moduleClashes
-- Look up the defined names in the new scope.
let namesInScope' = (allNamesInScope scope' :: ThingsInScope AbstractName)
let modulesInScope' = (allNamesInScope scope' :: ThingsInScope AbstractModule)
let look x = List1.head . Map.findWithDefault __IMPOSSIBLE__ 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
-- Amy, 2025-05-12: to support `record where`, we also need to
-- update the concrete name of the "target" to match the concrete
-- name that the user wrote--- otherwise we get import directives
-- from user code like
--
-- open Some.Qualified renaming (original to new)
--
-- that print (and, more importantly, generate record fields!) like
--
-- renaming (Some.Qualifed.original to Some.Qualified.original)
--
-- because the new concrete name is a thin alias for the existing
-- abstract QName, rather than
--
-- renaming (Some.Qualified.Original to new)
--
-- Andreas, 2026-10-02
-- Even though @record where@ has been removed again, and @upd@
-- does not make an observable difference any more, we can leave
-- @upd@ in.
upd :: C.Name -> A.QName -> A.QName
upd x nm = setRange (getRange x) $ qualify_ $ (qnameName nm) { nameConcrete = x }
definedA = for definedNames $ \case
ImportedName x -> ImportedName . (x,) . upd x . anameName $ look x namesInScope'
ImportedModule x -> ImportedModule . (x,) . setRange (getRange x) . amodName $ look x modulesInScope'
let adir = mapImportDir namesA definedA 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 = restrictPrivate scope0
-- Return names in the @using@ directive, discarding duplicates.
-- Monadic for the sake of throwing warnings.
discardDuplicatesInUsing :: C.Using -> ScopeM [C.ImportedName]
discardDuplicatesInUsing = \case
UseEverything -> return []
Using xs -> do
let (ys, dups) = nubAndDuplicatesOn id xs
List1.unlessNull dups $ warning . DuplicateUsing
return 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 notMentioned = \case
dir@(ImportDirective{ using = Using{}, hiding = ys }) -> do
let useless = \case
ImportedName{} -> True
ImportedModule y -> notMentioned (ImportedName y)
() <- List1.unlessNull (filter useless ys) $ 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 = [] }
dir -> return dir
addExtraModules :: (C.Name -> Bool) -> C.ImportDirective -> C.ImportDirective
addExtraModules extra dir =
dir{ using = mapUsing (concatMap addExtra) $ using dir
, hiding = concatMap addExtra $ hiding dir
, impRenaming = concatMap extraRenaming $ impRenaming dir
}
where
addExtra f@(ImportedName y) | extra y = [f, ImportedModule y]
addExtra m = [m]
extraRenaming = \case
r@(Renaming (ImportedName y) (ImportedName z) _fixity rng) | extra y ->
[ r , Renaming (ImportedModule y) (ImportedModule z) Nothing rng ]
r -> [r]
-- Names and modules (abstract) in scope before the import.
namesInScope = (allNamesInScope scope :: ThingsInScope AbstractName)
modulesInScope = (allNamesInScope scope :: ThingsInScope AbstractModule)
concreteNamesInScope = (Map.keys namesInScope ++ Map.keys 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 xs = partitionEithers $ for xs $ \ name -> case name of
ImportedName x -> ImportedName . (x,) . setRange (getRange x) . anameName <$> resolve name x namesInScope
ImportedModule x -> ImportedModule . (x,) . setRange (getRange x) . amodName <$> resolve name x modulesInScope
where
resolve :: Ord a => err -> a -> Map a (List1 b) -> Either err b
resolve err x m = maybe (Left err) (Right . List1.head) $ Map.lookup x 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 src0 tgt0 (ImportDirective r u h ren open) =
ImportDirective r
(mapUsing (map (lookupImportedName src)) u)
(map (lookupImportedName src) h)
(map (mapRenaming src tgt) ren)
open
where
src = importedNameMapFromList src0
tgt = importedNameMapFromList tgt0
-- | A finite map for @ImportedName@s.
data ImportedNameMap n1 n2 m1 m2 = ImportedNameMap
{ inameMap :: Map n1 n2
, imoduleMap :: Map m1 m2
}
-- | Create a 'ImportedNameMap'.
importedNameMapFromList
:: (Ord n1, Ord m1)
=> [ImportedName' (n1,n2) (m1,m2)]
-> ImportedNameMap n1 n2 m1 m2
importedNameMapFromList = foldr (flip add) $ ImportedNameMap Map.empty Map.empty
where
add (ImportedNameMap nm mm) = \case
ImportedName (x,y) -> ImportedNameMap (Map.insert x y nm) mm
ImportedModule (x,y) -> ImportedNameMap nm (Map.insert x y mm)
-- | Apply a 'ImportedNameMap'.
lookupImportedName
:: (Ord n1, Ord m1)
=> ImportedNameMap n1 n2 m1 m2
-> ImportedName' n1 m1
-> ImportedName' n2 m2
lookupImportedName (ImportedNameMap nm mm) = \case
ImportedName x -> ImportedName $ Map.findWithDefault __IMPOSSIBLE__ x nm
ImportedModule x -> ImportedModule $ Map.findWithDefault __IMPOSSIBLE__ x 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 src tgt (Renaming from to fixity r) =
Renaming (lookupImportedName src from) (lookupImportedName tgt to) fixity r
---------------------------------------------------------------------------
-- * Opening a module
---------------------------------------------------------------------------
data OpenKind = LetOpenModule | TopOpenModule
noGeneralizedVarsIfLetOpen :: OpenKind -> Scope -> Scope
noGeneralizedVarsIfLetOpen TopOpenModule = id
noGeneralizedVarsIfLetOpen LetOpenModule = disallowGeneralizedVars
-- | Open a module.
openModule_ :: KwRange -> OpenKind -> C.QName -> C.ImportDirective -> ScopeM A.ImportDirective
openModule_ kwr kind cm dir = openModule kwr kind Nothing cm dir
-- | Open a module, possibly given an already resolved module name.
openModule :: KwRange -> OpenKind -> Maybe A.ModuleName -> C.QName -> C.ImportDirective -> ScopeM A.ImportDirective
openModule kwr kind mam cm dir = do
current <- getCurrentModule
m <- caseMaybe mam (amodName <$> resolveModule cm) return
let acc | Nothing <- publicOpen dir = PrivateNS
| m `isLtChildModuleOf` current = PublicNS
| otherwise = ImportedNS
-- Get the scope exported by module to be opened.
(adir, s') <- applyImportDirectiveM cm dir . inScopeBecause (Opened cm) .
dropRecordConstructorPseudoName .
noGeneralizedVarsIfLetOpen kind =<< getNamedScope m
registerModuleOpening kwr current cm dir s' -- For the unused import warning
let s = setScopeAccess acc s'
let ns = scopeNameSpace acc s
modifyCurrentScope \current -> recomputeNameParts $ mergeScope current s
recomputeInverseScope
-- 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 (\ (c,x) -> c <$ notShadowedLocal x) <$> getLocalVars
let newdefs = Map.keys $ nsNames ns
shadowed = locals `List.intersect` 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 $ \ c x ->
case Map.lookup c $ nsNames ns of
Nothing -> x
Just ys -> shadowLocal ys x
return adir
where
-- Only checks for clashes that would lead to the same
-- name being exported twice from the module.
checkForClashes = when (isJust $ publicOpen dir) $ do
exported <- allThingsInScope . restrictPrivate <$> (getNamedScope =<< getCurrentModule)
-- Get all exported concrete names that are mapped to at least 2 abstract names
let defClashes = filter (\ (_c, as) -> length as >= 2) $ Map.toList $ nsNames exported
modClashes = filter (\ (_c, as) -> length as >= 2) $ Map.toList $ nsModules exported
-- No ambiguity if concrete identifier is only mapped to
-- constructor names or only to projection names or only to pattern synonyms.
defClash (_, qs) = not $ or
[ all (isJust . isConName) ks
, all (== FldName) ks
, all (== PatternSynName) ks
]
where ks = fmap anameKind qs
-- We report the first clashing exported identifier.
() <- List1.unlessNull (filter defClash defClashes) $
\ ((x, q :| _) :| _) -> typeError $ ClashingDefinition (C.QName x) (ClashingAbstractName q) Nothing
List1.unlessNull modClashes $ \ ((_, ms) :| _) -> do
caseMaybe (List1.last2 ms) __IMPOSSIBLE__ $ \ (m0, m1) -> do
typeError $ ClashingModule (amodName m0) (amodName m1)