diff --git a/app/Commands/Dev/Repl/Options.hs b/app/Commands/Dev/Repl/Options.hs
index 99f6c8499..ebf142cf1 100644
--- 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
diff --git a/app/Commands/Repl.hs b/app/Commands/Repl.hs
index eb96d1cc5..4cd56516b 100644
--- 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
diff --git a/app/Commands/Repl/Options.hs b/app/Commands/Repl/Options.hs
index 540c3c2be..7f6ac6a35 100644
--- 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
diff --git a/src/Juvix/Compiler/Concrete/Data/Scope.hs b/src/Juvix/Compiler/Concrete/Data/Scope.hs
index 46c2d5999..751dbdd14 100644
--- 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
diff --git a/src/Juvix/Compiler/Concrete/Data/Scope/Base.hs b/src/Juvix/Compiler/Concrete/Data/Scope/Base.hs
new file mode 100644
index 000000000..02413be71
--- /dev/null
+++ 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
diff --git a/src/Juvix/Compiler/Concrete/Extra.hs b/src/Juvix/Compiler/Concrete/Extra.hs
index 81d9b2233..1a125237f 100644
--- 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]
diff --git a/src/Juvix/Compiler/Concrete/Gen.hs b/src/Juvix/Compiler/Concrete/Gen.hs
new file mode 100644
index 000000000..c4629f3bf
--- /dev/null
+++ 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
+      }
diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs
index 2a360d9af..607e2263b 100644
--- 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
diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
index 01cc0ab7a..bec041f02 100644
--- 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)))
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
index 6a8418b17..9fa521c0d 100644
--- 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
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
index 2a3f193ba..14c28d0b2 100644
--- 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
diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
index e04791117..abf55d098 100644
--- 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
         )
 
diff --git a/src/Juvix/Compiler/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Internal/Data/InfoTable.hs
index 0505893e2..97e889119 100644
--- 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
+  ]
diff --git a/src/Juvix/Compiler/Internal/Data/InfoTable/Base.hs b/src/Juvix/Compiler/Internal/Data/InfoTable/Base.hs
index e0dcd205c..e5bff7593 100644
--- 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
   }
 
diff --git a/src/Juvix/Compiler/Internal/Extra.hs b/src/Juvix/Compiler/Internal/Extra.hs
index d248e6e7e..364b2e1e0 100644
--- 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
+          }
diff --git a/src/Juvix/Compiler/Internal/Translation.hs b/src/Juvix/Compiler/Internal/Translation.hs
index 0bb6f27f2..30406b098 100644
--- 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
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index 18d9c2ad7..a829d12be 100644
--- 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 =>
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs
index a70fa1ed2..ffa731d22 100644
--- 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
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
index 01f8096bf..939773c62 100644
--- 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
diff --git a/src/Juvix/Compiler/Pipeline/Artifacts.hs b/src/Juvix/Compiler/Pipeline/Artifacts.hs
index c71cf8eb2..e38539485 100644
--- 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
     )
diff --git a/src/Juvix/Compiler/Pipeline/Repl.hs b/src/Juvix/Compiler/Pipeline/Repl.hs
index c57f769ee..ea605d46e 100644
--- 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
 
diff --git a/src/Juvix/Data/Effect/Fail.hs b/src/Juvix/Data/Effect/Fail.hs
index 1a0240cbe..7d06d19fb 100644
--- 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 #-}
diff --git a/src/Juvix/Prelude.hs b/src/Juvix/Prelude.hs
index 844111bdb..2ce7f2a97 100644
--- 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
diff --git a/src/Juvix/Prelude/Pretty.hs b/src/Juvix/Prelude/Pretty.hs
index 1cac0d21d..8b03bf725 100644
--- 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
 
diff --git a/src/Juvix/Prelude/Stream.hs b/src/Juvix/Prelude/Stream.hs
new file mode 100644
index 000000000..d30086686
--- /dev/null
+++ 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)
diff --git a/test/Typecheck/Positive.hs b/test/Typecheck/Positive.hs
index d1fcbffa1..5b8a70989 100644
--- 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
        ]
diff --git a/tests/positive/Projections.juvix b/tests/positive/Projections.juvix
new file mode 100644
index 000000000..daab2c761
--- /dev/null
+++ 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;
diff --git a/tests/positive/Records.juvix b/tests/positive/Records.juvix
index 30a7f57ef..b62320feb 100644
--- 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;
diff --git a/tests/smoke/Commands/repl.smoke.yaml b/tests/smoke/Commands/repl.smoke.yaml
index 0d227fd56..0a0d4a6b9 100644
--- 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