diff --git a/.hlint.yaml b/.hlint.yaml
index df9b14e18..80a50d0ba 100644
--- a/.hlint.yaml
+++ b/.hlint.yaml
@@ -13,6 +13,7 @@
         - DataKinds
         - DerivingStrategies
         - GADTs
+        - FunctionalDependencies
         - ImportQualifiedPost
         - LambdaCase
         - NoImplicitPrelude
diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature.hs
index f2af6debc..3be9f769c 100644
--- a/src/Juvix/Compiler/Concrete/Data/NameSignature.hs
+++ b/src/Juvix/Compiler/Concrete/Data/NameSignature.hs
@@ -1,8 +1,6 @@
 module Juvix.Compiler.Concrete.Data.NameSignature
-  ( module Juvix.Compiler.Concrete.Data.NameSignature.Base,
-    module Juvix.Compiler.Concrete.Data.NameSignature.Builder,
+  ( module Juvix.Compiler.Concrete.Data.NameSignature.Builder,
   )
 where
 
-import Juvix.Compiler.Concrete.Data.NameSignature.Base
 import Juvix.Compiler.Concrete.Data.NameSignature.Builder
diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Base.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Base.hs
deleted file mode 100644
index 30f776cfe..000000000
--- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Base.hs
+++ /dev/null
@@ -1,27 +0,0 @@
-module Juvix.Compiler.Concrete.Data.NameSignature.Base where
-
-import Juvix.Compiler.Concrete.Data.Name
-import Juvix.Prelude hiding (show)
-
-data NameBlock = NameBlock
-  { -- | Symbols map to themselves so we can retrive the location
-    -- | NOTE the index is wrt to the block, not the whole signature.
-    _nameBlock :: HashMap Symbol (Symbol, Int),
-    _nameImplicit :: IsImplicit
-  }
-  deriving stock (Show)
-
--- | Two consecutive blocks should have different implicitness
-newtype NameSignature = NameSignature
-  { _nameSignatureArgs :: [NameBlock]
-  }
-  deriving stock (Show)
-
-newtype RecordNameSignature = RecordNameSignature
-  { _recordNames :: HashMap Symbol (Symbol, Int)
-  }
-  deriving stock (Show)
-
-makeLenses ''NameSignature
-makeLenses ''RecordNameSignature
-makeLenses ''NameBlock
diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs
index 4e472c72c..89c44ec01 100644
--- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs
+++ b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs
@@ -1,90 +1,92 @@
+{-# LANGUAGE FunctionalDependencies #-}
+
 module Juvix.Compiler.Concrete.Data.NameSignature.Builder
   ( mkNameSignature,
     mkRecordNameSignature,
     HasNameSignature,
-    module Juvix.Compiler.Concrete.Data.NameSignature.Base,
     -- to supress unused warning
     getBuilder,
   )
 where
 
 import Data.HashMap.Strict qualified as HashMap
-import Juvix.Compiler.Concrete.Data.NameSignature.Base
 import Juvix.Compiler.Concrete.Data.NameSignature.Error
+import Juvix.Compiler.Concrete.Extra (symbolParsed)
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error
 import Juvix.Prelude
 
-data NameSignatureBuilder m a where
-  AddSymbol :: IsImplicit -> Symbol -> NameSignatureBuilder m ()
-  EndBuild :: NameSignatureBuilder m a
+data NameSignatureBuilder s m a where
+  AddSymbol :: IsImplicit -> Maybe (ArgDefault s) -> Symbol -> NameSignatureBuilder s m ()
+  EndBuild :: Proxy s -> NameSignatureBuilder s m a
   -- | for debugging
-  GetBuilder :: NameSignatureBuilder m BuilderState
+  GetBuilder :: NameSignatureBuilder s m (BuilderState s)
 
-data BuilderState = BuilderState
+data BuilderState (s :: Stage) = BuilderState
   { _stateCurrentImplicit :: Maybe IsImplicit,
     _stateNextIx :: Int,
     -- | maps to itself
     _stateSymbols :: HashMap Symbol Symbol,
-    _stateReverseClosedBlocks :: [NameBlock],
-    _stateCurrentBlock :: HashMap Symbol (Symbol, Int)
+    _stateReverseClosedBlocks :: [NameBlock s],
+    _stateCurrentBlock :: HashMap Symbol (NameItem s)
   }
 
 makeLenses ''BuilderState
 makeSem ''NameSignatureBuilder
 
-class HasNameSignature d where
-  addArgs :: (Members '[NameSignatureBuilder] r) => d -> Sem r ()
+class HasNameSignature (s :: Stage) d | d -> s where
+  addArgs :: (Members '[NameSignatureBuilder s] r) => d -> Sem r ()
 
-instance HasNameSignature (AxiomDef 'Parsed) where
-  addArgs :: (Members '[NameSignatureBuilder] r) => AxiomDef 'Parsed -> Sem r ()
-  addArgs a = addAtoms (a ^. axiomType)
+instance (SingI s) => HasNameSignature s (AxiomDef s) where
+  addArgs :: (Members '[NameSignatureBuilder s] r) => AxiomDef s -> Sem r ()
+  addArgs a = addExpressionType (a ^. axiomType)
 
-instance HasNameSignature (FunctionDef 'Parsed) where
+instance (SingI s) => HasNameSignature s (FunctionDef s) where
   addArgs a = do
     mapM_ addSigArg (a ^. signArgs)
-    whenJust (a ^. signRetType) addAtoms
+    whenJust (a ^. signRetType) addExpressionType
 
-instance HasNameSignature (InductiveDef 'Parsed, ConstructorDef 'Parsed) where
+instance (SingI s) => HasNameSignature s (InductiveDef s, ConstructorDef s) where
   addArgs ::
     forall r.
-    (Members '[NameSignatureBuilder] r) =>
-    (InductiveDef 'Parsed, ConstructorDef 'Parsed) ->
+    (Members '[NameSignatureBuilder s] r) =>
+    (InductiveDef s, ConstructorDef s) ->
     Sem r ()
   addArgs (i, c) = do
     mapM_ addConstructorParams (i ^. inductiveParameters)
     addRhs (c ^. constructorRhs)
     where
-      addRecord :: RhsRecord 'Parsed -> Sem r ()
+      addRecord :: RhsRecord s -> Sem r ()
       addRecord RhsRecord {..} = mapM_ addField _rhsRecordFields
         where
-          addField :: RecordField 'Parsed -> Sem r ()
-          addField RecordField {..} = addSymbol Explicit _fieldName
-      addRhs :: ConstructorRhs 'Parsed -> Sem r ()
+          addField :: RecordField s -> Sem r ()
+          addField RecordField {..} = addSymbol @s Explicit Nothing (symbolParsed _fieldName)
+      addRhs :: ConstructorRhs s -> Sem r ()
       addRhs = \case
-        ConstructorRhsGadt g -> addAtoms (g ^. rhsGadtType)
+        ConstructorRhsGadt g -> addExpressionType (g ^. rhsGadtType)
         ConstructorRhsRecord g -> addRecord g
         ConstructorRhsAdt {} -> return ()
 
-instance HasNameSignature (InductiveDef 'Parsed) where
+instance (SingI s) => HasNameSignature s (InductiveDef s) where
   addArgs a = do
     mapM_ addInductiveParams (a ^. inductiveParameters)
-    whenJust (a ^. inductiveType) addAtoms
+    whenJust (a ^. inductiveType) addExpressionType
 
 mkNameSignature ::
-  (Members '[Error ScoperError] r, HasNameSignature d) =>
+  forall s d r.
+  (SingI s, Members '[Error ScoperError] r, HasNameSignature s d) =>
   d ->
-  Sem r NameSignature
+  Sem r (NameSignature s)
 mkNameSignature d = do
   fmap (fromBuilderState . fromLeft impossible)
     . mapError ErrNameSignature
-    . runError @BuilderState
+    . runError @(BuilderState s)
     . evalState iniBuilderState
     . re
     $ do
       addArgs d
-      endBuild
+      endBuild (Proxy @s)
 
-iniBuilderState :: BuilderState
+iniBuilderState :: BuilderState s
 iniBuilderState =
   BuilderState
     { _stateCurrentImplicit = Nothing,
@@ -94,70 +96,87 @@ iniBuilderState =
       _stateCurrentBlock = mempty
     }
 
-fromBuilderState :: BuilderState -> NameSignature
+fromBuilderState :: forall s. BuilderState s -> NameSignature s
 fromBuilderState b =
   NameSignature
     { _nameSignatureArgs = reverse (addCurrent (b ^. stateReverseClosedBlocks))
     }
   where
-    addCurrent :: [NameBlock] -> [NameBlock]
+    addCurrent :: [NameBlock s] -> [NameBlock s]
     addCurrent
       | null (b ^. stateCurrentBlock) = id
-      | Just i <- b ^. stateCurrentImplicit = (NameBlock (b ^. stateCurrentBlock) i :)
+      | Just i <- b ^. stateCurrentImplicit =
+          (NameBlock (b ^. stateCurrentBlock) i :)
       | otherwise = id
 
-addAtoms :: forall r. (Members '[NameSignatureBuilder] r) => ExpressionAtoms 'Parsed -> Sem r ()
+addExpression :: forall r. (Members '[NameSignatureBuilder 'Scoped] r) => Expression -> Sem r ()
+addExpression = \case
+  ExpressionFunction f -> addFunction f
+  _ -> endBuild (Proxy @'Scoped)
+  where
+    addFunction :: Function 'Scoped -> Sem r ()
+    addFunction f = do
+      addFunctionParameters (f ^. funParameters)
+      addExpression (f ^. funReturn)
+
+addFunctionParameters :: forall s r. (SingI s, Members '[NameSignatureBuilder s] r) => FunctionParameters s -> Sem r ()
+addFunctionParameters FunctionParameters {..} = forM_ _paramNames addParameter
+  where
+    addParameter :: FunctionParameter s -> Sem r ()
+    addParameter = \case
+      FunctionParameterName p -> addSymbol @s _paramImplicit Nothing (symbolParsed p)
+      FunctionParameterWildcard {} -> endBuild (Proxy @s)
+
+addExpressionType :: forall s r. (SingI s, Members '[NameSignatureBuilder s] r) => ExpressionType s -> Sem r ()
+addExpressionType = case sing :: SStage s of
+  SParsed -> addAtoms
+  SScoped -> addExpression
+
+addAtoms :: forall r. (Members '[NameSignatureBuilder 'Parsed] r) => ExpressionAtoms 'Parsed -> Sem r ()
 addAtoms atoms = addAtom . (^. expressionAtoms . _head1) $ atoms
   where
     addAtom :: ExpressionAtom 'Parsed -> Sem r ()
     addAtom = \case
       AtomFunction f -> do
-        addParameters (f ^. funParameters)
+        addFunctionParameters (f ^. funParameters)
         addAtoms (f ^. funReturn)
-      _ -> endBuild
+      _ -> endBuild (Proxy @'Parsed)
 
-    addParameters :: FunctionParameters 'Parsed -> Sem r ()
-    addParameters FunctionParameters {..} = forM_ _paramNames addParameter
-      where
-        addParameter :: FunctionParameter 'Parsed -> Sem r ()
-        addParameter = \case
-          FunctionParameterName s -> addSymbol _paramImplicit s
-          FunctionParameterWildcard {} -> endBuild
+addInductiveParams' :: forall s r. (SingI s) => (Members '[NameSignatureBuilder s] r) => IsImplicit -> InductiveParameters s -> Sem r ()
+addInductiveParams' i a = forM_ (a ^. inductiveParametersNames) (addSymbol @s i Nothing . symbolParsed)
 
-addInductiveParams' :: (Members '[NameSignatureBuilder] r) => IsImplicit -> InductiveParameters 'Parsed -> Sem r ()
-addInductiveParams' i a = forM_ (a ^. inductiveParametersNames) (addSymbol i)
-
-addInductiveParams :: (Members '[NameSignatureBuilder] r) => InductiveParameters 'Parsed -> Sem r ()
+addInductiveParams :: (SingI s, Members '[NameSignatureBuilder s] r) => InductiveParameters s -> Sem r ()
 addInductiveParams = addInductiveParams' Explicit
 
-addConstructorParams :: (Members '[NameSignatureBuilder] r) => InductiveParameters 'Parsed -> Sem r ()
+addConstructorParams :: (SingI s, Members '[NameSignatureBuilder s] r) => InductiveParameters s -> Sem r ()
 addConstructorParams = addInductiveParams' Implicit
 
-addSigArg :: (Members '[NameSignatureBuilder] r) => SigArg 'Parsed -> Sem r ()
+addSigArg :: (SingI s, Members '[NameSignatureBuilder s] r) => SigArg s -> Sem r ()
 addSigArg a = forM_ (a ^. sigArgNames) $ \case
-  ArgumentSymbol s -> addSymbol (a ^. sigArgImplicit) s
+  ArgumentSymbol s -> addSymbol (a ^. sigArgImplicit) (a ^. sigArgDefault) (symbolParsed s)
   ArgumentWildcard {} -> return ()
 
-type Re r = State BuilderState ': Error BuilderState ': Error NameSignatureError ': r
+type Re s r = State (BuilderState s) ': Error (BuilderState s) ': Error NameSignatureError ': r
 
 re ::
-  forall r a.
-  Sem (NameSignatureBuilder ': r) a ->
-  Sem (Re r) a
+  forall s r a.
+  (SingI s) =>
+  Sem (NameSignatureBuilder s ': r) a ->
+  Sem (Re s r) a
 re = reinterpret3 $ \case
-  AddSymbol impl k -> addSymbol' impl k
-  EndBuild -> endBuild'
+  AddSymbol impl mdef k -> addSymbol' impl mdef k
+  EndBuild {} -> endBuild'
   GetBuilder -> get
 {-# INLINE re #-}
 
-addSymbol' :: forall r. IsImplicit -> Symbol -> Sem (Re r) ()
-addSymbol' impl sym = do
-  curImpl <- gets (^. stateCurrentImplicit)
+addSymbol' :: forall s r. (SingI s) => IsImplicit -> Maybe (ArgDefault s) -> Symbol -> Sem (Re s r) ()
+addSymbol' impl mdef sym = do
+  curImpl <- gets @(BuilderState s) (^. stateCurrentImplicit)
   if
       | Just impl == curImpl -> addToCurrentBlock
       | otherwise -> startNewBlock
   where
-    errDuplicateName :: Symbol -> Sem (Re r) ()
+    errDuplicateName :: Symbol -> Sem (Re s r) ()
     errDuplicateName _dupNameFirst =
       throw $
         ErrDuplicateName
@@ -166,31 +185,33 @@ addSymbol' impl sym = do
               ..
             }
 
-    addToCurrentBlock :: Sem (Re r) ()
+    addToCurrentBlock :: Sem (Re s r) ()
     addToCurrentBlock = do
-      idx <- (sym,) <$> gets (^. stateNextIx)
-      modify' (over stateNextIx succ)
-      whenJustM (gets (^. stateSymbols . at sym)) errDuplicateName
-      modify' (set (stateSymbols . at sym) (Just sym))
-      modify' (set (stateCurrentBlock . at sym) (Just idx))
+      idx <- gets @(BuilderState s) (^. stateNextIx)
+      let itm = NameItem sym idx mdef
+      modify' @(BuilderState s) (over stateNextIx succ)
+      whenJustM (gets @(BuilderState s) (^. stateSymbols . at sym)) errDuplicateName
+      modify' @(BuilderState s) (set (stateSymbols . at sym) (Just sym))
+      modify' @(BuilderState s) (set (stateCurrentBlock . at sym) (Just itm))
 
-    startNewBlock :: Sem (Re r) ()
+    startNewBlock :: Sem (Re s r) ()
     startNewBlock = do
-      curBlock <- gets (^. stateCurrentBlock)
-      mcurImpl <- gets (^. stateCurrentImplicit)
-      modify' (set stateCurrentImplicit (Just impl))
-      modify' (set stateCurrentBlock mempty)
-      modify' (set stateNextIx 0)
-      whenJust mcurImpl $ \curImpl -> modify' (over stateReverseClosedBlocks (NameBlock curBlock curImpl :))
-      addSymbol' impl sym
+      curBlock <- gets @(BuilderState s) (^. stateCurrentBlock)
+      mcurImpl <- gets @(BuilderState s) (^. stateCurrentImplicit)
+      modify' @(BuilderState s) (set stateCurrentImplicit (Just impl))
+      modify' @(BuilderState s) (set stateCurrentBlock mempty)
+      modify' @(BuilderState s) (set stateNextIx 0)
+      whenJust mcurImpl $ \curImpl ->
+        modify' (over stateReverseClosedBlocks (NameBlock curBlock curImpl :))
+      addSymbol' impl mdef sym
 
-endBuild' :: Sem (Re r) a
-endBuild' = get @BuilderState >>= throw
+endBuild' :: forall s r a. Sem (Re s r) a
+endBuild' = get @(BuilderState s) >>= throw
 
 mkRecordNameSignature :: RhsRecord 'Parsed -> RecordNameSignature
 mkRecordNameSignature rhs =
   RecordNameSignature
     ( HashMap.fromList
-        [ (s, (s, idx)) | (Indexed idx field) <- indexFrom 0 (toList (rhs ^. rhsRecordFields)), let s = field ^. fieldName
+        [ (s, NameItem s idx Nothing) | (Indexed idx field) <- indexFrom 0 (toList (rhs ^. rhsRecordFields)), let s = field ^. fieldName
         ]
     )
diff --git a/src/Juvix/Compiler/Concrete/Data/Scope/Base.hs b/src/Juvix/Compiler/Concrete/Data/Scope/Base.hs
index 670475858..7d3aca08a 100644
--- a/src/Juvix/Compiler/Concrete/Data/Scope/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Data/Scope/Base.hs
@@ -1,6 +1,5 @@
 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
@@ -60,7 +59,8 @@ data ScoperState = ScoperState
     _scoperModules :: HashMap S.ModuleNameId (ModuleRef' 'S.NotConcrete),
     _scoperScope :: HashMap TopModulePath Scope,
     _scoperAlias :: HashMap S.NameId PreSymbolEntry,
-    _scoperSignatures :: HashMap S.NameId NameSignature,
+    _scoperSignatures :: HashMap S.NameId (NameSignature 'Parsed),
+    _scoperScopedSignatures :: HashMap S.NameId (NameSignature 'Scoped),
     -- | Indexed by the inductive type. This is used for record updates
     _scoperRecordFields :: HashMap S.NameId RecordInfo,
     -- | Indexed by constructor. This is used for record patterns
diff --git a/src/Juvix/Compiler/Concrete/Extra.hs b/src/Juvix/Compiler/Concrete/Extra.hs
index e28de814d..6eebeb6a9 100644
--- a/src/Juvix/Compiler/Concrete/Extra.hs
+++ b/src/Juvix/Compiler/Concrete/Extra.hs
@@ -10,13 +10,13 @@ module Juvix.Compiler.Concrete.Extra
     getExpressionAtomIden,
     getPatternAtomIden,
     isBodyExpression,
+    symbolParsed,
   )
 where
 
 import Data.HashMap.Strict qualified as HashMap
 import Data.IntMap.Strict qualified as IntMap
 import Data.List.NonEmpty qualified as NonEmpty
-import Juvix.Compiler.Concrete.Data.NameSignature.Base
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Language
 import Juvix.Prelude hiding (some)
@@ -117,11 +117,6 @@ groupStatements = \case
       StatementFunctionDef d -> n == symbolParsed (d ^. signName)
       _ -> False
       where
-        symbolParsed :: SymbolType s -> Symbol
-        symbolParsed sym = case sing :: SStage s of
-          SParsed -> sym
-          SScoped -> sym ^. S.nameConcrete
-
         syms :: InductiveDef s -> [Symbol]
         syms InductiveDef {..} =
           let constructors = toList _inductiveConstructors
@@ -132,13 +127,21 @@ groupStatements = \case
                     ^. S.nameConcrete
                     : map (^. constructorName . S.nameConcrete) constructors
 
+symbolParsed :: forall s. (SingI s) => SymbolType s -> Symbol
+symbolParsed sym = case sing :: SStage s of
+  SParsed -> sym
+  SScoped -> sym ^. S.nameConcrete
+
 flattenStatement :: Statement s -> [Statement s]
 flattenStatement = \case
   StatementModule m -> concatMap flattenStatement (m ^. moduleBody)
   s -> [s]
 
 recordNameSignatureByIndex :: RecordNameSignature -> IntMap Symbol
-recordNameSignatureByIndex = IntMap.fromList . (^.. recordNames . each . to swap)
+recordNameSignatureByIndex = IntMap.fromList . (^.. recordNames . each . to mkAssoc)
+  where
+    mkAssoc :: NameItem s -> (Int, Symbol)
+    mkAssoc NameItem {..} = (_nameItemIndex, _nameItemSymbol)
 
 getExpressionAtomIden :: ExpressionAtom 'Scoped -> Maybe S.Name
 getExpressionAtomIden = \case
diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs
index f0f14b99c..01265680e 100644
--- a/src/Juvix/Compiler/Concrete/Language.hs
+++ b/src/Juvix/Compiler/Concrete/Language.hs
@@ -24,7 +24,6 @@ import Juvix.Compiler.Concrete.Data.Literal
 import Juvix.Compiler.Concrete.Data.ModuleIsTop
 import Juvix.Compiler.Concrete.Data.Name
 import Juvix.Compiler.Concrete.Data.NameRef
-import Juvix.Compiler.Concrete.Data.NameSignature.Base
 import Juvix.Compiler.Concrete.Data.NameSpace
 import Juvix.Compiler.Concrete.Data.PublicAnn
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
@@ -123,7 +122,7 @@ type family RecordNameSignatureType s = res | res -> s where
 type NameSignatureType :: Stage -> GHC.Type
 type family NameSignatureType s = res | res -> s where
   NameSignatureType 'Parsed = ()
-  NameSignatureType 'Scoped = NameSignature
+  NameSignatureType 'Scoped = NameSignature 'Scoped
 
 type ModulePathType :: Stage -> ModuleIsTop -> GHC.Type
 type family ModulePathType s t = res | res -> t s where
@@ -149,6 +148,28 @@ type family ModuleEndType t = res | res -> t where
 -- choices on the user.
 type ParsedPragmas = WithLoc (WithSource Pragmas)
 
+data NameItem (s :: Stage) = NameItem
+  { _nameItemSymbol :: Symbol,
+    _nameItemIndex :: Int,
+    _nameItemDefault :: Maybe (ArgDefault s)
+  }
+
+data NameBlock (s :: Stage) = NameBlock
+  { -- | Symbols map to themselves so we can retrive the location
+    -- | NOTE the index is wrt to the block, not the whole signature.
+    _nameBlock :: HashMap Symbol (NameItem s),
+    _nameImplicit :: IsImplicit
+  }
+
+-- | Two consecutive blocks should have different implicitness
+newtype NameSignature (s :: Stage) = NameSignature
+  { _nameSignatureArgs :: [NameBlock s]
+  }
+
+newtype RecordNameSignature = RecordNameSignature
+  { _recordNames :: HashMap Symbol (NameItem 'Parsed)
+  }
+
 data Argument (s :: Stage)
   = ArgumentSymbol (SymbolType s)
   | ArgumentWildcard Wildcard
@@ -386,6 +407,23 @@ data IteratorSyntaxDef = IteratorSyntaxDef
 instance HasLoc IteratorSyntaxDef where
   getLoc IteratorSyntaxDef {..} = getLoc _iterSyntaxKw <> getLoc _iterSymbol
 
+data ArgDefault (s :: Stage) = ArgDefault
+  { _argDefaultAssign :: Irrelevant KeywordRef,
+    _argDefaultValue :: ExpressionType s
+  }
+
+deriving stock instance Show (ArgDefault 'Parsed)
+
+deriving stock instance Show (ArgDefault 'Scoped)
+
+deriving stock instance Eq (ArgDefault 'Parsed)
+
+deriving stock instance Eq (ArgDefault 'Scoped)
+
+deriving stock instance Ord (ArgDefault 'Parsed)
+
+deriving stock instance Ord (ArgDefault 'Scoped)
+
 data SigArg (s :: Stage) = SigArg
   { _sigArgDelims :: Irrelevant (KeywordRef, KeywordRef),
     _sigArgImplicit :: IsImplicit,
@@ -394,7 +432,8 @@ data SigArg (s :: Stage) = SigArg
     _sigArgColon :: Maybe (Irrelevant KeywordRef),
     -- | The type is only optional for implicit arguments. Omitting the rhs is
     -- equivalent to writing `: Type`.
-    _sigArgType :: Maybe (ExpressionType s)
+    _sigArgType :: Maybe (ExpressionType s),
+    _sigArgDefault :: Maybe (ArgDefault s)
   }
 
 deriving stock instance Show (SigArg 'Parsed)
@@ -1541,14 +1580,12 @@ data RecordUpdateExtra = RecordUpdateExtra
     _recordUpdateExtraVars :: [S.Symbol],
     _recordUpdateExtraSignature :: RecordNameSignature
   }
-  deriving stock (Show)
 
 data RecordCreationExtra = RecordCreationExtra
   { -- | Implicitly bound fields sorted by index
     _recordCreationExtraVars :: [S.Symbol],
     _recordCreationExtraSignature :: RecordNameSignature
   }
-  deriving stock (Show)
 
 newtype ParensRecordUpdate = ParensRecordUpdate
   { _parensRecordUpdate :: RecordUpdate 'Scoped
@@ -1583,8 +1620,7 @@ data RecordUpdateApp = RecordUpdateApp
 
 data NamedApplication (s :: Stage) = NamedApplication
   { _namedAppName :: IdentifierType s,
-    _namedAppArgs :: NonEmpty (ArgumentBlock s),
-    _namedAppSignature :: Irrelevant (NameSignatureType s)
+    _namedAppArgs :: NonEmpty (ArgumentBlock s)
   }
 
 deriving stock instance Show (NamedApplication 'Parsed)
@@ -1842,6 +1878,7 @@ makeLenses ''IteratorSyntaxDef
 makeLenses ''ConstructorDef
 makeLenses ''Module
 makeLenses ''SigArg
+makeLenses ''ArgDefault
 makeLenses ''FunctionDef
 makeLenses ''AxiomDef
 makeLenses ''ExportInfo
@@ -1872,6 +1909,10 @@ makeLenses ''AliasDef
 makeLenses ''FixitySyntaxDef
 makeLenses ''ParsedFixityInfo
 makeLenses ''ParsedFixityFields
+makeLenses ''NameSignature
+makeLenses ''RecordNameSignature
+makeLenses ''NameBlock
+makeLenses ''NameItem
 
 fixityFieldHelper :: SimpleGetter (ParsedFixityFields s) (Maybe a) -> SimpleGetter (ParsedFixityInfo s) (Maybe a)
 fixityFieldHelper l = to (^? fixityFields . _Just . l . _Just)
@@ -2172,6 +2213,9 @@ getLocExpressionType = case sing :: SStage s of
   SParsed -> getLoc
   SScoped -> getLoc
 
+instance (SingI s) => HasLoc (ArgDefault s) where
+  getLoc ArgDefault {..} = getLoc _argDefaultAssign <> getLocExpressionType _argDefaultValue
+
 instance HasLoc (SigArg s) where
   getLoc SigArg {..} = getLoc l <> getLoc r
     where
diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
index 7b07b5bc4..0466af8a0 100644
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Print/Base.hs
@@ -10,7 +10,6 @@ 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 qualified as Concrete
@@ -56,15 +55,14 @@ docNoComments :: (PrettyPrint c) => Options -> c -> Doc Ann
 docNoComments = docHelper Nothing
 
 docHelper :: (PrettyPrint c) => Maybe FileComments -> Options -> c -> Doc Ann
-docHelper cs opts x =
+docHelper cs opts =
   run
     . execExactPrint cs
     . runReader opts
     . ppCode
-    $ x
 
 docNoLoc :: (PrettyPrint c) => Options -> c -> Doc Ann
-docNoLoc opts x = docHelper Nothing opts x
+docNoLoc = docHelper Nothing
 
 doc :: (PrettyPrint c, HasLoc c) => Options -> Comments -> c -> Doc Ann
 doc opts cs x = docHelper (Just (fileComments file cs)) opts x
@@ -167,21 +165,27 @@ instance (SingI s) => PrettyPrint (ListPattern s) where
 instance PrettyPrint Void where
   ppCode = absurd
 
-instance PrettyPrint NameBlock where
-  ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => NameBlock -> Sem r ()
+instance (SingI s) => PrettyPrint (NameItem s) where
+  ppCode NameItem {..} = do
+    let defaultVal = do
+          d <- _nameItemDefault
+          return (noLoc C.kwAssign <+> ppExpressionType (d ^. argDefaultValue))
+    ppCode _nameItemSymbol <> ppCode Kw.kwExclamation <> noLoc (pretty _nameItemIndex)
+      <+?> defaultVal
+
+instance (SingI s) => PrettyPrint (NameBlock s) where
+  ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => NameBlock s -> Sem r ()
   ppCode NameBlock {..} = do
     let delims = case _nameImplicit of
           Implicit -> braces
           ImplicitInstance -> doubleBraces
           Explicit -> parens
-        ppElem :: (Symbol, Int) -> Sem r ()
-        ppElem (sym, idx) = ppCode sym <> ppCode Kw.kwExclamation <> noLoc (pretty idx)
-    delims (hsepSemicolon (map ppElem (toList _nameBlock)))
+    delims (hsepSemicolon (map ppCode (toList _nameBlock)))
 
 instance (PrettyPrint a, PrettyPrint b) => PrettyPrint (a, b) where
   ppCode (a, b) = tuple [ppCode a, ppCode b]
 
-instance PrettyPrint NameSignature where
+instance (SingI s) => PrettyPrint (NameSignature s) where
   ppCode NameSignature {..}
     | null _nameSignatureArgs = noLoc (pretty @Text "<empty name signature>")
     | otherwise = hsep . map ppCode $ _nameSignatureArgs
@@ -910,6 +914,10 @@ instance (SingI s) => PrettyPrint (Argument s) where
     ArgumentSymbol s -> ppSymbolType s
     ArgumentWildcard w -> ppCode w
 
+instance (SingI s) => PrettyPrint (ArgDefault s) where
+  ppCode ArgDefault {..} = do
+    ppCode _argDefaultAssign <+> ppExpressionType _argDefaultValue
+
 instance (SingI s) => PrettyPrint (SigArg s) where
   ppCode :: (Members '[ExactPrint, Reader Options] r) => SigArg s -> Sem r ()
   ppCode SigArg {..} = do
@@ -918,9 +926,11 @@ instance (SingI s) => PrettyPrint (SigArg s) where
         colon' = ppCode <$> _sigArgColon
         ty = ppExpressionType <$> _sigArgType
         arg = case _sigArgImplicit of
-          ImplicitInstance | isNothing colon' -> mempty <>? ty
+          ImplicitInstance
+            | isNothing colon' -> mempty <>? ty
           _ -> names' <+?> colon' <+?> ty
-    ppCode l <> arg <> ppCode r
+        defaultVal = ppCode <$> _sigArgDefault
+    ppCode l <> arg <+?> defaultVal <> ppCode r
 
 ppFunctionSignature :: (SingI s) => PrettyPrinting (FunctionDef s)
 ppFunctionSignature FunctionDef {..} = do
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
index 8a479cc70..2d4915aef 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@@ -38,6 +38,7 @@ iniScoperState =
       _scoperModules = mempty,
       _scoperScope = mempty,
       _scoperSignatures = mempty,
+      _scoperScopedSignatures = mempty,
       _scoperRecordFields = mempty,
       _scoperAlias = mempty,
       _scoperConstructorFields = mempty
@@ -186,7 +187,7 @@ freshSymbol _nameKind _nameConcrete = do
 reserveSymbolSignatureOf ::
   forall (k :: NameKind) r d.
   ( Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder] r,
-    HasNameSignature d,
+    HasNameSignature 'Parsed d,
     SingI (NameKindNameSpace k)
   ) =>
   Sing k ->
@@ -197,6 +198,13 @@ reserveSymbolSignatureOf k d s = do
   sig <- mkNameSignature d
   reserveSymbolOf k (Just sig) s
 
+registerDefaultArgs ::
+  (Members '[State ScoperState, Error ScoperError] r, HasNameSignature 'Scoped d) =>
+  S.NameId ->
+  d ->
+  Sem r ()
+registerDefaultArgs uid = mkNameSignature >=> modify . (set (scoperScopedSignatures . at uid)) . Just
+
 reserveSymbolOf ::
   forall (nameKind :: NameKind) (ns :: NameSpace) r.
   ( Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder] r,
@@ -204,7 +212,7 @@ reserveSymbolOf ::
     SingI ns
   ) =>
   Sing nameKind ->
-  Maybe NameSignature ->
+  Maybe (NameSignature 'Parsed) ->
   Symbol ->
   Sem r S.Symbol
 reserveSymbolOf k nameSig s = do
@@ -798,32 +806,46 @@ checkFunctionDef ::
   Sem r (FunctionDef 'Scoped)
 checkFunctionDef FunctionDef {..} = do
   sigName' <- bindFunctionSymbol _signName
+  topScope <- get
   sigDoc' <- mapM checkJudoc _signDoc
   (args', sigType', sigBody') <- withLocalScope $ do
-    a' <- mapM checkArg _signArgs
+    a' <- mapM (checkArg topScope) _signArgs
     t' <- mapM checkParseExpressionAtoms _signRetType
     b' <- checkBody
     return (a', t', b')
-  registerFunctionDef
-    @$> FunctionDef
-      { _signName = sigName',
-        _signRetType = sigType',
-        _signDoc = sigDoc',
-        _signBody = sigBody',
-        _signArgs = args',
-        ..
-      }
+  let def =
+        FunctionDef
+          { _signName = sigName',
+            _signRetType = sigType',
+            _signDoc = sigDoc',
+            _signBody = sigBody',
+            _signArgs = args',
+            ..
+          }
+  registerDefaultArgs (sigName' ^. S.nameId) def
+  registerFunctionDef @$> def
   where
-    checkArg :: SigArg 'Parsed -> Sem r (SigArg 'Scoped)
-    checkArg SigArg {..} = do
+    checkArg :: Scope -> SigArg 'Parsed -> Sem r (SigArg 'Scoped)
+    checkArg topScope arg@SigArg {..} = do
       names' <- forM _sigArgNames $ \case
         ArgumentSymbol s -> ArgumentSymbol <$> bindVariableSymbol s
         ArgumentWildcard w -> return $ ArgumentWildcard w
       ty' <- mapM checkParseExpressionAtoms _sigArgType
+      default' <- case _sigArgDefault of
+        Nothing -> return Nothing
+        Just ArgDefault {..} ->
+          let err = throw (ErrWrongDefaultValue WrongDefaultValue {_wrongDefaultValue = arg})
+           in case _sigArgImplicit of
+                Explicit -> err
+                ImplicitInstance -> err
+                Implicit -> do
+                  val' <- withScope topScope (checkParseExpressionAtoms _argDefaultValue)
+                  return (Just ArgDefault {_argDefaultValue = val', ..})
       return
         SigArg
           { _sigArgNames = names',
             _sigArgType = ty',
+            _sigArgDefault = default',
             ..
           }
     checkBody :: Sem r (FunctionDefBody 'Scoped)
@@ -881,20 +903,24 @@ checkInductiveDef InductiveDef {..} = do
             | (cname, cdef) <- zipExact (toList constructorNames') (toList _inductiveConstructors)
           ]
     return (inductiveParameters', inductiveType', inductiveDoc', inductiveConstructors')
-  registerInductive
-    @$> InductiveDef
-      { _inductiveName = inductiveName',
-        _inductiveDoc = inductiveDoc',
-        _inductivePragmas = _inductivePragmas,
-        _inductiveParameters = inductiveParameters',
-        _inductiveType = inductiveType',
-        _inductiveConstructors = inductiveConstructors',
-        _inductiveBuiltin,
-        _inductivePositive,
-        _inductiveTrait,
-        _inductiveAssignKw,
-        _inductiveKw
-      }
+  let indDef =
+        InductiveDef
+          { _inductiveName = inductiveName',
+            _inductiveDoc = inductiveDoc',
+            _inductivePragmas = _inductivePragmas,
+            _inductiveParameters = inductiveParameters',
+            _inductiveType = inductiveType',
+            _inductiveConstructors = inductiveConstructors',
+            _inductiveBuiltin,
+            _inductivePositive,
+            _inductiveTrait,
+            _inductiveAssignKw,
+            _inductiveKw
+          }
+  registerDefaultArgs (inductiveName' ^. S.nameId) indDef
+  forM_ inductiveConstructors' $ \c ->
+    registerDefaultArgs (c ^. constructorName . S.nameId) (indDef, c)
+  registerInductive @$> indDef
   where
     -- note that the constructor name is not bound here
     checkConstructorDef :: S.Symbol -> S.Symbol -> ConstructorDef 'Parsed -> Sem r (ConstructorDef 'Scoped)
@@ -1051,6 +1077,14 @@ withTopScope ma = do
   put scope'
   ma
 
+withScope :: (Members '[State Scope] r) => Scope -> Sem r a -> Sem r a
+withScope scope ma = do
+  before <- get @Scope
+  put scope
+  x <- ma
+  put before
+  return x
+
 withLocalScope :: (Members '[State Scope] r) => Sem r a -> Sem r a
 withLocalScope ma = do
   before <- get @Scope
@@ -1631,7 +1665,9 @@ checkAxiomDef AxiomDef {..} = do
   axiomType' <- withLocalScope (checkParseExpressionAtoms _axiomType)
   axiomName' <- bindAxiomSymbol _axiomName
   axiomDoc' <- withLocalScope (mapM checkJudoc _axiomDoc)
-  registerAxiom @$> AxiomDef {_axiomName = axiomName', _axiomType = axiomType', _axiomDoc = axiomDoc', ..}
+  let a = AxiomDef {_axiomName = axiomName', _axiomType = axiomType', _axiomDoc = axiomDoc', ..}
+  registerDefaultArgs (a ^. axiomName . S.nameId) a
+  registerAxiom @$> a
 
 entryToSymbol :: forall (ns :: NameSpace). (SingI ns) => NameSpaceEntryType ns -> Symbol -> S.Symbol
 entryToSymbol sentry csym = set S.nameConcrete csym (sentry ^. nsEntry)
@@ -1735,7 +1771,7 @@ checkRecordPattern r = do
       RecordPatternItemFieldPun a -> RecordPatternItemFieldPun <$> checkPun a
       where
         findField :: Symbol -> Sem r' Int
-        findField f = fromMaybeM (throw err) (asks (^? recordNames . at f . _Just . _2))
+        findField f = fromMaybeM (throw err) (asks (^? recordNames . at f . _Just . nameItemIndex))
           where
             err :: ScoperError
             err = ErrUnexpectedField (UnexpectedField f)
@@ -2171,7 +2207,7 @@ checkUpdateField ::
   Sem r (RecordUpdateField 'Scoped)
 checkUpdateField sig f = do
   value' <- checkParseExpressionAtoms (f ^. fieldUpdateValue)
-  idx' <- maybe (throw unexpectedField) return (sig ^? recordNames . at (f ^. fieldUpdateName) . _Just . _2)
+  idx' <- maybe (throw unexpectedField) return (sig ^? recordNames . at (f ^. fieldUpdateName) . _Just . nameItemIndex)
   return
     RecordUpdateField
       { _fieldUpdateName = f ^. fieldUpdateName,
@@ -2200,6 +2236,7 @@ checkNamedApplication napp = do
           _namedArgAssignKw = n ^. namedArgAssignKw
       _namedArgValue <- checkParseExpressionAtoms (n ^. namedArgValue)
       return NamedArgument {..}
+
     checkArgumentBlock :: ArgumentBlock 'Parsed -> Sem r (ArgumentBlock 'Scoped)
     checkArgumentBlock b = do
       let _argBlockDelims = b ^. argBlockDelims
@@ -2227,7 +2264,7 @@ getRecordInfo' loc name nameId =
     err :: Sem r a
     err = throw (ErrNotARecord (NotARecord name loc))
 
-getNameSignature :: (Members '[State ScoperState, Error ScoperError] r) => ScopedIden -> Sem r NameSignature
+getNameSignature :: (Members '[State ScoperState, Error ScoperError] r) => ScopedIden -> Sem r (NameSignature 'Parsed)
 getNameSignature s = do
   sig <- maybeM (throw err) return (lookupNameSignature (s ^. scopedIdenFinal . S.nameId))
   when (null (sig ^. nameSignatureArgs)) (throw err)
@@ -2235,7 +2272,7 @@ getNameSignature s = do
   where
     err = ErrNoNameSignature (NoNameSignature s)
 
-lookupNameSignature :: (Members '[State ScoperState] r) => S.NameId -> Sem r (Maybe NameSignature)
+lookupNameSignature :: (Members '[State ScoperState] r) => S.NameId -> Sem r (Maybe (NameSignature 'Parsed))
 lookupNameSignature s = gets (^. scoperSignatures . at s)
 
 checkIterator ::
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs
index 0e30a8e5f..755dad5f8 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs
@@ -50,6 +50,7 @@ data ScoperError
   | ErrIncomparablePrecedences IncomaprablePrecedences
   | ErrAliasCycle AliasCycle
   | ErrInvalidRangeNumber InvalidRangeNumber
+  | ErrWrongDefaultValue WrongDefaultValue
   | ErrUnsupported Unsupported
 
 instance ToGenericError ScoperError where
@@ -92,4 +93,5 @@ instance ToGenericError ScoperError where
     ErrIncomparablePrecedences e -> genericError e
     ErrAliasCycle e -> genericError e
     ErrInvalidRangeNumber e -> genericError e
+    ErrWrongDefaultValue e -> genericError e
     ErrUnsupported e -> genericError e
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs
index 9711e9f39..f1e010456 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs
@@ -910,7 +910,7 @@ instance ToGenericError IncomaprablePrecedences where
       i = getLoc _incomparablePrecedencesName1
 
 newtype AliasCycle = AliasCycle
-  { _aliasCycleDef :: (AliasDef 'Parsed)
+  { _aliasCycleDef :: AliasDef 'Parsed
   }
   deriving stock (Show)
 
@@ -931,6 +931,28 @@ instance ToGenericError AliasCycle where
       i :: Interval
       i = getLoc _aliasCycleDef
 
+newtype WrongDefaultValue = WrongDefaultValue
+  { _wrongDefaultValue :: SigArg 'Parsed
+  }
+  deriving stock (Show)
+
+instance ToGenericError WrongDefaultValue where
+  genericError WrongDefaultValue {..} = do
+    opts <- fromGenericOptions <$> ask
+    let msg =
+          "Invalid argument "
+            <+> ppCode opts _wrongDefaultValue
+            <+> ".\nOnly implicit arguments can have default values."
+    return
+      GenericError
+        { _genericErrorLoc = i,
+          _genericErrorMessage = mkAnsiText msg,
+          _genericErrorIntervals = [i]
+        }
+    where
+      i :: Interval
+      i = getLoc _wrongDefaultValue
+
 data Unsupported = Unsupported
   { _unsupportedMsg :: Text,
     _unsupportedLoc :: Interval
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
index 3e87e9b92..d8913259c 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@@ -327,10 +327,9 @@ parseYaml l r = do
   void (P.chunk l)
   off <- P.getOffset
   str <- P.manyTill P.anySingle (P.chunk r)
-  let str' =
-        if
-            | elem '\n' str -> str
-            | otherwise -> '{' : str ++ "}"
+  let str'
+        | elem '\n' str = str
+        | otherwise = '{' : str ++ "}"
   space
   let bs = BS.fromString str'
   case decodeEither bs of
@@ -1098,6 +1097,10 @@ functionDefinition allowOmitType allowInstance _signBuiltin = P.label "<function
               return Nothing
         _ ->
           Just <$> parseExpressionAtoms
+      _sigArgDefault <- optional $ do
+        _argDefaultAssign <- Irrelevant <$> kw kwAssign
+        _argDefaultValue <- parseExpressionAtoms
+        return ArgDefault {..}
       closeDelim <- implicitClose _sigArgImplicit
       let _sigArgDelims = Irrelevant (openDelim, closeDelim)
       return SigArg {..}
diff --git a/src/Juvix/Compiler/Internal/Extra.hs b/src/Juvix/Compiler/Internal/Extra.hs
index f0ac2101a..0b45331ed 100644
--- a/src/Juvix/Compiler/Internal/Extra.hs
+++ b/src/Juvix/Compiler/Internal/Extra.hs
@@ -93,6 +93,7 @@ genFieldProjection _funDefName info fieldIx = do
         _funDefTerminating = False,
         _funDefInstance = False,
         _funDefBuiltin = Nothing,
+        _funDefDefaultSignature = mempty,
         _funDefPragmas = mempty {_pragmasInline = Just InlineAlways},
         _funDefBody = body',
         _funDefType = foldFunType (inductiveArgs ++ [saturatedTy]) retTy,
diff --git a/src/Juvix/Compiler/Internal/Extra/Base.hs b/src/Juvix/Compiler/Internal/Extra/Base.hs
index 26afe0f0a..f3722c2fa 100644
--- a/src/Juvix/Compiler/Internal/Extra/Base.hs
+++ b/src/Juvix/Compiler/Internal/Extra/Base.hs
@@ -162,16 +162,22 @@ subsHoles s = over leafExpressions helper
 instance HasExpressions Example where
   leafExpressions f = traverseOf exampleExpression (leafExpressions f)
 
+instance HasExpressions DefaultSignature where
+  leafExpressions f (DefaultSignature a) =
+    DefaultSignature <$> traverse (traverse (leafExpressions f)) a
+
 instance HasExpressions FunctionDef where
   leafExpressions f FunctionDef {..} = do
     body' <- leafExpressions f _funDefBody
     ty' <- leafExpressions f _funDefType
     examples' <- traverse (leafExpressions f) _funDefExamples
+    defaults' <- leafExpressions f _funDefDefaultSignature
     pure
       FunctionDef
         { _funDefBody = body',
           _funDefType = ty',
           _funDefExamples = examples',
+          _funDefDefaultSignature = defaults',
           _funDefTerminating,
           _funDefInstance,
           _funDefName,
@@ -568,6 +574,14 @@ freshVar _nameLoc n = do
         _nameLoc
       }
 
+genWildcard :: forall r'. (Members '[NameIdGen] r') => Interval -> IsImplicit -> Sem r' PatternArg
+genWildcard loc impl = do
+  var <- varFromWildcard (Wildcard loc)
+  return (PatternArg impl Nothing (PatternVariable var))
+
+freshWildcard :: (Members '[NameIdGen] r) => Interval -> Sem r Hole
+freshWildcard l = mkHole l <$> freshNameId
+
 freshHole :: (Members '[NameIdGen] r) => Interval -> Sem r Hole
 freshHole l = mkHole l <$> freshNameId
 
diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs
index a605dfa35..5a3ee1676 100644
--- a/src/Juvix/Compiler/Internal/Language.hs
+++ b/src/Juvix/Compiler/Internal/Language.hs
@@ -86,6 +86,7 @@ data FunctionDef = FunctionDef
     _funDefTerminating :: Bool,
     _funDefInstance :: Bool,
     _funDefBuiltin :: Maybe BuiltinFunction,
+    _funDefDefaultSignature :: DefaultSignature,
     _funDefPragmas :: Pragmas
   }
   deriving stock (Eq, Generic, Data)
@@ -290,6 +291,14 @@ data ConstructorDef = ConstructorDef
   }
   deriving stock (Data)
 
+newtype DefaultSignature = DefaultSignature
+  { _defaultSignature :: [Maybe Expression]
+  }
+  deriving stock (Eq, Generic, Data)
+  deriving newtype (Monoid, Semigroup)
+
+instance Hashable DefaultSignature
+
 data FunctionParameter = FunctionParameter
   { _paramName :: Maybe VarName,
     _paramImplicit :: IsImplicit,
@@ -313,6 +322,7 @@ newtype ModuleIndex = ModuleIndex
   deriving stock (Data)
 
 makeLenses ''ModuleIndex
+makeLenses ''DefaultSignature
 makeLenses ''WildcardConstructor
 makeLenses ''Case
 makeLenses ''CaseBranch
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index ce5247a12..eb6ba071f 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -13,7 +13,7 @@ import Data.HashMap.Strict qualified as HashMap
 import Data.IntMap.Strict qualified as IntMap
 import Data.List.NonEmpty qualified as NonEmpty
 import Juvix.Compiler.Builtins
-import Juvix.Compiler.Concrete.Data.NameSignature.Base
+import Juvix.Compiler.Concrete.Data.Scope.Base (ScoperState, scoperScopedSignatures)
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Extra qualified as Concrete
 import Juvix.Compiler.Concrete.Gen qualified as Gen
@@ -48,6 +48,7 @@ fromConcrete _resultScoper =
       runReader @Pragmas mempty
         . runReader @ExportsTable exportTbl
         . evalState @ConstructorInfos mempty
+        . runReader namesSigs
         . runCacheEmpty goModuleNoCache
         $ mapM goTopModule ms
     let _resultTable = buildTable _resultModules
@@ -57,6 +58,7 @@ fromConcrete _resultScoper =
   where
     ms = _resultScoper ^. Scoper.resultModules
     exportTbl = _resultScoper ^. Scoper.resultExports
+    namesSigs = _resultScoper ^. Scoper.resultScoperState . scoperScopedSignatures
 
 -- | `StatementInclude`s are not included in the result
 buildMutualBlocks ::
@@ -133,11 +135,13 @@ buildLetMutualBlocks ss = nonEmpty' . mapMaybe nameToPreStatement $ scomponents
           AcyclicSCC a -> AcyclicSCC <$> a
           CyclicSCC p -> CyclicSCC . toList <$> nonEmpty (catMaybes p)
 
-fromConcreteExpression :: (Members '[Builtins, Error JuvixError, NameIdGen, Termination] r) => Scoper.Expression -> Sem r Internal.Expression
+fromConcreteExpression :: (Members '[Builtins, Error JuvixError, NameIdGen, Termination, State ScoperState] r) => Scoper.Expression -> Sem r Internal.Expression
 fromConcreteExpression e = do
+  nameSigs <- gets (^. scoperScopedSignatures)
   e' <-
     mapError (JuvixError @ScoperError)
       . runReader @Pragmas mempty
+      . runReader nameSigs
       . goExpression
       $ e
   checkTerminationShallow e'
@@ -157,7 +161,7 @@ fromConcreteImport i = do
   return i'
 
 goLocalModule ::
-  (Members '[Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ConstructorInfos] r) =>
+  (Members '[Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ConstructorInfos, Reader NameSignatures] r) =>
   Module 'Scoped 'ModuleLocal ->
   Sem r [Internal.PreStatement]
 goLocalModule = concatMapM goAxiomInductive . (^. moduleBody)
@@ -169,7 +173,7 @@ goTopModule ::
 goTopModule = cacheGet . ModuleIndex
 
 goModuleNoCache ::
-  (Members '[Reader EntryPoint, Reader ExportsTable, Error JuvixError, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache, State ConstructorInfos, Termination] r) =>
+  (Members '[Reader EntryPoint, Reader ExportsTable, Error JuvixError, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache, State ConstructorInfos, Termination, Reader NameSignatures] r) =>
   ModuleIndex ->
   Sem r Internal.Module
 goModuleNoCache (ModuleIndex m) = do
@@ -220,7 +224,7 @@ traverseM' f x = sequence <$> traverse f x
 
 toPreModule ::
   forall r t.
-  (SingI t, Members '[Reader ExportsTable, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache, State ConstructorInfos] r) =>
+  (SingI t, Members '[Reader ExportsTable, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache, State ConstructorInfos, Reader NameSignatures] r) =>
   Module 'Scoped t ->
   Sem r Internal.PreModule
 toPreModule Module {..} = do
@@ -285,7 +289,7 @@ fromPreModuleBody b = do
 
 goModuleBody ::
   forall r.
-  (Members '[Reader ExportsTable, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache, State ConstructorInfos] r) =>
+  (Members '[Reader ExportsTable, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache, State ConstructorInfos, Reader NameSignatures] r) =>
   [Statement 'Scoped] ->
   Sem r Internal.PreModuleBody
 goModuleBody stmts = do
@@ -316,11 +320,11 @@ goModuleBody stmts = do
       sequence
         [ Indexed i <$> funDef
           | Indexed i (StatementFunctionDef f) <- ss,
-            let funDef = goTopFunctionDef f
+            let funDef = goFunctionDef f
         ]
 
 scanImports :: [Statement 'Scoped] -> [Import 'Scoped]
-scanImports stmts = mconcatMap go stmts
+scanImports = mconcatMap go
   where
     go :: Statement 'Scoped -> [Import 'Scoped]
     go = \case
@@ -350,7 +354,7 @@ goImport Import {..} = do
 -- | Ignores functions
 goAxiomInductive ::
   forall r.
-  (Members '[Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ConstructorInfos] r) =>
+  (Members '[Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ConstructorInfos, Reader NameSignatures] r) =>
   Statement 'Scoped ->
   Sem r [Internal.PreStatement]
 goAxiomInductive = \case
@@ -373,12 +377,12 @@ goProjectionDef ProjectionDef {..} = do
   info <- gets @ConstructorInfos (^?! at c . _Just)
   Internal.genFieldProjection (goSymbol _projectionField) info _projectionFieldIx
 
-goTopFunctionDef ::
+goFunctionDef ::
   forall r.
-  (Members '[Reader Pragmas, Error ScoperError, Builtins, NameIdGen] r) =>
+  (Members '[Reader Pragmas, Error ScoperError, Builtins, NameIdGen, Reader NameSignatures] r) =>
   FunctionDef 'Scoped ->
   Sem r Internal.FunctionDef
-goTopFunctionDef FunctionDef {..} = do
+goFunctionDef FunctionDef {..} = do
   let _funDefName = goSymbol _signName
       _funDefTerminating = isJust _signTerminating
       _funDefInstance = isJust _signInstance
@@ -387,10 +391,27 @@ goTopFunctionDef FunctionDef {..} = do
   _funDefExamples <- goExamples _signDoc
   _funDefPragmas <- goPragmas _signPragmas
   _funDefBody <- goBody
+  msig <- asks @NameSignatures (^. at (_funDefName ^. Internal.nameId))
+  _funDefDefaultSignature <- maybe (return mempty) goNameSignature msig
   let fun = Internal.FunctionDef {..}
   whenJust _signBuiltin (registerBuiltinFunction fun . (^. withLocParam))
   return fun
   where
+    goNameSignature :: NameSignature 'Scoped -> Sem r Internal.DefaultSignature
+    goNameSignature = fmap Internal.DefaultSignature . concatMapM goBlock . (^. nameSignatureArgs)
+      where
+        goBlock :: NameBlock 'Scoped -> Sem r [Maybe Internal.Expression]
+        goBlock blk = do
+          let tbl = indexedByInt (^. nameItemIndex) (blk ^. nameBlock)
+              mmaxIx = fst <$> IntMap.lookupMax tbl
+          case mmaxIx of
+            Nothing -> return []
+            Just maxIx ->
+              execOutputList $ forM_ [0 .. maxIx] $ \idx ->
+                case tbl ^. at idx of
+                  Nothing -> output (Nothing @Internal.Expression)
+                  Just i -> mapM goExpression (i ^? nameItemDefault . _Just . argDefaultValue) >>= output
+
     goBody :: Sem r Internal.Expression
     goBody = do
       commonPatterns <- concatMapM (fmap toList . argToPattern) _signArgs
@@ -465,7 +486,7 @@ goTopFunctionDef FunctionDef {..} = do
 
 goExamples ::
   forall r.
-  (Members '[Builtins, NameIdGen, Error ScoperError, Reader Pragmas] r) =>
+  (Members '[Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader NameSignatures] r) =>
   Maybe (Judoc 'Scoped) ->
   Sem r [Internal.Example]
 goExamples = mapM goExample . maybe [] judocExamples
@@ -481,7 +502,7 @@ goExamples = mapM goExample . maybe [] judocExamples
 
 goInductiveParameters ::
   forall r.
-  (Members '[Builtins, NameIdGen, Error ScoperError, Reader Pragmas] r) =>
+  (Members '[Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader NameSignatures] r) =>
   InductiveParameters 'Scoped ->
   Sem r [Internal.InductiveParameter]
 goInductiveParameters params@InductiveParameters {..} = do
@@ -575,7 +596,7 @@ registerBuiltinAxiom d = \case
   BuiltinIntPrint -> registerIntPrint d
 
 goInductive ::
-  (Members '[NameIdGen, Reader Pragmas, Builtins, Error ScoperError, State ConstructorInfos] r) =>
+  (Members '[NameIdGen, Reader Pragmas, Builtins, Error ScoperError, State ConstructorInfos, Reader NameSignatures] r) =>
   InductiveDef 'Scoped ->
   Sem r Internal.InductiveDef
 goInductive ty@InductiveDef {..} = do
@@ -613,7 +634,7 @@ registerInductiveConstructors indDef = do
 
 goConstructorDef ::
   forall r.
-  (Members '[Builtins, NameIdGen, Error ScoperError, Reader Pragmas] r) =>
+  (Members '[Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader NameSignatures] r) =>
   Internal.Expression ->
   ConstructorDef 'Scoped ->
   Sem r Internal.ConstructorDef
@@ -712,7 +733,7 @@ goListPattern l = do
 
 goExpression ::
   forall r.
-  (Members '[Builtins, NameIdGen, Error ScoperError, Reader Pragmas] r) =>
+  (Members '[Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader NameSignatures] r) =>
   Expression ->
   Sem r Internal.Expression
 goExpression = \case
@@ -758,9 +779,7 @@ goExpression = \case
                           { _argBlockDelims = Irrelevant Nothing,
                             _argBlockImplicit = Explicit,
                             _argBlockArgs = args
-                          },
-                    _namedAppSignature =
-                      Irrelevant (NameSignature [NameBlock (_recordCreationExtra ^. unIrrelevant . recordCreationExtraSignature . recordNames) Explicit])
+                          }
                   }
           cls <- goLetFunDefs (fmap Concrete.LetFunctionDef defs)
           e <- runNamedArguments app >>= goExpression
@@ -887,7 +906,7 @@ goExpression = \case
           where
             preLetStatement :: LetStatement 'Scoped -> Sem r (Maybe Internal.PreLetStatement)
             preLetStatement = \case
-              LetFunctionDef f -> Just . Internal.PreLetFunctionDef <$> goTopFunctionDef f
+              LetFunctionDef f -> Just . Internal.PreLetFunctionDef <$> goFunctionDef f
               LetAliasDef {} -> return Nothing
               LetOpen {} -> return Nothing
 
@@ -953,7 +972,7 @@ goExpression = \case
         mkApp :: Internal.Expression -> Internal.Expression -> Internal.Expression
         mkApp a1 a2 = Internal.ExpressionApplication $ Internal.Application a1 a2 Explicit
 
-goCase :: forall r. (Members '[Builtins, NameIdGen, Error ScoperError, Reader Pragmas] r) => Case 'Scoped -> Sem r Internal.Case
+goCase :: forall r. (Members '[Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader NameSignatures] r) => Case 'Scoped -> Sem r Internal.Case
 goCase c = do
   _caseExpression <- goExpression (c ^. caseExpression)
   _caseBranches <- mapM goBranch (c ^. caseBranches)
@@ -968,7 +987,7 @@ goCase c = do
       _caseBranchExpression <- goExpression (b ^. caseBranchExpression)
       return Internal.CaseBranch {..}
 
-goNewCase :: forall r. (Members '[Builtins, NameIdGen, Error ScoperError, Reader Pragmas] r) => NewCase 'Scoped -> Sem r Internal.Case
+goNewCase :: forall r. (Members '[Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader NameSignatures] r) => NewCase 'Scoped -> Sem r Internal.Case
 goNewCase c = do
   _caseExpression <- goExpression (c ^. newCaseExpression)
   _caseBranches <- mapM goBranch (c ^. newCaseBranches)
@@ -983,7 +1002,7 @@ goNewCase c = do
       _caseBranchExpression <- goExpression (b ^. newCaseBranchExpression)
       return Internal.CaseBranch {..}
 
-goLambda :: forall r. (Members '[Builtins, NameIdGen, Error ScoperError, Reader Pragmas] r) => Lambda 'Scoped -> Sem r Internal.Lambda
+goLambda :: forall r. (Members '[Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader NameSignatures] r) => Lambda 'Scoped -> Sem r Internal.Lambda
 goLambda l = do
   clauses' <- mapM goClause (l ^. lambdaClauses)
   return
@@ -1003,7 +1022,7 @@ goUniverse u
   | isSmallUniverse u = SmallUniverse (getLoc u)
   | otherwise = error "only small universe is supported"
 
-goFunction :: (Members '[Builtins, NameIdGen, Error ScoperError, Reader Pragmas] r) => Function 'Scoped -> Sem r Internal.Function
+goFunction :: (Members '[Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader NameSignatures] r) => Function 'Scoped -> Sem r Internal.Function
 goFunction f = do
   headParam :| tailParams <- goFunctionParameters (f ^. funParameters)
   ret <- goExpression (f ^. funReturn)
@@ -1014,7 +1033,7 @@ goFunction f = do
       }
 
 goFunctionParameters ::
-  (Members '[Builtins, NameIdGen, Error ScoperError, Reader Pragmas] r) =>
+  (Members '[Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader NameSignatures] r) =>
   FunctionParameters 'Scoped ->
   Sem r (NonEmpty Internal.FunctionParameter)
 goFunctionParameters FunctionParameters {..} = do
@@ -1181,7 +1200,7 @@ goRecordPattern r = do
               v <- Internal.freshVar loc ("x" <> show idx)
               output (Internal.patternArgFromVar Internal.Explicit v)
 
-goAxiom :: (Members '[Reader Pragmas, Error ScoperError, Builtins, NameIdGen] r) => AxiomDef 'Scoped -> Sem r Internal.AxiomDef
+goAxiom :: (Members '[Reader Pragmas, Error ScoperError, Builtins, NameIdGen, Reader NameSignatures] r) => AxiomDef 'Scoped -> Sem r Internal.AxiomDef
 goAxiom a = do
   _axiomType' <- goExpression (a ^. axiomType)
   _axiomPragmas' <- goPragmas (a ^. axiomPragmas)
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete/NamedArguments.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete/NamedArguments.hs
index d9271704f..35b15471c 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete/NamedArguments.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete/NamedArguments.hs
@@ -1,46 +1,64 @@
 module Juvix.Compiler.Internal.Translation.FromConcrete.NamedArguments
   ( runNamedArguments,
+    NameSignatures,
   )
 where
 
 import Data.HashMap.Strict qualified as HashMap
 import Data.IntMap.Strict qualified as IntMap
-import Juvix.Compiler.Concrete.Data.NameSignature.Base
+import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Gen qualified as Gen
 import Juvix.Compiler.Concrete.Keywords
 import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error
 import Juvix.Prelude
 
+type NameSignatures = HashMap NameId (NameSignature 'Scoped)
+
 data BuilderState = BuilderState
   { _stateRemainingArgs :: [ArgumentBlock 'Scoped],
-    _stateRemainingNames :: [NameBlock]
+    _stateRemainingNames :: [NameBlock 'Scoped]
   }
 
 makeLenses ''BuilderState
 
 runNamedArguments ::
   forall r.
-  (Members '[NameIdGen, Error ScoperError] r) =>
+  (Members '[NameIdGen, Error ScoperError, Reader NameSignatures, Reader NameSignatures] r) =>
   NamedApplication 'Scoped ->
   Sem r Expression
 runNamedArguments napp = do
+  iniSt <- mkIniBuilderState
   args <-
     execOutputList
       . mapError ErrNamedArgumentsError
-      . execState iniBuilderState
+      . execState iniSt
       $ helper (getLoc napp)
   return (foldl' mkApp (ExpressionIdentifier (napp ^. namedAppName)) args)
   where
-    sig :: NameSignature = napp ^. namedAppSignature . unIrrelevant
     mkApp :: Expression -> Expression -> Expression
     mkApp a = ExpressionApplication . Application a
-    iniBuilderState :: BuilderState
-    iniBuilderState =
-      BuilderState
-        { _stateRemainingArgs = toList (napp ^. namedAppArgs),
-          _stateRemainingNames = sig ^. nameSignatureArgs
-        }
+
+    mkIniBuilderState :: Sem r BuilderState
+    mkIniBuilderState = do
+      let name = napp ^. namedAppName . scopedIdenName
+      msig <- asks @NameSignatures (^. at (name ^. S.nameId))
+      let sig = fromMaybe err msig
+            where
+              err = error ("impossible: could not find name signature for " <> prettyText name)
+      return
+        BuilderState
+          { _stateRemainingArgs = toList (napp ^. namedAppArgs),
+            _stateRemainingNames = sig ^. nameSignatureArgs
+          }
+
+type Defaults = IntMap (ArgDefault 'Scoped)
+
+mkDefaults :: [NameItem 'Scoped] -> IntMap (ArgDefault 'Scoped)
+mkDefaults l =
+  IntMap.fromList
+    [ (i ^. nameItemIndex, def) | i <- l, Just def <- [i ^. nameItemDefault]
+    ]
 
 helper ::
   forall r.
@@ -50,43 +68,46 @@ helper ::
 helper loc = do
   whenJustM nextArgumentGroup $ \(impl, args, isLastBlock) -> do
     checkRepeated args
-    names <- nextNameGroup impl
+    names :: [NameItem 'Scoped] <- nextNameGroup impl
+
     (pendingArgs, (omittedNames, argmap)) <- scanGroup impl names args
-    emitArgs impl isLastBlock omittedNames argmap
+    emitArgs impl isLastBlock (mkDefaults names) omittedNames argmap
     whenJust (nonEmpty pendingArgs) $ \pendingArgs' -> do
       sig <- nextNameGroup Implicit
-      emitImplicit False sig mempty
+      emitImplicit False (mkDefaults sig) sig mempty
       moreNames <- not . null <$> gets (^. stateRemainingNames)
       if
           | moreNames -> modify' (over stateRemainingArgs (ArgumentBlock (Irrelevant Nothing) Explicit (nonEmpty' pendingArgs) :))
           | otherwise -> throw . ErrUnexpectedArguments $ UnexpectedArguments pendingArgs'
     helper loc
   where
-    nextNameGroup :: IsImplicit -> Sem r (HashMap Symbol Int)
-    nextNameGroup impl = do
+    nextNameGroup :: IsImplicit -> Sem r [NameItem 'Scoped]
+    nextNameGroup implArgs = do
       remb <- gets (^. stateRemainingNames)
       case remb of
         [] -> return mempty
-        b : bs -> do
-          let implNames = b ^. nameImplicit
+        (b :: NameBlock 'Scoped) : bs -> do
+          let implSig = b ^. nameImplicit
+              defaults = mkDefaults (toList (b ^. nameBlock))
           modify' (set stateRemainingNames bs)
-          let r = snd <$> b ^. nameBlock
-          case (impl, implNames) of
-            (Explicit, Explicit) -> return r
-            (Implicit, Implicit) -> return r
-            (ImplicitInstance, ImplicitInstance) -> return r
+          let r = toList (b ^. nameBlock)
+              matches = return r
+          case (implArgs, implSig) of
+            (Explicit, Explicit) -> matches
+            (Implicit, Implicit) -> matches
+            (ImplicitInstance, ImplicitInstance) -> matches
             (Explicit, Implicit) -> do
-              emitImplicit False r mempty
-              nextNameGroup impl
+              emitImplicit False defaults r mempty
+              nextNameGroup implArgs
             (Explicit, ImplicitInstance) -> do
-              emitImplicitInstance False r mempty
-              nextNameGroup impl
+              emitImplicitInstance False defaults r mempty
+              nextNameGroup implArgs
             (Implicit, ImplicitInstance) -> do
-              emitImplicitInstance False r mempty
-              nextNameGroup impl
+              emitImplicitInstance False defaults r mempty
+              nextNameGroup implArgs
             (ImplicitInstance, Implicit) -> do
-              emitImplicit False r mempty
-              nextNameGroup impl
+              emitImplicit False defaults r mempty
+              nextNameGroup implArgs
             (Implicit, Explicit) -> return mempty
             (ImplicitInstance, Explicit) -> return mempty
 
@@ -106,40 +127,43 @@ helper loc = do
     checkRepeated args = whenJust (nonEmpty (findRepeated (map (^. namedArgName) args))) $ \reps ->
       throw . ErrDuplicateArgument $ DuplicateArgument reps
 
-    emitArgs :: IsImplicit -> Bool -> HashMap Symbol Int -> IntMap Expression -> Sem r ()
+    emitArgs :: IsImplicit -> Bool -> Defaults -> [NameItem 'Scoped] -> IntMap Expression -> Sem r ()
     emitArgs = \case
       Implicit -> emitImplicit
       Explicit -> emitExplicit
       ImplicitInstance -> emitImplicitInstance
-
-    -- omitting arguments is only allowed at the end
-    emitExplicit :: Bool -> HashMap Symbol Int -> IntMap Expression -> Sem r ()
-    emitExplicit lastBlock omittedArgs args = do
-      if
-          | lastBlock ->
-              unless
-                (IntMap.keys args == [0 .. IntMap.size args - 1])
-                (missingErr (nonEmpty' (map fst (filterMissing (HashMap.toList omittedArgs)))))
-          | otherwise -> whenJust (nonEmpty (HashMap.keys omittedArgs)) missingErr
-      forM_ args output
       where
-        filterMissing :: [(Symbol, Int)] -> [(Symbol, Int)]
-        filterMissing = case maximumGiven of
-          Nothing -> id
-          Just m -> filter ((< m) . snd)
-        maximumGiven :: Maybe Int
-        maximumGiven = fst <$> IntMap.lookupMax args
-        missingErr :: NonEmpty Symbol -> Sem r ()
-        missingErr = throw . ErrMissingArguments . MissingArguments loc
+        -- omitting arguments is only allowed at the end
+        emitExplicit :: Bool -> Defaults -> [NameItem 'Scoped] -> IntMap Expression -> Sem r ()
+        emitExplicit lastBlock _ omittedArgs args = do
+          if
+              | lastBlock ->
+                  unless
+                    (IntMap.keys args == [0 .. IntMap.size args - 1])
+                    (missingErr (nonEmpty' (map (^. nameItemSymbol) (filterMissing omittedArgs))))
+              | otherwise -> whenJust (nonEmpty (map (^. nameItemSymbol) omittedArgs)) missingErr
+          forM_ args output
+          where
+            filterMissing :: [NameItem 'Scoped] -> [NameItem 'Scoped]
+            filterMissing = case maximumGiven of
+              Nothing -> id
+              Just m -> filter ((< m) . (^. nameItemIndex))
+
+            maximumGiven :: Maybe Int
+            maximumGiven = fst <$> IntMap.lookupMax args
+
+            missingErr :: NonEmpty Symbol -> Sem r ()
+            missingErr = throw . ErrMissingArguments . MissingArguments loc
 
     emitImplicitHelper ::
       (WithLoc Expression -> Expression) ->
       (HoleType 'Scoped -> Expression) ->
       Bool ->
-      HashMap Symbol Int ->
+      Defaults ->
+      [NameItem 'Scoped] ->
       IntMap Expression ->
       Sem r ()
-    emitImplicitHelper exprBraces exprHole lastBlock omittedArgs args = go 0 (IntMap.toAscList args)
+    emitImplicitHelper exprBraces exprHole lastBlock defaults omittedArgs args = go 0 (IntMap.toAscList args)
       where
         go :: Int -> [(Int, Expression)] -> Sem r ()
         go n = \case
@@ -151,16 +175,22 @@ helper loc = do
             output (exprBraces (WithLoc (getLoc e) e))
             go (n' + 1) rest
           where
-            fillUntil n' = replicateM_ (n' - n) (mkWildcard >>= output)
-            mkWildcard :: (Members '[NameIdGen] r') => Sem r' Expression
-            mkWildcard = exprBraces . WithLoc loc . exprHole . mkHole loc <$> freshNameId
-        maxIx :: Maybe Int
-        maxIx = fmap maximum1 . nonEmpty . toList $ omittedArgs
+            fillUntil n' = forM_ [n .. n' - 1] (fillPosition >=> output)
 
-    emitImplicit :: Bool -> HashMap Symbol Int -> IntMap Expression -> Sem r ()
+            fillPosition :: (Members '[NameIdGen] r') => Int -> Sem r' Expression
+            fillPosition idx =
+              exprBraces . WithLoc loc
+                <$> case defaults ^. at idx of
+                  Nothing -> exprHole . mkHole loc <$> freshNameId
+                  -- TODO update location
+                  Just d -> return (d ^. argDefaultValue)
+        maxIx :: Maybe Int
+        maxIx = fmap maximum1 . nonEmpty . map (^. nameItemIndex) $ omittedArgs
+
+    emitImplicit :: Bool -> Defaults -> [NameItem 'Scoped] -> IntMap Expression -> Sem r ()
     emitImplicit = emitImplicitHelper ExpressionBraces ExpressionHole
 
-    emitImplicitInstance :: Bool -> HashMap Symbol Int -> IntMap Expression -> Sem r ()
+    emitImplicitInstance :: Bool -> Defaults -> [NameItem 'Scoped] -> IntMap Expression -> Sem r ()
     emitImplicitInstance = emitImplicitHelper mkDoubleBraces ExpressionInstanceHole
       where
         mkDoubleBraces :: WithLoc Expression -> Expression
@@ -176,22 +206,29 @@ helper loc = do
 
     scanGroup ::
       IsImplicit ->
-      HashMap Symbol Int ->
+      [NameItem 'Scoped] ->
       [NamedArgument 'Scoped] ->
-      Sem r ([NamedArgument 'Scoped], (HashMap Symbol Int, IntMap Expression))
-    scanGroup impl names = runOutputList . runState names . execState mempty . mapM_ go
+      Sem r ([NamedArgument 'Scoped], ([NameItem 'Scoped], IntMap Expression))
+    scanGroup impl names =
+      fmap (second (first toList))
+        . runOutputList
+        . runState namesBySymbol
+        . execState mempty
+        . mapM_ go
       where
+        namesBySymbol :: HashMap Symbol (NameItem 'Scoped)
+        namesBySymbol = HashMap.fromList [(i ^. nameItemSymbol, i) | i <- names]
         go ::
-          (Members '[State (IntMap Expression), State (HashMap Symbol Int), State BuilderState, Output (NamedArgument 'Scoped), Error NamedArgumentsError] r') =>
+          (Members '[State (IntMap Expression), State (HashMap Symbol (NameItem 'Scoped)), State BuilderState, Output (NamedArgument 'Scoped), Error NamedArgumentsError] r') =>
           NamedArgument 'Scoped ->
           Sem r' ()
         go arg = do
           let sym = arg ^. namedArgName
-          midx :: Maybe Int <- gets @(HashMap Symbol Int) (^. at sym)
+          midx :: Maybe (NameItem 'Scoped) <- gets @(HashMap Symbol (NameItem 'Scoped)) (^. at sym)
           case midx of
             Just idx -> do
-              modify' (IntMap.insert idx (arg ^. namedArgValue))
-              modify' @(HashMap Symbol Int) (HashMap.delete sym)
+              modify' (IntMap.insert (idx ^. nameItemIndex) (arg ^. namedArgValue))
+              modify' @(HashMap Symbol (NameItem 'Scoped)) (HashMap.delete sym)
             Nothing -> case impl of
               Explicit -> do
                 -- the arg may belong to the next explicit group
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 f76c692b4..0c93e43ff 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs
@@ -118,6 +118,7 @@ checkMutualBlock ::
 checkMutualBlock (MutualBlock funs) = MutualBlock <$> mapM checkMutualStatement funs
 
 checkFunctionDef ::
+  forall r.
   (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r) =>
   FunctionDef ->
   Sem r FunctionDef
@@ -126,17 +127,40 @@ checkFunctionDef FunctionDef {..} = do
   _funDefType' <- withEmptyLocalVars (checkType _funDefType)
   _funDefBody' <- checkFunctionBody arity _funDefBody
   _funDefExamples' <- withEmptyLocalVars (mapM checkExample _funDefExamples)
+  let argTys = fst (unfoldFunType _funDefType')
+  _funDefDefaultSignature' <- checkDefaultArguments _funDefDefaultSignature argTys
   return
     FunctionDef
       { _funDefBody = _funDefBody',
         _funDefExamples = _funDefExamples',
         _funDefType = _funDefType',
+        _funDefDefaultSignature = _funDefDefaultSignature',
         _funDefName,
         _funDefTerminating,
         _funDefInstance,
         _funDefBuiltin,
         _funDefPragmas
       }
+  where
+    checkDefaultArguments :: DefaultSignature -> [FunctionParameter] -> Sem r DefaultSignature
+    checkDefaultArguments (DefaultSignature defaults) =
+      fmap DefaultSignature
+        . execOutputList
+        . go defaults
+      where
+        go :: [Maybe Expression] -> [FunctionParameter] -> Sem (Output (Maybe Expression) ': r) ()
+        go = \case
+          [] -> const (return ())
+          d : ds' -> \case
+            [] -> impossible
+            p : ps' -> do
+              dval <- case (d, p ^. paramImplicit) of
+                (Nothing, _) -> return Nothing
+                (Just val, Implicit) ->
+                  Just <$> withEmptyLocalVars (checkExpression (typeArity (p ^. paramType)) val)
+                (Just {}, _) -> impossible
+              output dval
+              go ds' ps'
 
 checkFunctionBody ::
   (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r) =>
@@ -225,7 +249,7 @@ guessArity = \case
           (Implicit : _, ParamExplicit {} : _) -> Nothing
           (ImplicitInstance : _, ParamExplicit {} : _) -> Nothing
           (Implicit : _, ParamImplicitInstance : _) -> Nothing
-          (ImplicitInstance : _, ParamImplicit : _) -> Nothing
+          (ImplicitInstance : _, ParamImplicit {} : _) -> Nothing
           ([], ps') -> Just ps'
           (_ : _, []) -> Nothing
 
@@ -286,7 +310,7 @@ checkLhs loc guessedBody ariSignature pats = do
         Just tailUnderscores -> do
           let n = length tailUnderscores
               a' = foldArity (over ufoldArityParams (drop n) (unfoldArity' a))
-          wildcards <- mapM genWildcard tailUnderscores
+          wildcards <- mapM genWildcard' tailUnderscores
           return (wildcards, a')
       lhs@(p : ps) -> case a of
         ArityUnit ->
@@ -301,7 +325,7 @@ checkLhs loc guessedBody ariSignature pats = do
           first (p' :) <$> goLhs ArityUnknown ps
         ArityFunction (FunctionArity l r) ->
           case (p ^. patternArgIsImplicit, l) of
-            (Implicit, ParamImplicit) -> do
+            (Implicit, ParamImplicit {}) -> do
               b' <- checkPattern (arityParameter l) p
               first (b' :) <$> goLhs r ps
             (Implicit, ParamExplicit {}) ->
@@ -332,22 +356,20 @@ checkLhs loc guessedBody ariSignature pats = do
                       }
                 )
             (ImplicitInstance, ParamImplicit {}) -> do
-              wildcard <- genWildcard Implicit
+              wildcard <- genWildcard' Implicit
               first (wildcard :) <$> goLhs r lhs
-            (Explicit, ParamImplicit) -> do
-              wildcard <- genWildcard Implicit
+            (Explicit, ParamImplicit {}) -> do
+              wildcard <- genWildcard' Implicit
               first (wildcard :) <$> goLhs r lhs
             (Explicit, ParamImplicitInstance) -> do
-              wildcard <- genWildcard ImplicitInstance
+              wildcard <- genWildcard' ImplicitInstance
               first (wildcard :) <$> goLhs r lhs
             (Explicit, ParamExplicit pa) -> do
               p' <- checkPattern pa p
               first (p' :) <$> goLhs r ps
       where
-        genWildcard :: forall r'. (Members '[NameIdGen] r') => IsImplicit -> Sem r' PatternArg
-        genWildcard impl = do
-          var <- varFromWildcard (Wildcard loc)
-          return (PatternArg impl Nothing (PatternVariable var))
+        genWildcard' :: forall r'. (Members '[NameIdGen] r') => IsImplicit -> Sem r' PatternArg
+        genWildcard' = genWildcard loc
 
     -- This is an heuristic and it can have an undesired result.
     -- Sometimes the outcome may even be confusing.
@@ -366,7 +388,7 @@ checkLhs loc guessedBody ariSignature pats = do
             isParamImplicit :: ArityParameter -> Bool
             isParamImplicit = \case
               ParamExplicit {} -> False
-              ParamImplicit -> True
+              ParamImplicit {} -> True
               ParamImplicitInstance -> True
         aI :: Int
         aI = preceedingImplicits a
@@ -375,7 +397,7 @@ checkLhs loc guessedBody ariSignature pats = do
         paramToImplicit :: ArityParameter -> IsImplicit
         paramToImplicit = \case
           ParamExplicit {} -> impossible
-          ParamImplicit -> Implicit
+          ParamImplicit {} -> Implicit
           ParamImplicitInstance -> ImplicitInstance
 
 checkPattern ::
@@ -412,7 +434,7 @@ checkWildcardConstructor ::
 checkWildcardConstructor w = do
   let c = w ^. wildcardConstructor
   numArgs <- length . constructorArgs . (^. constructorInfoType) <$> lookupConstructor c
-  holeArgs <- replicateM numArgs (explicitPatternArg . PatternVariable . varFromHole <$> newHole (getLoc w))
+  holeArgs <- replicateM numArgs (genWildcard (getLoc w) Explicit)
   return
     ConstructorApp
       { _constrAppConstructor = c,
@@ -508,10 +530,31 @@ idenArity :: (Members '[Reader LocalVars, Reader InfoTable] r) => Iden -> Sem r
 idenArity = \case
   IdenVar v -> getLocalArity v
   IdenInductive i -> typeArity <$> lookupInductiveType i
-  IdenFunction f -> typeArity . (^. functionInfoDef . funDefType) <$> lookupFunction f
+  IdenFunction f -> do
+    fun <- (^. functionInfoDef) <$> lookupFunction f
+    let ari = typeArity (fun ^. funDefType)
+        defaults = fun ^. funDefDefaultSignature
+    return (addDefaults defaults ari)
   IdenConstructor c -> typeArity <$> lookupConstructorType c
   IdenAxiom a -> typeArity . (^. axiomInfoDef . axiomType) <$> lookupAxiom a
 
+addDefaults :: DefaultSignature -> Arity -> Arity
+addDefaults = unfoldingArity . helper . (^. defaultSignature)
+  where
+    helper :: [Maybe Expression] -> UnfoldedArity -> UnfoldedArity
+    helper = over ufoldArityParams . go
+
+    go :: [Maybe Expression] -> [ArityParameter] -> [ArityParameter]
+    go ds as = case ds of
+      [] -> as
+      md : ds' -> case as of
+        [] -> impossible
+        a : as' -> case md of
+          Nothing -> a : go ds' (tail as)
+          Just d -> case a of
+            ParamImplicit i -> ParamImplicit (set implicitParamDefault (Just d) i) : go ds' as'
+            _ -> impossible
+
 -- | let x be some expression of type T. The argument of this function is T and it returns
 -- the arity of x. In other words, given (T : Type), it returns the arity of the elements of T.
 typeArity :: Expression -> Arity
@@ -553,7 +596,7 @@ typeArity = go
     goParam :: FunctionParameter -> ArityParameter
     goParam (FunctionParameter _ i e) = case i of
       ImplicitInstance -> ParamImplicitInstance
-      Implicit -> ParamImplicit
+      Implicit -> ParamImplicit (ImplicitParam Nothing)
       Explicit -> ParamExplicit (go e)
 
     goFun :: Function -> FunctionArity
@@ -692,45 +735,51 @@ checkExpression hintArity expr = case expr of
               Arity ->
               [ApplicationArg] ->
               Sem r [ApplicationArg]
-            go idx ari goargs = case (ari, goargs) of
-              (ArityFunction (FunctionArity ParamImplicit r), (ApplicationArg Implicit e) : rest) ->
-                ((ApplicationArg Implicit e) :) <$> go (succ idx) r rest
-              (ArityFunction (FunctionArity ParamImplicitInstance r), (ApplicationArg ImplicitInstance e) : rest) ->
-                ((ApplicationArg ImplicitInstance e) :) <$> go (succ idx) r rest
-              (ArityFunction (FunctionArity (ParamExplicit {}) r), (ApplicationArg Explicit e) : rest) ->
-                ((ApplicationArg Explicit e) :) <$> go (succ idx) r rest
-              (ArityFunction (FunctionArity impl _), [])
-                -- When there are no remaining arguments and the expected arity of the
-                -- expression matches the current arity we should *not* insert a hole.
-                | (impl == ParamImplicit || impl == ParamImplicitInstance)
-                    && ari == hint ->
-                    return []
-              (ArityFunction (FunctionArity ParamImplicit r), _) -> do
-                h <- newHole loc
-                ((ApplicationArg Implicit (ExpressionHole h)) :) <$> go (succ idx) r goargs
-              (ArityFunction (FunctionArity ParamImplicitInstance r), _) -> do
-                h <- newHole loc
-                ((ApplicationArg ImplicitInstance (ExpressionInstanceHole h)) :) <$> go (succ idx) r goargs
-              (ArityFunction (FunctionArity (ParamExplicit {}) _), (ApplicationArg _ _) : _) ->
-                throw
-                  ( ErrExpectedExplicitArgument
-                      ExpectedExplicitArgument
-                        { _expectedExplicitArgumentApp = (fun0, args),
-                          _expectedExplicitArgumentIx = idx
-                        }
-                  )
-              (ArityUnit, []) -> return []
-              (ArityFunction (FunctionArity (ParamExplicit _) _), []) -> return []
-              (ArityUnit, _ : _) ->
-                throw
-                  ( ErrTooManyArguments
-                      TooManyArguments
-                        { _tooManyArgumentsApp = (fun0, args),
-                          _tooManyArgumentsUnexpected = length goargs
-                        }
-                  )
-              (ArityUnknown, []) -> return []
-              (ArityUnknown, p : ps) -> (p :) <$> go (succ idx) ArityUnknown ps
+            go idx ari goargs =
+              case (ari, goargs) of
+                (ArityFunction (FunctionArity (ParamImplicit {}) r), (ApplicationArg Implicit e) : rest) ->
+                  ((ApplicationArg Implicit e) :) <$> go (succ idx) r rest
+                (ArityFunction (FunctionArity ParamImplicitInstance r), (ApplicationArg ImplicitInstance e) : rest) ->
+                  ((ApplicationArg ImplicitInstance e) :) <$> go (succ idx) r rest
+                (ArityFunction (FunctionArity (ParamExplicit {}) r), (ApplicationArg Explicit e) : rest) ->
+                  ((ApplicationArg Explicit e) :) <$> go (succ idx) r rest
+                (ArityFunction (FunctionArity impl _), [])
+                  -- When there are no remaining arguments and the expected arity of the
+                  -- expression matches the current arity we should *not* insert a hole.
+                  | arityParameterImplicitOrInstance impl
+                      && ari == hint ->
+                      return []
+                (ArityFunction (FunctionArity (ParamImplicit defaul) r), _) -> do
+                  h <- newHoleImplicit defaul loc
+                  ((ApplicationArg Implicit h) :) <$> go (succ idx) r goargs
+                (ArityFunction (FunctionArity ParamImplicitInstance r), _) -> do
+                  h <- newHoleInstance loc
+                  ((ApplicationArg ImplicitInstance (ExpressionInstanceHole h)) :) <$> go (succ idx) r goargs
+                (ArityFunction (FunctionArity (ParamExplicit {}) _), (ApplicationArg _ _) : _) ->
+                  throw
+                    ( ErrExpectedExplicitArgument
+                        ExpectedExplicitArgument
+                          { _expectedExplicitArgumentApp = (fun0, args),
+                            _expectedExplicitArgumentIx = idx
+                          }
+                    )
+                (ArityUnit, []) -> return []
+                (ArityFunction (FunctionArity (ParamExplicit _) _), []) -> return []
+                (ArityUnit, _ : _) ->
+                  throw
+                    ( ErrTooManyArguments
+                        TooManyArguments
+                          { _tooManyArgumentsApp = (fun0, args),
+                            _tooManyArgumentsUnexpected = length goargs
+                          }
+                    )
+                (ArityUnknown, []) -> return []
+                (ArityUnknown, p : ps) -> (p :) <$> go (succ idx) ArityUnknown ps
 
-newHole :: (Member NameIdGen r) => Interval -> Sem r Hole
-newHole loc = mkHole loc <$> freshNameId
+newHoleImplicit :: (Member NameIdGen r) => ImplicitParam -> Interval -> Sem r Expression
+newHoleImplicit i loc = case i ^. implicitParamDefault of
+  Nothing -> ExpressionHole . mkHole loc <$> freshNameId
+  Just e -> return e
+
+newHoleInstance :: (Member NameIdGen r) => Interval -> Sem r Hole
+newHoleInstance loc = mkHole loc <$> freshNameId
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/Types.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/Types.hs
index 0156af6c9..c645394a7 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/Types.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/Types.hs
@@ -1,5 +1,6 @@
 module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Types where
 
+import Juvix.Compiler.Internal.Language
 import Juvix.Prelude
 import Juvix.Prelude.Pretty
 
@@ -28,18 +29,35 @@ data UnfoldedArity = UnfoldedArity
 
 data ArityParameter
   = ParamExplicit Arity
-  | ParamImplicit
+  | ParamImplicit ImplicitParam
   | ParamImplicitInstance
   deriving stock (Eq)
 
+newtype ImplicitParam = ImplicitParam
+  { _implicitParamDefault :: Maybe Expression
+  }
+
+instance Eq ImplicitParam where
+  ImplicitParam _ == ImplicitParam _ = True
+
 makeLenses ''UnfoldedArity
+makeLenses ''ImplicitParam
+
+unfoldingArity :: (UnfoldedArity -> UnfoldedArity) -> Arity -> Arity
+unfoldingArity f = foldArity . f . unfoldArity'
 
 arityParameter :: ArityParameter -> Arity
 arityParameter = \case
-  ParamImplicit -> ArityUnit
+  ParamImplicit {} -> ArityUnit
   ParamImplicitInstance -> ArityUnit
   ParamExplicit a -> a
 
+arityParameterImplicitOrInstance :: ArityParameter -> Bool
+arityParameterImplicitOrInstance = \case
+  ParamExplicit {} -> False
+  ParamImplicit {} -> True
+  ParamImplicitInstance -> True
+
 arityCommonPrefix :: Arity -> Arity -> [ArityParameter]
 arityCommonPrefix p1 p2 = commonPrefix u1 u2
   where
@@ -72,12 +90,7 @@ foldArity UnfoldedArity {..} = go _ufoldArityParams
       [] -> case _ufoldArityRest of
         ArityRestUnit -> ArityUnit
         ArityRestUnknown -> ArityUnknown
-      (a : as) -> ArityFunction (FunctionArity l (go as))
-        where
-          l = case a of
-            ParamExplicit e -> ParamExplicit e
-            ParamImplicit -> ParamImplicit
-            ParamImplicitInstance -> ParamImplicitInstance
+      (a : as) -> ArityFunction (FunctionArity a (go as))
 
 instance HasAtomicity FunctionArity where
   atomicity = const (Aggregate funFixity)
@@ -90,7 +103,7 @@ instance HasAtomicity Arity where
 
 instance Pretty ArityParameter where
   pretty = \case
-    ParamImplicit -> "{𝟙}"
+    ParamImplicit {} -> "{𝟙}"
     ParamImplicitInstance -> "{{𝟙}}"
     ParamExplicit f -> pretty f
 
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 b66e292bd..88bbf551d 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
@@ -176,24 +176,45 @@ checkMutualStatement = \case
     return $ StatementAxiom ax
 
 checkFunctionDef ::
+  forall r.
   (Members '[HighlightBuilder, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Inference, Termination, Output TypedHole] r) =>
   FunctionDef ->
   Sem r FunctionDef
 checkFunctionDef FunctionDef {..} = do
   funDef <- do
     _funDefType' <- checkDefType _funDefType
+    _funDefExamples' <- mapM checkExample _funDefExamples
     registerIdenType _funDefName _funDefType'
     _funDefBody' <- checkExpression _funDefType' _funDefBody
+    let params = fst (unfoldFunType _funDefType')
+    _funDefDefaultSignature' <- checkDefaultValues params
     return
       FunctionDef
         { _funDefBody = _funDefBody',
           _funDefType = _funDefType',
-          ..
+          _funDefExamples = _funDefExamples',
+          _funDefDefaultSignature = _funDefDefaultSignature',
+          _funDefName,
+          _funDefTerminating,
+          _funDefInstance,
+          _funDefBuiltin,
+          _funDefPragmas
         }
   when _funDefInstance $
     checkInstanceType funDef
   registerFunctionDef funDef
-  traverseOf funDefExamples (mapM checkExample) funDef
+  return funDef
+  where
+    -- Since default arguments come from the left of the : then it must be that
+    -- there are at least n FunctionParameter
+    checkDefaultValues :: [FunctionParameter] -> Sem r DefaultSignature
+    checkDefaultValues allparams = DefaultSignature <$> mapM go (zipExact defaults params)
+      where
+        params = take n allparams
+        defaults = _funDefDefaultSignature ^. defaultSignature
+        n = length defaults
+        go :: (Maybe Expression, FunctionParameter) -> Sem r (Maybe Expression)
+        go (me, p) = forM me $ \e' -> checkExpression (p ^. paramType) e'
 
 checkIsType ::
   (Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable, Termination, Output TypedHole] r) =>
diff --git a/src/Juvix/Compiler/Pipeline/Artifacts.hs b/src/Juvix/Compiler/Pipeline/Artifacts.hs
index f4686518b..4a7689f29 100644
--- a/src/Juvix/Compiler/Pipeline/Artifacts.hs
+++ b/src/Juvix/Compiler/Pipeline/Artifacts.hs
@@ -141,4 +141,5 @@ runFromConcreteCache =
       . runReader (mempty :: Pragmas)
       . evalState (mempty :: Internal.ConstructorInfos)
       . runTerminationArtifacts
+      . runReaderArtifacts (artifactScoperState . scoperScopedSignatures)
       . Internal.goModuleNoCache
diff --git a/src/Juvix/Data/Irrelevant.hs b/src/Juvix/Data/Irrelevant.hs
index 60125cdba..17590f60f 100644
--- a/src/Juvix/Data/Irrelevant.hs
+++ b/src/Juvix/Data/Irrelevant.hs
@@ -5,11 +5,14 @@ module Juvix.Data.Irrelevant where
 import Juvix.Data.Loc
 import Juvix.Prelude.Base
 import Juvix.Prelude.Pretty
+import Prelude (show)
 
 newtype Irrelevant a = Irrelevant
   { _unIrrelevant :: a
   }
-  deriving stock (Show)
+
+instance Show (Irrelevant a) where
+  show = const "Irrelevant {}"
 
 instance (HasLoc a) => HasLoc (Irrelevant a) where
   getLoc (Irrelevant a) = getLoc a
diff --git a/src/Juvix/Prelude/Base.hs b/src/Juvix/Prelude/Base.hs
index 134ac33c3..91b6c56a9 100644
--- a/src/Juvix/Prelude/Base.hs
+++ b/src/Juvix/Prelude/Base.hs
@@ -111,6 +111,7 @@ import Data.HashSet qualified as HashSet
 import Data.Hashable
 import Data.Int
 import Data.IntMap.Strict (IntMap)
+import Data.IntMap.Strict qualified as IntMap
 import Data.IntSet (IntSet)
 import Data.List.Extra hiding (allSame, groupSortOn, head, last, mconcatMap)
 import Data.List.Extra qualified as List
@@ -547,3 +548,6 @@ popFirstJust f = \case
 
 uncurryF :: (Functor f) => (a -> b -> c) -> f (a, b) -> f c
 uncurryF g input = uncurry g <$> input
+
+indexedByInt :: (Foldable f) => (a -> Int) -> f a -> IntMap a
+indexedByInt getIx l = IntMap.fromList [(getIx i, i) | i <- toList l]
diff --git a/test/Scope/Negative.hs b/test/Scope/Negative.hs
index e29c15251..75415f25d 100644
--- a/test/Scope/Negative.hs
+++ b/test/Scope/Negative.hs
@@ -358,6 +358,13 @@ scoperErrorTests =
       $ \case
         ErrAmbiguousSym {} -> Nothing
         _ -> wrongError,
+    NegTest
+      "Invalid default"
+      $(mkRelDir ".")
+      $(mkRelFile "InvalidDefault.juvix")
+      $ \case
+        ErrWrongDefaultValue {} -> Nothing
+        _ -> wrongError,
     NegTest
       "Unsupported type"
       $(mkRelDir ".")
diff --git a/test/Typecheck/Negative.hs b/test/Typecheck/Negative.hs
index d8f9139cc..e3b89fb7e 100644
--- a/test/Typecheck/Negative.hs
+++ b/test/Typecheck/Negative.hs
@@ -201,6 +201,13 @@ tests =
       $(mkRelFile "InstanceTermination.juvix")
       $ \case
         ErrTraitNotTerminating {} -> Nothing
+        _ -> wrongError,
+    NegTest
+      "Default value wrong type"
+      $(mkRelDir "Internal")
+      $(mkRelFile "DefaultTypeError.juvix")
+      $ \case
+        ErrWrongType {} -> Nothing
         _ -> wrongError
   ]
 
diff --git a/tests/negative/Internal/DefaultTypeError.juvix b/tests/negative/Internal/DefaultTypeError.juvix
new file mode 100644
index 000000000..45ee37eb8
--- /dev/null
+++ b/tests/negative/Internal/DefaultTypeError.juvix
@@ -0,0 +1,6 @@
+module DefaultTypeError;
+
+type T := mkT;
+type U := mkU;
+
+g {a : T := mkU} : T := a;
diff --git a/tests/negative/InvalidDefault.juvix b/tests/negative/InvalidDefault.juvix
new file mode 100644
index 000000000..4bff045f2
--- /dev/null
+++ b/tests/negative/InvalidDefault.juvix
@@ -0,0 +1,3 @@
+module InvalidDefault;
+
+f (x : Type := Type) : Type := x;
diff --git a/tests/positive/DefaultValues.juvix b/tests/positive/DefaultValues.juvix
new file mode 100644
index 000000000..6abbb13c4
--- /dev/null
+++ b/tests/positive/DefaultValues.juvix
@@ -0,0 +1,45 @@
+module DefaultValues;
+
+import Stdlib.Data.Product open;
+
+axiom A : Type;
+
+axiom B : Type;
+
+axiom C : Type;
+
+axiom D : Type;
+
+axiom a : A;
+
+axiom b : B;
+
+axiom c : C;
+
+axiom d : D;
+
+mk {f1 : A := a} {f2 : Type} {f3 : C := c} (x : f2) : A × f2 × C :=
+  f1, x, f3;
+
+x1 : A × B × C := mk (x := b);
+
+mk2 {f1 : A := a} {f2 : Type} {f3 : C := c} (x : f2) {f4 : D := d} (y : f2) : A × f2 × C :=
+  f1, x, f3;
+
+x2 : A × B × C := mk2 (x := b) (y := b);
+
+mk3 {A := Type} {f1 : D := d} : D := f1;
+
+x3 : D := mk3;
+
+mk4 {A := Type} {f1 f2 f3 : D := d} : _ := f3;
+
+x4 : D := mk4;
+
+mk5 {A := Type} {f1 f2 f3 : D := mk4} : _ := f3;
+
+x5 : D := mk5;
+
+rec1 {a1 : A := rec2 {a}} : A := rec2 {a1 := a1};
+
+rec2 {a1 : A := rec1 {a}} : A := a1;