From 8cd3a62e7505aa4ce4c1092e3ac2de3c65d5846c Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Wed, 20 Nov 2024 11:28:19 +0100
Subject: [PATCH 01/15] patterns in FunctionDef (wip)

---
 juvix-stdlib                                  |  2 +-
 src/Juvix/Compiler/Concrete/Extra.hs          |  2 +-
 src/Juvix/Compiler/Concrete/Gen.hs            | 20 ++++++++-
 src/Juvix/Compiler/Concrete/Language.hs       |  2 +-
 src/Juvix/Compiler/Concrete/Language/Base.hs  | 43 +++++++++++++++----
 src/Juvix/Compiler/Concrete/Print/Base.hs     |  2 +-
 .../FromParsed/Analysis/Scoping.hs            | 12 +++---
 .../Concrete/Translation/FromSource.hs        | 37 ++++++++++------
 src/Juvix/Compiler/Pipeline/Package/Loader.hs |  6 ++-
 9 files changed, 91 insertions(+), 35 deletions(-)

diff --git a/juvix-stdlib b/juvix-stdlib
index f0a1e1ed77..0080b1183a 160000
--- a/juvix-stdlib
+++ b/juvix-stdlib
@@ -1 +1 @@
-Subproject commit f0a1e1ed77e9e94467434b85736839e110d021d5
+Subproject commit 0080b1183ab55e5180e69bfc3987e4cd6edbc230
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..c42b643113 100644
--- a/src/Juvix/Compiler/Concrete/Gen.hs
+++ b/src/Juvix/Compiler/Concrete/Gen.hs
@@ -24,10 +24,11 @@ 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,
+      _signPattern = pat,
       _signBody = SigBodyExpression funBody,
       _signTypeSig =
         TypeSig
@@ -42,6 +43,21 @@ simplestFunctionDef funName funBody =
       _signInstance = Nothing,
       _signCoercion = Nothing
     }
+  where
+    pat :: PatternAtomType s
+    pat = case sing :: SStage s of
+      SParsed -> PatternAtomIden (NameUnqualified funName)
+      SScoped ->
+        PatternArg
+          { _patternArgPattern = PatternVariable funName,
+            _patternArgName = Nothing,
+            _patternArgIsImplicit = Explicit
+          }
+
+    name :: FunctionSymbolType s
+    name = case sing :: SStage s of
+      SParsed -> Just funName
+      SScoped -> funName
 
 smallUniverseExpression :: forall s r. (SingI s) => (Members '[Reader Interval] r) => Sem r (ExpressionType s)
 smallUniverseExpression = do
diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs
index 6b332ab8b8..3f226929db 100644
--- a/src/Juvix/Compiler/Concrete/Language.hs
+++ b/src/Juvix/Compiler/Concrete/Language.hs
@@ -30,7 +30,7 @@ statementLabel = \case
   StatementSyntax s -> goSyntax s
   StatementOpenModule {} -> Nothing
   StatementProjectionDef {} -> Nothing
-  StatementFunctionDef f -> Just (f ^. signName . symbolTypeLabel)
+  StatementFunctionDef f -> withFunctionSymbol Nothing (Just . (^. symbolTypeLabel)) (f ^. signName)
   StatementDeriving f -> Just (f ^. derivingFunLhs . funLhsName . symbolTypeLabel)
   StatementImport i -> Just (i ^. importModulePath . to modulePathTypeLabel)
   StatementInductive i -> Just (i ^. inductiveName . symbolTypeLabel)
diff --git a/src/Juvix/Compiler/Concrete/Language/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs
index 6fbe2cc3b5..850a69a64d 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 = Maybe Symbol
+  FunctionSymbolType 'Scoped = S.Symbol
+
 type IdentifierType :: Stage -> GHCType
 type family IdentifierType s = res | res -> s where
   IdentifierType 'Parsed = Name
@@ -702,7 +707,10 @@ deriving stock instance Ord (Deriving 'Parsed)
 deriving stock instance Ord (Deriving 'Scoped)
 
 data FunctionDef (s :: Stage) = FunctionDef
-  { _signName :: FunctionName s,
+  { -- _signName must be a `Just` if the definition is
+    -- function-like: _signArgs is not empty or _signBody is SigBodyClauses
+    _signName :: FunctionSymbolType s,
+    _signPattern :: PatternAtomType s,
     _signTypeSig :: TypeSig s,
     _signDoc :: Maybe (Judoc s),
     _signPragmas :: Maybe ParsedPragmas,
@@ -2860,7 +2868,8 @@ data FunctionLhs (s :: Stage) = FunctionLhs
     _funLhsTerminating :: Maybe KeywordRef,
     _funLhsInstance :: Maybe KeywordRef,
     _funLhsCoercion :: Maybe KeywordRef,
-    _funLhsName :: FunctionName s,
+    _funLhsName :: FunctionSymbolType s,
+    _funLhsPattern :: PatternAtomType s,
     _funLhsTypeSig :: TypeSig s
   }
   deriving stock (Generic)
@@ -2984,6 +2993,7 @@ functionDefLhs FunctionDef {..} =
       _funLhsInstance = _signInstance,
       _funLhsCoercion = _signCoercion,
       _funLhsName = _signName,
+      _funLhsPattern = _signPattern,
       _funLhsTypeSig = _signTypeSig
     }
 
@@ -3396,8 +3406,8 @@ instance (SingI s) => HasLoc (FunctionDef s) where
       ?<> (getLoc <$> _signPragmas)
       ?<> (getLoc <$> _signBuiltin)
       ?<> (getLoc <$> _signTerminating)
-      ?<> getLocSymbolType _signName
-      <> (getLoc _signBody)
+      ?<> getLocPatternAtomType _signPattern
+      <> getLoc _signBody
 
 instance HasLoc (Example s) where
   getLoc e = e ^. exampleLoc
@@ -3433,6 +3443,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 +3596,27 @@ 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 -> fromJust sym
+  SScoped -> sym
+
+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
+  SScoped -> f sym
+
 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 (fromJust (a ^. namedArgumentFunctionDef . signName))
+    return $ NamedArgumentNewFunction (over namedArgumentFunctionDef (set signName (Just 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..3806d29c9b 100644
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Print/Base.hs
@@ -1168,7 +1168,7 @@ 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)
+        name' = withFunctionSymbol id annDef _funLhsName (ppPatternAtomType _funLhsPattern)
         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..e32f939f84 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@@ -407,7 +407,7 @@ reserveFunctionSymbol ::
   FunctionLhs 'Parsed ->
   Sem r S.Symbol
 reserveFunctionSymbol f =
-  reserveSymbolSignatureOf SKNameFunction f (toBuiltinPrim <$> f ^. funLhsBuiltin) (f ^. funLhsName)
+  reserveSymbolSignatureOf SKNameFunction f (toBuiltinPrim <$> f ^. funLhsBuiltin) (fromJust (f ^. funLhsName))
 
 reserveAxiomSymbol ::
   (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) =>
@@ -1075,7 +1075,7 @@ checkDeriving Deriving {..} = do
   typeSig' <- withLocalScope (checkTypeSig _funLhsTypeSig)
   name' <-
     if
-        | P.isLhsFunctionLike lhs -> getReservedDefinitionSymbol _funLhsName
+        | P.isLhsFunctionLike lhs -> getReservedDefinitionSymbol (fromJust _funLhsName)
         | otherwise -> reserveFunctionSymbol lhs
   let lhs' =
         FunctionLhs
@@ -1138,17 +1138,19 @@ checkFunctionDef ::
   Sem r (FunctionDef 'Scoped)
 checkFunctionDef fdef@FunctionDef {..} = do
   sigDoc' <- mapM checkJudoc _signDoc
-  (sig', sigBody') <- withLocalScope $ do
+  (sig', sigPattern', sigBody') <- withLocalScope $ do
     a' <- checkTypeSig _signTypeSig
+    p' <- checkParsePatternAtom _signPattern
     b' <- checkBody
-    return (a', b')
+    return (a', p', b')
   sigName' <-
     if
-        | P.isFunctionLike fdef -> getReservedDefinitionSymbol _signName
+        | P.isFunctionLike fdef -> getReservedDefinitionSymbol (fromJust _signName)
         | otherwise -> reserveFunctionSymbol (functionDefLhs fdef)
   let def =
         FunctionDef
           { _signName = sigName',
+            _signPattern = sigPattern',
             _signDoc = sigDoc',
             _signBody = sigBody',
             _signTypeSig = sig',
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
index f823c79f47..22859b9d2b 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@@ -1332,18 +1332,24 @@ 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
+  _funLhsPattern <- patternAtom
+  let _funLhsName = case _funLhsPattern of
+        PatternAtomIden (NameUnqualified s) -> Just s
+        _ -> Nothing
   let sigOpts =
         SigOptions
           { _sigAllowDefault = True,
             _sigAllowOmitType = allowOmitType
           }
   _funLhsTypeSig <- typeSig sigOpts
+  when (isNothing _funLhsName && not (null (_funLhsTypeSig ^. typeSigArgs))) $
+    parseFailure off "expected function name"
   return
     FunctionLhs
       { _funLhsInstance,
         _funLhsBuiltin,
         _funLhsCoercion,
+        _funLhsPattern,
         _funLhsName,
         _funLhsTypeSig,
         _funLhsTerminating
@@ -1399,6 +1405,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 +1416,22 @@ 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,
+            _signPattern = _funLhsPattern,
+            _signTypeSig = _funLhsTypeSig,
+            _signTerminating = _funLhsTerminating,
+            _signInstance = _funLhsInstance,
+            _signCoercion = _funLhsCoercion,
+            _signBuiltin = _funLhsBuiltin,
+            _signDoc,
+            _signPragmas,
+            _signBody
+          }
+  when (isNothing _funLhsName && not (P.isFunctionLike fdef)) $
+    parseFailure off0 "expected function name"
+  return fdef
   where
     parseBody :: ParsecS r (FunctionDefBody 'Parsed)
     parseBody =
diff --git a/src/Juvix/Compiler/Pipeline/Package/Loader.hs b/src/Juvix/Compiler/Pipeline/Package/Loader.hs
index 38bff632ca..dad2e3d685 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 =
@@ -90,6 +90,7 @@ toConcrete t p = run . runReader l $ do
                 _typeSigRetType,
                 _typeSigColonKw
               }
+          _signPattern = PatternAtomIden (NameUnqualified name')
       return
         ( StatementFunctionDef
             FunctionDef
@@ -99,7 +100,8 @@ toConcrete t p = run . runReader l $ do
                 _signDoc = Nothing,
                 _signCoercion = Nothing,
                 _signBuiltin = Nothing,
-                _signName,
+                _signName = Just name',
+                _signPattern,
                 _signBody,
                 _signTypeSig
               }

From c951840dba2e367c6e5e105aa94a328b9956d64b Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Wed, 20 Nov 2024 16:17:31 +0100
Subject: [PATCH 02/15] fix scoping

---
 .../FromParsed/Analysis/Scoping.hs            | 137 ++++++++++++++----
 1 file changed, 111 insertions(+), 26 deletions(-)

diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
index e32f939f84..763a77f7d3 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 ->
@@ -446,6 +450,48 @@ 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
+        void (reservePatternName (NameUnqualified _recordPatternAssignField))
+        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
@@ -1138,15 +1184,18 @@ checkFunctionDef ::
   Sem r (FunctionDef 'Scoped)
 checkFunctionDef fdef@FunctionDef {..} = do
   sigDoc' <- mapM checkJudoc _signDoc
+  let isFun = P.isFunctionLike fdef
+  when (not isFun) $
+    reservePatternFunctionSymbols _signPattern
+  sigName' <-
+    if
+        | isFun -> getReservedDefinitionSymbol (fromJust _signName)
+        | otherwise -> reserveFunctionSymbol (functionDefLhs fdef)
   (sig', sigPattern', sigBody') <- withLocalScope $ do
     a' <- checkTypeSig _signTypeSig
-    p' <- checkParsePatternAtom _signPattern
+    p' <- runReader PatternNamesKindFunctions $ checkParsePatternAtom _signPattern
     b' <- checkBody
     return (a', p', b')
-  sigName' <-
-    if
-        | P.isFunctionLike fdef -> getReservedDefinitionSymbol (fromJust _signName)
-        | otherwise -> reserveFunctionSymbol (functionDefLhs fdef)
   let def =
         FunctionDef
           { _signName = sigName',
@@ -1167,7 +1216,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
@@ -2256,7 +2305,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
@@ -2278,7 +2327,7 @@ checkRecordPattern r = do
     noFields = ErrConstructorNotARecord . ConstructorNotARecord
     checkItem ::
       forall r'.
-      (Members '[Reader (RecordNameSignature 'Parsed), Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen] r') =>
+      (Members '[Reader PatternNamesKind, Reader (RecordNameSignature 'Parsed), Error ScoperError, State Scope, State ScoperState, State ScoperSyntax, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable, NameIdGen] r') =>
       RecordPatternItem 'Parsed ->
       Sem r' (RecordPatternItem 'Scoped)
     checkItem = \case
@@ -2316,7 +2365,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
@@ -2451,7 +2500,7 @@ checkCaseBranch ::
   CaseBranch 'Parsed ->
   Sem r (CaseBranch 'Scoped)
 checkCaseBranch CaseBranch {..} = withLocalScope $ do
-  pattern' <- checkParsePatternAtoms _caseBranchPattern
+  pattern' <- checkParsePatternAtoms' _caseBranchPattern
   rhs' <- checkCaseBranchRhs _caseBranchRhs
   return $
     CaseBranch
@@ -2466,7 +2515,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
@@ -2575,7 +2624,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
@@ -2642,23 +2691,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 ->
+              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' bindFunctionSymbol
+
+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
@@ -2702,26 +2775,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
@@ -2987,8 +3066,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
@@ -3001,7 +3080,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
@@ -3014,7 +3093,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
@@ -3108,11 +3187,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 ->

From 13582a9001b723a73c4779c274c82e556c43127f Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Wed, 20 Nov 2024 17:23:48 +0100
Subject: [PATCH 03/15] fix scoping bug

---
 .../Translation/FromParsed/Analysis/Scoping.hs | 18 ++++++++----------
 1 file changed, 8 insertions(+), 10 deletions(-)

diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
index 763a77f7d3..431181e77d 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@@ -1184,18 +1184,16 @@ checkFunctionDef ::
   Sem r (FunctionDef 'Scoped)
 checkFunctionDef fdef@FunctionDef {..} = do
   sigDoc' <- mapM checkJudoc _signDoc
-  let isFun = P.isFunctionLike fdef
-  when (not isFun) $
-    reservePatternFunctionSymbols _signPattern
-  sigName' <-
-    if
-        | isFun -> getReservedDefinitionSymbol (fromJust _signName)
-        | otherwise -> reserveFunctionSymbol (functionDefLhs fdef)
-  (sig', sigPattern', sigBody') <- withLocalScope $ do
+  (sig', sigBody') <- withLocalScope $ do
     a' <- checkTypeSig _signTypeSig
-    p' <- runReader PatternNamesKindFunctions $ checkParsePatternAtom _signPattern
     b' <- checkBody
-    return (a', p', b')
+    return (a', b')
+  when (not (P.isFunctionLike fdef)) $
+    reservePatternFunctionSymbols _signPattern
+  sigName' <- case _signName of
+    Just name' -> getReservedDefinitionSymbol name'
+    Nothing -> freshSymbol KNameFunction KNameFunction (WithLoc (getLoc _signPattern) "__pattern__")
+  sigPattern' <- runReader PatternNamesKindFunctions $ checkParsePatternAtom _signPattern
   let def =
         FunctionDef
           { _signName = sigName',

From 72fe0cd353ea012c3ebe8752f65b3197c714210b Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Thu, 21 Nov 2024 13:27:23 +0100
Subject: [PATCH 04/15] fix constructor clash

---
 src/Juvix/Compiler/Concrete/Gen.hs            | 12 +---------
 src/Juvix/Compiler/Concrete/Language/Base.hs  | 12 +++++-----
 src/Juvix/Compiler/Concrete/Print/Base.hs     |  4 +++-
 .../FromParsed/Analysis/Scoping.hs            | 24 ++++++++++++++-----
 .../Concrete/Translation/FromSource.hs        | 11 +++++----
 src/Juvix/Compiler/Pipeline/Package/Loader.hs |  2 +-
 6 files changed, 36 insertions(+), 29 deletions(-)

diff --git a/src/Juvix/Compiler/Concrete/Gen.hs b/src/Juvix/Compiler/Concrete/Gen.hs
index c42b643113..5be7526555 100644
--- a/src/Juvix/Compiler/Concrete/Gen.hs
+++ b/src/Juvix/Compiler/Concrete/Gen.hs
@@ -28,7 +28,7 @@ simplestFunctionDef :: forall s. (SingI s) => FunctionName s -> ExpressionType s
 simplestFunctionDef funName funBody =
   FunctionDef
     { _signName = name,
-      _signPattern = pat,
+      _signPattern = Nothing,
       _signBody = SigBodyExpression funBody,
       _signTypeSig =
         TypeSig
@@ -44,16 +44,6 @@ simplestFunctionDef funName funBody =
       _signCoercion = Nothing
     }
   where
-    pat :: PatternAtomType s
-    pat = case sing :: SStage s of
-      SParsed -> PatternAtomIden (NameUnqualified funName)
-      SScoped ->
-        PatternArg
-          { _patternArgPattern = PatternVariable funName,
-            _patternArgName = Nothing,
-            _patternArgIsImplicit = Explicit
-          }
-
     name :: FunctionSymbolType s
     name = case sing :: SStage s of
       SParsed -> Just funName
diff --git a/src/Juvix/Compiler/Concrete/Language/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs
index 850a69a64d..865d19d0f1 100644
--- a/src/Juvix/Compiler/Concrete/Language/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Language/Base.hs
@@ -707,10 +707,10 @@ deriving stock instance Ord (Deriving 'Parsed)
 deriving stock instance Ord (Deriving 'Scoped)
 
 data FunctionDef (s :: Stage) = FunctionDef
-  { -- _signName must be a `Just` if the definition is
-    -- function-like: _signArgs is not empty or _signBody is SigBodyClauses
+  { -- When s = 'Parsed, _signName must be present if the definition is
+    -- function-like. One of _signName or _signPattern must be present.
     _signName :: FunctionSymbolType s,
-    _signPattern :: PatternAtomType s,
+    _signPattern :: Maybe (PatternAtomType s),
     _signTypeSig :: TypeSig s,
     _signDoc :: Maybe (Judoc s),
     _signPragmas :: Maybe ParsedPragmas,
@@ -2869,7 +2869,7 @@ data FunctionLhs (s :: Stage) = FunctionLhs
     _funLhsInstance :: Maybe KeywordRef,
     _funLhsCoercion :: Maybe KeywordRef,
     _funLhsName :: FunctionSymbolType s,
-    _funLhsPattern :: PatternAtomType s,
+    _funLhsPattern :: Maybe (PatternAtomType s),
     _funLhsTypeSig :: TypeSig s
   }
   deriving stock (Generic)
@@ -3406,8 +3406,8 @@ instance (SingI s) => HasLoc (FunctionDef s) where
       ?<> (getLoc <$> _signPragmas)
       ?<> (getLoc <$> _signBuiltin)
       ?<> (getLoc <$> _signTerminating)
-      ?<> getLocPatternAtomType _signPattern
-      <> getLoc _signBody
+      ?<> (getLocPatternAtomType <$> _signPattern)
+      ?<> getLoc _signBody
 
 instance HasLoc (Example s) where
   getLoc e = e ^. exampleLoc
diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
index 3806d29c9b..ca86ed3da9 100644
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Print/Base.hs
@@ -1168,7 +1168,9 @@ 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' = withFunctionSymbol id annDef _funLhsName (ppPatternAtomType _funLhsPattern)
+        name' = case _funLhsPattern 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 431181e77d..3d608c9757 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@@ -351,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
@@ -1188,12 +1189,23 @@ checkFunctionDef fdef@FunctionDef {..} = do
     a' <- checkTypeSig _signTypeSig
     b' <- checkBody
     return (a', b')
-  when (not (P.isFunctionLike fdef)) $
-    reservePatternFunctionSymbols _signPattern
+  whenJust _signPattern $
+    reservePatternFunctionSymbols
   sigName' <- case _signName of
-    Just name' -> getReservedDefinitionSymbol name'
-    Nothing -> freshSymbol KNameFunction KNameFunction (WithLoc (getLoc _signPattern) "__pattern__")
-  sigPattern' <- runReader PatternNamesKindFunctions $ checkParsePatternAtom _signPattern
+    Just name'
+      | P.isFunctionLike fdef ->
+          getReservedDefinitionSymbol name'
+      | otherwise ->
+          reserveFunctionSymbol fdef
+    Nothing ->
+      freshSymbol KNameFunction KNameFunction (WithLoc (getLoc (fromJust _signPattern)) "__pattern__")
+  sigPattern' <-
+    case _signPattern of
+      Just pat ->
+        fmap Just
+          . runReader PatternNamesKindFunctions
+          $ checkParsePatternAtom pat
+      Nothing -> return Nothing
   let def =
         FunctionDef
           { _signName = sigName',
@@ -2706,7 +2718,7 @@ checkPatternName' bindFun n = do
           <$> case pk of
             PatternNamesKindVariables ->
               bindVariableSymbol sym
-            PatternNamesKindFunctions ->
+            PatternNamesKindFunctions -> do
               bindFun sym
       NameQualified {} -> nameNotInScope n
   where
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
index 22859b9d2b..d83c7aa2df 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@@ -1332,10 +1332,13 @@ functionDefinitionLhs opts _funLhsBuiltin = P.label "<function definition>" $ do
     parseFailure off0 "instance not allowed here"
   when (isJust _funLhsCoercion && isNothing _funLhsInstance) $
     parseFailure off0 "expected: instance"
-  _funLhsPattern <- patternAtom
-  let _funLhsName = case _funLhsPattern of
-        PatternAtomIden (NameUnqualified s) -> Just s
-        _ -> Nothing
+  _funLhsName <- optional $ do
+    n <- symbol
+    P.notFollowedBy (kw kwAt)
+    return n
+  _funLhsPattern <- case _funLhsName of
+    Nothing -> Just <$> patternAtom
+    Just {} -> return Nothing
   let sigOpts =
         SigOptions
           { _sigAllowDefault = True,
diff --git a/src/Juvix/Compiler/Pipeline/Package/Loader.hs b/src/Juvix/Compiler/Pipeline/Package/Loader.hs
index dad2e3d685..3083c9ba49 100644
--- a/src/Juvix/Compiler/Pipeline/Package/Loader.hs
+++ b/src/Juvix/Compiler/Pipeline/Package/Loader.hs
@@ -90,7 +90,7 @@ toConcrete t p = run . runReader l $ do
                 _typeSigRetType,
                 _typeSigColonKw
               }
-          _signPattern = PatternAtomIden (NameUnqualified name')
+          _signPattern :: Maybe (PatternAtom 'Parsed) = Nothing
       return
         ( StatementFunctionDef
             FunctionDef

From 045ed03567e957c2dcf2d3fbc0ae499ff77a3d59 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Thu, 21 Nov 2024 17:35:44 +0100
Subject: [PATCH 05/15] fix parsing

---
 src/Juvix/Compiler/Concrete/Translation/FromSource.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
index d83c7aa2df..6d96ac8ed3 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@@ -1432,7 +1432,7 @@ functionDefinition opts _signBuiltin = P.label "<function definition>" $ do
             _signPragmas,
             _signBody
           }
-  when (isNothing _funLhsName && not (P.isFunctionLike fdef)) $
+  when (isNothing _funLhsName && P.isFunctionLike fdef) $
     parseFailure off0 "expected function name"
   return fdef
   where

From cadc289a7ca924b12d0ba926a3afb15119b7d972 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Thu, 21 Nov 2024 19:37:47 +0100
Subject: [PATCH 06/15] generate pattern defs

---
 src/Juvix/Compiler/Internal/Extra.hs          | 56 +++++++++++++++++++
 .../Internal/Translation/FromConcrete.hs      | 33 ++++++-----
 .../Analysis/TypeChecking/CheckerNew.hs       |  6 +-
 test/Compilation/Positive.hs                  |  7 ++-
 tests/Compilation/positive/out/test086.out    |  1 +
 tests/Compilation/positive/test086.juvix      |  9 +++
 6 files changed, 95 insertions(+), 17 deletions(-)
 create mode 100644 tests/Compilation/positive/out/test086.out
 create mode 100644 tests/Compilation/positive/test086.juvix

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..af5fda6ccd 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -671,7 +671,7 @@ 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
       _funDefTerminating = isJust _signTerminating
@@ -688,7 +688,12 @@ goFunctionDef def@FunctionDef {..} = do
   let _funDefDocComment = fmap ppPrintJudoc _signDoc
       fun = Internal.FunctionDef {..}
   whenJust _signBuiltin (checkBuiltinFunction fun . (^. withLocParam))
-  return fun
+  case _signPattern 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 +755,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
@@ -1198,10 +1201,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 +1469,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/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/positive/out/test086.out b/tests/Compilation/positive/out/test086.out
new file mode 100644
index 0000000000..7ed6ff82de
--- /dev/null
+++ b/tests/Compilation/positive/out/test086.out
@@ -0,0 +1 @@
+5
diff --git a/tests/Compilation/positive/test086.juvix b/tests/Compilation/positive/test086.juvix
new file mode 100644
index 0000000000..d55fc59321
--- /dev/null
+++ b/tests/Compilation/positive/test086.juvix
@@ -0,0 +1,9 @@
+module test086;
+
+import Stdlib.Prelude open;
+
+f (p : Pair Nat Nat) : Nat :=
+  let (x, y) := p
+  in x + 2 * y;
+
+main : Nat := f (1, 2);

From 9359ebf1aa74f35e10cde088876a14b87eb0f780 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Fri, 22 Nov 2024 12:37:14 +0100
Subject: [PATCH 07/15] fix record pattern scoping

---
 .../FromParsed/Analysis/Scoping.hs            | 11 ++++++---
 tests/Compilation/positive/out/test086.out    |  2 +-
 tests/Compilation/positive/test086.juvix      | 24 +++++++++++++++++--
 3 files changed, 31 insertions(+), 6 deletions(-)

diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
index 3d608c9757..f0ca55db79 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@@ -482,7 +482,6 @@ reservePatternFunctionSymbols = goAtom
       RecordPatternItemFieldPun FieldPun {..} -> do
         void (reservePatternName (NameUnqualified _fieldPunField))
       RecordPatternItemAssign RecordPatternAssign {..} -> do
-        void (reservePatternName (NameUnqualified _recordPatternAssignField))
         goAtoms _recordPatternAssignPattern
 
     goAtoms :: PatternAtoms 'Parsed -> Sem r ()
@@ -2335,9 +2334,10 @@ checkRecordPattern r = do
   where
     noFields :: ScopedIden -> ScoperError
     noFields = ErrConstructorNotARecord . ConstructorNotARecord
+
     checkItem ::
       forall r'.
-      (Members '[Reader PatternNamesKind, Reader (RecordNameSignature 'Parsed), Error ScoperError, State Scope, State ScoperState, State ScoperSyntax, Reader BindingStrategy, 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
@@ -2366,7 +2366,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
+              bindFunctionSymbol (f ^. fieldPunField)
           return
             FieldPun
               { _fieldPunIx = idx',
diff --git a/tests/Compilation/positive/out/test086.out b/tests/Compilation/positive/out/test086.out
index 7ed6ff82de..f599e28b8a 100644
--- a/tests/Compilation/positive/out/test086.out
+++ b/tests/Compilation/positive/out/test086.out
@@ -1 +1 @@
-5
+10
diff --git a/tests/Compilation/positive/test086.juvix b/tests/Compilation/positive/test086.juvix
index d55fc59321..6bebdded2d 100644
--- a/tests/Compilation/positive/test086.juvix
+++ b/tests/Compilation/positive/test086.juvix
@@ -3,7 +3,27 @@ module test086;
 import Stdlib.Prelude open;
 
 f (p : Pair Nat Nat) : Nat :=
-  let (x, y) := p
+  let
+    (x, y) := p;
   in x + 2 * y;
 
-main : Nat := f (1, 2);
+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 := x1; y}) := r
+  in x1 + 2 * y;
+
+main : Nat := f (px, py) + g rr;

From 97bc5a7026b26b351528434931717297e6fa07c0 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Fri, 22 Nov 2024 12:43:34 +0100
Subject: [PATCH 08/15] fix record pattern parsing

---
 src/Juvix/Compiler/Concrete/Translation/FromSource.hs | 2 +-
 tests/Compilation/positive/out/test086.out            | 2 +-
 tests/Compilation/positive/test086.juvix              | 6 ++++--
 3 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
index 6d96ac8ed3..83b2d54ef3 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@@ -1332,7 +1332,7 @@ functionDefinitionLhs opts _funLhsBuiltin = P.label "<function definition>" $ do
     parseFailure off0 "instance not allowed here"
   when (isJust _funLhsCoercion && isNothing _funLhsInstance) $
     parseFailure off0 "expected: instance"
-  _funLhsName <- optional $ do
+  _funLhsName <- optional $ P.try $ do
     n <- symbol
     P.notFollowedBy (kw kwAt)
     return n
diff --git a/tests/Compilation/positive/out/test086.out b/tests/Compilation/positive/out/test086.out
index f599e28b8a..60d3b2f4a4 100644
--- a/tests/Compilation/positive/out/test086.out
+++ b/tests/Compilation/positive/out/test086.out
@@ -1 +1 @@
-10
+15
diff --git a/tests/Compilation/positive/test086.juvix b/tests/Compilation/positive/test086.juvix
index 6bebdded2d..a85cea0c08 100644
--- a/tests/Compilation/positive/test086.juvix
+++ b/tests/Compilation/positive/test086.juvix
@@ -23,7 +23,9 @@ rr : R :=
 
 g (r : R) : Nat :=
   let
-    (mkR@{x := x1; y}) := r
+    mkR@{x := x1; y} := r
   in x1 + 2 * y;
 
-main : Nat := f (px, py) + g rr;
+mkR@{x := rx; y := ry} : R := rr;
+
+main : Nat := f (px, py) + g rr + f (rx, ry);

From c459f40218eb1347ff7182c488f8c9a8f683a5a5 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Fri, 22 Nov 2024 12:44:45 +0100
Subject: [PATCH 09/15] test

---
 tests/Compilation/positive/test086.juvix | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/Compilation/positive/test086.juvix b/tests/Compilation/positive/test086.juvix
index a85cea0c08..63094d7e15 100644
--- a/tests/Compilation/positive/test086.juvix
+++ b/tests/Compilation/positive/test086.juvix
@@ -23,8 +23,8 @@ rr : R :=
 
 g (r : R) : Nat :=
   let
-    mkR@{x := x1; y} := r
-  in x1 + 2 * y;
+    mkR@{x := x; y} := r
+  in x + 2 * y;
 
 mkR@{x := rx; y := ry} : R := rr;
 

From 2874550458717c0ddc47b6753be9cd3c488c1366 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Fri, 22 Nov 2024 13:01:48 +0100
Subject: [PATCH 10/15] add negative test

---
 test/Compilation/Negative.hs             |  6 +++++-
 tests/Compilation/negative/test014.juvix | 16 ++++++++++++++++
 2 files changed, 21 insertions(+), 1 deletion(-)
 create mode 100644 tests/Compilation/negative/test014.juvix

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/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;

From 760a669d841cfaffc4d2d9361dee99dcedb1f48c Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Fri, 22 Nov 2024 13:29:59 +0100
Subject: [PATCH 11/15] update stdlib

---
 juvix-stdlib | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/juvix-stdlib b/juvix-stdlib
index 0080b1183a..a6abb99562 160000
--- a/juvix-stdlib
+++ b/juvix-stdlib
@@ -1 +1 @@
-Subproject commit 0080b1183ab55e5180e69bfc3987e4cd6edbc230
+Subproject commit a6abb9956261f152cea5b14a0d31a9cce6c1957f

From 5578a49e849a871480aea2b63ff128acc55aa6c3 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Fri, 22 Nov 2024 14:03:09 +0100
Subject: [PATCH 12/15] fix after rebase

---
 src/Juvix/Compiler/Concrete/Language.hs       |  2 +-
 src/Juvix/Compiler/Concrete/Language/Base.hs  | 17 +++++-----
 .../FromParsed/Analysis/Scoping.hs            |  8 +++--
 .../Concrete/Translation/FromSource.hs        |  2 ++
 .../Internal/Translation/FromConcrete.hs      | 31 ++++++++++---------
 5 files changed, 32 insertions(+), 28 deletions(-)

diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs
index 3f226929db..47b7af06c6 100644
--- a/src/Juvix/Compiler/Concrete/Language.hs
+++ b/src/Juvix/Compiler/Concrete/Language.hs
@@ -31,7 +31,7 @@ statementLabel = \case
   StatementOpenModule {} -> Nothing
   StatementProjectionDef {} -> Nothing
   StatementFunctionDef f -> withFunctionSymbol Nothing (Just . (^. symbolTypeLabel)) (f ^. signName)
-  StatementDeriving f -> Just (f ^. derivingFunLhs . funLhsName . symbolTypeLabel)
+  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 865d19d0f1..056a7baa3f 100644
--- a/src/Juvix/Compiler/Concrete/Language/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Language/Base.hs
@@ -3156,10 +3156,17 @@ instance HasLoc (OpenModule s short) where
 instance HasLoc (ProjectionDef s) where
   getLoc = getLoc . (^. projectionConstructor)
 
+getFunLhsLoc :: (SingI s) => FunctionLhs s -> Maybe Interval
+getFunLhsLoc FunctionLhs {..} =
+  (Just . getLoc <$> _funLhsBuiltin)
+    ?<> (Just . getLoc <$> _funLhsTerminating)
+    ?<> (Just . getLocPatternAtomType <$> _funLhsPattern)
+    ?<> (getLocExpressionType <$> _funLhsTypeSig ^. typeSigRetType)
+
 instance (SingI s) => HasLoc (Deriving s) where
   getLoc Deriving {..} =
     getLoc _derivingKw
-      <> getLoc _derivingFunLhs
+      <>? getFunLhsLoc _derivingFunLhs
 
 instance HasLoc (Statement 'Scoped) where
   getLoc :: Statement 'Scoped -> Interval
@@ -3392,14 +3399,6 @@ 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)
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
index f0ca55db79..7e3fcfeabb 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@@ -1118,6 +1118,7 @@ checkDeriving ::
   Sem r (Deriving 'Scoped)
 checkDeriving Deriving {..} = do
   let lhs@FunctionLhs {..} = _derivingFunLhs
+  massert (isNothing _funLhsPattern)
   typeSig' <- withLocalScope (checkTypeSig _funLhsTypeSig)
   name' <-
     if
@@ -1127,6 +1128,7 @@ checkDeriving Deriving {..} = do
         FunctionLhs
           { _funLhsName = name',
             _funLhsTypeSig = typeSig',
+            _funLhsPattern = Nothing,
             ..
           }
   return
@@ -1195,7 +1197,7 @@ checkFunctionDef fdef@FunctionDef {..} = do
       | P.isFunctionLike fdef ->
           getReservedDefinitionSymbol name'
       | otherwise ->
-          reserveFunctionSymbol fdef
+          reserveFunctionSymbol (functionDefLhs fdef)
     Nothing ->
       freshSymbol KNameFunction KNameFunction (WithLoc (getLoc (fromJust _signPattern)) "__pattern__")
   sigPattern' <-
@@ -2371,7 +2373,7 @@ checkRecordPattern r = do
             PatternNamesKindVariables ->
               bindVariableSymbol (f ^. fieldPunField)
             PatternNamesKindFunctions -> do
-              bindFunctionSymbol (f ^. fieldPunField)
+              getReservedDefinitionSymbol (f ^. fieldPunField)
           return
             FieldPun
               { _fieldPunIx = idx',
@@ -2736,7 +2738,7 @@ checkPatternName ::
   (Members '[Reader PatternNamesKind, Error ScoperError, State Scope, NameIdGen, State ScoperState, State ScoperSyntax, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) =>
   Name ->
   Sem r PatternScopedIden
-checkPatternName = checkPatternName' bindFunctionSymbol
+checkPatternName = checkPatternName' getReservedDefinitionSymbol
 
 reservePatternName ::
   forall r.
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
index 83b2d54ef3..0f464f190b 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`"
+  unless (isJust (_derivingFunLhs ^. funLhsPattern)) $
+    parseFailure off "Patterns not allowed for `deriving instance`"
   return Deriving {..}
 
 statement :: (Members '[Error ParserError, ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (Statement 'Parsed)
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index af5fda6ccd..e0d02f527d 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

From 5e4c18f1e54ab926f4b9f2e99dfc76a0b8e1ed25 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Fri, 22 Nov 2024 14:08:49 +0100
Subject: [PATCH 13/15] fix parsing

---
 src/Juvix/Compiler/Concrete/Translation/FromSource.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
index 0f464f190b..410f51f20e 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@@ -481,7 +481,7 @@ derivingInstance = do
   _derivingFunLhs <- functionDefinitionLhs opts Nothing
   unless (isJust (_derivingFunLhs ^. funLhsInstance)) $
     parseFailure off "Expected `deriving instance`"
-  unless (isJust (_derivingFunLhs ^. funLhsPattern)) $
+  unless (isNothing (_derivingFunLhs ^. funLhsPattern)) $
     parseFailure off "Patterns not allowed for `deriving instance`"
   return Deriving {..}
 

From 39de2a2eb66b9c5aa4247124dd7af76fcf19baa8 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Fri, 22 Nov 2024 18:13:22 +0100
Subject: [PATCH 14/15] Jan/let patterns (#3188)

refactors _signName so that the type is more explicit
---
 .../Backend/Html/Translation/FromTyped.hs     |  4 +-
 .../Concrete/Data/InfoTableBuilder.hs         |  8 +-
 src/Juvix/Compiler/Concrete/Gen.hs            | 13 +--
 src/Juvix/Compiler/Concrete/Language/Base.hs  | 85 ++++++++++++++-----
 src/Juvix/Compiler/Concrete/Print/Base.hs     |  3 +-
 .../FromParsed/Analysis/Scoping.hs            | 56 +++++++-----
 .../Concrete/Translation/FromSource.hs        | 16 ++--
 .../Internal/Translation/FromConcrete.hs      | 16 ++--
 src/Juvix/Compiler/Pipeline/Package/Loader.hs |  4 +-
 9 files changed, 130 insertions(+), 75 deletions(-)

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/Gen.hs b/src/Juvix/Compiler/Concrete/Gen.hs
index 5be7526555..957a41d199 100644
--- a/src/Juvix/Compiler/Concrete/Gen.hs
+++ b/src/Juvix/Compiler/Concrete/Gen.hs
@@ -28,7 +28,6 @@ simplestFunctionDef :: forall s. (SingI s) => FunctionName s -> ExpressionType s
 simplestFunctionDef funName funBody =
   FunctionDef
     { _signName = name,
-      _signPattern = Nothing,
       _signBody = SigBodyExpression funBody,
       _signTypeSig =
         TypeSig
@@ -46,8 +45,12 @@ simplestFunctionDef funName funBody =
   where
     name :: FunctionSymbolType s
     name = case sing :: SStage s of
-      SParsed -> Just funName
-      SScoped -> funName
+      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
@@ -290,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
 
@@ -303,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/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs
index 056a7baa3f..1721130356 100644
--- a/src/Juvix/Compiler/Concrete/Language/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Language/Base.hs
@@ -83,8 +83,8 @@ type family SymbolType s = res | res -> s where
 
 type FunctionSymbolType :: Stage -> GHCType
 type family FunctionSymbolType s = res | res -> s where
-  FunctionSymbolType 'Parsed = Maybe Symbol
-  FunctionSymbolType 'Scoped = S.Symbol
+  FunctionSymbolType 'Parsed = FunctionDefNameParsed
+  FunctionSymbolType 'Scoped = FunctionDefNameScoped
 
 type IdentifierType :: Stage -> GHCType
 type family IdentifierType s = res | res -> s where
@@ -706,11 +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
-  { -- When s = 'Parsed, _signName must be present if the definition is
-    -- function-like. One of _signName or _signPattern must be present.
-    _signName :: FunctionSymbolType s,
-    _signPattern :: Maybe (PatternAtomType s),
+  { _signName :: FunctionSymbolType s,
     _signTypeSig :: TypeSig s,
     _signDoc :: Maybe (Judoc s),
     _signPragmas :: Maybe ParsedPragmas,
@@ -2869,7 +2885,6 @@ data FunctionLhs (s :: Stage) = FunctionLhs
     _funLhsInstance :: Maybe KeywordRef,
     _funLhsCoercion :: Maybe KeywordRef,
     _funLhsName :: FunctionSymbolType s,
-    _funLhsPattern :: Maybe (PatternAtomType s),
     _funLhsTypeSig :: TypeSig s
   }
   deriving stock (Generic)
@@ -2895,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
@@ -2984,6 +3000,7 @@ makeLenses ''MarkdownInfo
 makeLenses ''Deriving
 
 makePrisms ''NamedArgumentNew
+makePrisms ''FunctionDefNameParsed
 
 functionDefLhs :: FunctionDef s -> FunctionLhs s
 functionDefLhs FunctionDef {..} =
@@ -2993,7 +3010,6 @@ functionDefLhs FunctionDef {..} =
       _funLhsInstance = _signInstance,
       _funLhsCoercion = _signCoercion,
       _funLhsName = _signName,
-      _funLhsPattern = _signPattern,
       _funLhsTypeSig = _signTypeSig
     }
 
@@ -3156,17 +3172,33 @@ instance HasLoc (OpenModule s short) where
 instance HasLoc (ProjectionDef s) where
   getLoc = getLoc . (^. projectionConstructor)
 
-getFunLhsLoc :: (SingI s) => FunctionLhs s -> Maybe Interval
-getFunLhsLoc FunctionLhs {..} =
-  (Just . getLoc <$> _funLhsBuiltin)
-    ?<> (Just . getLoc <$> _funLhsTerminating)
-    ?<> (Just . getLocPatternAtomType <$> _funLhsPattern)
-    ?<> (getLocExpressionType <$> _funLhsTypeSig ^. typeSigRetType)
+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
-      <>? getFunLhsLoc _derivingFunLhs
+      <> getLoc _derivingFunLhs
 
 instance HasLoc (Statement 'Scoped) where
   getLoc :: Statement 'Scoped -> Interval
@@ -3405,8 +3437,8 @@ instance (SingI s) => HasLoc (FunctionDef s) where
       ?<> (getLoc <$> _signPragmas)
       ?<> (getLoc <$> _signBuiltin)
       ?<> (getLoc <$> _signTerminating)
-      ?<> (getLocPatternAtomType <$> _signPattern)
-      ?<> getLoc _signBody
+      ?<> (getLocFunctionSymbolType _signName)
+      <> getLoc _signBody
 
 instance HasLoc (Example s) where
   getLoc e = e ^. exampleLoc
@@ -3597,13 +3629,20 @@ symbolParsed sym = case sing :: SStage s of
 
 getFunctionSymbol :: forall s. (SingI s) => FunctionSymbolType s -> SymbolType s
 getFunctionSymbol sym = case sing :: SStage s of
-  SParsed -> fromJust sym
-  SScoped -> sym
+  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
-  SScoped -> f sym
+  SParsed -> maybe a f (sym ^? _FunctionDefName)
+  SScoped -> f (sym ^. functionDefName)
 
 namedArgumentNewSymbolParsed :: (SingI s) => SimpleGetter (NamedArgumentNew s) Symbol
 namedArgumentNewSymbolParsed = to $ \case
@@ -3614,8 +3653,8 @@ namedArgumentNewSymbol :: Lens' (NamedArgumentNew 'Parsed) Symbol
 namedArgumentNewSymbol f = \case
   NamedArgumentItemPun a -> NamedArgumentItemPun <$> (namedArgumentPunSymbol f a)
   NamedArgumentNewFunction a -> do
-    a' <- f (fromJust (a ^. namedArgumentFunctionDef . signName))
-    return $ NamedArgumentNewFunction (over namedArgumentFunctionDef (set signName (Just a')) a)
+    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 ca86ed3da9..656a817066 100644
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Print/Base.hs
@@ -1168,7 +1168,8 @@ 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' = case _funLhsPattern of
+        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
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
index 7e3fcfeabb..f56907996d 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@@ -412,7 +412,7 @@ reserveFunctionSymbol ::
   FunctionLhs 'Parsed ->
   Sem r S.Symbol
 reserveFunctionSymbol f =
-  reserveSymbolSignatureOf SKNameFunction f (toBuiltinPrim <$> f ^. funLhsBuiltin) (fromJust (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) =>
@@ -1118,17 +1118,24 @@ checkDeriving ::
   Sem r (Deriving 'Scoped)
 checkDeriving Deriving {..} = do
   let lhs@FunctionLhs {..} = _derivingFunLhs
-  massert (isNothing _funLhsPattern)
+  massert (isJust (_funLhsName ^? _FunctionDefName))
+  let name = case _funLhsName of
+        FunctionDefName n -> n
+        FunctionDefNamePattern {} -> impossible
   typeSig' <- withLocalScope (checkTypeSig _funLhsTypeSig)
   name' <-
     if
-        | P.isLhsFunctionLike lhs -> getReservedDefinitionSymbol (fromJust _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',
-            _funLhsPattern = Nothing,
             ..
           }
   return
@@ -1190,33 +1197,36 @@ checkFunctionDef fdef@FunctionDef {..} = do
     a' <- checkTypeSig _signTypeSig
     b' <- checkBody
     return (a', b')
-  whenJust _signPattern $
-    reservePatternFunctionSymbols
+  whenJust (functionSymbolPattern _signName) reservePatternFunctionSymbols
   sigName' <- case _signName of
-    Just name'
-      | P.isFunctionLike fdef ->
-          getReservedDefinitionSymbol name'
-      | otherwise ->
-          reserveFunctionSymbol (functionDefLhs fdef)
-    Nothing ->
-      freshSymbol KNameFunction KNameFunction (WithLoc (getLoc (fromJust _signPattern)) "__pattern__")
-  sigPattern' <-
-    case _signPattern of
-      Just pat ->
-        fmap Just
-          . runReader PatternNamesKindFunctions
-          $ checkParsePatternAtom pat
-      Nothing -> return Nothing
+    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',
-            _signPattern = sigPattern',
+            -- _signPattern = sigPattern',
             _signDoc = sigDoc',
             _signBody = sigBody',
             _signTypeSig = sig',
             ..
           }
-  registerNameSignature (sigName' ^. S.nameId) def
+  registerNameSignature (sigName' ^. functionDefName . S.nameId) def
   registerFunctionDef @$> def
   where
     checkBody :: Sem r (FunctionDefBody 'Scoped)
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
index 410f51f20e..396ce5060c 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@@ -481,7 +481,7 @@ derivingInstance = do
   _derivingFunLhs <- functionDefinitionLhs opts Nothing
   unless (isJust (_derivingFunLhs ^. funLhsInstance)) $
     parseFailure off "Expected `deriving instance`"
-  unless (isNothing (_derivingFunLhs ^. funLhsPattern)) $
+  when (has _FunctionDefNamePattern (_derivingFunLhs ^. funLhsName)) $
     parseFailure off "Patterns not allowed for `deriving instance`"
   return Deriving {..}
 
@@ -1334,27 +1334,26 @@ functionDefinitionLhs opts _funLhsBuiltin = P.label "<function definition>" $ do
     parseFailure off0 "instance not allowed here"
   when (isJust _funLhsCoercion && isNothing _funLhsInstance) $
     parseFailure off0 "expected: instance"
-  _funLhsName <- optional $ P.try $ do
+  mname <- optional . P.try $ do
     n <- symbol
     P.notFollowedBy (kw kwAt)
     return n
-  _funLhsPattern <- case _funLhsName of
-    Nothing -> Just <$> patternAtom
-    Just {} -> return Nothing
+  _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 && not (null (_funLhsTypeSig ^. typeSigArgs))) $
+  when (isNothing (_funLhsName ^? _FunctionDefName) && notNull (_funLhsTypeSig ^. typeSigArgs)) $
     parseFailure off "expected function name"
   return
     FunctionLhs
       { _funLhsInstance,
         _funLhsBuiltin,
         _funLhsCoercion,
-        _funLhsPattern,
         _funLhsName,
         _funLhsTypeSig,
         _funLhsTerminating
@@ -1424,7 +1423,6 @@ functionDefinition opts _signBuiltin = P.label "<function definition>" $ do
   let fdef =
         FunctionDef
           { _signName = _funLhsName,
-            _signPattern = _funLhsPattern,
             _signTypeSig = _funLhsTypeSig,
             _signTerminating = _funLhsTerminating,
             _signInstance = _funLhsInstance,
@@ -1434,7 +1432,7 @@ functionDefinition opts _signBuiltin = P.label "<function definition>" $ do
             _signPragmas,
             _signBody
           }
-  when (isNothing _funLhsName && P.isFunctionLike fdef) $
+  when (isNothing (_funLhsName ^? _FunctionDefName) && P.isFunctionLike fdef) $
     parseFailure off0 "expected function name"
   return fdef
   where
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index e0d02f527d..9a6b85f731 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -418,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
@@ -674,7 +674,7 @@ goFunctionDef ::
   FunctionDef 'Scoped ->
   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
@@ -689,7 +689,7 @@ goFunctionDef def@FunctionDef {..} = do
   let _funDefDocComment = fmap ppPrintJudoc _signDoc
       fun = Internal.FunctionDef {..}
   whenJust _signBuiltin (checkBuiltinFunction fun . (^. withLocParam))
-  case _signPattern of
+  case _signName ^. functionDefNamePattern of
     Just pat -> do
       pat' <- goPatternArg pat
       (fun :) <$> Internal.genPatternDefs _funDefName pat'
@@ -1097,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 ::
@@ -1190,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 =
diff --git a/src/Juvix/Compiler/Pipeline/Package/Loader.hs b/src/Juvix/Compiler/Pipeline/Package/Loader.hs
index 3083c9ba49..7c24a72d36 100644
--- a/src/Juvix/Compiler/Pipeline/Package/Loader.hs
+++ b/src/Juvix/Compiler/Pipeline/Package/Loader.hs
@@ -90,7 +90,6 @@ toConcrete t p = run . runReader l $ do
                 _typeSigRetType,
                 _typeSigColonKw
               }
-          _signPattern :: Maybe (PatternAtom 'Parsed) = Nothing
       return
         ( StatementFunctionDef
             FunctionDef
@@ -100,8 +99,7 @@ toConcrete t p = run . runReader l $ do
                 _signDoc = Nothing,
                 _signCoercion = Nothing,
                 _signBuiltin = Nothing,
-                _signName = Just name',
-                _signPattern,
+                _signName = FunctionDefName name',
                 _signBody,
                 _signTypeSig
               }

From b25fb9d0472d12167d6c9a896f3d53f3da10dc18 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C5=81ukasz=20Czajka?=
 <62751+lukaszcz@users.noreply.github.com>
Date: Fri, 22 Nov 2024 20:21:55 +0100
Subject: [PATCH 15/15] Update Scoping.hs

---
 .../Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
index f56907996d..f904efc182 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@@ -1220,7 +1220,6 @@ checkFunctionDef fdef@FunctionDef {..} = do
   let def =
         FunctionDef
           { _signName = sigName',
-            -- _signPattern = sigPattern',
             _signDoc = sigDoc',
             _signBody = sigBody',
             _signTypeSig = sig',