Add field projections for records (#2260)

- Closes #2258 # Overview When we define a type with a single constructor and one ore more fields, a local module is generated with the same name as the inductive type. This module contains a projection for every field. Projections can be used as any other function. E.g. If we have ``` type Pair (A B : Type) := mkPair { fst : A; snd : B; }; ``` Then we generate ``` module Pair; fst {A B : Type} : Pair A B -> A | (mkPair a b) := a; snd : {A B : Type} : Pair A B -> B | (mkPair a b) := b; end; ```
2024-12-01 00:04:58 +03:00 · 2023-08-01 10:46:22 +02:00 · 2023-08-01 10:46:22 +02:00 · 4a6a7e6540
commit 4a6a7e6540
parent 3c5cc744ec
29 changed files with 702 additions and 303 deletions
--- a/app/Commands/Dev/Repl/Options.hs
+++ b/app/Commands/Dev/Repl/Options.hs
@ -7,6 +7,7 @@ import Juvix.Compiler.Core.Data.TransformationId (toEvalTransformations)
 parseDevRepl :: Parser ReplOptions
 parseDevRepl = do
  let _replPrintValues = False
+      _replIsDev = True
  _replInputFile <- optional parseInputJuvixFile
  _replTransformations <- do
    ts <- optTransformationIds
--- a/app/Commands/Repl.hs
+++ b/app/Commands/Repl.hs
@ -44,11 +44,16 @@ import System.Console.Haskeline
 import System.Console.Repline
 import System.Console.Repline qualified as Repline

-helpTxt :: MonadIO m => m ()
-helpTxt =
-  liftIO
-    ( putStrLn
-        [__i|
+printHelpTxt :: ReplOptions -> Repl ()
+printHelpTxt opts = do
+  liftIO $ do
+    putStrLn normalCmds
+    let isDev = opts ^. replIsDev
+    when isDev (putStrLn devCmds)
+  where
+    normalCmds :: Text
+    normalCmds =
+      [__i|
  EXPRESSION                Evaluate an expression in the context of the currently loaded module
  :help                     Print help text and describe options
  :load       FILE          Load a file into the REPL
@ -62,7 +67,12 @@ helpTxt =
  :version                  Display the Juvix version
  :quit                     Exit the REPL
  |]
-    )
+
+    devCmds :: Text
+    devCmds =
+      [__i|
+  :dev        DEV CMD       Command reserved for debugging
+  |]

 replDefaultLoc :: Interval
 replDefaultLoc = singletonInterval (mkInitialLoc replPath)
@ -93,9 +103,6 @@ noFileLoadedErr = replError (mkAnsiText @Text "No file loaded. Load a file using
 welcomeMsg :: MonadIO m => m ()
 welcomeMsg = liftIO (putStrLn [i|Juvix REPL version #{versionTag}: https://juvix.org. Run :help for help|])

-printHelpTxt :: String -> Repl ()
-printHelpTxt _ = helpTxt
-
 multilineCmd :: String
 multilineCmd = "multiline"

@ -207,6 +214,25 @@ core input = do
  compileRes <- liftIO (compileReplInputIO' ctx (strip (pack input))) >>= replFromEither . snd
  whenJust compileRes (renderOutLn . Core.ppOut opts)

+dev :: String -> Repl ()
+dev input = do
+  ctx <- replGetContext
+  if
+      | input == scoperStateCmd -> do
+          renderOutLn (Concrete.ppTrace (ctx ^. replContextArtifacts . artifactScoperState))
+      | otherwise ->
+          renderOutLn
+            ( "Unrecognized command "
+                <> input
+                <> "\nAvailable commands: "
+                <> unwords cmds
+            )
+  where
+    cmds :: [String]
+    cmds = [scoperStateCmd]
+    scoperStateCmd :: String
+    scoperStateCmd = "scoperState"
+
 ppConcrete :: Concrete.PrettyPrint a => a -> Repl AnsiText
 ppConcrete a = do
  gopts <- State.gets (^. replStateGlobalOptions)
@ -356,8 +382,8 @@ inferType input = do
  n <- replExpressionUpToTyped (strip (pack input))
  renderOutLn (Internal.ppOut (project' @GenericOptions gopts) (n ^. Internal.typedType))

-replCommands :: [(String, String -> Repl ())]
-replCommands = catchable ++ nonCatchable
+replCommands :: ReplOptions -> [(String, String -> Repl ())]
+replCommands opts = catchable ++ nonCatchable
  where
    nonCatchable :: [(String, String -> Repl ())]
    nonCatchable =
@ -367,7 +393,7 @@ replCommands = catchable ++ nonCatchable
    catchable =
      map
        (second (catchAll .))
-        [ ("help", printHelpTxt),
+        [ ("help", const (printHelpTxt opts)),
          -- `multiline` is included here for auto-completion purposes only.
          -- `repline`'s `multilineCommand` logic overrides this no-op.
          (multilineCmd, const (return ())),
@ -378,7 +404,8 @@ replCommands = catchable ++ nonCatchable
          ("doc", printDocumentation),
          ("type", inferType),
          ("version", displayVersion),
-          ("core", core)
+          ("core", core),
+          ("dev", dev)
        ]

 catchAll :: Repl () -> Repl ()
@ -395,7 +422,8 @@ defaultMatcher = [(":load", fileCompleter)]

 optsCompleter :: WordCompleter ReplS
 optsCompleter n = do
-  let names = (":" <>) . fst <$> replCommands
+  opts <- Reader.asks (^. replOptions)
+  let names = (":" <>) . fst <$> replCommands opts
  return (filter (isPrefixOf n) names)

 replBanner :: MultiLine -> Repl String
@ -456,7 +484,7 @@ runCommand opts = do
              finaliser = replFinaliser,
              tabComplete = replTabComplete,
              command = replCommand opts,
-              options = replCommands,
+              options = replCommands opts,
              banner = replBanner
            }
  globalOptions <- askGlobalOptions
--- a/app/Commands/Repl/Options.hs
+++ b/app/Commands/Repl/Options.hs
@ -5,7 +5,8 @@ import Juvix.Compiler.Core.Pretty.Options qualified as Core
 import Juvix.Compiler.Core.Transformation

 data ReplOptions = ReplOptions
-  { _replInputFile :: Maybe (AppPath File),
+  { _replIsDev :: Bool,
+    _replInputFile :: Maybe (AppPath File),
    _replShowDeBruijn :: Bool,
    _replNoPrelude :: Bool,
    _replTransformations :: [TransformationId],
@ -28,6 +29,7 @@ parseRepl = do
      _replShowDeBruijn = False
      _replNoDisambiguate = False
      _replPrintValues = True
+      _replIsDev = False
  _replInputFile <- optional parseInputJuvixFile
  _replNoPrelude <-
    switch
--- a/src/Juvix/Compiler/Concrete/Data/Scope.hs
+++ b/src/Juvix/Compiler/Concrete/Data/Scope.hs
@ -2,26 +2,17 @@ module Juvix.Compiler.Concrete.Data.Scope
  ( module Juvix.Compiler.Concrete.Data.Scope,
    module Juvix.Compiler.Concrete.Data.InfoTable,
    module Juvix.Compiler.Concrete.Data.NameSpace,
+    module Juvix.Compiler.Concrete.Data.Scope.Base,
  )
 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.Scope.Base
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Language
 import Juvix.Prelude

-type LocalVariable = S.Symbol
-
-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 (NameSpaceEntryType n)
-  }
-  deriving newtype (Semigroup, Monoid)
-
 nsEntry :: forall ns. SingI ns => Lens' (NameSpaceEntryType ns) (S.Name' ())
 nsEntry = case sing :: SNameSpace ns of
  SNameSpaceModules -> moduleEntry
@ -30,32 +21,6 @@ nsEntry = case sing :: SNameSpace ns of
 mkModuleRef' :: SingI t => ModuleRef'' 'S.NotConcrete t -> ModuleRef' 'S.NotConcrete
 mkModuleRef' m = ModuleRef' (sing :&: m)

-data BindingStrategy
-  = -- | Local binding allows shadowing
-    BindingLocal
-  | -- | Top binding does not allow shadowing. It may result in an ambiguous error
-    BindingTop
-
-data Scope = Scope
-  { _scopePath :: S.AbsModulePath,
-    _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;
-    -- import B as X;
-    _scopeTopModules :: HashMap TopModulePath (HashMap S.NameId (ModuleRef'' 'S.NotConcrete 'ModuleTop)),
-    -- | Symbols that have been defined in the current scope level. Every symbol
-    -- 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,
-    _scopeLocalModuleSymbols :: HashMap Symbol S.Symbol
-  }
-
-makeLenses ''SymbolInfo
-makeLenses ''Scope
-
 scopeNameSpace :: forall (ns :: NameSpace). SingI ns => Lens' Scope (HashMap Symbol (SymbolInfo ns))
 scopeNameSpace = case sing :: SNameSpace ns of
  SNameSpaceSymbols -> scopeSymbols
@ -66,57 +31,6 @@ scopeNameSpaceLocal s = case s of
  SNameSpaceSymbols -> scopeLocalSymbols
  SNameSpaceModules -> scopeLocalModuleSymbols

-newtype ModulesCache = ModulesCache
-  { _cachedModules :: HashMap TopModulePath (ModuleRef'' 'S.NotConcrete 'ModuleTop)
-  }
-
-makeLenses ''ModulesCache
-
-data ScopeParameters = ScopeParameters
-  { -- | Used for import cycle detection.
-    _scopeTopParents :: [Import 'Parsed],
-    _scopeParsedModules :: HashMap TopModulePath (Module 'Parsed 'ModuleTop)
-  }
-
-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
-  }
-
-makeLenses ''ScoperState
-
-data SymbolFixity = SymbolFixity
-  { _symbolFixityUsed :: Bool,
-    _symbolFixityDef :: OperatorSyntaxDef
-  }
-
-makeLenses ''SymbolFixity
-
-newtype ScoperFixities = ScoperFixites
-  { _scoperFixities :: HashMap Symbol SymbolFixity
-  }
-  deriving newtype (Semigroup, Monoid)
-
-makeLenses ''ScoperFixities
-
-data SymbolIterator = SymbolIterator
-  { _symbolIteratorUsed :: Bool,
-    _symbolIteratorDef :: IteratorSyntaxDef
-  }
-
-newtype ScoperIterators = ScoperIterators
-  { _scoperIterators :: HashMap Symbol SymbolIterator
-  }
-  deriving newtype (Semigroup, Monoid)
-
-makeLenses ''ScoperIterators
-makeLenses ''SymbolIterator
-
 emptyScope :: S.AbsModulePath -> Scope
 emptyScope absPath =
  Scope
--- a/src/Juvix/Compiler/Concrete/Data/Scope/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Data/Scope/Base.hs
@ -0,0 +1,86 @@
+module Juvix.Compiler.Concrete.Data.Scope.Base where
+
+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
+
+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 (NameSpaceEntryType n)
+  }
+  deriving newtype (Semigroup, Monoid)
+
+data BindingStrategy
+  = -- | Local binding allows shadowing
+    BindingLocal
+  | -- | Top binding does not allow shadowing. It may result in an ambiguous error
+    BindingTop
+
+data Scope = Scope
+  { _scopePath :: S.AbsModulePath,
+    _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;
+    -- import B as X;
+    _scopeTopModules :: HashMap TopModulePath (HashMap S.NameId (ModuleRef'' 'S.NotConcrete 'ModuleTop)),
+    -- | Symbols that have been defined in the current scope level. Every symbol
+    -- 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,
+    _scopeLocalModuleSymbols :: HashMap Symbol S.Symbol
+  }
+
+newtype ModulesCache = ModulesCache
+  { _cachedModules :: HashMap TopModulePath (ModuleRef'' 'S.NotConcrete 'ModuleTop)
+  }
+
+data ScopeParameters = ScopeParameters
+  { -- | Used for import cycle detection.
+    _scopeTopParents :: [Import 'Parsed],
+    _scopeParsedModules :: HashMap TopModulePath (Module 'Parsed 'ModuleTop)
+  }
+
+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
+  }
+
+data SymbolFixity = SymbolFixity
+  { _symbolFixityUsed :: Bool,
+    _symbolFixityDef :: OperatorSyntaxDef
+  }
+
+newtype ScoperFixities = ScoperFixites
+  { _scoperFixities :: HashMap Symbol SymbolFixity
+  }
+  deriving newtype (Semigroup, Monoid)
+
+data SymbolIterator = SymbolIterator
+  { _symbolIteratorUsed :: Bool,
+    _symbolIteratorDef :: IteratorSyntaxDef
+  }
+
+newtype ScoperIterators = ScoperIterators
+  { _scoperIterators :: HashMap Symbol SymbolIterator
+  }
+  deriving newtype (Semigroup, Monoid)
+
+makeLenses ''ScoperIterators
+makeLenses ''SymbolIterator
+makeLenses ''SymbolInfo
+makeLenses ''Scope
+makeLenses ''ScoperFixities
+makeLenses ''SymbolFixity
+makeLenses ''ScoperState
+makeLenses ''ScopeParameters
+makeLenses ''ModulesCache
--- a/src/Juvix/Compiler/Concrete/Extra.hs
+++ b/src/Juvix/Compiler/Concrete/Extra.hs
@ -114,6 +114,8 @@ groupStatements = \case
          SParsed -> fun1 ^. clauseOwnerFunction == fun2 ^. clauseOwnerFunction
          SScoped -> fun1 ^. clauseOwnerFunction == fun2 ^. clauseOwnerFunction
      (StatementFunctionClause {}, _) -> False
+      (StatementProjectionDef {}, StatementProjectionDef {}) -> True
+      (StatementProjectionDef {}, _) -> False
    definesSymbol :: Symbol -> Statement s -> Bool
    definesSymbol n s = case s of
      StatementTypeSignature sig -> n == symbolParsed (sig ^. sigName)
@ -154,6 +156,7 @@ migrateFunctionSyntax m = over moduleBody (mapMaybe goStatement) m
      StatementOpenModule {} -> Just s
      StatementFunctionDef {} -> Just s
      StatementFunctionClause {} -> Nothing
+      StatementProjectionDef {} -> Just s
      StatementTypeSignature sig -> Just (StatementFunctionDef (mkFunctionDef sig (getClauses (sig ^. sigName))))

    ss' :: [Statement 'Scoped]
--- a/src/Juvix/Compiler/Concrete/Gen.hs
+++ b/src/Juvix/Compiler/Concrete/Gen.hs
@ -0,0 +1,19 @@
+module Juvix.Compiler.Concrete.Gen
+  ( module Juvix.Compiler.Concrete.Gen,
+    module Juvix.Compiler.Concrete.Keywords,
+  )
+where
+
+import Juvix.Compiler.Concrete.Keywords
+import Juvix.Compiler.Concrete.Language
+import Juvix.Prelude
+
+kw :: Members '[Reader Interval] r => Keyword -> Sem r KeywordRef
+kw k = do
+  loc <- ask
+  return
+    KeywordRef
+      { _keywordRefKeyword = k,
+        _keywordRefUnicode = Ascii,
+        _keywordRefInterval = loc
+      }
--- a/src/Juvix/Compiler/Concrete/Language.hs
+++ b/src/Juvix/Compiler/Concrete/Language.hs
@ -113,6 +113,11 @@ type family ModulePathType s t = res | res -> t s where
  ModulePathType 'Parsed 'ModuleLocal = Symbol
  ModulePathType 'Scoped 'ModuleLocal = S.Symbol

+type ModuleInductiveType :: ModuleIsTop -> GHC.Type
+type family ModuleInductiveType t = res | res -> t where
+  ModuleInductiveType 'ModuleTop = ()
+  ModuleInductiveType 'ModuleLocal = Bool
+
 type ModuleEndType :: ModuleIsTop -> GHC.Type
 type family ModuleEndType t = res | res -> t where
  ModuleEndType 'ModuleTop = ()
@ -151,6 +156,7 @@ data Definition (s :: Stage)
  | DefinitionInductive (InductiveDef s)
  | DefinitionAxiom (AxiomDef s)
  | DefinitionTypeSignature (TypeSignature s)
+  | DefinitionProjectionDef (ProjectionDef s)

 data NonDefinition (s :: Stage)
  = NonDefinitionImport (Import s)
@ -168,6 +174,7 @@ data Statement (s :: Stage)
  | StatementOpenModule (OpenModule s)
  | StatementFunctionClause (FunctionClause s)
  | StatementAxiom (AxiomDef s)
+  | StatementProjectionDef (ProjectionDef s)

 deriving stock instance Show (Statement 'Parsed)

@ -181,6 +188,24 @@ deriving stock instance Ord (Statement 'Parsed)

 deriving stock instance Ord (Statement 'Scoped)

+data ProjectionDef s = ProjectionDef
+  { _projectionConstructor :: S.Symbol,
+    _projectionField :: SymbolType s,
+    _projectionFieldIx :: Int
+  }
+
+deriving stock instance Show (ProjectionDef 'Parsed)
+
+deriving stock instance Show (ProjectionDef 'Scoped)
+
+deriving stock instance Eq (ProjectionDef 'Parsed)
+
+deriving stock instance Eq (ProjectionDef 'Scoped)
+
+deriving stock instance Ord (ProjectionDef 'Parsed)
+
+deriving stock instance Ord (ProjectionDef 'Scoped)
+
 data Import (s :: Stage) = Import
  { _importKw :: KeywordRef,
    _importModule :: ImportType s,
@ -643,7 +668,8 @@ data Module (s :: Stage) (t :: ModuleIsTop) = Module
    _moduleDoc :: Maybe (Judoc s),
    _modulePragmas :: Maybe ParsedPragmas,
    _moduleBody :: [Statement s],
-    _moduleKwEnd :: ModuleEndType t
+    _moduleKwEnd :: ModuleEndType t,
+    _moduleInductive :: ModuleInductiveType t
  }

 deriving stock instance Show (Module 'Parsed 'ModuleTop)
@ -1397,6 +1423,9 @@ newtype ModuleIndex = ModuleIndex
  }

 makeLenses ''PatternArg
+makeLenses ''NonDefinitionsSection
+makeLenses ''DefinitionsSection
+makeLenses ''ProjectionDef
 makeLenses ''ScopedIden'
 makeLenses ''SymbolEntry
 makeLenses ''ModuleSymbolEntry
@ -1522,17 +1551,20 @@ instance SingI s => HasAtomicity (FunctionParameters s) where
 instance HasLoc ScopedIden where
  getLoc = getLoc . (^. scopedIden)

-instance HasLoc (InductiveDef 'Scoped) where
+instance SingI s => HasLoc (InductiveParameters s) where
+  getLoc i = getLocSymbolType (i ^. inductiveParametersNames . _head1) <> getLocExpressionType (i ^. inductiveParametersType)
+
+instance HasLoc (InductiveDef s) where
  getLoc i = (getLoc <$> i ^. inductivePositive) ?<> getLoc (i ^. inductiveKw)

-instance HasLoc (FunctionClause 'Scoped) where
-  getLoc c = getLoc (c ^. clauseOwnerFunction) <> getLoc (c ^. clauseBody)
+instance SingI s => HasLoc (FunctionClause s) where
+  getLoc c = getLocSymbolType (c ^. clauseOwnerFunction) <> getLocExpressionType (c ^. clauseBody)

 instance HasLoc ModuleRef where
  getLoc (ModuleRef' (_ :&: r)) = getLoc r

-instance HasLoc (AxiomDef 'Scoped) where
-  getLoc m = getLoc (m ^. axiomKw) <> getLoc (m ^. axiomType)
+instance SingI s => HasLoc (AxiomDef s) where
+  getLoc m = getLoc (m ^. axiomKw) <> getLocExpressionType (m ^. axiomType)

 instance HasLoc (OpenModule 'Scoped) where
  getLoc m =
@ -1540,6 +1572,9 @@ instance HasLoc (OpenModule 'Scoped) where
      <> getLoc (m ^. openModuleName)
      <>? fmap getLoc (m ^. openPublicKw . unIrrelevant)

+instance HasLoc (ProjectionDef s) where
+  getLoc = getLoc . (^. projectionConstructor)
+
 instance HasLoc (Statement 'Scoped) where
  getLoc :: Statement 'Scoped -> Interval
  getLoc = \case
@ -1552,6 +1587,7 @@ instance HasLoc (Statement 'Scoped) where
    StatementOpenModule t -> getLoc t
    StatementFunctionClause t -> getLoc t
    StatementAxiom t -> getLoc t
+    StatementProjectionDef t -> getLoc t

 instance HasLoc Application where
  getLoc (Application l r) = getLoc l <> getLoc r
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Print/Base.hs
@ -7,9 +7,11 @@ module Juvix.Compiler.Concrete.Print.Base
  )
 where

+import Data.HashMap.Strict qualified as HashMap
 import Data.List.NonEmpty.Extra qualified as NonEmpty
 import Juvix.Compiler.Concrete.Data.InfoTable
 import Juvix.Compiler.Concrete.Data.NameSignature.Base
+import Juvix.Compiler.Concrete.Data.Scope.Base
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Extra (fromAmbiguousIterator)
 import Juvix.Compiler.Concrete.Extra qualified as Concrete
@ -349,8 +351,12 @@ instance PrettyPrint a => PrettyPrint [a] where
    encloseSep (ppCode @Text "[") (ppCode @Text "]") (ppCode @Text ", ") cs

 ppStatements :: forall s r. (SingI s, Members '[ExactPrint, Reader Options] r) => [Statement s] -> Sem r ()
-ppStatements ss = paragraphs (ppGroup <$> Concrete.groupStatements ss)
+ppStatements ss = paragraphs (ppGroup <$> Concrete.groupStatements (filter (not . isInductiveModule) ss))
  where
+    isInductiveModule :: Statement s -> Bool
+    isInductiveModule = \case
+      StatementModule m -> m ^. moduleInductive
+      _ -> False
    ppGroup :: NonEmpty (Statement s) -> Sem r ()
    ppGroup = vsep . sepEndSemicolon . fmap ppCode

@ -988,6 +994,15 @@ instance SingI s => PrettyPrint (InductiveDef s) where
      ppConstructorBlock :: NonEmpty (ConstructorDef s) -> Sem r ()
      ppConstructorBlock cs = vsep (ppCode <$> cs)

+instance SingI s => PrettyPrint (ProjectionDef s) where
+  ppCode ProjectionDef {..} =
+    do
+      ppSymbolType _projectionField
+      <+> noLoc ":= projection"
+      <+> noLoc (pretty _projectionFieldIx)
+      <+> noLoc "for"
+      <+> ppCode _projectionConstructor
+
 instance SingI s => PrettyPrint (Statement s) where
  ppCode = \case
    StatementSyntax s -> ppCode s
@ -999,6 +1014,7 @@ instance SingI s => PrettyPrint (Statement s) where
    StatementOpenModule o -> ppCode o
    StatementFunctionClause c -> ppCode c
    StatementAxiom a -> ppCode a
+    StatementProjectionDef a -> ppCode a

 instance PrettyPrint SymbolEntry where
  ppCode ent =
@ -1027,3 +1043,13 @@ instance PrettyPrint ModuleSymbolEntry where
      kindWord :: Doc Ann =
        let k = getNameKind ent
         in (pretty (nameKindText k))
+
+header :: Members '[ExactPrint] r => Text -> Sem r ()
+header txt = annotated AnnImportant (noLoc (pretty (txt <> "\n")))
+
+instance PrettyPrint ScoperState where
+  ppCode :: Members '[ExactPrint, Reader Options] r => ScoperState -> Sem r ()
+  ppCode s =
+    do
+      header "scoperModules"
+      <> sepSemicolon (map ppCode (HashMap.toList (s ^. scoperModules)))
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@ -17,6 +17,7 @@ import Juvix.Compiler.Concrete.Data.Scope
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Extra (fromAmbiguousIterator)
 import Juvix.Compiler.Concrete.Extra qualified as P
+import Juvix.Compiler.Concrete.Gen qualified as G
 import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Pretty (ppTrace)
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Data.Context
@ -91,7 +92,7 @@ scopeCheckExpressionAtoms tab as = mapError (JuvixError @ScoperError) $ do

 scopeCheckExpression ::
  forall r.
-  (Members '[Error JuvixError, NameIdGen, State Scope] r) =>
+  (Members '[Error JuvixError, NameIdGen, State Scope, State ScoperState] r) =>
  InfoTable ->
  ExpressionAtoms 'Parsed ->
  Sem r Expression
@ -100,7 +101,6 @@ scopeCheckExpression tab as = mapError (JuvixError @ScoperError) $ do
    . ignoreHighlightBuilder
    . runInfoTableBuilder tab
    . runReader iniScopeParameters
-    . evalState iniScoperState
    . withLocalScope
    $ checkParseExpressionAtoms as
  where
@ -128,6 +128,20 @@ scopeCheckOpenModule = mapError (JuvixError @ScoperError) . checkOpenModule
 freshVariable :: Members '[NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, State ScoperState] r => Symbol -> Sem r S.Symbol
 freshVariable = freshSymbol KNameLocal

+checkProjectionDef ::
+  forall r.
+  Members '[Error ScoperError, InfoTableBuilder, Reader BindingStrategy, State Scope, State ScoperState, NameIdGen, State ScoperFixities, State ScoperIterators] r =>
+  ProjectionDef 'Parsed ->
+  Sem r (ProjectionDef 'Scoped)
+checkProjectionDef p = do
+  _projectionField <- getReservedDefinitionSymbol (p ^. projectionField)
+  return
+    ProjectionDef
+      { _projectionFieldIx = p ^. projectionFieldIx,
+        _projectionConstructor = p ^. projectionConstructor,
+        _projectionField
+      }
+
 freshSymbol ::
  forall r.
  Members '[State Scope, State ScoperState, NameIdGen, State ScoperFixities, State ScoperIterators] r =>
@ -256,6 +270,12 @@ reserveInductiveSymbol ::
  Sem r S.Symbol
 reserveInductiveSymbol d = reserveSymbolSignatureOf SKNameInductive d (d ^. inductiveName)

+reserveProjectionSymbol ::
+  Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, Reader BindingStrategy, InfoTableBuilder, State ScoperState] r =>
+  ProjectionDef 'Parsed ->
+  Sem r S.Symbol
+reserveProjectionSymbol d = reserveSymbolOf SKNameFunction Nothing (d ^. projectionField)
+
 reserveConstructorSymbol ::
  Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder] r =>
  InductiveDef 'Parsed ->
@ -351,10 +371,18 @@ 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)
+getModuleExportInfo :: forall r. Members '[State ScoperState] r => ModuleSymbolEntry -> Sem r ExportInfo
+getModuleExportInfo m = fromMaybeM err (gets (^? scoperModules . at (m ^. moduleEntry . S.nameId) . _Just . to getModuleRefExportInfo))
+  where
+    err :: Sem r a
+    err = do
+      ms <- toList <$> gets (^. scoperModules)
+      error
+        ( "impossible. Could not find "
+            <> ppTrace m
+            <> "\nModules in the state: "
+            <> ppTrace ms
+        )

 -- | Do not call directly. Looks for a symbol in (possibly) nested local modules
 lookupSymbolAux ::
@ -814,6 +842,7 @@ checkTopModule m@Module {..} = do
                    _moduleDoc = doc',
                    _modulePragmas = _modulePragmas,
                    _moduleKw,
+                    _moduleInductive,
                    _moduleKwEnd
                  }
              _moduleRefName = S.unConcrete path'
@ -881,98 +910,158 @@ checkModuleBody body = do
      where
        goNonDefinitions :: forall t. Members '[Output (Statement s)] t => NonDefinitionsSection s -> Sem t ()
        goNonDefinitions NonDefinitionsSection {..} = do
-          mapM_ go _nonDefinitionsSection
+          mapM_ (output . toStatement) _nonDefinitionsSection
          whenJust _nonDefinitionsNext goDefinitions
          where
-            go :: NonDefinition s -> Sem t ()
-            go = \case
-              NonDefinitionImport d -> output (StatementImport d)
-              NonDefinitionModule d -> output (StatementModule d)
-              NonDefinitionFunctionClause d -> output (StatementFunctionClause d)
-              NonDefinitionOpenModule d -> output (StatementOpenModule d)
+            toStatement :: NonDefinition s -> Statement s
+            toStatement = \case
+              NonDefinitionImport d -> StatementImport d
+              NonDefinitionModule d -> StatementModule d
+              NonDefinitionFunctionClause d -> StatementFunctionClause d
+              NonDefinitionOpenModule d -> StatementOpenModule d

        goDefinitions :: forall t. Members '[Output (Statement s)] t => DefinitionsSection s -> Sem t ()
        goDefinitions DefinitionsSection {..} = do
-          mapM_ go _definitionsSection
+          mapM_ (output . toStatement) _definitionsSection
          whenJust _definitionsNext goNonDefinitions
          where
-            go :: Definition s -> Sem t ()
-            go = \case
-              DefinitionSyntax d -> output @(Statement s) (StatementSyntax d)
-              DefinitionAxiom d -> output (StatementAxiom d)
-              DefinitionFunctionDef d -> output @(Statement s) (StatementFunctionDef d)
-              DefinitionInductive d -> output @(Statement s) (StatementInductive d)
-              DefinitionTypeSignature d -> output @(Statement s) (StatementTypeSignature d)
+            toStatement :: Definition s -> Statement s
+            toStatement = \case
+              DefinitionSyntax d -> StatementSyntax d
+              DefinitionAxiom d -> StatementAxiom d
+              DefinitionFunctionDef d -> StatementFunctionDef d
+              DefinitionInductive d -> StatementInductive d
+              DefinitionTypeSignature d -> StatementTypeSignature d
+              DefinitionProjectionDef d -> StatementProjectionDef d

 checkSections ::
  forall r.
  Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators] r =>
  StatementSections 'Parsed ->
  Sem r (StatementSections 'Scoped)
-checkSections sec = topBindings $ case sec of
-  SectionsEmpty -> return SectionsEmpty
-  SectionsDefinitions d -> SectionsDefinitions <$> goDefinitions d
-  SectionsNonDefinitions d -> SectionsNonDefinitions <$> goNonDefinitions d
+checkSections sec = do
+  (inductiveModules, sec' :: StatementSections 'Scoped) <- runOutputList (topBindings helper)
+  return $ case (fmap NonDefinitionModule) <$> nonEmpty inductiveModules of
+    Nothing -> sec'
+    Just im -> case sec' of
+      SectionsNonDefinitions d -> SectionsNonDefinitions (over nonDefinitionsSection (im <>) d)
+      SectionsEmpty ->
+        SectionsNonDefinitions
+          NonDefinitionsSection
+            { _nonDefinitionsSection = im,
+              _nonDefinitionsNext = Nothing
+            }
+      SectionsDefinitions d ->
+        SectionsNonDefinitions
+          NonDefinitionsSection
+            { _nonDefinitionsSection = im,
+              _nonDefinitionsNext = Just d
+            }
  where
-    goNonDefinitions :: NonDefinitionsSection 'Parsed -> Sem (Reader BindingStrategy ': r) (NonDefinitionsSection 'Scoped)
-    goNonDefinitions NonDefinitionsSection {..} = do
-      sec' <- mapM goNonDefinition _nonDefinitionsSection
-      next' <- mapM goDefinitions _nonDefinitionsNext
-      return
-        NonDefinitionsSection
-          { _nonDefinitionsNext = next',
-            _nonDefinitionsSection = sec'
-          }
+    helper ::
+      forall r'.
+      (r' ~ Reader BindingStrategy ': Output (Module 'Scoped 'ModuleLocal) ': r) =>
+      Sem r' (StatementSections 'Scoped)
+    helper = case sec of
+      SectionsEmpty -> return SectionsEmpty
+      SectionsDefinitions d -> SectionsDefinitions <$> goDefinitions d
+      SectionsNonDefinitions d -> SectionsNonDefinitions <$> goNonDefinitions d
      where
-        goNonDefinition :: NonDefinition 'Parsed -> Sem (Reader BindingStrategy ': r) (NonDefinition 'Scoped)
-        goNonDefinition = \case
-          NonDefinitionModule m -> NonDefinitionModule <$> checkLocalModule m
-          NonDefinitionImport i -> NonDefinitionImport <$> checkImport i
-          NonDefinitionFunctionClause i -> NonDefinitionFunctionClause <$> checkFunctionClause i
-          NonDefinitionOpenModule i -> NonDefinitionOpenModule <$> checkOpenModule i
+        goNonDefinitions :: NonDefinitionsSection 'Parsed -> Sem r' (NonDefinitionsSection 'Scoped)
+        goNonDefinitions NonDefinitionsSection {..} = do
+          sec' <- mapM goNonDefinition _nonDefinitionsSection
+          next' <- mapM goDefinitions _nonDefinitionsNext
+          return
+            NonDefinitionsSection
+              { _nonDefinitionsNext = next',
+                _nonDefinitionsSection = sec'
+              }
+          where
+            goNonDefinition :: NonDefinition 'Parsed -> Sem r' (NonDefinition 'Scoped)
+            goNonDefinition = \case
+              NonDefinitionModule m -> NonDefinitionModule <$> checkLocalModule m
+              NonDefinitionImport i -> NonDefinitionImport <$> checkImport i
+              NonDefinitionFunctionClause i -> NonDefinitionFunctionClause <$> checkFunctionClause i
+              NonDefinitionOpenModule i -> NonDefinitionOpenModule <$> checkOpenModule i

-    goDefinitions :: DefinitionsSection 'Parsed -> Sem (Reader BindingStrategy ': r) (DefinitionsSection 'Scoped)
-    goDefinitions DefinitionsSection {..} = do
-      mapM_ reserveDefinition _definitionsSection
-      sec' <- mapM goDefinition _definitionsSection
-      next' <- mapM goNonDefinitions _definitionsNext
-      return
-        DefinitionsSection
-          { _definitionsNext = next',
-            _definitionsSection = sec'
-          }
-      where
-        reserveDefinition :: Definition 'Parsed -> Sem (Reader BindingStrategy ': r) ()
-        reserveDefinition = \case
-          DefinitionSyntax s -> void (checkSyntaxDef s)
-          DefinitionFunctionDef d -> void (reserveFunctionSymbol d)
-          DefinitionTypeSignature d -> void (reserveSymbolOf SKNameFunction Nothing (d ^. sigName))
-          DefinitionAxiom d -> void (reserveAxiomSymbol d)
-          DefinitionInductive d -> do
-            void (reserveInductiveSymbol d)
-            mapM_ (reserveConstructorSymbol d) (d ^.. inductiveConstructors . each)
-        goDefinition :: Definition 'Parsed -> Sem (Reader BindingStrategy ': r) (Definition 'Scoped)
-        goDefinition = \case
-          DefinitionSyntax s -> return (DefinitionSyntax s)
-          DefinitionFunctionDef d -> DefinitionFunctionDef <$> checkFunctionDef d
-          DefinitionTypeSignature d -> DefinitionTypeSignature <$> checkTypeSignature d
-          DefinitionAxiom d -> DefinitionAxiom <$> checkAxiomDef d
-          DefinitionInductive d -> DefinitionInductive <$> checkInductiveDef d
+        goDefinitions :: DefinitionsSection 'Parsed -> Sem r' (DefinitionsSection 'Scoped)
+        goDefinitions DefinitionsSection {..} = do
+          mapM_ reserveDefinition _definitionsSection
+          sec' <- mapM goDefinition _definitionsSection
+          next' <- mapM goNonDefinitions _definitionsNext
+          return
+            DefinitionsSection
+              { _definitionsNext = next',
+                _definitionsSection = sec'
+              }
+          where
+            reserveDefinition :: Definition 'Parsed -> Sem r' ()
+            reserveDefinition = \case
+              DefinitionSyntax s -> void (checkSyntaxDef s)
+              DefinitionFunctionDef d -> void (reserveFunctionSymbol d)
+              DefinitionTypeSignature d -> void (reserveSymbolOf SKNameFunction Nothing (d ^. sigName))
+              DefinitionAxiom d -> void (reserveAxiomSymbol d)
+              DefinitionProjectionDef d -> void (reserveProjectionSymbol d)
+              DefinitionInductive d -> reserveInductive d
+              where
+                reserveInductive :: InductiveDef 'Parsed -> Sem r' ()
+                reserveInductive d = do
+                  void (reserveInductiveSymbol d)
+                  constrs <- mapM (reserveConstructorSymbol d) (d ^. inductiveConstructors)
+                  void (defineInductiveModule (head constrs) d)

-checkStatement ::
-  Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators] r =>
-  Statement 'Parsed ->
-  Sem r (Statement 'Scoped)
-checkStatement s = topBindings $ case s of
-  StatementSyntax synDef -> StatementSyntax <$> checkSyntaxDef synDef
-  StatementTypeSignature tySig -> StatementTypeSignature <$> checkTypeSignature tySig
-  StatementFunctionDef tySig -> StatementFunctionDef <$> checkFunctionDef tySig
-  StatementImport imp -> StatementImport <$> checkImport imp
-  StatementInductive dt -> StatementInductive <$> checkInductiveDef dt
-  StatementModule dt -> StatementModule <$> checkLocalModule dt
-  StatementOpenModule open -> StatementOpenModule <$> checkOpenModule open
-  StatementFunctionClause clause -> StatementFunctionClause <$> checkFunctionClause clause
-  StatementAxiom ax -> StatementAxiom <$> checkAxiomDef ax
+            goDefinition :: Definition 'Parsed -> Sem r' (Definition 'Scoped)
+            goDefinition = \case
+              DefinitionSyntax s -> return (DefinitionSyntax s)
+              DefinitionFunctionDef d -> DefinitionFunctionDef <$> checkFunctionDef d
+              DefinitionTypeSignature d -> DefinitionTypeSignature <$> checkTypeSignature d
+              DefinitionAxiom d -> DefinitionAxiom <$> checkAxiomDef d
+              DefinitionInductive d -> DefinitionInductive <$> checkInductiveDef d
+              DefinitionProjectionDef d -> DefinitionProjectionDef <$> checkProjectionDef d
+
+            defineInductiveModule :: S.Symbol -> InductiveDef 'Parsed -> Sem r' ()
+            defineInductiveModule headConstr i = do
+              m <- runReader (getLoc (i ^. inductiveName)) genModule
+              checkLocalModule m >>= output
+              where
+                genModule :: forall s'. Members '[Reader Interval] s' => Sem s' (Module 'Parsed 'ModuleLocal)
+                genModule = do
+                  _moduleKw <- G.kw G.kwModule
+                  _moduleKwEnd <- G.kw G.kwEnd
+                  let _modulePath = i ^. inductiveName
+                  _moduleBody <- genBody
+                  return
+                    Module
+                      { _moduleDoc = Nothing,
+                        _modulePragmas = Nothing,
+                        _moduleInductive = True,
+                        ..
+                      }
+                  where
+                    genBody :: Sem s' [Statement 'Parsed]
+                    genBody = fromMaybe [] <$> runFail genFieldProjections
+                      where
+                        genFieldProjections :: Sem (Fail ': s') [Statement 'Parsed]
+                        genFieldProjections = do
+                          fs <- indexFrom 0 . toList <$> getFields
+                          return (map (StatementProjectionDef . mkProjection) fs)
+                          where
+                            mkProjection ::
+                              Indexed (RecordField 'Parsed) ->
+                              ProjectionDef 'Parsed
+                            mkProjection (Indexed idx field) =
+                              ProjectionDef
+                                { _projectionConstructor = headConstr,
+                                  _projectionField = field ^. fieldName,
+                                  _projectionFieldIx = idx
+                                }
+
+                            getFields :: Sem (Fail ': s') (NonEmpty (RecordField 'Parsed))
+                            getFields = case i ^. inductiveConstructors of
+                              c :| [] -> case c ^. constructorRhs of
+                                ConstructorRhsRecord r -> return (r ^. rhsRecordFields)
+                                _ -> fail
+                              _ -> fail

 mkLetSections :: [LetClause 'Parsed] -> StatementSections 'Parsed
 mkLetSections = mkSections . map fromLetClause
@ -1024,6 +1113,7 @@ mkSections = \case
      StatementFunctionDef n -> Left (DefinitionFunctionDef n)
      StatementInductive i -> Left (DefinitionInductive i)
      StatementSyntax s -> Left (DefinitionSyntax s)
+      StatementProjectionDef s -> Left (DefinitionProjectionDef s)
      StatementImport i -> Right (NonDefinitionImport i)
      StatementModule m -> Right (NonDefinitionModule m)
      StatementOpenModule o -> Right (NonDefinitionOpenModule o)
@ -1058,6 +1148,7 @@ checkLocalModule Module {..} = do
            _moduleDoc = moduleDoc',
            _modulePragmas = _modulePragmas,
            _moduleKw,
+            _moduleInductive,
            _moduleKwEnd
          }
      mref :: ModuleRef' 'S.NotConcrete
@ -1125,18 +1216,6 @@ lookupModuleSymbol n = do
      NameUnqualified s -> ([], s)
      NameQualified (QualifiedName (SymbolPath p) s) -> (toList p, s)

-getExportInfo ::
-  forall r.
-  (Members '[State ScoperState] r) =>
-  S.ModuleNameId ->
-  Sem r ExportInfo
-getExportInfo modId = do
-  l <-
-    HashMap.lookupDefault impossible modId
-      <$> gets (^. scoperModules)
-  return $ case l ^. unModuleRef' of
-    _ :&: ent -> ent ^. moduleExportInfo
-
 checkOpenImportModule ::
  (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
  OpenModule 'Parsed ->
@ -1159,27 +1238,27 @@ checkOpenImportModule op
                      _openImportAsName = Nothing,
                      _openModuleName = maybe (op ^. openModuleName) topModulePathToName (op ^. openImportAsName)
                    }
-            scopedOpen <- checkOpenModuleNoImport op'
+            scopedOpen <- checkOpenModuleNoImport (Just (import' ^. importModule)) op'
            return
              scopedOpen
                { _openModuleImportKw = Just k,
                  _openModuleName = project (import' ^. importModule),
-                  _openImportAsName =
-                    if
-                        | Just asTxt <- (op ^. openImportAsName) -> Just (set S.nameConcrete asTxt topName)
-                        | otherwise -> Nothing
+                  _openImportAsName = (\asTxt -> set S.nameConcrete asTxt topName) <$> op ^. openImportAsName
                }
  | otherwise = impossible

 checkOpenModuleNoImport ::
  forall r.
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
+  Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
+  Maybe (ModuleRef'' 'S.Concrete 'ModuleTop) ->
  OpenModule 'Parsed ->
  Sem r (OpenModule 'Scoped)
-checkOpenModuleNoImport OpenModule {..}
+checkOpenModuleNoImport importModuleHint OpenModule {..}
  | isJust _openModuleImportKw = impossible
  | otherwise = do
-      openModuleName'@(ModuleRef' (_ :&: moduleRef'')) <- lookupModuleSymbol _openModuleName
+      openModuleName'@(ModuleRef' (_ :&: moduleRef'')) <- case importModuleHint of
+        Nothing -> lookupModuleSymbol _openModuleName
+        Just m -> return (project m)
      let exportInfo = moduleRef'' ^. moduleExportInfo
      registerName (moduleRef'' ^. moduleRefName)

@ -1338,7 +1417,7 @@ checkOpenModule ::
  Sem r (OpenModule 'Scoped)
 checkOpenModule op
  | isJust (op ^. openModuleImportKw) = checkOpenImportModule op
-  | otherwise = checkOpenModuleNoImport op
+  | otherwise = checkOpenModuleNoImport Nothing op

 checkFunctionClause ::
  forall r.
@ -1432,6 +1511,7 @@ checkLetClauses =
              DefinitionTypeSignature d -> LetTypeSig d
              DefinitionFunctionDef {} -> impossible
              DefinitionInductive {} -> impossible
+              DefinitionProjectionDef {} -> impossible
              DefinitionAxiom {} -> impossible
              DefinitionSyntax {} -> impossible
        fromNonDefs :: NonDefinitionsSection s -> NonEmpty (LetClause s)
@ -1550,8 +1630,8 @@ checkLambdaClause LambdaClause {..} = withLocalScope $ do
      }

 scopedVar ::
-  (Members '[InfoTableBuilder] r) =>
-  LocalVariable ->
+  Members '[InfoTableBuilder] r =>
+  S.Symbol ->
  Symbol ->
  Sem r S.Symbol
 scopedVar s n = do
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@ -1144,12 +1144,16 @@ moduleDef = P.label "<module definition>" $ do
  _moduleDoc <- getJudoc
  _modulePragmas <- getPragmas
  _modulePath <- pmodulePath
-  _moduleParameters <- many inductiveParams
  semicolon
  _moduleBody <- P.sepEndBy statement semicolon
  _moduleKwEnd <- endModule
  return Module {..}
  where
+    _moduleInductive :: ModuleInductiveType t
+    _moduleInductive = case sing :: SModuleIsTop t of
+      SModuleLocal -> False
+      SModuleTop -> ()
+
    endModule :: ParsecS r (ModuleEndType t)
    endModule = case sing :: SModuleIsTop t of
      SModuleLocal -> kw kwEnd
--- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
@ -219,7 +219,7 @@ goConstructor sym ctor = do
    ctorType =
      runReader
        initIndexTable
-        ( Internal.constructorType ctorName
+        ( Internal.lookupConstructorType ctorName
            >>= goType
        )

--- a/src/Juvix/Compiler/Internal/Data/InfoTable.hs
+++ b/src/Juvix/Compiler/Internal/Data/InfoTable.hs
@ -1,20 +1,19 @@
 module Juvix.Compiler.Internal.Data.InfoTable
  ( module Juvix.Compiler.Internal.Data.InfoTable.Base,
    buildTable,
-    buildTable1,
    extendWithReplExpression,
    lookupConstructor,
    lookupConstructorArgTypes,
    lookupFunction,
-    constructorReturnType,
-    constructorArgTypes,
+    lookupConstructorReturnType,
    lookupInductive,
    lookupAxiom,
    lookupInductiveType,
-    constructorType,
+    lookupConstructorType,
    getAxiomBuiltinInfo,
    getFunctionBuiltinInfo,
    buildTableShallow,
+    mkConstructorEntries,
  )
 where

@ -28,14 +27,13 @@ import Juvix.Prelude
 type MCache = Cache ModuleIndex InfoTable

 buildTable :: Foldable f => f Module -> InfoTable
-buildTable = run . evalCache computeTable mempty . getMany
+buildTable = run . evalCache (computeTable True) mempty . getMany

-buildTable1 :: Module -> InfoTable
-buildTable1 = buildTable . pure @[]
+buildTable' :: Foldable f => Bool -> f Module -> InfoTable
+buildTable' recurIntoImports = run . evalCache (computeTable recurIntoImports) mempty . getMany

-- TODO do not recurse into imports
 buildTableShallow :: Module -> InfoTable
-buildTableShallow = buildTable . pure @[]
+buildTableShallow = buildTable' False . pure @[]

 getMany :: (Members '[MCache] r, Foldable f) => f Module -> Sem r InfoTable
 getMany = mconcatMap (cacheGet . ModuleIndex)
@ -64,8 +62,8 @@ letFunctionDefs e =
      LetFunDef f -> pure f
      LetMutualBlock (MutualBlockLet fs) -> fs

-computeTable :: forall r. (Members '[MCache] r) => ModuleIndex -> Sem r InfoTable
-computeTable (ModuleIndex m) = compute
+computeTable :: forall r. Members '[MCache] r => Bool -> ModuleIndex -> Sem r InfoTable
+computeTable recurIntoImports (ModuleIndex m) = compute
  where
    compute :: Sem r InfoTable
    compute = do
@ -73,7 +71,9 @@ computeTable (ModuleIndex m) = compute
      return (InfoTable {..} <> infoInc)

    imports :: [Import]
-    imports = m ^. moduleBody . moduleImports
+    imports
+      | recurIntoImports = m ^. moduleBody . moduleImports
+      | otherwise = []

    mutuals :: [MutualStatement]
    mutuals =
@ -98,14 +98,9 @@ computeTable (ModuleIndex m) = compute
    _infoConstructors :: HashMap Name ConstructorInfo
    _infoConstructors =
      HashMap.fromList
-        [ (c ^. inductiveConstructorName, ConstructorInfo params ty ind builtin)
+        [ e
          | d <- inductives,
-            let ind = d ^. inductiveName
-                n = length (d ^. inductiveConstructors)
-                params = d ^. inductiveParameters
-                builtins = maybe (replicate n Nothing) (map Just . builtinConstructors) (d ^. inductiveBuiltin),
-            (builtin, c) <- zipExact builtins (d ^. inductiveConstructors),
-            let ty = c ^. inductiveConstructorType
+            e <- mkConstructorEntries d
        ]

    _infoFunctions :: HashMap Name FunctionInfo
@ -195,43 +190,11 @@ lookupInductiveType v = do
  where
    uni = smallUniverseE (getLoc v)

-constructorArgTypes :: ConstructorInfo -> ([VarName], [Expression])
-constructorArgTypes i =
-  ( map (^. inductiveParamName) (i ^. constructorInfoInductiveParameters),
-    constructorArgs (i ^. constructorInfoType)
-  )
+lookupConstructorType :: Member (Reader InfoTable) r => ConstrName -> Sem r Expression
+lookupConstructorType = fmap constructorType . lookupConstructor

-constructorType :: Member (Reader InfoTable) r => ConstrName -> Sem r Expression
-constructorType c = do
-  info <- lookupConstructor c
-  let (inductiveParams, constrArgs) = constructorArgTypes info
-      args =
-        map (typeAbstraction Implicit) inductiveParams
-          ++ map unnamedParameter constrArgs
-  saturatedTy <- constructorReturnType c
-  return (foldFunType args saturatedTy)
-
-constructorReturnType :: Member (Reader InfoTable) r => ConstrName -> Sem r Expression
-constructorReturnType c = do
-  info <- lookupConstructor c
-  let inductiveParams = fst (constructorArgTypes info)
-      ind = ExpressionIden (IdenInductive (info ^. constructorInfoInductive))
-      saturatedTy1 = foldExplicitApplication ind (map (ExpressionIden . IdenVar) inductiveParams)
-      saturatedTy =
-        foldl'
-          ( \t v ->
-              ExpressionApplication
-                ( Application
-                    { _appLeft = t,
-                      _appRight = ExpressionIden (IdenVar v),
-                      _appImplicit = Explicit
-                    }
-                )
-          )
-          ind
-          inductiveParams
-  unless (saturatedTy1 == saturatedTy) impossible
-  return saturatedTy
+lookupConstructorReturnType :: Member (Reader InfoTable) r => ConstrName -> Sem r Expression
+lookupConstructorReturnType = fmap constructorReturnType . lookupConstructor

 getAxiomBuiltinInfo :: Member (Reader InfoTable) r => Name -> Sem r (Maybe BuiltinAxiom)
 getAxiomBuiltinInfo n = do
@ -246,3 +209,15 @@ getFunctionBuiltinInfo n = do
  return $ case maybeFunInfo of
    Just funInfo -> funInfo ^. functionInfoDef . funDefBuiltin
    Nothing -> Nothing
+
+mkConstructorEntries :: InductiveDef -> [(ConstructorName, ConstructorInfo)]
+mkConstructorEntries d =
+  [ (c ^. inductiveConstructorName, ConstructorInfo {..})
+    | let _constructorInfoInductive = d ^. inductiveName
+          n = length (d ^. inductiveConstructors)
+          _constructorInfoInductiveParameters = d ^. inductiveParameters
+          builtins = maybe (replicate n Nothing) (map Just . builtinConstructors) (d ^. inductiveBuiltin),
+      (_constructorInfoBuiltin, c) <- zipExact builtins (d ^. inductiveConstructors),
+      let _constructorInfoType = c ^. inductiveConstructorType,
+      let _constructorInfoName = c ^. inductiveConstructorName
+  ]
--- a/src/Juvix/Compiler/Internal/Data/InfoTable/Base.hs
+++ b/src/Juvix/Compiler/Internal/Data/InfoTable/Base.hs
@ -7,6 +7,7 @@ data ConstructorInfo = ConstructorInfo
  { _constructorInfoInductiveParameters :: [InductiveParameter],
    _constructorInfoType :: Expression,
    _constructorInfoInductive :: InductiveName,
+    _constructorInfoName :: ConstructorName,
    _constructorInfoBuiltin :: Maybe BuiltinConstructor
  }

--- a/src/Juvix/Compiler/Internal/Extra.hs
+++ b/src/Juvix/Compiler/Internal/Extra.hs
@ -7,6 +7,8 @@ where
 import Data.Generics.Uniplate.Data hiding (holes)
 import Data.HashMap.Strict qualified as HashMap
 import Data.HashSet qualified as HashSet
+import Data.Stream qualified as Stream
+import Juvix.Compiler.Internal.Data.InfoTable.Base
 import Juvix.Compiler.Internal.Data.LocalVars
 import Juvix.Compiler.Internal.Language
 import Juvix.Prelude
@ -525,7 +527,7 @@ infixl 9 @@
 (@@) :: (IsExpression a, IsExpression b) => a -> b -> Expression
 a @@ b = toExpression (Application (toExpression a) (toExpression b) Explicit)

-freshVar :: (Member NameIdGen r) => Interval -> Text -> Sem r VarName
+freshVar :: Member NameIdGen r => Interval -> Text -> Sem r VarName
 freshVar _nameLoc n = do
  uid <- freshNameId
  return
@ -670,3 +672,90 @@ idenName = \case
  IdenVar v -> v
  IdenInductive i -> i
  IdenAxiom a -> a
+
+constructorArgTypes :: ConstructorInfo -> ([VarName], [Expression])
+constructorArgTypes i =
+  ( map (^. inductiveParamName) (i ^. constructorInfoInductiveParameters),
+    constructorArgs (i ^. constructorInfoType)
+  )
+
+constructorReturnType :: ConstructorInfo -> Expression
+constructorReturnType info =
+  let inductiveParams = fst (constructorArgTypes info)
+      ind = ExpressionIden (IdenInductive (info ^. constructorInfoInductive))
+      saturatedTy = foldExplicitApplication ind (map (ExpressionIden . IdenVar) inductiveParams)
+   in saturatedTy
+
+constructorType :: ConstructorInfo -> Expression
+constructorType info =
+  let (inductiveParams, constrArgs) = constructorArgTypes info
+      args =
+        map (typeAbstraction Implicit) inductiveParams
+          ++ map unnamedParameter constrArgs
+      saturatedTy = constructorReturnType info
+   in foldFunType args saturatedTy
+
+patternArgFromVar :: IsImplicit -> VarName -> PatternArg
+patternArgFromVar i v =
+  PatternArg
+    { _patternArgIsImplicit = i,
+      _patternArgName = Nothing,
+      _patternArgPattern = PatternVariable v
+    }
+
+-- | Given `mkPair`, returns (mkPair a b, [a, b])
+genConstructorPattern :: Members '[NameIdGen] r => ConstructorInfo -> Sem r (PatternArg, [VarName])
+genConstructorPattern info = do
+  let nargs = length (snd (constructorArgTypes info))
+      loc = getLoc (info ^. constructorInfoName)
+  vars <- mapM (freshVar loc) (Stream.take nargs allWords)
+  let app =
+        ConstructorApp
+          { _constrAppConstructor = info ^. constructorInfoName,
+            _constrAppParameters = map (patternArgFromVar Explicit) vars,
+            _constrAppType = Nothing
+          }
+      pat =
+        PatternArg
+          { _patternArgIsImplicit = Explicit,
+            _patternArgName = Nothing,
+            _patternArgPattern = PatternConstructorApp app
+          }
+  return (pat, vars)
+
+-- | Assumes the constructor does not have implicit arguments (which is not
+-- allowed at the moment).
+genFieldProjection ::
+  forall r.
+  Members '[NameIdGen] r =>
+  FunctionName ->
+  ConstructorInfo ->
+  Int ->
+  Sem r FunctionDef
+genFieldProjection _funDefName info fieldIx = do
+  clause <- genClause
+  let (inductiveParams, constrArgs) = constructorArgTypes info
+      saturatedTy = unnamedParameter (constructorReturnType info)
+      inductiveArgs = map (typeAbstraction Implicit) inductiveParams
+      retTy = constrArgs !! fieldIx
+  return
+    FunctionDef
+      { _funDefExamples = [],
+        _funDefTerminating = False,
+        _funDefBuiltin = Nothing,
+        _funDefPragmas = mempty,
+        _funDefClauses = pure clause,
+        _funDefType = foldFunType (inductiveArgs ++ [saturatedTy]) retTy,
+        ..
+      }
+  where
+    genClause :: Sem r FunctionClause
+    genClause = do
+      (pat, vars) <- genConstructorPattern info
+      let body = toExpression (vars !! fieldIx)
+      return
+        FunctionClause
+          { _clauseName = _funDefName,
+            _clausePatterns = [pat],
+            _clauseBody = body
+          }
--- a/src/Juvix/Compiler/Internal/Translation.hs
+++ b/src/Juvix/Compiler/Internal/Translation.hs
@ -8,7 +8,7 @@ module Juvix.Compiler.Internal.Translation
 where

 import Juvix.Compiler.Internal.Language
-import Juvix.Compiler.Internal.Translation.FromConcrete hiding (MCache, goModuleNoCache, goStatement)
+import Juvix.Compiler.Internal.Translation.FromConcrete hiding (MCache, goModuleNoCache)
 import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context
 import Juvix.Compiler.Internal.Translation.FromInternal
 import Juvix.Compiler.Internal.Translation.FromInternal.Data
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@ -25,6 +25,9 @@ import Juvix.Prelude

 type MCache = Cache Concrete.ModuleIndex Internal.Module

+-- | Needed to generate field projections.
+type ConstructorInfos = HashMap Internal.ConstructorName ConstructorInfo
+
 unsupported :: Text -> a
 unsupported msg = error $ msg <> "Scoped to Internal: not yet supported"

@ -37,6 +40,7 @@ fromConcrete _resultScoper =
    (modulesCache, _resultModules) <-
      runReader @Pragmas mempty
        . runReader @ExportsTable exportTbl
+        . evalState @ConstructorInfos mempty
        . runCacheEmpty goModuleNoCache
        $ mapM goTopModule ms
    let _resultTable = buildTable _resultModules
@ -139,10 +143,10 @@ fromConcreteOpenImport ::
 fromConcreteOpenImport = mapError (JuvixError @ScoperError) . runReader @Pragmas mempty . goOpenModule'

 goLocalModule ::
-  Members '[Error ScoperError, Builtins, NameIdGen, Reader Pragmas] r =>
+  Members '[Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ConstructorInfos] r =>
  Module 'Scoped 'ModuleLocal ->
  Sem r [Internal.PreStatement]
-goLocalModule = concatMapM goStatement . (^. moduleBody)
+goLocalModule = concatMapM goAxiomInductive . (^. moduleBody)

 goTopModule ::
  Members '[Reader ExportsTable, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache] r =>
@ -151,7 +155,7 @@ goTopModule ::
 goTopModule = cacheGet . ModuleIndex

 goModuleNoCache ::
-  Members '[Reader EntryPoint, Reader ExportsTable, Error JuvixError, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache] r =>
+  Members '[Reader EntryPoint, Reader ExportsTable, Error JuvixError, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache, State ConstructorInfos] r =>
  ModuleIndex ->
  Sem r Internal.Module
 goModuleNoCache (ModuleIndex m) = do
@ -207,7 +211,7 @@ traverseM' f x = sequence <$> traverse f x

 toPreModule ::
  forall r t.
-  (SingI t, Members '[Reader ExportsTable, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache] r) =>
+  (SingI t, Members '[Reader ExportsTable, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache, State ConstructorInfos] r) =>
  Module 'Scoped t ->
  Sem r Internal.PreModule
 toPreModule Module {..} = do
@ -272,21 +276,17 @@ fromPreModuleBody b = do

 goModuleBody ::
  forall r.
-  Members '[Reader ExportsTable, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache] r =>
+  Members '[Reader ExportsTable, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache, State ConstructorInfos] r =>
  [Statement 'Scoped] ->
  Sem r Internal.PreModuleBody
 goModuleBody stmts = do
  _moduleImports <- mapM goImport (scanImports stmts)
-  otherThanFunctions :: [Indexed Internal.PreStatement] <- concatMapM (traverseM' goStatement) ss
+  otherThanFunctions :: [Indexed Internal.PreStatement] <- concatMapM (traverseM' goAxiomInductive) ss
  functions <- map (fmap Internal.PreFunctionDef) <$> compiledFunctions
  newFunctions <- map (fmap Internal.PreFunctionDef) <$> newCompiledFunctions
-  let _moduleStatements =
-        map
-          (^. indexedThing)
-          ( sortOn
-              (^. indexedIx)
-              (otherThanFunctions <> functions <> newFunctions)
-          )
+  projections <- map (fmap Internal.PreFunctionDef) <$> mkProjections
+  let unsorted = otherThanFunctions <> functions <> newFunctions <> projections
+      _moduleStatements = map (^. indexedThing) (sortOn (^. indexedIx) unsorted)
  return Internal.ModuleBody {..}
  where
    ss' :: [Statement 'Scoped]
@ -295,6 +295,14 @@ goModuleBody stmts = do
    ss :: [Indexed (Statement 'Scoped)]
    ss = zipWith Indexed [0 ..] ss'

+    mkProjections :: Sem r [Indexed Internal.FunctionDef]
+    mkProjections =
+      sequence
+        [ Indexed i <$> funDef
+          | Indexed i (StatementProjectionDef f) <- ss,
+            let funDef = goProjectionDef f
+        ]
+
    newCompiledFunctions :: Sem r [Indexed Internal.FunctionDef]
    newCompiledFunctions =
      sequence
@ -331,6 +339,7 @@ scanImports stmts = mconcatMap go stmts
      StatementAxiom {} -> []
      StatementSyntax {} -> []
      StatementFunctionDef {} -> []
+      StatementProjectionDef {} -> []
      where
        openImport :: OpenModule 'Scoped -> Maybe (Import 'Scoped)
        openImport o = case o ^. openModuleImportKw of
@ -365,12 +374,12 @@ guardNotCached (hit, m) = do
  return m

 -- | Ignores functions
-goStatement ::
+goAxiomInductive ::
  forall r.
-  Members '[Error ScoperError, Builtins, NameIdGen, Reader Pragmas] r =>
+  Members '[Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ConstructorInfos] r =>
  Statement 'Scoped ->
  Sem r [Internal.PreStatement]
-goStatement = \case
+goAxiomInductive = \case
  StatementInductive i -> pure . Internal.PreInductiveDef <$> goInductive i
  StatementAxiom d -> pure . Internal.PreAxiomDef <$> goAxiom d
  StatementModule f -> goLocalModule f
@ -380,6 +389,7 @@ goStatement = \case
  StatementOpenModule {} -> return []
  StatementTypeSignature {} -> return []
  StatementFunctionClause {} -> return []
+  StatementProjectionDef {} -> return []

 goOpenModule' ::
  forall r.
@ -444,9 +454,19 @@ goFunctionDefHelper sig@TypeSignature {..} clauses = do
    (Nothing, Just clauses') -> mapM goFunctionClause clauses'
  return Internal.FunctionDef {..}

+goProjectionDef ::
+  forall r.
+  Members '[NameIdGen, State ConstructorInfos] r =>
+  ProjectionDef 'Scoped ->
+  Sem r Internal.FunctionDef
+goProjectionDef ProjectionDef {..} = do
+  let c = goSymbol _projectionConstructor
+  info <- gets @ConstructorInfos (^?! at c . _Just)
+  Internal.genFieldProjection (goSymbol _projectionField) info _projectionFieldIx
+
 goTopNewFunctionDef ::
  forall r.
-  (Members '[Reader Pragmas, Error ScoperError, Builtins, NameIdGen] r) =>
+  Members '[Reader Pragmas, Error ScoperError, Builtins, NameIdGen] r =>
  FunctionDef 'Scoped ->
  Sem r Internal.FunctionDef
 goTopNewFunctionDef FunctionDef {..} = do
@ -627,7 +647,7 @@ registerBuiltinAxiom d = \case
  BuiltinIntPrint -> registerIntPrint d

 goInductive ::
-  Members '[NameIdGen, Reader Pragmas, Builtins, Error ScoperError] r =>
+  Members '[NameIdGen, Reader Pragmas, Builtins, Error ScoperError, State ConstructorInfos] r =>
  InductiveDef 'Scoped ->
  Sem r Internal.InductiveDef
 goInductive ty@InductiveDef {..} = do
@ -653,8 +673,15 @@ goInductive ty@InductiveDef {..} = do
            _inductivePositive = isJust (ty ^. inductivePositive)
          }
  whenJust ((^. withLocParam) <$> _inductiveBuiltin) (registerBuiltinInductive indDef)
+  registerInductiveConstructors indDef
  return indDef

+-- | Registers constructors so we can access them for generating field projections
+registerInductiveConstructors :: Members '[State ConstructorInfos] r => Internal.InductiveDef -> Sem r ()
+registerInductiveConstructors indDef = do
+  m <- get
+  put (foldr (uncurry HashMap.insert) m (mkConstructorEntries indDef))
+
 goConstructorDef ::
  forall r.
  Members [Builtins, NameIdGen, Error ScoperError, Reader Pragmas] r =>
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs
@ -465,7 +465,7 @@ idenArity = \case
  IdenVar v -> getLocalArity v
  IdenInductive i -> typeArity <$> lookupInductiveType i
  IdenFunction f -> typeArity . (^. functionInfoDef . funDefType) <$> lookupFunction f
-  IdenConstructor c -> typeArity <$> constructorType c
+  IdenConstructor c -> typeArity <$> lookupConstructorType c
  IdenAxiom a -> typeArity . (^. axiomInfoDef . axiomType) <$> lookupAxiom a

 -- | let x be some expression of type T. The argument of this function is T and it returns
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
@ -22,7 +22,7 @@ type MCache = Cache ModuleIndex Module

 registerConstructor :: Members '[HighlightBuilder, State TypesTable, Reader InfoTable] r => ConstructorDef -> Sem r ()
 registerConstructor ctr = do
-  ty <- constructorType (ctr ^. inductiveConstructorName)
+  ty <- lookupConstructorType (ctr ^. inductiveConstructorName)
  registerNameIdType (ctr ^. inductiveConstructorName . nameId) ty

 registerNameIdType :: Members '[HighlightBuilder, State TypesTable, Reader InfoTable] r => NameId -> Expression -> Sem r ()
@ -122,7 +122,7 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do
        }
    goConstructor :: ConstructorDef -> Sem (Inference ': r) ConstructorDef
    goConstructor ConstructorDef {..} = do
-      expectedRetTy <- constructorReturnType _inductiveConstructorName
+      expectedRetTy <- lookupConstructorReturnType _inductiveConstructorName
      cty' <-
        runReader paramLocals $
          checkIsType (getLoc _inductiveConstructorType) _inductiveConstructorType
@ -708,7 +708,7 @@ inferExpression' hint e = case e of
        info <- lookupFunction fun
        return (TypedExpression (info ^. functionInfoDef . funDefType) (ExpressionIden i))
      IdenConstructor c -> do
-        ty <- constructorType c
+        ty <- lookupConstructorType c
        return (TypedExpression ty (ExpressionIden i))
      IdenVar v -> do
        ty <- lookupVar v
--- a/src/Juvix/Compiler/Pipeline/Artifacts.hs
+++ b/src/Juvix/Compiler/Pipeline/Artifacts.hs
@ -133,5 +133,6 @@ runFromConcreteCache =
    (artifactInternalModuleCache . Internal.cachedModules)
    ( mapError (JuvixError @ScoperError)
        . runReader (mempty :: Pragmas)
+        . evalState (mempty :: Internal.ConstructorInfos)
        . Internal.goModuleNoCache
    )
--- a/src/Juvix/Compiler/Pipeline/Repl.hs
+++ b/src/Juvix/Compiler/Pipeline/Repl.hs
@ -21,10 +21,10 @@ arityCheckExpression ::
  Sem r Internal.Expression
 arityCheckExpression p = do
  scopeTable <- gets (^. artifactScopeTable)
-  ( runNameIdGenArtifacts
-      . runBuiltinsArtifacts
-      . runScoperScopeArtifacts
-    )
+  runNameIdGenArtifacts
+    . runBuiltinsArtifacts
+    . runScoperScopeArtifacts
+    . runStateArtifacts artifactScoperState
    $ Scoper.scopeCheckExpression scopeTable p
      >>= Internal.fromConcreteExpression
      >>= Internal.arityCheckExpression
@ -61,6 +61,7 @@ scopeCheckExpression p = do
  runNameIdGenArtifacts
    . runBuiltinsArtifacts
    . runScoperScopeArtifacts
+    . runStateArtifacts artifactScoperState
    . Scoper.scopeCheckExpression scopeTable
    $ p

--- a/src/Juvix/Data/Effect/Fail.hs
+++ b/src/Juvix/Data/Effect/Fail.hs
@ -15,6 +15,12 @@ runFail ::
 runFail = fmap (^? _Right) . runError @() . reinterpret (\Fail -> throw ())
 {-# INLINE runFail #-}

+ignoreFail ::
+  Sem (Fail ': r) a ->
+  Sem r ()
+ignoreFail = void . runFail
+{-# INLINE ignoreFail #-}
+
 failWhen :: Member Fail r => Bool -> Sem r ()
 failWhen c = when c fail
 {-# INLINE failWhen #-}
--- a/src/Juvix/Prelude.hs
+++ b/src/Juvix/Prelude.hs
@ -1,6 +1,7 @@
 module Juvix.Prelude
  ( module Juvix.Prelude.Base,
    module Juvix.Prelude.Lens,
+    module Juvix.Prelude.Stream,
    module Juvix.Prelude.Trace,
    module Juvix.Prelude.Path,
    module Juvix.Prelude.Prepath,
@ -14,5 +15,6 @@ import Juvix.Prelude.Base
 import Juvix.Prelude.Lens
 import Juvix.Prelude.Path
 import Juvix.Prelude.Prepath
+import Juvix.Prelude.Stream
 import Juvix.Prelude.Tagged
 import Juvix.Prelude.Trace
--- a/src/Juvix/Prelude/Pretty.hs
+++ b/src/Juvix/Prelude/Pretty.hs
@ -55,10 +55,17 @@ mkAnsiText = AnsiText . pure . AnsiTextAtom

 makeLenses ''AnsiText

+instance HasTextBackend String where
+  toTextStream = toTextStream . pretty
+  toTextDoc = toTextDoc . pretty
+
 instance HasTextBackend Text where
  toTextStream = toTextStream . pretty
  toTextDoc = toTextDoc . pretty

+instance HasAnsiBackend String where
+  toAnsiDoc = pretty
+
 instance HasAnsiBackend Text where
  toAnsiDoc = pretty

--- a/src/Juvix/Prelude/Stream.hs
+++ b/src/Juvix/Prelude/Stream.hs
@ -0,0 +1,24 @@
+module Juvix.Prelude.Stream where
+
+import Data.Stream qualified as Stream
+import Juvix.Prelude.Base
+
+allWords :: Stream Text
+allWords = pack . toList <$> allFiniteSequences ('a' :| ['b' .. 'z'])
+
+-- | Returns all non-empty finite sequences
+allFiniteSequences :: forall a. NonEmpty a -> Stream (NonEmpty a)
+allFiniteSequences elems = build 0 []
+  where
+    build :: Integer -> [NonEmpty a] -> Stream (NonEmpty a)
+    build n = \case
+      [] -> build (succ n) (toList (ofLength (succ n)))
+      s : ss -> Stream.Cons s (build n ss)
+    ofLength :: Integer -> NonEmpty (NonEmpty a)
+    ofLength n
+      | n < 1 = impossible
+      | n == 1 = pure <$> elems
+      | otherwise = do
+          seq <- ofLength (n - 1)
+          e <- elems
+          return (pure e <> seq)
--- a/test/Typecheck/Positive.hs
+++ b/test/Typecheck/Positive.hs
@ -248,7 +248,11 @@ tests =
    posTest
      "Record declaration"
      $(mkRelDir ".")
-      $(mkRelFile "Records.juvix")
+      $(mkRelFile "Records.juvix"),
+    posTest
+      "Record projections"
+      $(mkRelDir ".")
+      $(mkRelFile "Projections.juvix")
  ]
    <> [ compilationTest t | t <- Compilation.tests
       ]
--- a/tests/positive/Projections.juvix
+++ b/tests/positive/Projections.juvix
@ -0,0 +1,55 @@
+module Projections;
+
+type Maybe (A : Type) :=
+  | nothing : Maybe A
+  | just : A -> Maybe A;
+
+type T :=
+  | t : T;
+
+module M;
+  type RecA (A B : Type) :=
+    | mkRecA {
+        arg : Maybe (RecB B A);
+        arg2 : A
+      };
+
+  type RecB (A B : Type) :=
+    | mkRecB {
+        arg : RecA B A;
+        arg2 : T
+      };
+
+  p1 : RecA T (Maybe T) :=
+    mkRecA
+      (arg := just
+         (mkRecB
+           (arg := mkRecA (arg := nothing; arg2 := t); arg2 := t));
+       arg2 := t);
+end;
+
+p3 : T := M.RecA.arg2 M.p1;
+
+open M;
+
+p2 : T := RecA.arg2 p1;
+
+open M.RecA;
+
+p4 : T := arg2 p1;
+
+module M2;
+  type Pair (A B : Type) :=
+    | mkPair {
+        fst : A;
+        snd : B
+      };
+
+  open Pair public;
+end;
+
+proj1 {A B : Type} (p : M2.Pair A B) : A := M2.fst p;
+
+import Stdlib.Data.Int.Ord as Int;
+
+x : _ := 1 Int.== 1;
--- a/tests/positive/Records.juvix
+++ b/tests/positive/Records.juvix
@ -29,3 +29,9 @@ p2 : Pair EnumRecord EnumRecord :=

 type newtype :=
  | mknewtype {f : T};
+
+p3 : Pair T T -> T := Pair.fst;
+
+open Pair;
+
+p4 {A : Type} : Pair A T -> A := fst;
--- a/tests/smoke/Commands/repl.smoke.yaml
+++ b/tests/smoke/Commands/repl.smoke.yaml
@ -429,7 +429,9 @@ tests:
    command:
      - juvix
      - repl
-    stdin: "import Stdlib.Data.Int.Ord as Int\n1 Int.== 1"
+    stdin: |
+      import Stdlib.Data.Int.Ord as Int
+      1 Int.== 1
    stdout:
      contains: "true"
    exit-status: 0
@ -438,7 +440,7 @@ tests:
    command:
      - juvix
      - repl
-    stdin: "import Stdlib.Data.Int.Ord as Int\nopen Int\n1 == 1"
+    stdin: "import Stdlib.Data.Int.Ord as Int open\n1 == 1"
    stdout:
      contains: "true"
    exit-status: 0