Add default arguments (#2408)

2024-07-07 04:36:19 +03:00 · 2023-10-10 23:28:06 +02:00 · 2023-10-10 23:28:06 +02:00 · a5516a5a08
commit a5516a5a08
parent 407a74004c
28 changed files with 691 additions and 337 deletions
--- a/.hlint.yaml
+++ b/.hlint.yaml
@ -13,6 +13,7 @@
        - DataKinds
        - DerivingStrategies
        - GADTs
+        - FunctionalDependencies
        - ImportQualifiedPost
        - LambdaCase
        - NoImplicitPrelude
--- 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
--- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Data/NameSignature/Base.hs
@ -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
--- 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
        ]
    )
--- 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
--- 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
--- 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
--- 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
--- 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 ::
--- 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
--- 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
--- 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 {..}
--- 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,
--- 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

--- 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
--- 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)
--- 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
--- 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
--- 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

--- 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) =>
--- 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
--- 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
--- 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]
--- 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 ".")
--- 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
  ]

--- a/tests/negative/Internal/DefaultTypeError.juvix
+++ b/tests/negative/Internal/DefaultTypeError.juvix
@ -0,0 +1,6 @@
+module DefaultTypeError;
+
+type T := mkT;
+type U := mkU;
+
+g {a : T := mkU} : T := a;
--- a/tests/negative/InvalidDefault.juvix
+++ b/tests/negative/InvalidDefault.juvix
@ -0,0 +1,3 @@
+module InvalidDefault;
+
+f (x : Type := Type) : Type := x;
--- a/tests/positive/DefaultValues.juvix
+++ 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;