Separate modules namespace (#2257)

app/Commands/Repl.hs

@@ -251,12 +251,15 @@ printDocumentation = replParseIdentifiers >=> printIdentifiers
 
         printIdentifier :: Concrete.ScopedIden -> Repl ()
         printIdentifier s = do
-          mdoc <- case s of
+          let n = s ^. Concrete.scopedIden . Scoped.nameId
-            Concrete.ScopedAxiom a -> getDocAxiom (a ^. Scoped.nameId)
+          mdoc <- case getNameKind s of
-            Concrete.ScopedInductive a -> getDocInductive (a ^. Scoped.nameId)
+            KNameAxiom -> getDocAxiom n
-            Concrete.ScopedVar {} -> return Nothing
+            KNameInductive -> getDocInductive n
-            Concrete.ScopedFunction f -> getDocFunction (f ^. Scoped.nameId)
+            KNameLocal -> return Nothing
-            Concrete.ScopedConstructor c -> getDocConstructor (c ^. Scoped.nameId)
+            KNameFunction -> getDocFunction n
+            KNameConstructor -> getDocConstructor n
+            KNameLocalModule -> impossible
+            KNameTopModule -> impossible
           printDoc mdoc
           where
             printDoc :: Maybe (Concrete.Judoc 'Concrete.Scoped) -> Repl ()
@@ -303,13 +306,16 @@ printDefinition = replParseIdentifiers >=> printIdentifiers
         getInfoTable = (^. replContextArtifacts . artifactScopeTable) <$> replGetContext
 
         printIdentifier :: Concrete.ScopedIden -> Repl ()
-        printIdentifier s = do
+        printIdentifier s =
-          case s of
+          let n = s ^. Concrete.scopedIden . Scoped.nameId
-            Concrete.ScopedAxiom a -> printAxiom (a ^. Scoped.nameId)
+           in case getNameKind s of
-            Concrete.ScopedInductive a -> printInductive (a ^. Scoped.nameId)
+                KNameAxiom -> printAxiom n
-            Concrete.ScopedVar {} -> return ()
+                KNameInductive -> printInductive n
-            Concrete.ScopedFunction f -> printFunction (f ^. Scoped.nameId)
+                KNameLocal -> return ()
-            Concrete.ScopedConstructor c -> printConstructor (c ^. Scoped.nameId)
+                KNameFunction -> printFunction n
+                KNameConstructor -> printConstructor n
+                KNameLocalModule -> impossible
+                KNameTopModule -> impossible
           where
             printLocation :: HasLoc s => s -> Repl ()
             printLocation def = do

src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs

@@ -15,7 +15,7 @@ data InfoTableBuilder m a where
   RegisterTypeSignature :: TypeSignature 'Scoped -> InfoTableBuilder m ()
   RegisterFunctionDef :: FunctionDef 'Scoped -> InfoTableBuilder m ()
   RegisterFunctionClause :: FunctionClause 'Scoped -> InfoTableBuilder m ()
-  RegisterName :: (HasLoc c) => S.Name' c -> InfoTableBuilder m ()
+  RegisterName :: HasLoc c => S.Name' c -> InfoTableBuilder m ()
   RegisterModule :: Module 'Scoped 'ModuleTop -> InfoTableBuilder m ()
 
 makeSem ''InfoTableBuilder

src/Juvix/Compiler/Concrete/Data/NameSpace.hs

@@ -0,0 +1,27 @@
+module Juvix.Compiler.Concrete.Data.NameSpace where
+
+import Data.Kind qualified as GHC
+import Juvix.Data.NameKind
+import Juvix.Prelude
+
+data NameSpace
+  = NameSpaceSymbols
+  | NameSpaceModules
+  deriving stock (Eq, Generic, Enum, Bounded, Show, Ord)
+
+instance Hashable NameSpace
+
+type AnyNameSpace (k :: NameSpace -> GHC.Type) =
+  Σ NameSpace (TyCon1 k)
+
+$(genSingletons [''NameSpace])
+
+type NameKindNameSpace :: NameKind -> NameSpace
+type family NameKindNameSpace s = res where
+  NameKindNameSpace 'KNameLocal = 'NameSpaceSymbols
+  NameKindNameSpace 'KNameConstructor = 'NameSpaceSymbols
+  NameKindNameSpace 'KNameInductive = 'NameSpaceSymbols
+  NameKindNameSpace 'KNameFunction = 'NameSpaceSymbols
+  NameKindNameSpace 'KNameAxiom = 'NameSpaceSymbols
+  NameKindNameSpace 'KNameLocalModule = 'NameSpaceModules
+  NameKindNameSpace 'KNameTopModule = 'NameSpaceModules

src/Juvix/Compiler/Concrete/Data/Scope.hs

@@ -1,24 +1,31 @@
 module Juvix.Compiler.Concrete.Data.Scope
   ( module Juvix.Compiler.Concrete.Data.Scope,
     module Juvix.Compiler.Concrete.Data.InfoTable,
+    module Juvix.Compiler.Concrete.Data.NameSpace,
   )
 where
 
 import Juvix.Compiler.Concrete.Data.InfoTable
 import Juvix.Compiler.Concrete.Data.NameSignature.Base
+import Juvix.Compiler.Concrete.Data.NameSpace
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Language
 import Juvix.Prelude
 
 type LocalVariable = S.Symbol
 
-newtype SymbolInfo = SymbolInfo
+newtype SymbolInfo (n :: NameSpace) = SymbolInfo
   { -- | This map must have at least one entry. If there are more than one
     -- entry, it means that the same symbol has been brought into scope from two
     -- different places
-    _symbolInfo :: HashMap S.AbsModulePath SymbolEntry
+    _symbolInfo :: HashMap S.AbsModulePath (NameSpaceEntryType n)
   }
-  deriving newtype (Show, Semigroup, Monoid)
+  deriving newtype (Semigroup, Monoid)
+
+nsEntry :: forall ns. SingI ns => Lens' (NameSpaceEntryType ns) (S.Name' ())
+nsEntry = case sing :: SNameSpace ns of
+  SNameSpaceModules -> moduleEntry
+  SNameSpaceSymbols -> symbolEntry
 
 mkModuleRef' :: SingI t => ModuleRef'' 'S.NotConcrete t -> ModuleRef' 'S.NotConcrete
 mkModuleRef' m = ModuleRef' (sing :&: m)
@@ -31,7 +38,8 @@ data BindingStrategy
 
 data Scope = Scope
   { _scopePath :: S.AbsModulePath,
-    _scopeSymbols :: HashMap Symbol SymbolInfo,
+    _scopeSymbols :: HashMap Symbol (SymbolInfo 'NameSpaceSymbols),
+    _scopeModuleSymbols :: HashMap Symbol (SymbolInfo 'NameSpaceModules),
     -- | The map from S.NameId to Modules is needed because we support merging
     -- several imports under the same name. E.g.
     -- import A as X;
@@ -41,14 +49,23 @@ data Scope = Scope
     -- should map to itself. This is needed because we may query it with a
     -- symbol with a different location but we may want the location of the
     -- original symbol
-    _scopeLocalSymbols :: HashMap Symbol S.Symbol
+    _scopeLocalSymbols :: HashMap Symbol S.Symbol,
+    _scopeLocalModuleSymbols :: HashMap Symbol S.Symbol
   }
-  deriving stock (Show)
 
-makeLenses ''ExportInfo
 makeLenses ''SymbolInfo
 makeLenses ''Scope
 
+scopeNameSpace :: forall (ns :: NameSpace). SingI ns => Lens' Scope (HashMap Symbol (SymbolInfo ns))
+scopeNameSpace = case sing :: SNameSpace ns of
+  SNameSpaceSymbols -> scopeSymbols
+  SNameSpaceModules -> scopeModuleSymbols
+
+scopeNameSpaceLocal :: forall (ns :: NameSpace). Sing ns -> Lens' Scope (HashMap Symbol S.Symbol)
+scopeNameSpaceLocal s = case s of
+  SNameSpaceSymbols -> scopeLocalSymbols
+  SNameSpaceModules -> scopeLocalModuleSymbols
+
 newtype ModulesCache = ModulesCache
   { _cachedModules :: HashMap TopModulePath (ModuleRef'' 'S.NotConcrete 'ModuleTop)
   }
@@ -65,6 +82,7 @@ makeLenses ''ScopeParameters
 
 data ScoperState = ScoperState
   { _scoperModulesCache :: ModulesCache,
+    -- | Local and top modules
     _scoperModules :: HashMap S.ModuleNameId (ModuleRef' 'S.NotConcrete),
     _scoperScope :: HashMap TopModulePath Scope,
     _scoperSignatures :: HashMap S.NameId NameSignature
@@ -104,6 +122,8 @@ emptyScope absPath =
   Scope
     { _scopePath = absPath,
       _scopeSymbols = mempty,
+      _scopeModuleSymbols = mempty,
       _scopeTopModules = mempty,
-      _scopeLocalSymbols = mempty
+      _scopeLocalSymbols = mempty,
+      _scopeLocalModuleSymbols = mempty
     }

src/Juvix/Compiler/Concrete/Data/ScopedName.hs

@@ -112,8 +112,11 @@ isConstructor n = case n ^. nameKind of
 fromQualifiedName :: C.QualifiedName -> C.Symbol
 fromQualifiedName (C.QualifiedName _ s) = s
 
-topModulePathName :: TopModulePath -> Symbol
+topModulePathSymbol :: TopModulePath -> Symbol
-topModulePathName = over nameConcrete (^. C.modulePathName)
+topModulePathSymbol = over nameConcrete (^. C.modulePathName)
+
+topModulePathName :: TopModulePath -> Name
+topModulePathName = over nameConcrete C.topModulePathToName
 
 unConcrete :: Name' a -> Name' ()
 unConcrete = set nameConcrete ()

src/Juvix/Compiler/Concrete/Language.hs

@@ -23,8 +23,8 @@ import Juvix.Compiler.Concrete.Data.ModuleIsTop
 import Juvix.Compiler.Concrete.Data.Name
 import Juvix.Compiler.Concrete.Data.NameRef
 import Juvix.Compiler.Concrete.Data.NameSignature.Base (NameSignature)
+import Juvix.Compiler.Concrete.Data.NameSpace
 import Juvix.Compiler.Concrete.Data.PublicAnn
-import Juvix.Compiler.Concrete.Data.ScopedName (unqualifiedSymbol)
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Data.Stage
 import Juvix.Compiler.Concrete.Data.VisibilityAnn
@@ -41,6 +41,11 @@ import Prelude (show)
 
 type Delims = Irrelevant (Maybe (KeywordRef, KeywordRef))
 
+type NameSpaceEntryType :: NameSpace -> GHC.Type
+type family NameSpaceEntryType s = res | res -> s where
+  NameSpaceEntryType 'NameSpaceSymbols = SymbolEntry
+  NameSpaceEntryType 'NameSpaceModules = ModuleSymbolEntry
+
 type SymbolType :: Stage -> GHC.Type
 type family SymbolType s = res | res -> s where
   SymbolType 'Parsed = Symbol
@@ -665,8 +670,9 @@ deriving stock instance Ord (Module 'Parsed 'ModuleLocal)
 
 deriving stock instance Ord (Module 'Scoped 'ModuleLocal)
 
-newtype HidingItem (s :: Stage) = HidingItem
+data HidingItem (s :: Stage) = HidingItem
-  { _hidingSymbol :: SymbolType s
+  { _hidingSymbol :: SymbolType s,
+    _hidingModuleKw :: Maybe KeywordRef
   }
 
 deriving stock instance Show (HidingItem 'Parsed)
@@ -683,6 +689,7 @@ deriving stock instance Ord (HidingItem 'Scoped)
 
 data UsingItem (s :: Stage) = UsingItem
   { _usingSymbol :: SymbolType s,
+    _usingModuleKw :: Maybe KeywordRef,
     _usingAsKw :: Irrelevant (Maybe KeywordRef),
     _usingAs :: Maybe (SymbolType s)
   }
@@ -771,8 +778,8 @@ getNameRefId = case sing :: S.SIsConcrete c of
   S.SConcrete -> (^. S.nameId)
   S.SNotConcrete -> (^. S.nameId)
 
-getModuleExportInfo :: ModuleRef' c -> ExportInfo
+getModuleRefExportInfo :: ModuleRef' c -> ExportInfo
-getModuleExportInfo (ModuleRef' (_ :&: ModuleRef'' {..})) = _moduleExportInfo
+getModuleRefExportInfo (ModuleRef' (_ :&: ModuleRef'' {..})) = _moduleExportInfo
 
 getModuleRefNameType :: ModuleRef' c -> RefNameType c
 getModuleRefNameType (ModuleRef' (_ :&: ModuleRef'' {..})) = _moduleRefName
@@ -800,21 +807,23 @@ instance Eq (ModuleRef'' 'S.Concrete t) where
 instance Ord (ModuleRef'' 'S.Concrete t) where
   compare (ModuleRef'' n _ _) (ModuleRef'' n' _ _) = compare n n'
 
-data SymbolEntry
+newtype SymbolEntry = SymbolEntry
-  = EntryAxiom (RefNameType 'S.NotConcrete)
+  { _symbolEntry :: S.Name' ()
-  | EntryInductive (RefNameType 'S.NotConcrete)
+  }
-  | EntryFunction (RefNameType 'S.NotConcrete)
+  deriving stock (Show)
-  | EntryConstructor (RefNameType 'S.NotConcrete)
+
-  | EntryModule (ModuleRef' 'S.NotConcrete)
+newtype ModuleSymbolEntry = ModuleSymbolEntry
-  | EntryVariable (S.Name' ())
+  { _moduleEntry :: S.Name' ()
+  }
   deriving stock (Show)
 
 instance SingI t => CanonicalProjection (ModuleRef'' c t) (ModuleRef' c) where
   project r = ModuleRef' (sing :&: r)
 
 -- | Symbols that a module exports
-newtype ExportInfo = ExportInfo
+data ExportInfo = ExportInfo
-  { _exportSymbols :: HashMap Symbol SymbolEntry
+  { _exportSymbols :: HashMap Symbol SymbolEntry,
+    _exportModuleSymbols :: HashMap Symbol ModuleSymbolEntry
   }
   deriving stock (Show)
 
@@ -842,12 +851,9 @@ deriving stock instance Ord (OpenModule 'Scoped)
 
 type ScopedIden = ScopedIden' 'S.Concrete
 
-data ScopedIden' (n :: S.IsConcrete)
+newtype ScopedIden' (n :: S.IsConcrete) = ScopedIden
-  = ScopedAxiom (RefNameType n)
+  { _scopedIden :: RefNameType n
-  | ScopedInductive (RefNameType n)
+  }
-  | ScopedVar S.Symbol
-  | ScopedFunction (RefNameType n)
-  | ScopedConstructor (RefNameType n)
 
 deriving stock instance
   (Eq (RefNameType s)) => Eq (ScopedIden' s)
@@ -858,18 +864,8 @@ deriving stock instance
 deriving stock instance
   (Show (RefNameType s)) => Show (ScopedIden' s)
 
-identifierName :: forall n. (SingI n) => ScopedIden' n -> RefNameType n
+identifierName :: forall n. ScopedIden' n -> RefNameType n
-identifierName = \case
+identifierName (ScopedIden n) = n
-  ScopedAxiom a -> a
-  ScopedInductive i -> i
-  ScopedVar v ->
-    ( case sing :: S.SIsConcrete n of
-        S.SConcrete -> id
-        S.SNotConcrete -> set S.nameConcrete ()
-    )
-      (unqualifiedSymbol v)
-  ScopedFunction f -> f
-  ScopedConstructor c -> c
 
 data Expression
   = ExpressionIdentifier ScopedIden
@@ -1401,6 +1397,9 @@ newtype ModuleIndex = ModuleIndex
   }
 
 makeLenses ''PatternArg
+makeLenses ''ScopedIden'
+makeLenses ''SymbolEntry
+makeLenses ''ModuleSymbolEntry
 makeLenses ''RecordField
 makeLenses ''RhsRecord
 makeLenses ''RhsGadt
@@ -1432,6 +1431,7 @@ makeLenses ''TypeSignature
 makeLenses ''SigArg
 makeLenses ''FunctionDef
 makeLenses ''AxiomDef
+makeLenses ''ExportInfo
 makeLenses ''FunctionClause
 makeLenses ''InductiveParameters
 makeLenses ''ModuleRef'
@@ -1520,12 +1520,7 @@ instance SingI s => HasAtomicity (FunctionParameters s) where
         SScoped -> atomicity (p ^. paramType)
 
 instance HasLoc ScopedIden where
-  getLoc = \case
+  getLoc = getLoc . (^. scopedIden)
-    ScopedAxiom a -> getLoc a
-    ScopedConstructor a -> getLoc a
-    ScopedInductive a -> getLoc a
-    ScopedFunction a -> getLoc a
-    ScopedVar a -> getLoc a
 
 instance HasLoc (InductiveDef 'Scoped) where
   getLoc i = (getLoc <$> i ^. inductivePositive) ?<> getLoc (i ^. inductiveKw)
@@ -1971,38 +1966,6 @@ instance HasAtomicity PatternArg where
     | isJust (p ^. patternArgName) = Atom
     | otherwise = atomicity (p ^. patternArgPattern)
 
-idenOverName :: (forall s. S.Name' s -> S.Name' s) -> ScopedIden -> ScopedIden
-idenOverName f = \case
-  ScopedAxiom a -> ScopedAxiom (f a)
-  ScopedInductive i -> ScopedInductive (f i)
-  ScopedVar v -> ScopedVar (f v)
-  ScopedFunction fun -> ScopedFunction (f fun)
-  ScopedConstructor c -> ScopedConstructor (f c)
-
-entryPrism :: (S.Name' () -> S.Name' ()) -> SymbolEntry -> (S.Name' (), SymbolEntry)
-entryPrism f = \case
-  EntryAxiom a -> (a, EntryAxiom (f a))
-  EntryInductive i -> (i, EntryInductive (f i))
-  EntryFunction fun -> (fun, EntryFunction (f fun))
-  EntryConstructor c -> (c, EntryConstructor (f c))
-  EntryModule m -> (getModuleRefNameType m, EntryModule (overModuleRef'' (over moduleRefName f) m))
-  EntryVariable m -> (m, EntryVariable (f m))
-
-entryOverName :: (S.Name' () -> S.Name' ()) -> SymbolEntry -> SymbolEntry
-entryOverName f = snd . entryPrism f
-
-entryName :: SymbolEntry -> S.Name' ()
-entryName = fst . entryPrism id
-
-entryIsExpression :: SymbolEntry -> Bool
-entryIsExpression = \case
-  EntryAxiom {} -> True
-  EntryInductive {} -> True
-  EntryFunction {} -> True
-  EntryConstructor {} -> True
-  EntryVariable {} -> True
-  EntryModule {} -> False
-
 judocExamples :: Judoc s -> [Example s]
 judocExamples (Judoc bs) = concatMap goGroup bs
   where
@@ -2020,30 +1983,32 @@ judocExamples (Judoc bs) = concatMap goGroup bs
       _ -> mempty
 
 instance HasLoc SymbolEntry where
-  getLoc = (^. S.nameDefined) . entryName
+  getLoc = (^. symbolEntry . S.nameDefined)
+
+instance HasNameKind ModuleSymbolEntry where
+  getNameKind (ModuleSymbolEntry s) = getNameKind s
+
+instance HasLoc ModuleSymbolEntry where
+  getLoc (ModuleSymbolEntry s) = s ^. S.nameDefined
 
 overModuleRef'' :: forall s s'. (forall t. ModuleRef'' s t -> ModuleRef'' s' t) -> ModuleRef' s -> ModuleRef' s'
 overModuleRef'' f = over unModuleRef' (\(t :&: m'') -> t :&: f m'')
 
 symbolEntryNameId :: SymbolEntry -> NameId
-symbolEntryNameId = (^. S.nameId) . symbolEntryToSName
+symbolEntryNameId = (^. symbolEntry . S.nameId)
-
-symbolEntryToSName :: SymbolEntry -> S.Name' ()
-symbolEntryToSName = \case
-  EntryAxiom a -> a
-  EntryInductive i -> i
-  EntryFunction f -> f
-  EntryConstructor c -> c
-  EntryModule m -> getModuleRefNameType m
-  EntryVariable m -> m
 
 instance HasNameKind ScopedIden where
-  getNameKind = \case
+  getNameKind = getNameKind . (^. scopedIden)
-    ScopedAxiom {} -> KNameAxiom
-    ScopedInductive {} -> KNameInductive
-    ScopedConstructor {} -> KNameConstructor
-    ScopedVar {} -> KNameLocal
-    ScopedFunction {} -> KNameFunction
 
 instance HasNameKind SymbolEntry where
-  getNameKind = getNameKind . entryName
+  getNameKind = getNameKind . (^. symbolEntry)
+
+exportAllNames :: SimpleFold ExportInfo (S.Name' ())
+exportAllNames =
+  exportSymbols . each . symbolEntry
+    <> exportModuleSymbols . each . moduleEntry
+
+exportNameSpace :: forall ns. SingI ns => Lens' ExportInfo (HashMap Symbol (NameSpaceEntryType ns))
+exportNameSpace = case sing :: SNameSpace ns of
+  SNameSpaceSymbols -> exportSymbols
+  SNameSpaceModules -> exportModuleSymbols

src/Juvix/Compiler/Concrete/Print/Base.hs

@@ -23,6 +23,7 @@ import Juvix.Data.CodeAnn qualified as C
 import Juvix.Data.Effect.ExactPrint
 import Juvix.Data.IteratorAttribs
 import Juvix.Data.Keyword.All qualified as Kw
+import Juvix.Data.NameKind
 import Juvix.Extra.Strings qualified as Str
 import Juvix.Prelude hiding ((<+>), (<+?>), (<?+>), (?<>))
 import Juvix.Prelude.Pretty (annotate, pretty)
@@ -377,16 +378,14 @@ instance PrettyPrint QualifiedName where
     let symbols = _qualifiedPath ^. pathParts NonEmpty.|> _qualifiedSymbol
     dotted (ppSymbolType <$> symbols)
 
-instance PrettyPrint (ModuleRef'' 'S.Concrete 'ModuleTop) where
+instance SingI t => PrettyPrint (ModuleRef'' 'S.NotConcrete t) where
+  ppCode = ppCode @(ModuleRef' 'S.NotConcrete) . project
+
+instance PrettyPrint (ModuleRef'' 'S.Concrete t) where
   ppCode m = ppCode (m ^. moduleRefName)
 
 instance PrettyPrint ScopedIden where
-  ppCode = \case
+  ppCode = ppCode . (^. scopedIden)
-    ScopedAxiom a -> ppCode a
-    ScopedInductive i -> ppCode i
-    ScopedVar n -> ppCode n
-    ScopedFunction f -> ppCode f
-    ScopedConstructor c -> ppCode c
 
 instance SingI s => PrettyPrint (Import s) where
   ppCode :: forall r. Members '[ExactPrint, Reader Options] r => Import s -> Sem r ()
@@ -803,7 +802,10 @@ ppUnkindedSymbol :: Members '[Reader Options, ExactPrint] r => WithLoc Text -> S
 ppUnkindedSymbol = region (annotate AnnUnkindedSym) . ppCode
 
 instance SingI s => PrettyPrint (HidingItem s) where
-  ppCode = ppSymbolType . (^. hidingSymbol)
+  ppCode h = do
+    let sym = ppSymbolType (h ^. hidingSymbol)
+        kwmodule = ppCode <$> (h ^. hidingModuleKw)
+    kwmodule <?+> sym
 
 instance SingI s => PrettyPrint (HidingList s) where
   ppCode HidingList {..} = do
@@ -829,7 +831,16 @@ instance SingI s => PrettyPrint (UsingItem s) where
     let kwAs' :: Maybe (Sem r ()) = ppCode <$> ui ^. usingAsKw . unIrrelevant
         alias' = ppSymbolType <$> ui ^. usingAs
         sym' = ppSymbolType (ui ^. usingSymbol)
-    sym' <+?> kwAs' <+?> alias'
+        kwmodule = ppCode <$> (ui ^. usingModuleKw)
+    kwmodule <?+> (sym' <+?> kwAs' <+?> alias')
+
+instance PrettyPrint (ModuleRef' 'S.NotConcrete) where
+  ppCode (ModuleRef' (t :&: m)) =
+    let path = m ^. moduleRefModule . modulePath
+        txt = case t of
+          SModuleTop -> annotate (AnnKind KNameTopModule) (pretty path)
+          SModuleLocal -> annotate (AnnKind KNameLocalModule) (pretty path)
+     in noLoc txt
 
 instance PrettyPrint ModuleRef where
   ppCode (ModuleRef' (_ :&: ModuleRef'' {..})) = ppCode _moduleRefName
@@ -991,19 +1002,26 @@ instance PrettyPrint SymbolEntry where
   ppCode ent =
     noLoc
       ( kindWord
-          P.<+> C.code (kindAnn (pretty (entryName ent ^. S.nameVerbatim)))
+          P.<+> C.code (kindAnn (pretty (ent ^. symbolEntry . S.nameVerbatim)))
           P.<+> "defined at"
           P.<+> pretty (getLoc ent)
       )
     where
       pretty' :: Text -> Doc a
       pretty' = pretty
-      (kindAnn :: Doc Ann -> Doc Ann, kindWord :: Doc Ann) = case ent of
+      (kindAnn :: Doc Ann -> Doc Ann, kindWord :: Doc Ann) =
-        EntryAxiom {} -> (C.annotateKind S.KNameAxiom, pretty' Str.axiom)
+        let k = getNameKind ent
-        EntryInductive {} -> (C.annotateKind S.KNameInductive, pretty' Str.inductive)
+         in (annotate (AnnKind k), pretty' (nameKindText k))
-        EntryFunction {} -> (C.annotateKind S.KNameFunction, pretty' Str.function)
+
-        EntryConstructor {} -> (C.annotateKind S.KNameConstructor, pretty' Str.constructor)
+instance PrettyPrint ModuleSymbolEntry where
-        EntryVariable {} -> (C.annotateKind S.KNameLocal, pretty' Str.variable)
+  ppCode ent = do
-        EntryModule (ModuleRef' (isTop :&: _))
+    let mname = ppCode (ent ^. moduleEntry . S.nameVerbatim)
-          | SModuleTop <- isTop -> (C.annotateKind S.KNameTopModule, pretty' Str.topModule)
+    noLoc
-          | SModuleLocal <- isTop -> (C.annotateKind S.KNameLocalModule, pretty' Str.localModule)
+      kindWord
+      <+> mname
+      <+> noLoc "defined at"
+      <+> noLoc (pretty (getLoc ent))
+    where
+      kindWord :: Doc Ann =
+        let k = getNameKind ent
+         in (pretty (nameKindText k))

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs

@@ -1,5 +1,3 @@
--- | Limitations:
--- 1. A symbol introduced by a type signature can only be used once per Module.
 module Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping
   ( module Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping,
     module Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Data.Context,
@@ -27,6 +25,7 @@ import Juvix.Compiler.Concrete.Translation.FromSource.Data.Context (ParserResult
 import Juvix.Compiler.Concrete.Translation.FromSource.Data.Context qualified as Parsed
 import Juvix.Compiler.Pipeline.EntryPoint
 import Juvix.Data.IteratorAttribs
+import Juvix.Data.NameKind
 import Juvix.Prelude
 
 iniScoperState :: ScoperState
@@ -117,22 +116,22 @@ scopeCheckImport ::
   Members '[Error JuvixError, InfoTableBuilder, NameIdGen, State Scope, Reader ScopeParameters, State ScoperState] r =>
   Import 'Parsed ->
   Sem r (Import 'Scoped)
-scopeCheckImport i = mapError (JuvixError @ScoperError) $ checkImport i
+scopeCheckImport = mapError (JuvixError @ScoperError) . checkImport
 
 scopeCheckOpenModule ::
   forall r.
   Members '[Error JuvixError, InfoTableBuilder, NameIdGen, State Scope, Reader ScopeParameters, State ScoperState] r =>
   OpenModule 'Parsed ->
   Sem r (OpenModule 'Scoped)
-scopeCheckOpenModule i = mapError (JuvixError @ScoperError) $ checkOpenModule i
+scopeCheckOpenModule = mapError (JuvixError @ScoperError) . checkOpenModule
 
 freshVariable :: Members '[NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, State ScoperState] r => Symbol -> Sem r S.Symbol
-freshVariable = freshSymbol S.KNameLocal
+freshVariable = freshSymbol KNameLocal
 
 freshSymbol ::
   forall r.
   Members '[State Scope, State ScoperState, NameIdGen, State ScoperFixities, State ScoperIterators] r =>
-  S.NameKind ->
+  NameKind ->
   Symbol ->
   Sem r S.Symbol
 freshSymbol _nameKind _nameConcrete = do
@@ -163,9 +162,12 @@ freshSymbol _nameKind _nameConcrete = do
       return attrs
 
 reserveSymbolSignatureOf ::
-  forall r d.
+  forall (k :: NameKind) r d.
-  (Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators, State Scope, State ScoperState, Reader BindingStrategy] r, HasNameSignature d) =>
+  ( Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder] r,
-  S.NameKind ->
+    HasNameSignature d,
+    SingI (NameKindNameSpace k)
+  ) =>
+  Sing k ->
   d ->
   Symbol ->
   Sem r S.Symbol
@@ -174,43 +176,48 @@ reserveSymbolSignatureOf k d s = do
   reserveSymbolOf k (Just sig) s
 
 reserveSymbolOf ::
-  forall r.
+  forall (nameKind :: NameKind) (ns :: NameSpace) r.
-  Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators, State Scope, State ScoperState, Reader BindingStrategy] r =>
+  ( Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder] r,
-  S.NameKind ->
+    ns ~ NameKindNameSpace nameKind,
+    SingI ns
+  ) =>
+  Sing nameKind ->
   Maybe NameSignature ->
   Symbol ->
   Sem r S.Symbol
 reserveSymbolOf k nameSig s = do
   checkNotBound
-  s' <- freshSymbol k s
-  whenJust nameSig (modify' . set (scoperSignatures . at (s' ^. S.nameId)) . Just)
   path <- gets (^. scopePath)
   strat <- ask
-  modify (set (scopeLocalSymbols . at s) (Just s'))
+  s' <- freshSymbol (fromSing k) s
-  let c = S.unConcrete s'
+  whenJust nameSig (modify' . set (scoperSignatures . at (s' ^. S.nameId)) . Just)
-      mentry :: Maybe SymbolEntry
+  modify (set (scopeNameSpaceLocal sns . at s) (Just s'))
-      mentry = case k of
+  registerName (S.unqualifiedSymbol s')
-        S.KNameConstructor -> Just (EntryConstructor c)
+  let entry :: NameSpaceEntryType (NameKindNameSpace nameKind)
-        S.KNameInductive -> Just (EntryInductive c)
+      entry =
-        S.KNameFunction -> Just (EntryFunction c)
+        let symE = SymbolEntry (S.unConcrete s')
-        S.KNameAxiom -> Just (EntryAxiom c)
+            modE = ModuleSymbolEntry (S.unConcrete s')
-        S.KNameLocal -> Just (EntryVariable c)
+         in case k of
-        S.KNameLocalModule -> Nothing
+              SKNameConstructor -> symE
-        S.KNameTopModule -> Nothing
+              SKNameInductive -> symE
-      addS :: SymbolEntry -> Maybe SymbolInfo -> SymbolInfo
+              SKNameFunction -> symE
-      addS entry m = case m of
+              SKNameAxiom -> symE
-        Nothing -> symbolInfoSingle entry
+              SKNameLocal -> symE
+              SKNameLocalModule -> modE
+              SKNameTopModule -> modE
+      addS :: NameSpaceEntryType ns -> Maybe (SymbolInfo ns) -> SymbolInfo ns
+      addS mentry m = case m of
+        Nothing -> symbolInfoSingle mentry
         Just SymbolInfo {..} -> case strat of
-          BindingLocal -> symbolInfoSingle entry
+          BindingLocal -> symbolInfoSingle mentry
-          BindingTop -> SymbolInfo (HashMap.insert path entry _symbolInfo)
+          BindingTop -> SymbolInfo (HashMap.insert path mentry _symbolInfo)
-  whenJust mentry $ \entry ->
+  modify (over scopeNameSpace (HashMap.alter (Just . addS entry) s))
-    modify (over scopeSymbols (HashMap.alter (Just . addS entry) s))
-
   return s'
   where
+    sns :: Sing ns = sing
     checkNotBound :: Sem r ()
     checkNotBound = do
-      exists <- HashMap.lookup s <$> gets (^. scopeLocalSymbols)
+      exists <- HashMap.lookup s <$> gets (^. scopeNameSpaceLocal sns)
       whenJust exists $ \d ->
         throw
           ( ErrMultipleDeclarations
@@ -220,49 +227,14 @@ reserveSymbolOf k nameSig s = do
                 }
           )
 
-bindReservedSymbol ::
+getReservedDefinitionSymbol ::
-  Members '[State Scope, InfoTableBuilder, Reader BindingStrategy] r =>
-  S.Symbol ->
-  SymbolEntry ->
-  Sem r ()
-bindReservedSymbol s' entry = do
-  path <- gets (^. scopePath)
-  strat <- ask
-  -- TODO only modules are meant to be stored here?
-  modify (over scopeSymbols (HashMap.alter (Just . addS strat path) s))
-  registerName (S.unqualifiedSymbol s')
-  where
-    s :: Symbol
-    s = s' ^. S.nameConcrete
-    addS :: BindingStrategy -> S.AbsModulePath -> Maybe SymbolInfo -> SymbolInfo
-    addS strat path m = case m of
-      Nothing -> symbolInfoSingle entry
-      Just SymbolInfo {..} -> case strat of
-        BindingLocal -> symbolInfoSingle entry
-        BindingTop -> SymbolInfo (HashMap.insert path entry _symbolInfo)
-
--- | Only for variables and local modules
-bindSymbolOf ::
   Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators, State Scope, InfoTableBuilder, State ScoperState, Reader BindingStrategy] r =>
-  S.NameKind ->
-  (S.Name' () -> SymbolEntry) ->
   Symbol ->
   Sem r S.Symbol
-bindSymbolOf k mkEntry s = do
+getReservedDefinitionSymbol s = do
-  s' <- reserveSymbolOf k Nothing s
-  bindReservedSymbol s' (mkEntry (S.unConcrete s'))
-  return s'
-
-bindReservedDefinitionSymbol ::
-  Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators, State Scope, InfoTableBuilder, State ScoperState, Reader BindingStrategy] r =>
-  (S.Name' () -> SymbolEntry) ->
-  Symbol ->
-  Sem r S.Symbol
-bindReservedDefinitionSymbol mkEntry s = do
   m <- gets (^. scopeLocalSymbols)
   let s' = fromMaybe err (m ^. at s)
       err = error ("impossible. Contents of scope:\n" <> ppTrace (toList m))
-  bindReservedSymbol s' (mkEntry (S.unConcrete s'))
   return s'
 
 ignoreFixities :: Sem (State ScoperFixities ': r) a -> Sem r a
@@ -276,69 +248,57 @@ bindVariableSymbol ::
   Members '[Error ScoperError, NameIdGen, State Scope, InfoTableBuilder, State ScoperState] r =>
   Symbol ->
   Sem r S.Symbol
-bindVariableSymbol = localBindings . ignoreFixities . ignoreIterators . bindSymbolOf S.KNameLocal EntryVariable
+bindVariableSymbol = localBindings . ignoreFixities . ignoreIterators . reserveSymbolOf SKNameLocal Nothing
 
 reserveInductiveSymbol ::
-  Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, State ScoperState, Reader BindingStrategy] r =>
+  Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder] r =>
   InductiveDef 'Parsed ->
   Sem r S.Symbol
-reserveInductiveSymbol d = reserveSymbolSignatureOf S.KNameInductive d (d ^. inductiveName)
+reserveInductiveSymbol d = reserveSymbolSignatureOf SKNameInductive d (d ^. inductiveName)
 
 reserveConstructorSymbol ::
-  Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, State ScoperState, Reader BindingStrategy] r =>
+  Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder] r =>
   InductiveDef 'Parsed ->
   ConstructorDef 'Parsed ->
   Sem r S.Symbol
-reserveConstructorSymbol d c = reserveSymbolSignatureOf S.KNameConstructor (d, c) (c ^. constructorName)
+reserveConstructorSymbol d c = reserveSymbolSignatureOf SKNameConstructor (d, c) (c ^. constructorName)
 
 reserveFunctionSymbol ::
-  Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, State ScoperState, Reader BindingStrategy] r =>
+  Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder] r =>
   FunctionDef 'Parsed ->
   Sem r S.Symbol
 reserveFunctionSymbol f =
-  reserveSymbolSignatureOf S.KNameFunction f (f ^. signName)
+  reserveSymbolSignatureOf SKNameFunction f (f ^. signName)
 
 reserveAxiomSymbol ::
-  Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, State ScoperState, Reader BindingStrategy] r =>
+  Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder] r =>
   AxiomDef 'Parsed ->
   Sem r S.Symbol
-reserveAxiomSymbol a = reserveSymbolSignatureOf S.KNameAxiom a (a ^. axiomName)
+reserveAxiomSymbol a = reserveSymbolSignatureOf SKNameAxiom a (a ^. axiomName)
 
--- | symbols must be reserved in advance
 bindFunctionSymbol ::
   Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, InfoTableBuilder, State ScoperState, Reader BindingStrategy] r =>
   Symbol ->
   Sem r S.Symbol
-bindFunctionSymbol = bindReservedDefinitionSymbol EntryFunction
+bindFunctionSymbol = getReservedDefinitionSymbol
 
 bindInductiveSymbol ::
   Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, InfoTableBuilder, State ScoperState, Reader BindingStrategy] r =>
   Symbol ->
   Sem r S.Symbol
-bindInductiveSymbol = bindReservedDefinitionSymbol EntryInductive
+bindInductiveSymbol = getReservedDefinitionSymbol
 
 bindAxiomSymbol ::
   Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, InfoTableBuilder, State ScoperState, Reader BindingStrategy] r =>
   Symbol ->
   Sem r S.Symbol
-bindAxiomSymbol = bindReservedDefinitionSymbol EntryAxiom
+bindAxiomSymbol = getReservedDefinitionSymbol
 
 bindConstructorSymbol ::
   Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, InfoTableBuilder, State ScoperState, Reader BindingStrategy] r =>
   Symbol ->
   Sem r S.Symbol
-bindConstructorSymbol = bindReservedDefinitionSymbol EntryConstructor
+bindConstructorSymbol = getReservedDefinitionSymbol
-
-bindLocalModuleSymbol ::
-  Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, InfoTableBuilder, State ScoperState, Reader BindingStrategy] r =>
-  ExportInfo ->
-  Module 'Scoped 'ModuleLocal ->
-  Symbol ->
-  Sem r S.Symbol
-bindLocalModuleSymbol _moduleExportInfo _moduleRefModule =
-  bindSymbolOf
-    S.KNameLocalModule
-    (\_moduleRefName -> EntryModule (mkModuleRef' (ModuleRef'' {..})))
 
 checkImport ::
   forall r.
@@ -391,99 +351,116 @@ getTopModulePath Module {..} =
       S._absLocalPath = mempty
     }
 
+-- getModuleRef :: Members '[State ScoperState] r => ModuleSymbolEntry -> Sem r
+
+getModuleExportInfo :: Members '[State ScoperState] r => ModuleSymbolEntry -> Sem r ExportInfo
+getModuleExportInfo m = gets (^?! scoperModules . at (m ^. moduleEntry . S.nameId) . _Just . to getModuleRefExportInfo)
+
 -- | Do not call directly. Looks for a symbol in (possibly) nested local modules
 lookupSymbolAux ::
   forall r.
-  Members '[State Scope] r =>
+  Members '[State ScoperState, State Scope, Output ModuleSymbolEntry, Output SymbolEntry] r =>
   [Symbol] ->
   Symbol ->
-  Sem r [SymbolEntry]
+  Sem r ()
 lookupSymbolAux modules final = do
-  local' <- hereOrInLocalModule
+  hereOrInLocalModule
-  import' <- importedTopModule
+  importedTopModule
-  return (local' ++ import')
   where
-    hereOrInLocalModule :: Sem r [SymbolEntry] =
+    hereOrInLocalModule :: Sem r () =
       case modules of
         [] -> do
-          r <- HashMap.lookup final <$> gets (^. scopeSymbols)
+          let helper ::
-          return $ case r of
+                forall ns r'.
-            Nothing -> []
+                (SingI ns, Members '[Output (NameSpaceEntryType ns), State Scope] r') =>
-            Just SymbolInfo {..} -> toList _symbolInfo
+                Proxy ns ->
+                Sem r' ()
+              helper Proxy =
+                gets (^.. scopeNameSpace @ns . at final . _Just . symbolInfo . each) >>= mapM_ output
+          helper (Proxy @'NameSpaceSymbols)
+          helper (Proxy @'NameSpaceModules)
         p : ps ->
-          mapMaybe (lookInExport final ps . getModuleExportInfo)
+          gets (^.. scopeModuleSymbols . at p . _Just . symbolInfo . each)
-            . concat
+            >>= mapM_ (getModuleExportInfo >=> lookInExport final ps)
-            . maybeToList
+    importedTopModule :: Sem r ()
-            . fmap (mapMaybe getModuleRef . toList . (^. symbolInfo))
-            . HashMap.lookup p
-            <$> gets (^. scopeSymbols)
-    importedTopModule :: Sem r [SymbolEntry]
     importedTopModule = do
       tbl <- gets (^. scopeTopModules)
-      return (tbl ^.. at path . _Just . each . to (EntryModule . mkModuleRef'))
+      mapM_ output (tbl ^.. at path . _Just . each . to (mkModuleEntry . mkModuleRef'))
       where
         path = TopModulePath modules final
 
-lookInExport :: Symbol -> [Symbol] -> ExportInfo -> Maybe SymbolEntry
+mkModuleEntry :: ModuleRef' 'S.NotConcrete -> ModuleSymbolEntry
+mkModuleEntry (ModuleRef' (t :&: m)) = ModuleSymbolEntry $ case t of
+  SModuleTop -> S.unConcrete (m ^. moduleRefModule . modulePath)
+  SModuleLocal -> S.unConcrete (m ^. moduleRefModule . modulePath)
+
+lookInExport ::
+  forall r.
+  Members '[State ScoperState, Output SymbolEntry, Output ModuleSymbolEntry] r =>
+  Symbol ->
+  [Symbol] ->
+  ExportInfo ->
+  Sem r ()
 lookInExport sym remaining e = case remaining of
-  [] -> HashMap.lookup sym (e ^. exportSymbols)
+  [] -> do
-  (s : ss) -> do
+    whenJust (e ^. exportSymbols . at sym) output
-    export <- mayModule e s
+    whenJust (e ^. exportModuleSymbols . at sym) output
-    lookInExport sym ss export
+  s : ss -> whenJustM (mayModule e s) (lookInExport sym ss)
   where
-    mayModule :: ExportInfo -> Symbol -> Maybe ExportInfo
+    mayModule :: ExportInfo -> Symbol -> Sem r (Maybe ExportInfo)
-    mayModule ExportInfo {..} s = do
+    mayModule ExportInfo {..} s =
-      entry <- HashMap.lookup s _exportSymbols
+      mapM getModuleExportInfo (HashMap.lookup s _exportModuleSymbols)
-      case entry of
-        EntryModule m -> Just (getModuleExportInfo m)
-        _ -> Nothing
 
 -- | We return a list of entries because qualified names can point to different
 -- modules due to nesting.
 lookupQualifiedSymbol ::
   forall r.
-  Members '[State Scope] r =>
+  Members '[State Scope, State ScoperState] r =>
   ([Symbol], Symbol) ->
-  Sem r [SymbolEntry]
+  Sem r ([SymbolEntry], [ModuleSymbolEntry])
-lookupQualifiedSymbol (path, sym) = do
+lookupQualifiedSymbol = runOutputList . execOutputList . go
-  here' <- here
-  there' <- there
-  return (here' ++ there')
   where
-    -- Current module.
+    go ::
-    here :: Sem r [SymbolEntry]
+      forall r'.
-    here = lookupSymbolAux path sym
+      Members [State ScoperState, State Scope, Output SymbolEntry, Output ModuleSymbolEntry] r' =>
-    -- Looks for a top level modules
+      ([Symbol], Symbol) ->
-    there :: Sem r [SymbolEntry]
+      Sem r' ()
-    there = do
+    go (path, sym) = do
-      concatMapM (uncurry lookInTopModule) allTopPaths
+      here
+      there
       where
-        allTopPaths :: [(TopModulePath, [Symbol])]
+        -- Current module.
-        allTopPaths = map (first nonEmptyToTopPath) raw
+        here :: Sem r' ()
+        here = lookupSymbolAux path sym
+        -- Looks for a top level modules
+        there :: Sem r' ()
+        there = mapM_ (uncurry lookInTopModule) allTopPaths
           where
-            lpath = toList path
+            allTopPaths :: [(TopModulePath, [Symbol])]
-            raw :: [(NonEmpty Symbol, [Symbol])]
+            allTopPaths = map (first nonEmptyToTopPath) raw
-            raw =
+              where
-              [ (l, r) | i <- [1 .. length path], (Just l, r) <- [first nonEmpty (splitAt i lpath)]
+                lpath = toList path
-              ]
+                raw :: [(NonEmpty Symbol, [Symbol])]
-            nonEmptyToTopPath :: NonEmpty Symbol -> TopModulePath
+                raw =
-            nonEmptyToTopPath l = TopModulePath (NonEmpty.init l) (NonEmpty.last l)
+                  [ (l, r) | i <- [1 .. length path], (Just l, r) <- [first nonEmpty (splitAt i lpath)]
-        lookInTopModule :: TopModulePath -> [Symbol] -> Sem r [SymbolEntry]
+                  ]
-        lookInTopModule topPath remaining = do
+                nonEmptyToTopPath :: NonEmpty Symbol -> TopModulePath
-          tbl <- gets (^. scopeTopModules)
+                nonEmptyToTopPath l = TopModulePath (NonEmpty.init l) (NonEmpty.last l)
-          return $
+            lookInTopModule :: TopModulePath -> [Symbol] -> Sem r' ()
-            catMaybes
+            lookInTopModule topPath remaining = do
-              [ lookInExport sym remaining (ref ^. moduleExportInfo)
+              tbl <- gets (^. scopeTopModules)
-                | Just t <- [tbl ^. at topPath],
+              sequence_
-                  ref <- toList t
+                [ lookInExport sym remaining (ref ^. moduleExportInfo)
-              ]
+                  | Just t <- [tbl ^. at topPath],
+                    ref <- toList t
+                ]
 
 checkQualifiedExpr ::
   (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder] r) =>
   QualifiedName ->
   Sem r ScopedIden
 checkQualifiedExpr q@(QualifiedName (SymbolPath p) sym) = do
-  es <- filter entryIsExpression <$> lookupQualifiedSymbol (toList p, sym)
+  es <- fst <$> lookupQualifiedSymbol (toList p, sym)
   case es of
     [] -> notInScope
     [e] -> entryToScopedIden q' e
@@ -492,48 +469,51 @@ checkQualifiedExpr q@(QualifiedName (SymbolPath p) sym) = do
     q' = NameQualified q
     notInScope = throw (ErrQualSymNotInScope (QualSymNotInScope q))
 
-entryToScopedIden :: (Members '[InfoTableBuilder] r) => Name -> SymbolEntry -> Sem r ScopedIden
+entryToScopedIden :: Members '[InfoTableBuilder] r => Name -> SymbolEntry -> Sem r ScopedIden
 entryToScopedIden name e = do
   let scopedName :: S.Name
-      scopedName = set S.nameConcrete name (entryName e)
+      scopedName = set S.nameConcrete name (e ^. symbolEntry)
   registerName scopedName
-  return $ case e of
+  return (ScopedIden (set S.nameConcrete name (e ^. symbolEntry)))
-    EntryAxiom ref -> ScopedAxiom (set S.nameConcrete name ref)
-    EntryInductive ref ->
-      ScopedInductive (set S.nameConcrete name ref)
-    EntryConstructor ref ->
-      ScopedConstructor (set S.nameConcrete name ref)
-    EntryFunction ref ->
-      ScopedFunction (set S.nameConcrete name ref)
-    EntryVariable v -> case name of
-      NameQualified {} -> impossible
-      NameUnqualified uname -> ScopedVar (set S.nameConcrete uname v)
-    EntryModule {} -> impossible
 
 -- | We gather all symbols which have been defined or marked to be public in the given scope.
-exportScope :: forall r. (Members '[State Scope, Error ScoperError] r) => Scope -> Sem r ExportInfo
+exportScope ::
+  forall r.
+  Members '[State Scope, Error ScoperError] r =>
+  Scope ->
+  Sem r ExportInfo
 exportScope Scope {..} = do
-  _exportSymbols <- getExportSymbols
+  _exportSymbols <- HashMap.fromList <$> mapMaybeM mkentry (HashMap.toList _scopeSymbols)
+  _exportModuleSymbols <- HashMap.fromList <$> mapMaybeM mkentry (HashMap.toList _scopeModuleSymbols)
   return ExportInfo {..}
   where
-    getExportSymbols :: Sem r (HashMap Symbol SymbolEntry)
+    mkentry ::
-    getExportSymbols = HashMap.fromList <$> mapMaybeM entry (HashMap.toList _scopeSymbols)
+      forall ns.
+      SingI ns =>
+      (Symbol, SymbolInfo ns) ->
+      Sem r (Maybe (Symbol, NameSpaceEntryType ns))
+    mkentry (s, SymbolInfo {..}) =
+      case filter shouldExport (toList _symbolInfo) of
+        [] -> return Nothing
+        [e] -> return (Just (s, e))
+        e : es -> err (e :| es)
       where
-        shouldExport :: SymbolEntry -> Bool
+        shouldExport :: NameSpaceEntryType ns -> Bool
-        shouldExport ent = _nameVisibilityAnn == VisPublic
+        shouldExport ent = ent ^. nsEntry . S.nameVisibilityAnn == VisPublic
-          where
-            S.Name' {..} = entryName ent
 
-        entry :: (Symbol, SymbolInfo) -> Sem r (Maybe (Symbol, SymbolEntry))
+        err :: NonEmpty (NameSpaceEntryType ns) -> Sem r a
-        entry (s, SymbolInfo {..}) =
+        err es =
-          case filter shouldExport (toList _symbolInfo) of
+          throw
-            [] -> return Nothing
+            ( ErrMultipleExport
-            [e] -> return $ Just (s, e)
+                ( MultipleExportConflict
-            (e : es) ->
+                    _scopePath
-              throw
+                    s
-                ( ErrMultipleExport
+                    ( case sing :: SNameSpace ns of
-                    (MultipleExportConflict _scopePath s (e :| es))
+                        SNameSpaceSymbols -> Left es
+                        SNameSpaceModules -> Right es
+                    )
                 )
+            )
 
 getParsedModule :: Members '[Reader ScopeParameters] r => TopModulePath -> Sem r (Module 'Parsed 'ModuleTop)
 getParsedModule i = asks (^?! scopeParsedModules . at i . _Just)
@@ -693,7 +673,6 @@ checkInductiveDef InductiveDef {..} = do
             | (cname, cdef) <- zipExact (toList constructorNames') (toList _inductiveConstructors)
           ]
     return (inductiveParameters', inductiveType', inductiveDoc', inductiveConstructors')
-  forM_ inductiveConstructors' bindConstructor
   registerInductive
     @$> InductiveDef
       { _inductiveName = inductiveName',
@@ -708,15 +687,6 @@ checkInductiveDef InductiveDef {..} = do
         _inductiveKw
       }
   where
-    bindConstructor :: ConstructorDef 'Scoped -> Sem r ()
-    bindConstructor d =
-      topBindings $
-        bindReservedSymbol
-          (d ^. constructorName)
-          ( EntryConstructor
-              ( S.unConcrete (d ^. constructorName)
-              )
-          )
     -- note that the constructor name is not bound here
     checkConstructorDef :: S.Symbol -> S.Symbol -> ConstructorDef 'Parsed -> Sem r (ConstructorDef 'Scoped)
     checkConstructorDef tyName constructorName' ConstructorDef {..} = do
@@ -770,16 +740,7 @@ checkInductiveDef InductiveDef {..} = do
           }
 
 createExportsTable :: ExportInfo -> HashSet NameId
-createExportsTable ei = foldr (HashSet.insert . getNameId) HashSet.empty (HashMap.elems (ei ^. exportSymbols))
+createExportsTable = HashSet.fromList . (^.. exportAllNames . S.nameId)
-  where
-    getNameId :: SymbolEntry -> NameId
-    getNameId = \case
-      EntryAxiom r -> getNameRefId r
-      EntryInductive r -> getNameRefId r
-      EntryFunction r -> getNameRefId r
-      EntryConstructor r -> getNameRefId r
-      EntryModule r -> getModuleRefNameId r
-      EntryVariable v -> v ^. S.nameId
 
 checkTopModules ::
   forall r.
@@ -823,7 +784,7 @@ checkTopModule m@Module {..} = do
       let _nameDefinedIn = S.topModulePathToAbsPath _modulePath
           _nameConcrete = _modulePath
           _nameDefined = getLoc (_modulePath ^. modulePathName)
-          _nameKind = S.KNameTopModule
+          _nameKind = KNameTopModule
           _nameFixity :: Maybe Fixity
           _nameFixity = Nothing
           -- This visibility annotation is not relevant
@@ -863,14 +824,22 @@ checkTopModule m@Module {..} = do
 withTopScope :: Members '[State Scope] r => Sem r a -> Sem r a
 withTopScope ma = do
   before <- get @Scope
-  let scope' = set scopeLocalSymbols mempty before
+  let scope' =
+        ( set scopeLocalSymbols mempty
+            . set scopeLocalModuleSymbols mempty
+        )
+          before
   put scope'
   ma
 
 withLocalScope :: Members '[State Scope] r => Sem r a -> Sem r a
 withLocalScope ma = do
   before <- get @Scope
-  let scope' = set scopeLocalSymbols mempty before
+  let scope' =
+        ( set scopeLocalSymbols mempty
+            . set scopeLocalModuleSymbols mempty
+        )
+          before
   put scope'
   x <- ma
   put before
@@ -977,7 +946,7 @@ checkSections sec = topBindings $ case sec of
         reserveDefinition = \case
           DefinitionSyntax s -> void (checkSyntaxDef s)
           DefinitionFunctionDef d -> void (reserveFunctionSymbol d)
-          DefinitionTypeSignature d -> void (reserveSymbolOf S.KNameFunction Nothing (d ^. sigName))
+          DefinitionTypeSignature d -> void (reserveSymbolOf SKNameFunction Nothing (d ^. sigName))
           DefinitionAxiom d -> void (reserveAxiomSymbol d)
           DefinitionInductive d -> do
             void (reserveInductiveSymbol d)
@@ -1065,7 +1034,7 @@ reserveLocalModuleSymbol ::
   Symbol ->
   Sem r S.Symbol
 reserveLocalModuleSymbol =
-  ignoreFixities . ignoreIterators . reserveSymbolOf S.KNameLocalModule Nothing
+  ignoreFixities . ignoreIterators . reserveSymbolOf SKNameLocalModule Nothing
 
 checkLocalModule ::
   forall r.
@@ -1091,11 +1060,10 @@ checkLocalModule Module {..} = do
             _moduleKw,
             _moduleKwEnd
           }
-      entry :: ModuleRef' 'S.NotConcrete
+      mref :: ModuleRef' 'S.NotConcrete
-      entry = mkModuleRef' @'ModuleLocal ModuleRef'' {..}
+      mref = mkModuleRef' @'ModuleLocal ModuleRef'' {..}
-  bindReservedSymbol _modulePath' (EntryModule entry)
+  modify (over scoperModules (HashMap.insert moduleId mref))
   registerName (S.unqualifiedSymbol _modulePath')
-  modify (over scoperModules (HashMap.insert moduleId entry))
   return _moduleRefModule
   where
     inheritScope :: Sem r ()
@@ -1103,12 +1071,15 @@ checkLocalModule Module {..} = do
       absPath <- (S.<.> _modulePath) <$> gets (^. scopePath)
       modify (set scopePath absPath)
       modify (over scopeSymbols (fmap inheritSymbol))
+      modify (over scopeModuleSymbols (fmap inheritSymbol))
       where
-        inheritSymbol :: SymbolInfo -> SymbolInfo
+        inheritSymbol :: forall ns. SingI ns => SymbolInfo ns -> SymbolInfo ns
-        inheritSymbol (SymbolInfo s) = SymbolInfo (fmap inheritEntry s)
+        inheritSymbol (SymbolInfo s) = SymbolInfo (inheritEntry <$> s)
-
+          where
-        inheritEntry :: SymbolEntry -> SymbolEntry
+            inheritEntry :: NameSpaceEntryType ns -> NameSpaceEntryType ns
-        inheritEntry = entryOverName (over S.nameWhyInScope S.BecauseInherited . set S.nameVisibilityAnn VisPrivate)
+            inheritEntry =
+              over (nsEntry . S.nameWhyInScope) S.BecauseInherited
+                . set (nsEntry . S.nameVisibilityAnn) VisPrivate
 
 checkOrphanFixities :: forall r. Members '[Error ScoperError, State ScoperFixities] r => Sem r ()
 checkOrphanFixities = do
@@ -1126,30 +1097,34 @@ checkOrphanIterators = do
     Nothing -> return ()
     Just x -> throw (ErrUnusedIteratorDef (UnusedIteratorDef x))
 
-symbolInfoSingle :: SymbolEntry -> SymbolInfo
+symbolInfoSingle :: SingI ns => NameSpaceEntryType ns -> SymbolInfo ns
-symbolInfoSingle p = SymbolInfo $ HashMap.singleton (entryName p ^. S.nameDefinedIn) p
+symbolInfoSingle p = SymbolInfo $ HashMap.singleton (p ^. nsEntry . S.nameDefinedIn) p
+
+getModuleRef ::
+  Members '[State ScoperState] r =>
+  ModuleSymbolEntry ->
+  Name ->
+  Sem r ModuleRef
+getModuleRef e n =
+  overModuleRef'' (set (moduleRefName . S.nameConcrete) n)
+    <$> gets (^?! scoperModules . at (e ^. moduleEntry . S.nameId) . _Just)
 
 lookupModuleSymbol ::
-  (Members '[Error ScoperError, State Scope, State ScoperState] r) =>
+  Members '[Error ScoperError, State Scope, State ScoperState] r =>
   Name ->
   Sem r ModuleRef
 lookupModuleSymbol n = do
-  es <- lookupQualifiedSymbol (path, sym)
+  es <- snd <$> lookupQualifiedSymbol (path, sym)
-  case mapMaybe getModuleRef es of
+  case nonEmpty (resolveShadowing es) of
-    [] -> notInScope
+    Nothing -> notInScope
-    [x] -> return (overModuleRef'' (set (moduleRefName . S.nameConcrete) n) x)
+    Just (x :| []) -> getModuleRef x n
-    _ -> throw (ErrAmbiguousModuleSym (AmbiguousModuleSym n es))
+    Just more -> throw (ErrAmbiguousModuleSym (AmbiguousModuleSym n more))
   where
     notInScope = throw (ErrModuleNotInScope (ModuleNotInScope n))
     (path, sym) = case n of
       NameUnqualified s -> ([], s)
       NameQualified (QualifiedName (SymbolPath p) s) -> (toList p, s)
 
-getModuleRef :: SymbolEntry -> Maybe (ModuleRef' 'S.NotConcrete)
-getModuleRef = \case
-  EntryModule m -> Just m
-  _ -> Nothing
-
 getExportInfo ::
   forall r.
   (Members '[State ScoperState] r) =>
@@ -1205,7 +1180,7 @@ checkOpenModuleNoImport OpenModule {..}
   | isJust _openModuleImportKw = impossible
   | otherwise = do
       openModuleName'@(ModuleRef' (_ :&: moduleRef'')) <- lookupModuleSymbol _openModuleName
-      let exportInfo@(ExportInfo tbl) = moduleRef'' ^. moduleExportInfo
+      let exportInfo = moduleRef'' ^. moduleExportInfo
       registerName (moduleRef'' ^. moduleRefName)
 
       let checkUsingHiding :: UsingHiding 'Parsed -> Sem r (UsingHiding 'Scoped)
@@ -1213,10 +1188,10 @@ checkOpenModuleNoImport OpenModule {..}
             Hiding h -> Hiding <$> checkHidingList h
             Using uh -> Using <$> checkUsingList uh
             where
-              scopeSymbol :: Symbol -> Sem r S.Symbol
+              scopeSymbol :: forall (ns :: NameSpace). SingI ns => Sing ns -> Symbol -> Sem r S.Symbol
-              scopeSymbol s = do
+              scopeSymbol _ s = do
-                let mentry :: Maybe SymbolEntry
+                let mentry :: Maybe (NameSpaceEntryType ns)
-                    mentry = tbl ^. at s
+                    mentry = exportInfo ^. exportNameSpace . at s
                     err =
                       throw
                         ( ErrModuleDoesNotExportSymbol
@@ -1252,11 +1227,25 @@ checkOpenModuleNoImport OpenModule {..}
                     }
 
               checkHidingItem :: HidingItem 'Parsed -> Sem r (HidingItem 'Scoped)
-              checkHidingItem h = HidingItem <$> scopeSymbol (h ^. hidingSymbol)
+              checkHidingItem h = do
+                let s = h ^. hidingSymbol
+                scopedSym <-
+                  if
+                      | isJust (h ^. hidingModuleKw) -> scopeSymbol SNameSpaceModules s
+                      | otherwise -> scopeSymbol SNameSpaceSymbols s
+                return
+                  HidingItem
+                    { _hidingSymbol = scopedSym,
+                      _hidingModuleKw = h ^. hidingModuleKw
+                    }
 
               checkUsingItem :: UsingItem 'Parsed -> Sem r (UsingItem 'Scoped)
               checkUsingItem i = do
-                scopedSym <- scopeSymbol (i ^. usingSymbol)
+                let s = i ^. usingSymbol
+                scopedSym <-
+                  if
+                      | isJust (i ^. usingModuleKw) -> scopeSymbol SNameSpaceModules s
+                      | otherwise -> scopeSymbol SNameSpaceSymbols s
                 let scopedAs = do
                       c <- i ^. usingAs
                       return (set S.nameConcrete c scopedSym)
@@ -1265,7 +1254,8 @@ checkOpenModuleNoImport OpenModule {..}
                   UsingItem
                     { _usingSymbol = scopedSym,
                       _usingAs = scopedAs,
-                      _usingAsKw = i ^. usingAsKw
+                      _usingAsKw = i ^. usingAsKw,
+                      _usingModuleKw = i ^. usingModuleKw
                     }
 
       usingHiding' <- mapM checkUsingHiding _openUsingHiding
@@ -1279,25 +1269,32 @@ checkOpenModuleNoImport OpenModule {..}
           }
   where
     mergeScope :: ExportInfo -> Sem r ()
-    mergeScope ExportInfo {..} =
+    mergeScope ei = do
-      mapM_ mergeSymbol (HashMap.toList _exportSymbols)
+      mapM_ mergeSymbol (HashMap.toList (ei ^. exportSymbols))
+      mapM_ mergeSymbol (HashMap.toList (ei ^. exportModuleSymbols))
       where
-        mergeSymbol :: (Symbol, SymbolEntry) -> Sem r ()
+        mergeSymbol :: forall ns. SingI ns => (Symbol, NameSpaceEntryType ns) -> Sem r ()
         mergeSymbol (s, entry) =
           modify
-            (over scopeSymbols (HashMap.insertWith (<>) s (symbolInfoSingle entry)))
+            (over scopeNameSpace (HashMap.insertWith (<>) s (symbolInfoSingle entry)))
 
     alterScope :: Maybe (UsingHiding 'Scoped) -> ExportInfo -> ExportInfo
     alterScope openModif = alterEntries . filterScope
       where
-        alterEntry :: SymbolEntry -> SymbolEntry
+        alterEntries :: ExportInfo -> ExportInfo
+        alterEntries nfo =
+          ExportInfo
+            { _exportSymbols = alterEntry <$> nfo ^. exportSymbols,
+              _exportModuleSymbols = alterEntry <$> nfo ^. exportModuleSymbols
+            }
+
+        alterEntry :: SingI ns => NameSpaceEntryType ns -> NameSpaceEntryType ns
         alterEntry =
-          entryOverName
+          over
+            nsEntry
             ( set S.nameWhyInScope S.BecauseImportedOpened
                 . set S.nameVisibilityAnn (publicAnnToVis _openPublic)
             )
-        alterEntries :: ExportInfo -> ExportInfo
-        alterEntries = over exportSymbols (fmap alterEntry)
 
         publicAnnToVis :: PublicAnn -> VisibilityAnn
         publicAnnToVis = \case
@@ -1306,11 +1303,17 @@ checkOpenModuleNoImport OpenModule {..}
 
         filterScope :: ExportInfo -> ExportInfo
         filterScope = case openModif of
-          Just (Using l) -> over exportSymbols (HashMap.fromList . mapMaybe inUsing . HashMap.toList)
+          Just (Using l) ->
+            over exportSymbols (HashMap.fromList . mapMaybe inUsing . HashMap.toList)
+              . over exportModuleSymbols (HashMap.fromList . mapMaybe inUsing . HashMap.toList)
             where
-              inUsing :: (Symbol, SymbolEntry) -> Maybe (Symbol, SymbolEntry)
+              inUsing ::
+                forall (ns :: NameSpace).
+                SingI ns =>
+                (Symbol, NameSpaceEntryType ns) ->
+                Maybe (Symbol, NameSpaceEntryType ns)
               inUsing (sym, e) = do
-                mayAs' <- u ^. at (symbolEntryNameId e)
+                mayAs' <- u ^. at (e ^. nsEntry . S.nameId)
                 return (fromMaybe sym mayAs', e)
               u :: HashMap NameId (Maybe Symbol)
               u =
@@ -1318,10 +1321,12 @@ checkOpenModuleNoImport OpenModule {..}
                   [ (i ^. usingSymbol . S.nameId, i ^? usingAs . _Just . S.nameConcrete)
                     | i <- toList (l ^. usingList)
                   ]
-          Just (Hiding l) -> over exportSymbols (HashMap.filter (not . inHiding))
+          Just (Hiding l) ->
+            over exportSymbols (HashMap.filter (not . inHiding))
+              . over exportModuleSymbols (HashMap.filter (not . inHiding))
             where
-              inHiding :: SymbolEntry -> Bool
+              inHiding :: forall ns. SingI ns => NameSpaceEntryType ns -> Bool
-              inHiding e = HashSet.member (symbolEntryNameId e) u
+              inHiding e = HashSet.member (e ^. nsEntry . S.nameId) u
               u :: HashSet NameId
               u = HashSet.fromList (map (^. hidingSymbol . S.nameId) (toList (l ^. hidingList)))
           Nothing -> id
@@ -1376,8 +1381,8 @@ checkAxiomDef AxiomDef {..} = do
   axiomDoc' <- withLocalScope (mapM checkJudoc _axiomDoc)
   registerAxiom @$> AxiomDef {_axiomName = axiomName', _axiomType = axiomType', _axiomDoc = axiomDoc', ..}
 
-entryToSymbol :: SymbolEntry -> Symbol -> S.Symbol
+entryToSymbol :: forall (ns :: NameSpace). SingI ns => NameSpaceEntryType ns -> Symbol -> S.Symbol
-entryToSymbol sentry csym = set S.nameConcrete csym (symbolEntryToSName sentry)
+entryToSymbol sentry csym = set S.nameConcrete csym (sentry ^. nsEntry)
 
 checkFunction ::
   forall r.
@@ -1572,9 +1577,7 @@ checkUnqualified s = do
   scope <- get
   -- Lookup at the global scope
   let err = throw (ErrSymNotInScope (NotInScope s scope))
-  entries <-
+  entries <- fst <$> lookupQualifiedSymbol ([], s)
-    filter S.isExprKind
-      <$> lookupQualifiedSymbol ([], s)
   case resolveShadowing entries of
     [] -> err
     [x] -> entryToScopedIden n x
@@ -1586,10 +1589,10 @@ checkUnqualified s = do
 -- shadowing rules for modules. For example, a symbol defined in the outer
 -- module with the same name as a symbol defined in the inner module will be
 -- removed.
-resolveShadowing :: [SymbolEntry] -> [SymbolEntry]
+resolveShadowing :: forall ns. SingI ns => [NameSpaceEntryType ns] -> [NameSpaceEntryType ns]
-resolveShadowing es = go [(e, entryName e ^. S.nameWhyInScope) | e <- es]
+resolveShadowing es = go [(e, e ^. nsEntry . S.nameWhyInScope) | e <- es]
   where
-    go :: [(SymbolEntry, S.WhyInScope)] -> [SymbolEntry]
+    go :: [(NameSpaceEntryType ns, S.WhyInScope)] -> [NameSpaceEntryType ns]
     go itms
       | any (((== S.BecauseImportedOpened) .||. (== S.BecauseDefined)) . snd) itms =
           [e | (e, w) <- itms, not (isInherited w)]
@@ -1625,16 +1628,16 @@ checkPatternName n = do
     -- check whether the symbol is a constructor in scope
     getConstructorRef :: Sem r (Maybe S.Name)
     getConstructorRef = do
-      entries <- mapMaybe getConstructor <$> lookupQualifiedSymbol (path, sym)
+      entries <- mapMaybe getConstructor . fst <$> lookupQualifiedSymbol (path, sym)
       case entries of
         [] -> case SymbolPath <$> nonEmpty path of
           Nothing -> return Nothing -- There is no constructor with such a name
           Just pth -> throw (ErrQualSymNotInScope (QualSymNotInScope (QualifiedName pth sym)))
         [e] -> return (Just (set S.nameConcrete n e)) -- There is one constructor with such a name
-        es -> throw (ErrAmbiguousSym (AmbiguousSym n (map EntryConstructor es)))
+        es -> throw (ErrAmbiguousSym (AmbiguousSym n (map SymbolEntry es)))
-    getConstructor :: SymbolEntry -> Maybe (RefNameType 'S.NotConcrete)
+    getConstructor :: SymbolEntry -> Maybe (S.Name' ())
-    getConstructor = \case
+    getConstructor e = case getNameKind e of
-      EntryConstructor r -> Just r
+      KNameConstructor -> Just (e ^. symbolEntry)
       _ -> Nothing
 
 checkPatternBinding ::
@@ -1836,7 +1839,7 @@ checkParens ::
 checkParens e@(ExpressionAtoms as _) = case as of
   AtomIdentifier s :| [] -> do
     scopedId <- checkName s
-    let scopedIdenNoFix = idenOverName (set S.nameFixity Nothing) scopedId
+    let scopedIdenNoFix = over scopedIden (set S.nameFixity Nothing) scopedId
     return (ExpressionParensIdentifier scopedIdenNoFix)
   AtomIterator i :| [] -> ExpressionIterator . set iteratorParens True <$> checkIterator i
   AtomCase c :| [] -> ExpressionCase . set caseParens True <$> checkCase c
@@ -2180,7 +2183,7 @@ makePatternTable (PatternAtoms latoms _) = [appOp] : operators
         unqualifiedSymbolOp :: S.Name -> Maybe (Precedence, P.Operator ParsePat PatternArg)
         unqualifiedSymbolOp S.Name' {..}
           | Just Fixity {..} <- _nameFixity,
-            _nameKind == S.KNameConstructor = Just $
+            _nameKind == KNameConstructor = Just $
               case _fixityArity of
                 Unary u -> (_fixityPrecedence, P.Postfix (unaryApp <$> parseSymbolId _nameId))
                   where

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs

@@ -10,7 +10,6 @@ import Juvix.Compiler.Concrete.Data.NameSignature.Error
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error.Pretty
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error.Types
 import Juvix.Compiler.Internal.Translation.FromConcrete.NamedArguments.Error
-import Juvix.Prelude
 
 data ScoperError
   = ErrInfixParser InfixError
@@ -43,7 +42,6 @@ data ScoperError
   | ErrNameSignature NameSignatureError
   | ErrNoNameSignature NoNameSignature
   | ErrNamedArgumentsError NamedArgumentsError
-  deriving stock (Show)
 
 instance ToGenericError ScoperError where
   genericError = \case

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs

@@ -286,7 +286,7 @@ instance ToGenericError DuplicateIterator where
 data MultipleExportConflict = MultipleExportConflict
   { _multipleExportModule :: S.AbsModulePath,
     _multipleExportSymbol :: Symbol,
-    _multipleExportEntries :: NonEmpty SymbolEntry
+    _multipleExportEntries :: Either (NonEmpty SymbolEntry) (NonEmpty ModuleSymbolEntry)
   }
   deriving stock (Show)
 
@@ -313,7 +313,6 @@ data NotInScope = NotInScope
   { _notInScopeSymbol :: Symbol,
     _notInScopeScope :: Scope
   }
-  deriving stock (Show)
 
 makeLenses ''NotInScope
 
@@ -469,11 +468,11 @@ instance ToGenericError AmbiguousSym where
           opts' = fromGenericOptions opts
           i = getLoc _ambiguousSymName
           is = map getLoc _ambiguousSymEntires
-          msg = ambiguousMessage opts' _ambiguousSymName _ambiguousSymEntires
+          msg = ambiguousMessage opts' _ambiguousSymName (map (ppCode opts') _ambiguousSymEntires)
 
 data AmbiguousModuleSym = AmbiguousModuleSym
   { _ambiguousModName :: Name,
-    _ambiguousModSymEntires :: [SymbolEntry]
+    _ambiguousModSymEntires :: NonEmpty ModuleSymbolEntry
   }
   deriving stock (Show)
 
@@ -490,8 +489,9 @@ instance ToGenericError AmbiguousModuleSym where
         where
           opts' = fromGenericOptions opts
           i = getLoc _ambiguousModName
-          is = map getLoc _ambiguousModSymEntires
+          entries = toList _ambiguousModSymEntires
-          msg = ambiguousMessage opts' _ambiguousModName _ambiguousModSymEntires
+          is = map getLoc entries
+          msg = ambiguousMessage opts' _ambiguousModName (map (ppCode opts') entries)
 
 infixErrorAux :: Doc Ann -> Doc Ann -> Doc Ann
 infixErrorAux kind pp =
@@ -501,7 +501,7 @@ infixErrorAux kind pp =
       <> line
       <> indent' pp
 
-ambiguousMessage :: Options -> Name -> [SymbolEntry] -> Doc Ann
+ambiguousMessage :: Options -> Name -> [Doc Ann] -> Doc Ann
 ambiguousMessage opts' n es =
   "The symbol"
     <+> ppCode opts' n
@@ -511,7 +511,7 @@ ambiguousMessage opts' n es =
       <> line
       <> "It could be any of:"
       <> line
-      <> itemize (map (ppMessage opts') es)
+      <> itemize es
 
 newtype DoubleBracesPattern = DoubleBracesPattern
   { _doubleBracesPatternArg :: PatternArg

src/Juvix/Compiler/Concrete/Translation/FromSource.hs

@@ -231,6 +231,7 @@ mkTopModulePath l = TopModulePath (NonEmpty.init l) (NonEmpty.last l)
 
 usingItem :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (UsingItem 'Parsed)
 usingItem = do
+  _usingModuleKw <- optional (kw kwModule)
   _usingSymbol <- symbol
   alias <- optional $ do
     k <- Irrelevant <$> kw kwAs
@@ -240,7 +241,10 @@ usingItem = do
   return UsingItem {..}
 
 hidingItem :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => ParsecS r (HidingItem 'Parsed)
-hidingItem = HidingItem <$> symbol
+hidingItem = do
+  _hidingModuleKw <- optional (kw kwModule)
+  _hidingSymbol <- symbol
+  return HidingItem {..}
 
 phidingList :: Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => ParsecS r (HidingList 'Parsed)
 phidingList = do

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -228,7 +228,7 @@ toPreModule Module {..} = do
       SModuleLocal -> goSymbol _modulePath
 
 goTopModulePath :: S.TopModulePath -> Internal.Name
-goTopModulePath p = goSymbolPretty (prettyText p) (S.topModulePathName p)
+goTopModulePath p = goSymbolPretty (prettyText p) (S.topModulePathSymbol p)
 
 fromPreModule ::
   forall r.
@@ -774,12 +774,16 @@ goExpression = \case
         loc = getLoc l
 
     goIden :: Concrete.ScopedIden -> Internal.Expression
-    goIden x = Internal.ExpressionIden $ case x of
+    goIden x = Internal.ExpressionIden $ case getNameKind x of
-      ScopedAxiom a -> Internal.IdenAxiom (goName a)
+      KNameAxiom -> Internal.IdenAxiom n'
-      ScopedInductive i -> Internal.IdenInductive (goName i)
+      KNameInductive -> Internal.IdenInductive n'
-      ScopedVar v -> Internal.IdenVar (goSymbol v)
+      KNameLocal -> Internal.IdenVar n'
-      ScopedFunction fun -> Internal.IdenFunction (goName fun)
+      KNameFunction -> Internal.IdenFunction n'
-      ScopedConstructor c -> Internal.IdenConstructor (goName c)
+      KNameConstructor -> Internal.IdenConstructor n'
+      KNameLocalModule -> impossible
+      KNameTopModule -> impossible
+      where
+        n' = goName (x ^. scopedIden)
 
     goLet :: Let 'Scoped -> Sem r Internal.Let
     goLet l = do

src/Juvix/Data/NameId.hs

@@ -7,6 +7,7 @@ newtype NameId = NameId
   { _unNameId :: Word64
   }
   deriving stock (Show, Eq, Ord, Generic, Data)
+  deriving newtype (Enum)
 
 makeLenses ''NameId
 

src/Juvix/Data/NameKind.hs

@@ -21,6 +21,8 @@ data NameKind
     KNameTopModule
   deriving stock (Show, Eq, Data)
 
+$(genSingletons [''NameKind])
+
 class HasNameKind a where
   getNameKind :: a -> NameKind
 
@@ -46,24 +48,19 @@ nameKindText = \case
   KNameLocalModule -> "local module"
   KNameTopModule -> "module"
 
-isLocallyBounded :: (HasNameKind a) => a -> Bool
+isExprKind :: HasNameKind a => a -> Bool
-isLocallyBounded k = case getNameKind k of
-  KNameLocal -> True
-  _ -> False
-
-isExprKind :: (HasNameKind a) => a -> Bool
 isExprKind k = case getNameKind k of
   KNameLocalModule -> False
   KNameTopModule -> False
   _ -> True
 
-isModuleKind :: (HasNameKind a) => a -> Bool
+isModuleKind :: HasNameKind a => a -> Bool
 isModuleKind k = case getNameKind k of
   KNameLocalModule -> True
   KNameTopModule -> True
   _ -> False
 
-canBeCompiled :: (HasNameKind a) => a -> Bool
+canBeCompiled :: HasNameKind a => a -> Bool
 canBeCompiled k = case getNameKind k of
   KNameConstructor -> True
   KNameInductive -> True
@@ -73,7 +70,7 @@ canBeCompiled k = case getNameKind k of
   KNameLocalModule -> False
   KNameTopModule -> False
 
-canHaveFixity :: (HasNameKind a) => a -> Bool
+canHaveFixity :: HasNameKind a => a -> Bool
 canHaveFixity k = case getNameKind k of
   KNameConstructor -> True
   KNameInductive -> True
@@ -83,7 +80,7 @@ canHaveFixity k = case getNameKind k of
   KNameLocalModule -> False
   KNameTopModule -> False
 
-canBeIterator :: (HasNameKind a) => a -> Bool
+canBeIterator :: HasNameKind a => a -> Bool
 canBeIterator k = case getNameKind k of
   KNameFunction -> True
   KNameAxiom -> True
@@ -103,7 +100,7 @@ nameKindAnsi k = case k of
   KNameLocal -> mempty
   KNameTopModule -> color Cyan
 
-isFunctionKind :: (HasNameKind a) => a -> Bool
+isFunctionKind :: HasNameKind a => a -> Bool
 isFunctionKind k = case getNameKind k of
   KNameFunction -> True
   _ -> False

test/Scope/Positive.hs

@@ -242,5 +242,9 @@ tests =
     PosTest
       "Format pragma"
       $(mkRelDir ".")
-      $(mkRelFile "FormatPragma.juvix")
+      $(mkRelFile "FormatPragma.juvix"),
+    PosTest
+      "Namespaces"
+      $(mkRelDir ".")
+      $(mkRelFile "Namespaces.juvix")
   ]

tests/positive/Namespaces.juvix

@@ -0,0 +1,45 @@
+module Namespaces;
+
+module Main;
+  module M;
+    axiom A : Type;
+  end;
+
+  axiom M : Type;
+
+end;
+
+module Test1;
+  open Main using {module M; M};
+  open M;
+
+  axiom x : M.A;
+
+  axiom x1 : A;
+
+  axiom x2 : M;
+end;
+
+module Test2;
+  open Main hiding {module M};
+
+  axiom x2 : M;
+
+  module M;
+
+  end;
+
+  open M;
+end;
+
+module Test3;
+  open Main using {M};
+
+  axiom x2 : M;
+
+  module M;
+
+  end;
+
+  open M;
+end;