diff --git a/juvix-stdlib b/juvix-stdlib
index f0a1e1ed77..a6abb99562 160000
--- a/juvix-stdlib
+++ b/juvix-stdlib
@@ -1 +1 @@
-Subproject commit f0a1e1ed77e9e94467434b85736839e110d021d5
+Subproject commit a6abb9956261f152cea5b14a0d31a9cce6c1957f
diff --git a/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs
index 4305f162e8..00a75e8937 100644
--- a/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs
+++ b/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs
@@ -541,12 +541,12 @@ goAxiom axiom = do
 goDeriving :: forall r. (Members '[Reader HtmlOptions] r) => Deriving 'Scoped -> Sem r Html
 goDeriving def = do
   sig <- ppHelper (ppCode def)
-  defHeader (def ^. derivingFunLhs . funLhsName) sig Nothing
+  defHeader (def ^. derivingFunLhs . funLhsName . functionDefName) sig Nothing
 
 goFunctionDef :: forall r. (Members '[Reader HtmlOptions] r) => FunctionDef 'Scoped -> Sem r Html
 goFunctionDef def = do
   sig <- ppHelper (ppCode (functionDefLhs def))
-  defHeader (def ^. signName) sig (def ^. signDoc)
+  defHeader (def ^. signName . functionDefName) sig (def ^. signDoc)
 
 goInductive :: forall r. (Members '[Reader HtmlOptions] r) => InductiveDef 'Scoped -> Sem r Html
 goInductive def = do
diff --git a/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs
index 5dc91201aa..72a252a951 100644
--- a/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs
+++ b/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs
@@ -60,11 +60,11 @@ runInfoTableBuilder ini = reinterpret (runState ini) $ \case
      in do
           modify' (over infoInductives (HashMap.insert (ity ^. inductiveName . nameId) ity))
           highlightDoc (ity ^. inductiveName . nameId) j
-  RegisterFunctionDef f ->
+  RegisterFunctionDef f -> do
     let j = f ^. signDoc
-     in do
-          modify' (over infoFunctions (HashMap.insert (f ^. signName . nameId) f))
-          highlightDoc (f ^. signName . nameId) j
+        fid = f ^. signName . functionDefName . nameId
+    modify' (over infoFunctions (HashMap.insert fid f))
+    highlightDoc fid j
   RegisterName n -> highlightName (S.anameFromName n)
   RegisterScopedIden n -> highlightName (anameFromScopedIden n)
   RegisterModuleDoc uid doc -> highlightDoc uid doc
diff --git a/src/Juvix/Compiler/Concrete/Extra.hs b/src/Juvix/Compiler/Concrete/Extra.hs
index cf8dcdcbb4..1484e573f2 100644
--- a/src/Juvix/Compiler/Concrete/Extra.hs
+++ b/src/Juvix/Compiler/Concrete/Extra.hs
@@ -72,7 +72,7 @@ groupStatements = \case
     definesSymbol n s = case s of
       StatementInductive d -> n `elem` syms d
       StatementAxiom d -> n == symbolParsed (d ^. axiomName)
-      StatementFunctionDef d -> n == symbolParsed (d ^. signName)
+      StatementFunctionDef d -> withFunctionSymbol False (\n' -> n == symbolParsed n') (d ^. signName)
       _ -> False
       where
         syms :: InductiveDef s -> [Symbol]
diff --git a/src/Juvix/Compiler/Concrete/Gen.hs b/src/Juvix/Compiler/Concrete/Gen.hs
index bb55008436..957a41d199 100644
--- a/src/Juvix/Compiler/Concrete/Gen.hs
+++ b/src/Juvix/Compiler/Concrete/Gen.hs
@@ -24,10 +24,10 @@ simplestFunctionDefParsed funNameTxt funBody = do
   funName <- symbol funNameTxt
   return (simplestFunctionDef funName (mkExpressionAtoms funBody))
 
-simplestFunctionDef :: FunctionName s -> ExpressionType s -> FunctionDef s
+simplestFunctionDef :: forall s. (SingI s) => FunctionName s -> ExpressionType s -> FunctionDef s
 simplestFunctionDef funName funBody =
   FunctionDef
-    { _signName = funName,
+    { _signName = name,
       _signBody = SigBodyExpression funBody,
       _signTypeSig =
         TypeSig
@@ -42,6 +42,15 @@ simplestFunctionDef funName funBody =
       _signInstance = Nothing,
       _signCoercion = Nothing
     }
+  where
+    name :: FunctionSymbolType s
+    name = case sing :: SStage s of
+      SParsed -> FunctionDefName funName
+      SScoped ->
+        FunctionDefNameScoped
+          { _functionDefName = funName,
+            _functionDefNamePattern = Nothing
+          }
 
 smallUniverseExpression :: forall s r. (SingI s) => (Members '[Reader Interval] r) => Sem r (ExpressionType s)
 smallUniverseExpression = do
@@ -284,7 +293,7 @@ mkTypeSigType ts = do
 
 mkTypeSigType' :: forall s. (SingI s) => ExpressionType s -> TypeSig s -> (ExpressionType s)
 mkTypeSigType' wildcard TypeSig {..} =
-  foldr mkFun rty (map mkFunctionParameters _typeSigArgs)
+  foldr (mkFun . mkFunctionParameters) rty _typeSigArgs
   where
     rty = fromMaybe wildcard _typeSigRetType
 
@@ -297,7 +306,7 @@ mkTypeSigType' wildcard TypeSig {..} =
         { _paramNames = getSigArgNames arg,
           _paramImplicit = _sigArgImplicit,
           _paramDelims = fmap Just _sigArgDelims,
-          _paramColon = Irrelevant $ maybe Nothing (Just . (^. unIrrelevant)) _sigArgColon,
+          _paramColon = Irrelevant $ fmap (^. unIrrelevant) _sigArgColon,
           _paramType = fromMaybe (univ (getLoc arg)) _sigArgType
         }
 
diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs
index 6b332ab8b8..47b7af06c6 100644
--- a/src/Juvix/Compiler/Concrete/Language.hs
+++ b/src/Juvix/Compiler/Concrete/Language.hs
@@ -30,8 +30,8 @@ statementLabel = \case
   StatementSyntax s -> goSyntax s
   StatementOpenModule {} -> Nothing
   StatementProjectionDef {} -> Nothing
-  StatementFunctionDef f -> Just (f ^. signName . symbolTypeLabel)
-  StatementDeriving f -> Just (f ^. derivingFunLhs . funLhsName . symbolTypeLabel)
+  StatementFunctionDef f -> withFunctionSymbol Nothing (Just . (^. symbolTypeLabel)) (f ^. signName)
+  StatementDeriving f -> withFunctionSymbol Nothing (Just . (^. symbolTypeLabel)) (f ^. derivingFunLhs . funLhsName)
   StatementImport i -> Just (i ^. importModulePath . to modulePathTypeLabel)
   StatementInductive i -> Just (i ^. inductiveName . symbolTypeLabel)
   StatementModule i -> Just (i ^. modulePath . to modulePathTypeLabel)
diff --git a/src/Juvix/Compiler/Concrete/Language/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs
index 6fbe2cc3b5..1721130356 100644
--- a/src/Juvix/Compiler/Concrete/Language/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Language/Base.hs
@@ -81,6 +81,11 @@ type family SymbolType s = res | res -> s where
   SymbolType 'Parsed = Symbol
   SymbolType 'Scoped = S.Symbol
 
+type FunctionSymbolType :: Stage -> GHCType
+type family FunctionSymbolType s = res | res -> s where
+  FunctionSymbolType 'Parsed = FunctionDefNameParsed
+  FunctionSymbolType 'Scoped = FunctionDefNameScoped
+
 type IdentifierType :: Stage -> GHCType
 type family IdentifierType s = res | res -> s where
   IdentifierType 'Parsed = Name
@@ -701,8 +706,27 @@ deriving stock instance Ord (Deriving 'Parsed)
 
 deriving stock instance Ord (Deriving 'Scoped)
 
+data FunctionDefNameParsed
+  = FunctionDefNamePattern (PatternAtom 'Parsed)
+  | FunctionDefName Symbol
+  deriving stock (Eq, Ord, Show, Generic)
+
+instance Serialize FunctionDefNameParsed
+
+instance NFData FunctionDefNameParsed
+
+data FunctionDefNameScoped = FunctionDefNameScoped
+  { _functionDefName :: S.Symbol,
+    _functionDefNamePattern :: Maybe PatternArg
+  }
+  deriving stock (Eq, Ord, Show, Generic)
+
+instance Serialize FunctionDefNameScoped
+
+instance NFData FunctionDefNameScoped
+
 data FunctionDef (s :: Stage) = FunctionDef
-  { _signName :: FunctionName s,
+  { _signName :: FunctionSymbolType s,
     _signTypeSig :: TypeSig s,
     _signDoc :: Maybe (Judoc s),
     _signPragmas :: Maybe ParsedPragmas,
@@ -2860,7 +2884,7 @@ data FunctionLhs (s :: Stage) = FunctionLhs
     _funLhsTerminating :: Maybe KeywordRef,
     _funLhsInstance :: Maybe KeywordRef,
     _funLhsCoercion :: Maybe KeywordRef,
-    _funLhsName :: FunctionName s,
+    _funLhsName :: FunctionSymbolType s,
     _funLhsTypeSig :: TypeSig s
   }
   deriving stock (Generic)
@@ -2886,6 +2910,7 @@ deriving stock instance Ord (FunctionLhs 'Parsed)
 deriving stock instance Ord (FunctionLhs 'Scoped)
 
 makeLenses ''SideIfs
+makeLenses ''FunctionDefNameScoped
 makeLenses ''TypeSig
 makeLenses ''FunctionLhs
 makeLenses ''Statements
@@ -2975,6 +3000,7 @@ makeLenses ''MarkdownInfo
 makeLenses ''Deriving
 
 makePrisms ''NamedArgumentNew
+makePrisms ''FunctionDefNameParsed
 
 functionDefLhs :: FunctionDef s -> FunctionLhs s
 functionDefLhs FunctionDef {..} =
@@ -3146,6 +3172,29 @@ instance HasLoc (OpenModule s short) where
 instance HasLoc (ProjectionDef s) where
   getLoc = getLoc . (^. projectionConstructor)
 
+getLocFunctionSymbolType :: forall s. (SingI s) => FunctionSymbolType s -> Interval
+getLocFunctionSymbolType = case sing :: SStage s of
+  SParsed -> getLoc
+  SScoped -> getLoc
+
+instance HasLoc FunctionDefNameScoped where
+  getLoc FunctionDefNameScoped {..} =
+    getLoc _functionDefName
+      <>? (getLoc <$> _functionDefNamePattern)
+
+instance HasLoc FunctionDefNameParsed where
+  getLoc = \case
+    FunctionDefNamePattern a -> getLoc a
+    FunctionDefName s -> getLoc s
+
+instance (SingI s) => HasLoc (FunctionLhs s) where
+  getLoc FunctionLhs {..} =
+    (getLoc <$> _funLhsBuiltin)
+      ?<> (getLoc <$> _funLhsTerminating)
+      ?<> ( getLocFunctionSymbolType _funLhsName
+              <>? (getLocExpressionType <$> _funLhsTypeSig ^. typeSigRetType)
+          )
+
 instance (SingI s) => HasLoc (Deriving s) where
   getLoc Deriving {..} =
     getLoc _derivingKw
@@ -3382,22 +3431,14 @@ instance (SingI s) => HasLoc (FunctionDefBody s) where
     SigBodyExpression e -> getLocExpressionType e
     SigBodyClauses cl -> getLocSpan cl
 
-instance (SingI s) => HasLoc (FunctionLhs s) where
-  getLoc FunctionLhs {..} =
-    (getLoc <$> _funLhsBuiltin)
-      ?<> (getLoc <$> _funLhsTerminating)
-      ?<> ( getLocSymbolType _funLhsName
-              <>? (getLocExpressionType <$> _funLhsTypeSig ^. typeSigRetType)
-          )
-
 instance (SingI s) => HasLoc (FunctionDef s) where
   getLoc FunctionDef {..} =
     (getLoc <$> _signDoc)
       ?<> (getLoc <$> _signPragmas)
       ?<> (getLoc <$> _signBuiltin)
       ?<> (getLoc <$> _signTerminating)
-      ?<> getLocSymbolType _signName
-      <> (getLoc _signBody)
+      ?<> (getLocFunctionSymbolType _signName)
+      <> getLoc _signBody
 
 instance HasLoc (Example s) where
   getLoc e = e ^. exampleLoc
@@ -3433,6 +3474,11 @@ getLocPatternParensType = case sing :: SStage s of
   SScoped -> getLoc
   SParsed -> getLoc
 
+getLocPatternAtomType :: forall s. (SingI s) => PatternAtomType s -> Interval
+getLocPatternAtomType = case sing :: SStage s of
+  SScoped -> getLoc
+  SParsed -> getLoc
+
 instance (SingI s) => HasLoc (RecordPatternAssign s) where
   getLoc a =
     getLoc (a ^. recordPatternAssignField)
@@ -3581,17 +3627,34 @@ symbolParsed sym = case sing :: SStage s of
   SParsed -> sym
   SScoped -> sym ^. S.nameConcrete
 
+getFunctionSymbol :: forall s. (SingI s) => FunctionSymbolType s -> SymbolType s
+getFunctionSymbol sym = case sing :: SStage s of
+  SParsed -> case sym of
+    FunctionDefName p -> p
+    FunctionDefNamePattern {} -> impossibleError "invalid call"
+  SScoped -> sym ^. functionDefName
+
+functionSymbolPattern :: forall s. (SingI s) => FunctionSymbolType s -> Maybe (PatternAtomType s)
+functionSymbolPattern f = case sing :: SStage s of
+  SParsed -> f ^? _FunctionDefNamePattern
+  SScoped -> f ^. functionDefNamePattern
+
+withFunctionSymbol :: forall s a. (SingI s) => a -> (SymbolType s -> a) -> FunctionSymbolType s -> a
+withFunctionSymbol a f sym = case sing :: SStage s of
+  SParsed -> maybe a f (sym ^? _FunctionDefName)
+  SScoped -> f (sym ^. functionDefName)
+
 namedArgumentNewSymbolParsed :: (SingI s) => SimpleGetter (NamedArgumentNew s) Symbol
 namedArgumentNewSymbolParsed = to $ \case
   NamedArgumentItemPun a -> a ^. namedArgumentPunSymbol
-  NamedArgumentNewFunction a -> symbolParsed (a ^. namedArgumentFunctionDef . signName)
+  NamedArgumentNewFunction a -> symbolParsed (getFunctionSymbol (a ^. namedArgumentFunctionDef . signName))
 
 namedArgumentNewSymbol :: Lens' (NamedArgumentNew 'Parsed) Symbol
 namedArgumentNewSymbol f = \case
-  NamedArgumentItemPun a -> NamedArgumentItemPun <$> namedArgumentPunSymbol f a
-  NamedArgumentNewFunction a ->
-    NamedArgumentNewFunction
-      <$> (namedArgumentFunctionDef . signName) f a
+  NamedArgumentItemPun a -> NamedArgumentItemPun <$> (namedArgumentPunSymbol f a)
+  NamedArgumentNewFunction a -> do
+    a' <- f (a ^?! namedArgumentFunctionDef . signName . _FunctionDefName)
+    return $ NamedArgumentNewFunction (over namedArgumentFunctionDef (set signName (FunctionDefName a')) a)
 
 scopedIdenSrcName :: Lens' ScopedIden S.Name
 scopedIdenSrcName f n = case n ^. scopedIdenAlias of
diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
index 37a5880eee..656a817066 100644
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Print/Base.hs
@@ -1168,7 +1168,10 @@ instance (SingI s) => PrettyPrint (FunctionLhs s) where
         coercion' = (<> if isJust instance' then space else line) . ppCode <$> _funLhsCoercion
         instance' = (<> line) . ppCode <$> _funLhsInstance
         builtin' = (<> line) . ppCode <$> _funLhsBuiltin
-        name' = annDef _funLhsName (ppSymbolType _funLhsName)
+        mpat :: Maybe (PatternAtomType s) = functionSymbolPattern _funLhsName
+        name' = case mpat of
+          Just pat -> withFunctionSymbol id annDef _funLhsName (ppPatternAtomType pat)
+          Nothing -> annDef (getFunctionSymbol _funLhsName) (ppSymbolType (getFunctionSymbol _funLhsName))
         sig' = ppCode _funLhsTypeSig
     builtin'
       ?<> termin'
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
index d58f772b71..f904efc182 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@@ -29,6 +29,10 @@ import Juvix.Compiler.Store.Scoped.Language as Store
 import Juvix.Data.FixityInfo qualified as FI
 import Juvix.Prelude
 
+data PatternNamesKind
+  = PatternNamesKindVariables
+  | PatternNamesKindFunctions
+
 scopeCheck ::
   (Members '[HighlightBuilder, Error JuvixError, NameIdGen] r) =>
   PackageId ->
@@ -347,6 +351,7 @@ reserveSymbolOf k =
 
 getReservedDefinitionSymbol ::
   forall r.
+  (HasCallStack) =>
   (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, InfoTableBuilder, Reader InfoTable, State ScoperState, Reader BindingStrategy] r) =>
   Symbol ->
   Sem r S.Symbol
@@ -407,7 +412,7 @@ reserveFunctionSymbol ::
   FunctionLhs 'Parsed ->
   Sem r S.Symbol
 reserveFunctionSymbol f =
-  reserveSymbolSignatureOf SKNameFunction f (toBuiltinPrim <$> f ^. funLhsBuiltin) (f ^. funLhsName)
+  reserveSymbolSignatureOf SKNameFunction f (toBuiltinPrim <$> f ^. funLhsBuiltin) (f ^?! funLhsName . _FunctionDefName)
 
 reserveAxiomSymbol ::
   (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) =>
@@ -446,6 +451,47 @@ bindFixitySymbol s = do
       err = error ("impossible. Contents of scope:\n" <> ppTrace (toList m))
   return s'
 
+reservePatternFunctionSymbols ::
+  forall r.
+  (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) =>
+  PatternAtomType 'Parsed ->
+  Sem r ()
+reservePatternFunctionSymbols = goAtom
+  where
+    goAtom :: PatternAtom 'Parsed -> Sem r ()
+    goAtom = \case
+      PatternAtomIden iden -> void (reservePatternName iden)
+      PatternAtomWildcard {} -> return ()
+      PatternAtomEmpty {} -> return ()
+      PatternAtomList x -> goList x
+      PatternAtomWildcardConstructor {} -> return ()
+      PatternAtomRecord x -> goRecord x
+      PatternAtomParens x -> goAtoms x
+      PatternAtomBraces x -> goAtoms x
+      PatternAtomDoubleBraces x -> goAtoms x
+      PatternAtomAt x -> goAt x
+
+    goList :: ListPattern 'Parsed -> Sem r ()
+    goList ListPattern {..} = mapM_ goAtoms _listpItems
+
+    goRecord :: RecordPattern 'Parsed -> Sem r ()
+    goRecord RecordPattern {..} = mapM_ goRecordItem _recordPatternItems
+
+    goRecordItem :: RecordPatternItem 'Parsed -> Sem r ()
+    goRecordItem = \case
+      RecordPatternItemFieldPun FieldPun {..} -> do
+        void (reservePatternName (NameUnqualified _fieldPunField))
+      RecordPatternItemAssign RecordPatternAssign {..} -> do
+        goAtoms _recordPatternAssignPattern
+
+    goAtoms :: PatternAtoms 'Parsed -> Sem r ()
+    goAtoms PatternAtoms {..} = mapM_ goAtom _patternAtoms
+
+    goAt :: PatternBinding -> Sem r ()
+    goAt PatternBinding {..} = do
+      void (reservePatternName (NameUnqualified _patternBindingName))
+      goAtom _patternBindingPattern
+
 checkImport ::
   forall r.
   ( Members
@@ -1072,14 +1118,23 @@ checkDeriving ::
   Sem r (Deriving 'Scoped)
 checkDeriving Deriving {..} = do
   let lhs@FunctionLhs {..} = _derivingFunLhs
+  massert (isJust (_funLhsName ^? _FunctionDefName))
+  let name = case _funLhsName of
+        FunctionDefName n -> n
+        FunctionDefNamePattern {} -> impossible
   typeSig' <- withLocalScope (checkTypeSig _funLhsTypeSig)
   name' <-
     if
-        | P.isLhsFunctionLike lhs -> getReservedDefinitionSymbol _funLhsName
+        | P.isLhsFunctionLike lhs -> getReservedDefinitionSymbol name
         | otherwise -> reserveFunctionSymbol lhs
+  let defname' =
+        FunctionDefNameScoped
+          { _functionDefName = name',
+            _functionDefNamePattern = Nothing
+          }
   let lhs' =
         FunctionLhs
-          { _funLhsName = name',
+          { _funLhsName = defname',
             _funLhsTypeSig = typeSig',
             ..
           }
@@ -1142,10 +1197,26 @@ checkFunctionDef fdef@FunctionDef {..} = do
     a' <- checkTypeSig _signTypeSig
     b' <- checkBody
     return (a', b')
-  sigName' <-
-    if
-        | P.isFunctionLike fdef -> getReservedDefinitionSymbol _signName
-        | otherwise -> reserveFunctionSymbol (functionDefLhs fdef)
+  whenJust (functionSymbolPattern _signName) reservePatternFunctionSymbols
+  sigName' <- case _signName of
+    FunctionDefName name -> do
+      name' <-
+        if
+            | P.isFunctionLike fdef -> getReservedDefinitionSymbol name
+            | otherwise -> reserveFunctionSymbol (functionDefLhs fdef)
+      return
+        FunctionDefNameScoped
+          { _functionDefName = name',
+            _functionDefNamePattern = Nothing
+          }
+    FunctionDefNamePattern p -> do
+      name' <- freshSymbol KNameFunction KNameFunction (WithLoc (getLoc p) "__pattern__")
+      p' <- runReader PatternNamesKindFunctions (checkParsePatternAtom p)
+      return
+        FunctionDefNameScoped
+          { _functionDefName = name',
+            _functionDefNamePattern = Just p'
+          }
   let def =
         FunctionDef
           { _signName = sigName',
@@ -1154,7 +1225,7 @@ checkFunctionDef fdef@FunctionDef {..} = do
             _signTypeSig = sig',
             ..
           }
-  registerNameSignature (sigName' ^. S.nameId) def
+  registerNameSignature (sigName' ^. functionDefName . S.nameId) def
   registerFunctionDef @$> def
   where
     checkBody :: Sem r (FunctionDefBody 'Scoped)
@@ -1165,7 +1236,7 @@ checkFunctionDef fdef@FunctionDef {..} = do
     checkClause :: FunctionClause 'Parsed -> Sem r (FunctionClause 'Scoped)
     checkClause FunctionClause {..} = do
       (patterns', body') <- withLocalScope $ do
-        p <- mapM checkParsePatternAtom _clausenPatterns
+        p <- mapM checkParsePatternAtom' _clausenPatterns
         b <- checkParseExpressionAtoms _clausenBody
         return (p, b)
       return
@@ -2254,7 +2325,7 @@ checkLetStatements =
 
 checkRecordPattern ::
   forall r.
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen] r) =>
+  (Members '[Reader PatternNamesKind, Error ScoperError, State Scope, State ScoperState, State ScoperSyntax, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable, NameIdGen] r) =>
   RecordPattern 'Parsed ->
   Sem r (RecordPattern 'Scoped)
 checkRecordPattern r = do
@@ -2274,9 +2345,10 @@ checkRecordPattern r = do
   where
     noFields :: ScopedIden -> ScoperError
     noFields = ErrConstructorNotARecord . ConstructorNotARecord
+
     checkItem ::
       forall r'.
-      (Members '[Reader (RecordNameSignature 'Parsed), Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen] r') =>
+      (Members '[Reader (RecordNameSignature 'Parsed), Reader PatternNamesKind, Error ScoperError, State Scope, State ScoperState, State ScoperSyntax, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable, NameIdGen] r') =>
       RecordPatternItem 'Parsed ->
       Sem r' (RecordPatternItem 'Scoped)
     checkItem = \case
@@ -2305,7 +2377,12 @@ checkRecordPattern r = do
         checkPun :: FieldPun 'Parsed -> Sem r' (FieldPun 'Scoped)
         checkPun f = do
           idx' <- findField (f ^. fieldPunField)
-          f' <- bindVariableSymbol (f ^. fieldPunField)
+          pk <- ask
+          f' <- case pk of
+            PatternNamesKindVariables ->
+              bindVariableSymbol (f ^. fieldPunField)
+            PatternNamesKindFunctions -> do
+              getReservedDefinitionSymbol (f ^. fieldPunField)
           return
             FieldPun
               { _fieldPunIx = idx',
@@ -2314,7 +2391,7 @@ checkRecordPattern r = do
 
 checkListPattern ::
   forall r.
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen] r) =>
+  (Members '[Reader PatternNamesKind, Error ScoperError, State Scope, State ScoperState, State ScoperSyntax, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable, NameIdGen] r) =>
   ListPattern 'Parsed ->
   Sem r (ListPattern 'Scoped)
 checkListPattern l = do
@@ -2449,7 +2526,7 @@ checkCaseBranch ::
   CaseBranch 'Parsed ->
   Sem r (CaseBranch 'Scoped)
 checkCaseBranch CaseBranch {..} = withLocalScope $ do
-  pattern' <- checkParsePatternAtoms _caseBranchPattern
+  pattern' <- checkParsePatternAtoms' _caseBranchPattern
   rhs' <- checkCaseBranchRhs _caseBranchRhs
   return $
     CaseBranch
@@ -2464,7 +2541,7 @@ checkDoBind ::
   Sem r (DoBind 'Scoped)
 checkDoBind DoBind {..} = do
   expr' <- checkParseExpressionAtoms _doBindExpression
-  pat' <- checkParsePatternAtoms _doBindPattern
+  pat' <- checkParsePatternAtoms' _doBindPattern
   unless (Explicit == pat' ^. patternArgIsImplicit) $
     throw (ErrDoBindImplicitPattern (DoBindImplicitPattern pat'))
   return
@@ -2573,7 +2650,7 @@ checkLambdaClause ::
   LambdaClause 'Parsed ->
   Sem r (LambdaClause 'Scoped)
 checkLambdaClause LambdaClause {..} = withLocalScope $ do
-  lambdaParameters' <- mapM checkParsePatternAtom _lambdaParameters
+  lambdaParameters' <- mapM checkParsePatternAtom' _lambdaParameters
   lambdaBody' <- checkParseExpressionAtoms _lambdaBody
   return
     LambdaClause
@@ -2640,23 +2717,47 @@ resolveShadowing es = go [(e, e ^. nsEntry . S.nameWhyInScope) | e <- es]
           S.BecauseInherited {} -> True
           _ -> False
 
-checkPatternName ::
+checkPatternName' ::
   forall r.
-  (Members '[Error ScoperError, State Scope, NameIdGen, State ScoperState, InfoTableBuilder, Reader InfoTable] r) =>
+  (Members '[Reader PatternNamesKind, Error ScoperError, State Scope, NameIdGen, State ScoperState, State ScoperSyntax, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) =>
+  (Symbol -> Sem r S.Symbol) ->
   Name ->
   Sem r PatternScopedIden
-checkPatternName n = do
+checkPatternName' bindFun n = do
   c <- getConstructorRef
   case c of
-    Just constr -> return (PatternScopedConstructor constr) -- the symbol is a constructor
+    Just constr -> return (PatternScopedConstructor constr)
     Nothing -> case n of
-      NameUnqualified {} -> PatternScopedVar <$> bindVariableSymbol sym -- the symbol is a variable
+      NameUnqualified {} -> do
+        pk <- ask
+        PatternScopedVar
+          <$> case pk of
+            PatternNamesKindVariables ->
+              bindVariableSymbol sym
+            PatternNamesKindFunctions -> do
+              bindFun sym
       NameQualified {} -> nameNotInScope n
   where
     sym = snd (splitName n)
     getConstructorRef :: Sem r (Maybe ScopedIden)
     getConstructorRef = lookupNameOfKind KNameConstructor n
 
+checkPatternName ::
+  forall r.
+  (Members '[Reader PatternNamesKind, Error ScoperError, State Scope, NameIdGen, State ScoperState, State ScoperSyntax, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) =>
+  Name ->
+  Sem r PatternScopedIden
+checkPatternName = checkPatternName' getReservedDefinitionSymbol
+
+reservePatternName ::
+  forall r.
+  (Members '[Error ScoperError, State Scope, NameIdGen, State ScoperState, State ScoperSyntax, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) =>
+  Name ->
+  Sem r PatternScopedIden
+reservePatternName =
+  runReader PatternNamesKindFunctions
+    . checkPatternName' (reserveSymbolOf SKNameFunction Nothing Nothing)
+
 nameNotInScope :: forall r a. (Members '[Error ScoperError, State Scope] r) => Name -> Sem r a
 nameNotInScope n = err >>= throw
   where
@@ -2700,26 +2801,32 @@ checkPatternBinding ::
   PatternBinding ->
   Sem r PatternArg
 checkPatternBinding PatternBinding {..} = do
-  p' <- checkParsePatternAtom _patternBindingPattern
+  p' <- checkParsePatternAtom' _patternBindingPattern
   n' <- bindVariableSymbol _patternBindingName
   if
       | isJust (p' ^. patternArgName) -> throw (ErrDoubleBinderPattern (DoubleBinderPattern n' p'))
       | otherwise -> return (set patternArgName (Just n') p')
 
 checkPatternAtoms ::
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen] r) =>
+  (Members '[Reader PatternNamesKind, Error ScoperError, State Scope, State ScoperState, State ScoperSyntax, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable, NameIdGen] r) =>
   PatternAtoms 'Parsed ->
   Sem r (PatternAtoms 'Scoped)
 checkPatternAtoms (PatternAtoms s i) = (`PatternAtoms` i) <$> mapM checkPatternAtom s
 
 checkParsePatternAtoms ::
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen] r) =>
+  (Members '[Reader PatternNamesKind, Error ScoperError, State Scope, State ScoperState, State ScoperSyntax, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable, NameIdGen] r) =>
   PatternAtoms 'Parsed ->
   Sem r PatternArg
 checkParsePatternAtoms = checkPatternAtoms >=> parsePatternAtoms
 
-checkPatternAtom ::
+checkParsePatternAtoms' ::
   (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen] r) =>
+  PatternAtoms 'Parsed ->
+  Sem r PatternArg
+checkParsePatternAtoms' = localBindings . ignoreSyntax . runReader PatternNamesKindVariables . checkParsePatternAtoms
+
+checkPatternAtom ::
+  (Members '[Reader PatternNamesKind, Error ScoperError, State Scope, State ScoperState, State ScoperSyntax, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable, NameIdGen] r) =>
   PatternAtom 'Parsed ->
   Sem r (PatternAtom 'Scoped)
 checkPatternAtom = \case
@@ -2985,8 +3092,8 @@ checkIterator iter = do
   let initAssignKws = iter ^.. iteratorInitializers . each . initializerAssignKw
       rangesInKws = iter ^.. iteratorRanges . each . rangeInKw
   withLocalScope $ do
-    inipats' <- mapM (checkParsePatternAtoms . (^. initializerPattern)) (iter ^. iteratorInitializers)
-    rngpats' <- mapM (checkParsePatternAtoms . (^. rangePattern)) (iter ^. iteratorRanges)
+    inipats' <- mapM (checkParsePatternAtoms' . (^. initializerPattern)) (iter ^. iteratorInitializers)
+    rngpats' <- mapM (checkParsePatternAtoms' . (^. rangePattern)) (iter ^. iteratorRanges)
     let _iteratorInitializers = [Initializer p k v | ((p, k), v) <- zipExact (zipExact inipats' initAssignKws) inivals']
         _iteratorRanges = [Range p k v | ((p, k), v) <- zipExact (zipExact rngpats' rangesInKws) rngvals']
         _iteratorParens = iter ^. iteratorParens
@@ -2999,7 +3106,7 @@ checkInitializer ::
   Initializer 'Parsed ->
   Sem r (Initializer 'Scoped)
 checkInitializer ini = do
-  _initializerPattern <- checkParsePatternAtoms (ini ^. initializerPattern)
+  _initializerPattern <- checkParsePatternAtoms' (ini ^. initializerPattern)
   _initializerExpression <- checkParseExpressionAtoms (ini ^. initializerExpression)
   return
     Initializer
@@ -3012,7 +3119,7 @@ checkRange ::
   Range 'Parsed ->
   Sem r (Range 'Scoped)
 checkRange rng = do
-  _rangePattern <- checkParsePatternAtoms (rng ^. rangePattern)
+  _rangePattern <- checkParsePatternAtoms' (rng ^. rangePattern)
   _rangeExpression <- checkParseExpressionAtoms (rng ^. rangeExpression)
   return
     Range
@@ -3106,11 +3213,17 @@ checkParseExpressionAtoms ::
 checkParseExpressionAtoms = checkExpressionAtoms >=> parseExpressionAtoms
 
 checkParsePatternAtom ::
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen] r) =>
+  (Members '[Reader PatternNamesKind, Error ScoperError, State Scope, State ScoperState, State ScoperSyntax, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable, NameIdGen] r) =>
   PatternAtom 'Parsed ->
   Sem r PatternArg
 checkParsePatternAtom = checkPatternAtom >=> parsePatternAtom
 
+checkParsePatternAtom' ::
+  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen] r) =>
+  PatternAtom 'Parsed ->
+  Sem r PatternArg
+checkParsePatternAtom' = localBindings . ignoreSyntax . runReader PatternNamesKindVariables . checkParsePatternAtom
+
 checkSyntaxDef ::
   (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader PackageId, State ScoperSyntax] r) =>
   SyntaxDef 'Parsed ->
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
index f823c79f47..396ce5060c 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@@ -481,6 +481,8 @@ derivingInstance = do
   _derivingFunLhs <- functionDefinitionLhs opts Nothing
   unless (isJust (_derivingFunLhs ^. funLhsInstance)) $
     parseFailure off "Expected `deriving instance`"
+  when (has _FunctionDefNamePattern (_derivingFunLhs ^. funLhsName)) $
+    parseFailure off "Patterns not allowed for `deriving instance`"
   return Deriving {..}
 
 statement :: (Members '[Error ParserError, ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (Statement 'Parsed)
@@ -1332,13 +1334,21 @@ functionDefinitionLhs opts _funLhsBuiltin = P.label "<function definition>" $ do
     parseFailure off0 "instance not allowed here"
   when (isJust _funLhsCoercion && isNothing _funLhsInstance) $
     parseFailure off0 "expected: instance"
-  _funLhsName <- symbol
+  mname <- optional . P.try $ do
+    n <- symbol
+    P.notFollowedBy (kw kwAt)
+    return n
+  _funLhsName <- case mname of
+    Nothing -> FunctionDefNamePattern <$> patternAtom
+    Just fname -> return (FunctionDefName fname)
   let sigOpts =
         SigOptions
           { _sigAllowDefault = True,
             _sigAllowOmitType = allowOmitType
           }
   _funLhsTypeSig <- typeSig sigOpts
+  when (isNothing (_funLhsName ^? _FunctionDefName) && notNull (_funLhsTypeSig ^. typeSigArgs)) $
+    parseFailure off "expected function name"
   return
     FunctionLhs
       { _funLhsInstance,
@@ -1399,6 +1409,7 @@ functionDefinition ::
   Maybe (WithLoc BuiltinFunction) ->
   ParsecS r (FunctionDef 'Parsed)
 functionDefinition opts _signBuiltin = P.label "<function definition>" $ do
+  off0 <- P.getOffset
   FunctionLhs {..} <- functionDefinitionLhs opts _signBuiltin
   off <- P.getOffset
   _signDoc <- getJudoc
@@ -1409,18 +1420,21 @@ functionDefinition opts _signBuiltin = P.label "<function definition>" $ do
         || (P.isBodyExpression _signBody && null (_funLhsTypeSig ^. typeSigArgs))
     )
     $ parseFailure off "expected result type"
-  return
-    FunctionDef
-      { _signName = _funLhsName,
-        _signTypeSig = _funLhsTypeSig,
-        _signTerminating = _funLhsTerminating,
-        _signInstance = _funLhsInstance,
-        _signCoercion = _funLhsCoercion,
-        _signBuiltin = _funLhsBuiltin,
-        _signDoc,
-        _signPragmas,
-        _signBody
-      }
+  let fdef =
+        FunctionDef
+          { _signName = _funLhsName,
+            _signTypeSig = _funLhsTypeSig,
+            _signTerminating = _funLhsTerminating,
+            _signInstance = _funLhsInstance,
+            _signCoercion = _funLhsCoercion,
+            _signBuiltin = _funLhsBuiltin,
+            _signDoc,
+            _signPragmas,
+            _signBody
+          }
+  when (isNothing (_funLhsName ^? _FunctionDefName) && P.isFunctionLike fdef) $
+    parseFailure off0 "expected function name"
+  return fdef
   where
     parseBody :: ParsecS r (FunctionDefBody 'Parsed)
     parseBody =
diff --git a/src/Juvix/Compiler/Internal/Extra.hs b/src/Juvix/Compiler/Internal/Extra.hs
index f1f3d133d7..8d27539ed7 100644
--- a/src/Juvix/Compiler/Internal/Extra.hs
+++ b/src/Juvix/Compiler/Internal/Extra.hs
@@ -162,6 +162,62 @@ genFieldProjection kind _funDefName _funDefType _funDefBuiltin _funDefArgsInfo m
             _lambdaClauses = pure cl
           }
 
+-- | Generates definitions for each variable in a given pattern.
+genPatternDefs ::
+  forall r.
+  (Members '[NameIdGen] r) =>
+  Name ->
+  PatternArg ->
+  Sem r [FunctionDef]
+genPatternDefs valueName pat =
+  execOutputList $ goPatternArg pat
+  where
+    goPatternArg :: PatternArg -> Sem (Output FunctionDef ': r) ()
+    goPatternArg PatternArg {..} = do
+      whenJust _patternArgName goPatternVariable
+      goPattern _patternArgPattern
+
+    goPattern :: Pattern -> Sem (Output FunctionDef ': r) ()
+    goPattern = \case
+      PatternVariable x -> goPatternVariable x
+      PatternWildcardConstructor {} -> return ()
+      PatternConstructorApp x -> goPatternConstructorApp x
+
+    goPatternVariable :: VarName -> Sem (Output FunctionDef ': r) ()
+    goPatternVariable var = do
+      h <- freshHole (getLoc valueName)
+      let body =
+            ExpressionCase
+              Case
+                { _caseExpression = ExpressionIden (IdenFunction valueName),
+                  _caseExpressionType = Nothing,
+                  _caseExpressionWholeType = Nothing,
+                  _caseBranches =
+                    pure $
+                      CaseBranch
+                        { _caseBranchPattern = pat,
+                          _caseBranchRhs =
+                            CaseBranchRhsExpression (ExpressionIden (IdenVar var))
+                        }
+                }
+      body' <- clone body
+      output $
+        FunctionDef
+          { _funDefTerminating = False,
+            _funDefIsInstanceCoercion = Nothing,
+            _funDefPragmas = mempty,
+            _funDefBody = body',
+            _funDefDocComment = Nothing,
+            _funDefType = ExpressionHole h,
+            _funDefName = var,
+            _funDefBuiltin = Nothing,
+            _funDefArgsInfo = []
+          }
+
+    goPatternConstructorApp :: ConstructorApp -> Sem (Output FunctionDef ': r) ()
+    goPatternConstructorApp ConstructorApp {..} = do
+      forM_ _constrAppParameters goPatternArg
+
 buildLetMutualBlocks ::
   NonEmpty PreLetStatement ->
   NonEmpty (SCC PreLetStatement)
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index a9bd8fc1aa..9a6b85f731 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -294,11 +294,12 @@ goModuleBody stmts = evalState emptyLocalTable $ do
   _moduleImports <- mapM goImport (scanImports stmts)
   otherThanFunctions :: [Indexed Internal.PreStatement] <- concatMapM (traverseM' goAxiomInductive) ss
   funs :: [Indexed Internal.PreStatement] <-
-    sequence
-      [ Indexed i . Internal.PreFunctionDef <$> d
-        | Indexed i s <- ss,
-          Just d <- [mkFunctionLike s]
-      ]
+    concat
+      <$> sequence
+        [ return . map (Indexed i . Internal.PreFunctionDef) =<< defs
+          | Indexed i s <- ss,
+            let defs = mkFunctionLike s
+        ]
   let unsorted = otherThanFunctions <> funs
       _moduleStatements = map (^. indexedThing) (sortOn (^. indexedIx) unsorted)
   return Internal.ModuleBody {..}
@@ -309,17 +310,17 @@ goModuleBody stmts = evalState emptyLocalTable $ do
     ss :: [Indexed (Statement 'Scoped)]
     ss = zipWith Indexed [0 ..] ss'
 
-    mkFunctionLike :: Statement 'Scoped -> Maybe (Sem (State LocalTable ': r) (Internal.FunctionDef))
+    mkFunctionLike :: Statement 'Scoped -> Sem (State LocalTable ': r) [Internal.FunctionDef]
     mkFunctionLike s = case s of
-      StatementFunctionDef d -> Just (goFunctionDef d)
-      StatementProjectionDef d -> Just (goProjectionDef d)
-      StatementDeriving d -> Just (goDeriving d)
-      StatementSyntax {} -> Nothing
-      StatementImport {} -> Nothing
-      StatementInductive {} -> Nothing
-      StatementModule {} -> Nothing
-      StatementOpenModule {} -> Nothing
-      StatementAxiom {} -> Nothing
+      StatementFunctionDef d -> goFunctionDef d
+      StatementProjectionDef d -> goProjectionDef d >>= return . pure
+      StatementDeriving d -> goDeriving d >>= return . pure
+      StatementSyntax {} -> return []
+      StatementImport {} -> return []
+      StatementInductive {} -> return []
+      StatementModule {} -> return []
+      StatementOpenModule {} -> return []
+      StatementAxiom {} -> return []
 
 scanImports :: [Statement 'Scoped] -> [Import 'Scoped]
 scanImports = mconcatMap go
@@ -417,7 +418,7 @@ goDeriving ::
   Sem r Internal.FunctionDef
 goDeriving Deriving {..} = do
   let FunctionLhs {..} = _derivingFunLhs
-      name = goSymbol _funLhsName
+      name = goSymbol (_funLhsName ^. functionDefName)
   (funArgs, ret) <- Internal.unfoldFunType <$> goDefType _derivingFunLhs
   let (mtrait, traitArgs) = Internal.unfoldExpressionApp ret
   (n, der) <- findDerivingTrait mtrait
@@ -671,9 +672,9 @@ goFunctionDef ::
   forall r.
   (Members '[Reader DefaultArgsStack, Reader Pragmas, Error ScoperError, NameIdGen, Reader S.InfoTable] r) =>
   FunctionDef 'Scoped ->
-  Sem r Internal.FunctionDef
+  Sem r [Internal.FunctionDef]
 goFunctionDef def@FunctionDef {..} = do
-  let _funDefName = goSymbol _signName
+  let _funDefName = goSymbol (_signName ^. functionDefName)
       _funDefTerminating = isJust _signTerminating
       _funDefIsInstanceCoercion
         | isJust _signCoercion = Just Internal.IsInstanceCoercionCoercion
@@ -688,7 +689,12 @@ goFunctionDef def@FunctionDef {..} = do
   let _funDefDocComment = fmap ppPrintJudoc _signDoc
       fun = Internal.FunctionDef {..}
   whenJust _signBuiltin (checkBuiltinFunction fun . (^. withLocParam))
-  return fun
+  case _signName ^. functionDefNamePattern of
+    Just pat -> do
+      pat' <- goPatternArg pat
+      (fun :) <$> Internal.genPatternDefs _funDefName pat'
+    Nothing ->
+      return [fun]
   where
     goBody :: Sem r Internal.Expression
     goBody = do
@@ -750,11 +756,9 @@ goDefType FunctionLhs {..} = do
   return (Internal.foldFunType args ret)
   where
     freshHole :: Sem r Internal.Expression
-    freshHole = do
-      i <- freshNameId
-      let loc = maybe (getLoc _funLhsName) getLoc (lastMay (_funLhsTypeSig ^. typeSigArgs))
-          h = mkHole loc i
-      return $ Internal.ExpressionHole h
+    freshHole =
+      Internal.ExpressionHole
+        <$> Internal.freshHole (maybe (getLoc _funLhsName) getLoc (lastMay (_funLhsTypeSig ^. typeSigArgs)))
 
     argToParam :: SigArg 'Scoped -> Sem r (NonEmpty Internal.FunctionParameter)
     argToParam a@SigArg {..} = do
@@ -1093,7 +1097,7 @@ createArgumentBlocks appargs =
   where
     namedArgumentRefSymbol :: NamedArgumentNew 'Scoped -> S.Symbol
     namedArgumentRefSymbol = \case
-      NamedArgumentNewFunction p -> p ^. namedArgumentFunctionDef . signName
+      NamedArgumentNewFunction p -> p ^. namedArgumentFunctionDef . signName . functionDefName
       NamedArgumentItemPun p -> over S.nameConcrete fromUnqualified' (p ^. namedArgumentReferencedSymbol . scopedIdenFinal)
     args0 :: HashSet S.Symbol = hashSet (namedArgumentRefSymbol <$> appargs)
     goBlock ::
@@ -1186,7 +1190,13 @@ goExpression = \case
           Nothing -> return compiledNameApp
           Just funs -> do
             cls <- funDefsToClauses funs
-            let funsNames :: [Internal.Name] = funs ^.. each . namedArgumentFunctionDef . signName . to goSymbol
+            let funsNames :: [Internal.Name] =
+                  funs
+                    ^.. each
+                      . namedArgumentFunctionDef
+                      . signName
+                      . functionDefName
+                      . to goSymbol
                 -- changes the kind from Variable to Function
                 updateKind :: Internal.Subs = Internal.subsKind funsNames KNameFunction
             let l =
@@ -1198,10 +1208,10 @@ goExpression = \case
             Internal.clone expr
             where
               funDefsToClauses :: NonEmpty (NamedArgumentFunctionDef 'Scoped) -> Sem r (NonEmpty Internal.LetClause)
-              funDefsToClauses args = mkLetClauses <$> mapM goArg args
+              funDefsToClauses args = (mkLetClauses . nonEmpty') <$> concatMapM goArg (toList args)
                 where
-                  goArg :: NamedArgumentFunctionDef 'Scoped -> Sem r Internal.PreLetStatement
-                  goArg = fmap Internal.PreLetFunctionDef . goFunctionDef . (^. namedArgumentFunctionDef)
+                  goArg :: NamedArgumentFunctionDef 'Scoped -> Sem r [Internal.PreLetStatement]
+                  goArg = fmap (map Internal.PreLetFunctionDef) . goFunctionDef . (^. namedArgumentFunctionDef)
 
     goDesugaredNamedApplication :: DesugaredNamedApplication -> Sem r Internal.Expression
     goDesugaredNamedApplication a = do
@@ -1466,13 +1476,13 @@ goLetFunDefs ::
 goLetFunDefs clauses = maybe [] (toList . mkLetClauses) . nonEmpty <$> preLetStatements clauses
   where
     preLetStatements :: NonEmpty (LetStatement 'Scoped) -> Sem r [Internal.PreLetStatement]
-    preLetStatements cl = mapMaybeM preLetStatement (toList cl)
+    preLetStatements cl = concatMapM preLetStatement (toList cl)
       where
-        preLetStatement :: LetStatement 'Scoped -> Sem r (Maybe Internal.PreLetStatement)
+        preLetStatement :: LetStatement 'Scoped -> Sem r [Internal.PreLetStatement]
         preLetStatement = \case
-          LetFunctionDef f -> Just . Internal.PreLetFunctionDef <$> goFunctionDef f
-          LetAliasDef {} -> return Nothing
-          LetOpen {} -> return Nothing
+          LetFunctionDef f -> map Internal.PreLetFunctionDef <$> goFunctionDef f
+          LetAliasDef {} -> return []
+          LetOpen {} -> return []
 
 goDo ::
   forall r.
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs
index 1989a3c98e..f253ef5c12 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs
@@ -613,7 +613,11 @@ inferExpression ::
   Sem r TypedExpression
 inferExpression hint = resolveInstanceHoles . resolveCastHoles . inferExpression' hint
 
-lookupVar :: (Members '[Reader LocalVars, Reader InfoTable] r) => Name -> Sem r Expression
+lookupVar ::
+  (HasCallStack) =>
+  (Members '[Reader LocalVars, Reader InfoTable] r) =>
+  Name ->
+  Sem r Expression
 lookupVar v = do
   locals <- asks (^. localTypes)
   return $ fromMaybe err (locals ^. at v)
diff --git a/src/Juvix/Compiler/Pipeline/Package/Loader.hs b/src/Juvix/Compiler/Pipeline/Package/Loader.hs
index 38bff632ca..7c24a72d36 100644
--- a/src/Juvix/Compiler/Pipeline/Package/Loader.hs
+++ b/src/Juvix/Compiler/Pipeline/Package/Loader.hs
@@ -81,7 +81,7 @@ toConcrete t p = run . runReader l $ do
     funDef = do
       packageTypeIdentifier <- identifier (t ^. packageDescriptionTypeName)
       _typeSigRetType <- Just <$> expressionAtoms' (packageTypeIdentifier :| [])
-      _signName <- symbol Str.package
+      name' <- symbol Str.package
       _typeSigColonKw <- Irrelevant . Just <$> kw kwColon
       let _signBody = (t ^. packageDescriptionTypeTransform) p
           _signTypeSig =
@@ -99,7 +99,7 @@ toConcrete t p = run . runReader l $ do
                 _signDoc = Nothing,
                 _signCoercion = Nothing,
                 _signBuiltin = Nothing,
-                _signName,
+                _signName = FunctionDefName name',
                 _signBody,
                 _signTypeSig
               }
diff --git a/test/Compilation/Negative.hs b/test/Compilation/Negative.hs
index f0def9172f..a860e46541 100644
--- a/test/Compilation/Negative.hs
+++ b/test/Compilation/Negative.hs
@@ -81,5 +81,9 @@ tests =
     NegTest
       "Test013: Redundant side condition detection"
       $(mkRelDir ".")
-      $(mkRelFile "test013.juvix")
+      $(mkRelFile "test013.juvix"),
+    NegTest
+      "Test014: Non-exhaustive left-hand side pattern"
+      $(mkRelDir ".")
+      $(mkRelFile "test014.juvix")
   ]
diff --git a/test/Compilation/Positive.hs b/test/Compilation/Positive.hs
index b7afcd21c1..3a46fc3a69 100644
--- a/test/Compilation/Positive.hs
+++ b/test/Compilation/Positive.hs
@@ -500,5 +500,10 @@ tests =
         "Test085: Deriving Eq"
         $(mkRelDir ".")
         $(mkRelFile "test085.juvix")
-        $(mkRelFile "out/test085.out")
+        $(mkRelFile "out/test085.out"),
+      posTest
+        "Test086: Patterns in definitions"
+        $(mkRelDir ".")
+        $(mkRelFile "test086.juvix")
+        $(mkRelFile "out/test086.out")
     ]
diff --git a/tests/Compilation/negative/test014.juvix b/tests/Compilation/negative/test014.juvix
new file mode 100644
index 0000000000..13f962a086
--- /dev/null
+++ b/tests/Compilation/negative/test014.juvix
@@ -0,0 +1,16 @@
+-- Non-exhaustive left-hand side pattern
+module test014;
+
+import Stdlib.Data.Nat open;
+
+type Tree A :=
+  | Leaf
+  | Node A (Tree A) (Tree A);
+
+t : Tree Nat :=
+  Node 1 Leaf Leaf;
+
+main : Nat :=
+  let
+    (Node x _ _) := t
+  in x;
diff --git a/tests/Compilation/positive/out/test086.out b/tests/Compilation/positive/out/test086.out
new file mode 100644
index 0000000000..60d3b2f4a4
--- /dev/null
+++ b/tests/Compilation/positive/out/test086.out
@@ -0,0 +1 @@
+15
diff --git a/tests/Compilation/positive/test086.juvix b/tests/Compilation/positive/test086.juvix
new file mode 100644
index 0000000000..63094d7e15
--- /dev/null
+++ b/tests/Compilation/positive/test086.juvix
@@ -0,0 +1,31 @@
+module test086;
+
+import Stdlib.Prelude open;
+
+f (p : Pair Nat Nat) : Nat :=
+  let
+    (x, y) := p;
+  in x + 2 * y;
+
+type R :=
+  mkR@{
+    x : Nat;
+    y : Nat;
+  };
+
+rr : R :=
+  mkR@{
+    x := 1;
+    y := 2;
+  };
+
+(px, py) : Pair Nat Nat := (1, 2);
+
+g (r : R) : Nat :=
+  let
+    mkR@{x := x; y} := r
+  in x + 2 * y;
+
+mkR@{x := rx; y := ry} : R := rr;
+
+main : Nat := f (px, py) + g rr + f (rx, ry);