diff --git a/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs
index 620547bdf3..806a2e74c8 100644
--- a/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs
+++ b/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs
@@ -543,7 +543,7 @@ goFunctionDef def = do
   defHeader (def ^. signName) sig' (def ^. signDoc)
   where
     funSig :: Sem r Html
-    funSig = ppHelper (ppFunctionSignature def)
+    funSig = ppHelper (ppCode (functionDefLhs def))
 
 goInductive :: forall r. (Members '[Reader HtmlOptions] r) => InductiveDef 'Scoped -> Sem r Html
 goInductive def = do
diff --git a/src/Juvix/Compiler/Concrete/Language/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs
index f6d135cb3f..25c122fc75 100644
--- a/src/Juvix/Compiler/Concrete/Language/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Language/Base.hs
@@ -2801,7 +2801,19 @@ deriving stock instance Ord (JudocAtom 'Parsed)
 
 deriving stock instance Ord (JudocAtom 'Scoped)
 
+data FunctionLhs (s :: Stage) = FunctionLhs
+  { _funLhsBuiltin :: Maybe (WithLoc BuiltinFunction),
+    _funLhsTerminating :: Maybe KeywordRef,
+    _funLhsInstance :: Maybe KeywordRef,
+    _funLhsCoercion :: Maybe KeywordRef,
+    _funLhsName :: FunctionName s,
+    _funLhsArgs :: [SigArg s],
+    _funLhsColonKw :: Irrelevant (Maybe KeywordRef),
+    _funLhsRetType :: Maybe (ExpressionType s)
+  }
+
 makeLenses ''SideIfs
+makeLenses ''FunctionLhs
 makeLenses ''Statements
 makeLenses ''NamedArgumentFunctionDef
 makeLenses ''NamedArgumentPun
@@ -2888,6 +2900,19 @@ makeLenses ''RecordInfo
 makeLenses ''MarkdownInfo
 makePrisms ''NamedArgumentNew
 
+functionDefLhs :: FunctionDef s -> FunctionLhs s
+functionDefLhs FunctionDef {..} =
+  FunctionLhs
+    { _funLhsBuiltin = _signBuiltin,
+      _funLhsTerminating = _signTerminating,
+      _funLhsInstance = _signInstance,
+      _funLhsCoercion = _signCoercion,
+      _funLhsName = _signName,
+      _funLhsArgs = _signArgs,
+      _funLhsColonKw = _signColonKw,
+      _funLhsRetType = _signRetType
+    }
+
 fixityFieldHelper :: SimpleGetter (ParsedFixityFields s) (Maybe a) -> SimpleGetter (ParsedFixityInfo s) (Maybe a)
 fixityFieldHelper l = to (^? fixityFields . _Just . l . _Just)
 
diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
index 8824e85130..0bb4d9be43 100644
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Print/Base.hs
@@ -1123,34 +1123,34 @@ instance (SingI s) => PrettyPrint (SigArg s) where
         defaultVal = ppCode <$> _sigArgDefault
     ppCode l <> arg <+?> defaultVal <> ppCode r
 
-ppFunctionSignature :: (SingI s) => PrettyPrinting (FunctionDef s)
-ppFunctionSignature FunctionDef {..} = do
-  let termin' = (<> line) . ppCode <$> _signTerminating
-      coercion' = (<> if isJust instance' then space else line) . ppCode <$> _signCoercion
-      instance' = (<> line) . ppCode <$> _signInstance
-      builtin' = (<> line) . ppCode <$> _signBuiltin
-      margs' = fmap ppCode <$> nonEmpty _signArgs
-      mtype' = case _signColonKw ^. unIrrelevant of
-        Just col -> Just (ppCode col <+> ppExpressionType (fromJust _signRetType))
-        Nothing -> Nothing
-      argsAndType' = case mtype' of
-        Nothing -> margs'
-        Just ty' -> case margs' of
-          Nothing -> Just (pure ty')
-          Just args' -> Just (args' <> pure ty')
-      name' = annDef _signName (ppSymbolType _signName)
-   in builtin'
-        ?<> termin'
-        ?<> coercion'
-        ?<> instance'
-        ?<> (name' <>? (oneLineOrNext . sep <$> argsAndType'))
+instance (SingI s) => PrettyPrint (FunctionLhs s) where
+  ppCode FunctionLhs {..} = do
+    let termin' = (<> line) . ppCode <$> _funLhsTerminating
+        coercion' = (<> if isJust instance' then space else line) . ppCode <$> _funLhsCoercion
+        instance' = (<> line) . ppCode <$> _funLhsInstance
+        builtin' = (<> line) . ppCode <$> _funLhsBuiltin
+        margs' = fmap ppCode <$> nonEmpty _funLhsArgs
+        mtype' = case _funLhsColonKw ^. unIrrelevant of
+          Just col -> Just (ppCode col <+> ppExpressionType (fromJust _funLhsRetType))
+          Nothing -> Nothing
+        argsAndType' = case mtype' of
+          Nothing -> margs'
+          Just ty' -> case margs' of
+            Nothing -> Just (pure ty')
+            Just args' -> Just (args' <> pure ty')
+        name' = annDef _funLhsName (ppSymbolType _funLhsName)
+    builtin'
+      ?<> termin'
+      ?<> coercion'
+      ?<> instance'
+      ?<> (name' <>? (oneLineOrNext . sep <$> argsAndType'))
 
 instance (SingI s) => PrettyPrint (FunctionDef s) where
   ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => FunctionDef s -> Sem r ()
   ppCode fun@FunctionDef {..} = do
     let doc' :: Maybe (Sem r ()) = ppCode <$> _signDoc
         pragmas' :: Maybe (Sem r ()) = ppCode <$> _signPragmas
-        sig' = ppFunctionSignature fun
+        sig' = ppCode (functionDefLhs fun)
         body' = case _signBody of
           SigBodyExpression e -> space <> ppCode Kw.kwAssign <> oneLineOrNext (ppTopExpressionType e)
           SigBodyClauses k -> line <> indent (vsep (ppCode <$> k))
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
index 7755ddab5b..5fab4fc798 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@@ -37,12 +37,18 @@ import Juvix.Prelude.Pretty
     prettyText,
   )
 
+data FunctionSyntaxOptions = FunctionSyntaxOptions
+  { _funAllowOmitType :: Bool,
+    _funAllowInstance :: Bool
+  }
+
 data MdModuleBuilder = MdModuleBuilder
   { _mdModuleBuilder :: Module 'Parsed 'ModuleTop,
     _mdModuleBuilderBlocksLengths :: [Int]
   }
 
 makeLenses ''MdModuleBuilder
+makeLenses ''FunctionSyntaxOptions
 
 type JudocStash = State (Maybe (Judoc 'Parsed))
 
@@ -275,13 +281,16 @@ runExpressionParser ::
 runExpressionParser fpath input_ = do
   m <-
     ignoreHighlightBuilder
-      $ runParserResultBuilder mempty
-        . evalState (Nothing @ParsedPragmas)
-        . evalState (Nothing @(Judoc 'Parsed))
+      . evalParserResultBuilder mempty
+      . evalState (Nothing @ParsedPragmas)
+      . evalState (Nothing @(Judoc 'Parsed))
+      . runError @ParserError
       $ P.runParserT parseExpressionAtoms (toFilePath fpath) input_
-  case m of
-    (_, Left err) -> return (Left (ErrMegaparsec (MegaparsecError err)))
-    (_, Right r) -> return (Right r)
+  return $ case m of
+    Left err -> Left err
+    Right x -> case x of
+      Left merr -> Left (ErrMegaparsec (MegaparsecError merr))
+      Right r -> return r
 
 -- | The first pipe is optional, and thus we need a `Maybe`. The rest of the elements are guaranteed to be given a `Just`.
 pipeSep1 :: (Member ParserResultBuilder r) => (Irrelevant (Maybe KeywordRef) -> ParsecS r a) -> ParsecS r (NonEmpty a)
@@ -297,14 +306,14 @@ top ::
 top p = space >> p <* (optional semicolon >> P.eof)
 
 topModuleDefStdin ::
-  (Members '[Error ParserError, ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  (Members '[Error ParserError, ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
   ParsecS r (Module 'Parsed 'ModuleTop)
 topModuleDefStdin = do
   optional_ stashJudoc
   top moduleDef
 
 topModuleDef ::
-  (Members '[Error ParserError, TopModuleNameChecker, ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  (Members '[Error ParserError, TopModuleNameChecker, ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
   ParsecS r (Module 'Parsed 'ModuleTop)
 topModuleDef = do
   space >> optional_ stashJudoc
@@ -356,7 +365,7 @@ juvixCodeBlockParser = do
           (Just $ t ^. withLocInt)
 
 topMarkdownModuleDef ::
-  (Members '[ParserResultBuilder, Error ParserError, PragmasStash, JudocStash] r) =>
+  (Members '[ParserResultBuilder, Error ParserError, PragmasStash, Error ParserError, JudocStash] r) =>
   ParsecS r (Module 'Parsed 'ModuleTop)
 topMarkdownModuleDef = do
   optional_ stashJudoc
@@ -365,7 +374,7 @@ topMarkdownModuleDef = do
 
 parseTopStatements ::
   forall r.
-  (Members '[ParserResultBuilder, Error ParserError, PragmasStash, JudocStash] r) =>
+  (Members '[ParserResultBuilder, Error ParserError, PragmasStash, Error ParserError, JudocStash] r) =>
   ParsecS r [Statement 'Parsed]
 parseTopStatements = top $ P.sepEndBy statement semicolon
 
@@ -380,20 +389,20 @@ replInput =
 -- Symbols and names
 --------------------------------------------------------------------------------
 
-symbol :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r Symbol
+symbol :: (Members '[ParserResultBuilder] r) => ParsecS r Symbol
 symbol = uncurry (flip WithLoc) <$> identifierL
 
-dottedSymbol :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (NonEmpty Symbol)
+dottedSymbol :: (Members '[ParserResultBuilder] r) => ParsecS r (NonEmpty Symbol)
 dottedSymbol = fmap (uncurry (flip WithLoc)) <$> dottedIdentifier
 
-name :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r Name
+name :: (Members '[ParserResultBuilder] r) => ParsecS r Name
 name = do
   parts <- dottedSymbol
   return $ case nonEmptyUnsnoc parts of
     (Just p, n) -> NameQualified (QualifiedName (SymbolPath p) n)
     (Nothing, n) -> NameUnqualified n
 
-usingItem :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (UsingItem 'Parsed)
+usingItem :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (UsingItem 'Parsed)
 usingItem = do
   _usingModuleKw <- optional (kw kwModule)
   _usingSymbol <- symbol
@@ -404,13 +413,13 @@ usingItem = do
       _usingAs = snd <$> alias
   return UsingItem {..}
 
-hidingItem :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (HidingItem 'Parsed)
+hidingItem :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (HidingItem 'Parsed)
 hidingItem = do
   _hidingModuleKw <- optional (kw kwModule)
   _hidingSymbol <- symbol
   return HidingItem {..}
 
-phidingList :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (HidingList 'Parsed)
+phidingList :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (HidingList 'Parsed)
 phidingList = do
   _hidingKw <- Irrelevant <$> kw kwHiding
   l <- kw delimBraceL
@@ -422,7 +431,7 @@ phidingList = do
         ..
       }
 
-pusingList :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (UsingList 'Parsed)
+pusingList :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (UsingList 'Parsed)
 pusingList = do
   _usingKw <- Irrelevant <$> kw kwUsing
   l <- kw delimBraceL
@@ -434,17 +443,32 @@ pusingList = do
         ..
       }
 
-topModulePath :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r TopModulePath
+topModulePath :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r TopModulePath
 topModulePath = mkTopModulePath <$> dottedSymbol
 
 --------------------------------------------------------------------------------
 -- Top level statement
 --------------------------------------------------------------------------------
 
-statement :: (Members '[Error ParserError, ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (Statement 'Parsed)
+recoverStashes :: (Members '[PragmasStash, JudocStash] r) => ParsecS r a -> ParsecS r a
+recoverStashes r = do
+  p <- P.lift (get @(Maybe ParsedPragmas))
+  j <- P.lift (get @(Maybe (Judoc 'Parsed)))
+  res <- r
+  P.lift $ do
+    put p
+    put j
+  return res
+
+statement :: (Members '[Error ParserError, ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (Statement 'Parsed)
 statement = P.label "<top level statement>" $ do
   optional_ stashJudoc
   optional_ stashPragmas
+  let funSyntax =
+        FunctionSyntaxOptions
+          { _funAllowInstance = True,
+            _funAllowOmitType = False
+          }
   ms <-
     optional
       ( StatementImport <$> import_
@@ -454,7 +478,7 @@ statement = P.label "<top level statement>" $ do
           <|> StatementModule <$> moduleDef
           <|> StatementAxiom <$> axiomDef Nothing
           <|> builtinStatement
-          <|> StatementFunctionDef <$> functionDefinition False True Nothing
+          <|> StatementFunctionDef <$> functionDefinition funSyntax Nothing
       )
   case ms of
     Just s -> return s
@@ -464,7 +488,7 @@ statement = P.label "<top level statement>" $ do
         Nothing -> P.failure Nothing mempty
         Just j -> P.lift . throw . ErrDanglingJudoc . DanglingJudoc $ j
 
-stashPragmas :: forall r. (Members '[ParserResultBuilder, PragmasStash] r) => ParsecS r ()
+stashPragmas :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError] r) => ParsecS r ()
 stashPragmas = do
   pragmas <- withLoc parsePragmas
   P.lift (registerPragmas (getLoc pragmas))
@@ -487,7 +511,7 @@ parseYaml l r = do
     Left err -> parseFailure off (prettyPrintParseException err)
     Right yaml -> return $ WithSource (fromString str) yaml
 
-stashJudoc :: forall r. (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r ()
+stashJudoc :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r ()
 stashJudoc = do
   b <- judoc
   many (judocEmptyLine False)
@@ -551,7 +575,7 @@ stashJudoc = do
 
 judocAtom ::
   forall r.
-  (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
   Bool ->
   ParsecS r (JudocAtom 'Parsed)
 judocAtom inBlock =
@@ -592,17 +616,17 @@ judocAtom inBlock =
       judocText_ (P.char ';')
       return e
 
-builtinInductive :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (WithLoc BuiltinInductive)
+builtinInductive :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (WithLoc BuiltinInductive)
 builtinInductive = builtinHelper
 
-builtinFunction :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (WithLoc BuiltinFunction)
+builtinFunction :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (WithLoc BuiltinFunction)
 builtinFunction = builtinHelper
 
-builtinAxiom :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (WithLoc BuiltinAxiom)
+builtinAxiom :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (WithLoc BuiltinAxiom)
 builtinAxiom = builtinHelper
 
 builtinHelper ::
-  (Members '[ParserResultBuilder, PragmasStash, JudocStash] r, Bounded a, Enum a, Pretty a) =>
+  (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r, Bounded a, Enum a, Pretty a) =>
   ParsecS r (WithLoc a)
 builtinHelper =
   P.choice
@@ -610,29 +634,35 @@ builtinHelper =
       | a <- allElements
     ]
 
-builtinInductiveDef :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => WithLoc BuiltinInductive -> ParsecS r (InductiveDef 'Parsed)
+builtinInductiveDef :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => WithLoc BuiltinInductive -> ParsecS r (InductiveDef 'Parsed)
 builtinInductiveDef = inductiveDef . Just
 
 builtinAxiomDef ::
-  (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
   WithLoc BuiltinAxiom ->
   ParsecS r (AxiomDef 'Parsed)
 builtinAxiomDef = axiomDef . Just
 
 builtinFunctionDef ::
-  (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
   WithLoc BuiltinFunction ->
   ParsecS r (FunctionDef 'Parsed)
-builtinFunctionDef = functionDefinition False True . Just
+builtinFunctionDef = functionDefinition funSyntax . Just
+  where
+    funSyntax =
+      FunctionSyntaxOptions
+        { _funAllowInstance = True,
+          _funAllowOmitType = False
+        }
 
-builtinStatement :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (Statement 'Parsed)
+builtinStatement :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (Statement 'Parsed)
 builtinStatement = do
   void (kw kwBuiltin)
   (builtinInductive >>= fmap StatementInductive . builtinInductiveDef)
     <|> (builtinFunction >>= fmap StatementFunctionDef . builtinFunctionDef)
     <|> (builtinAxiom >>= fmap StatementAxiom . builtinAxiomDef)
 
-builtinRecordField :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (WithLoc BuiltinFunction)
+builtinRecordField :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (WithLoc BuiltinFunction)
 builtinRecordField = do
   void (kw kwBuiltin)
   builtinFunction
@@ -641,7 +671,7 @@ builtinRecordField = do
 -- Syntax declaration
 --------------------------------------------------------------------------------
 
-syntaxDef :: forall r. (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (SyntaxDef 'Parsed)
+syntaxDef :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (SyntaxDef 'Parsed)
 syntaxDef = do
   syn <- kw kwSyntax
   SyntaxFixity <$> fixitySyntaxDef syn
@@ -649,7 +679,7 @@ syntaxDef = do
     <|> SyntaxIterator <$> iteratorSyntaxDef syn
     <|> SyntaxAlias <$> aliasDef syn
 
-aliasDef :: forall r. (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => KeywordRef -> ParsecS r (AliasDef 'Parsed)
+aliasDef :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => KeywordRef -> ParsecS r (AliasDef 'Parsed)
 aliasDef synKw = do
   let _aliasDefSyntaxKw = Irrelevant synKw
   _aliasDefAliasKw <- Irrelevant <$> kw kwAlias
@@ -660,7 +690,7 @@ aliasDef synKw = do
 
 parsedFixityFields ::
   forall r.
-  (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
   ParsecS r (ParsedFixityFields 'Parsed)
 parsedFixityFields = do
   l <- kw delimBraceL
@@ -699,7 +729,7 @@ parsedFixityFields = do
         <|> kw kwNone
           $> AssocNone
 
-parsedFixityInfo :: forall r. (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (ParsedFixityInfo 'Parsed)
+parsedFixityInfo :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (ParsedFixityInfo 'Parsed)
 parsedFixityInfo = do
   _fixityParsedArity <- withLoc ari
   _fixityFields <- optional parsedFixityFields
@@ -714,7 +744,7 @@ parsedFixityInfo = do
         <|> kw kwNone
           $> None
 
-fixitySyntaxDef :: forall r. (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => KeywordRef -> ParsecS r (FixitySyntaxDef 'Parsed)
+fixitySyntaxDef :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => KeywordRef -> ParsecS r (FixitySyntaxDef 'Parsed)
 fixitySyntaxDef _fixitySyntaxKw = P.label "<fixity declaration>" $ do
   _fixityDoc <- getJudoc
   _fixityKw <- kw kwFixity
@@ -723,7 +753,7 @@ fixitySyntaxDef _fixitySyntaxKw = P.label "<fixity declaration>" $ do
   _fixityInfo <- parsedFixityInfo
   return FixitySyntaxDef {..}
 
-operatorSyntaxDef :: forall r. (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => KeywordRef -> ParsecS r OperatorSyntaxDef
+operatorSyntaxDef :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => KeywordRef -> ParsecS r OperatorSyntaxDef
 operatorSyntaxDef _opSyntaxKw = do
   _opKw <- kw kwOperator
   _opSymbol <- symbol
@@ -732,7 +762,7 @@ operatorSyntaxDef _opSyntaxKw = do
 
 parsedIteratorInfo ::
   forall r.
-  (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
   ParsecS r ParsedIteratorInfo
 parsedIteratorInfo = do
   l <- kw delimBraceL
@@ -754,7 +784,7 @@ parsedIteratorInfo = do
       void (kw kwRange >> kw kwAssign)
       fmap fromIntegral <$> integer
 
-iteratorSyntaxDef :: forall r. (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => KeywordRef -> ParsecS r IteratorSyntaxDef
+iteratorSyntaxDef :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => KeywordRef -> ParsecS r IteratorSyntaxDef
 iteratorSyntaxDef _iterSyntaxKw = do
   _iterIteratorKw <- kw kwIterator
   _iterSymbol <- symbol
@@ -765,7 +795,7 @@ iteratorSyntaxDef _iterSyntaxKw = do
 -- Import statement
 --------------------------------------------------------------------------------
 
-import_ :: forall r. (Members '[ParserResultBuilder, PragmasStash, JudocStash, Error ParserError] r) => ParsecS r (Import 'Parsed)
+import_ :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash, Error ParserError] r) => ParsecS r (Import 'Parsed)
 import_ = do
   _importKw <- kw kwImport
   _importModulePath <- topModulePath
@@ -780,7 +810,7 @@ import_ = do
     pasName :: ParsecS r TopModulePath
     pasName = void (kw kwAs) >> topModulePath
 
-recordUpdateField :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (RecordUpdateField 'Parsed)
+recordUpdateField :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (RecordUpdateField 'Parsed)
 recordUpdateField = do
   _fieldUpdateName <- symbol
   _fieldUpdateAssignKw <- Irrelevant <$> kw kwAssign
@@ -788,7 +818,7 @@ recordUpdateField = do
   let _fieldUpdateArgIx = ()
   return RecordUpdateField {..}
 
-recordUpdate :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (RecordUpdate 'Parsed)
+recordUpdate :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (RecordUpdate 'Parsed)
 recordUpdate = do
   _recordUpdateAtKw <- Irrelevant <$> kw kwAt
   _recordUpdateTypeName <- name
@@ -799,7 +829,7 @@ recordUpdate = do
       _recordUpdateExtra = Irrelevant ()
   return RecordUpdate {..}
 
-expressionAtom :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (ExpressionAtom 'Parsed)
+expressionAtom :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (ExpressionAtom 'Parsed)
 expressionAtom =
   P.label "<expression>" $
     AtomLiteral <$> P.try literal
@@ -808,21 +838,21 @@ expressionAtom =
       <|> AtomList <$> parseList
       <|> AtomIf <$> multiwayIf
       <|> AtomIdentifier <$> name
+      <|> AtomFunction <$> function
       <|> AtomUniverse <$> universe
       <|> AtomLambda <$> lambda
       <|> AtomCase <$> case_
-      <|> AtomFunction <$> function
       <|> AtomLet <$> letBlock
       <|> AtomDo <$> doBlock
       <|> AtomFunArrow <$> kw kwRightArrow
       <|> AtomHole <$> hole
       <|> AtomParens <$> parens parseExpressionAtoms
       <|> AtomDoubleBraces <$> pdoubleBracesExpression
-      <|> AtomBraces <$> withLoc (braces parseExpressionAtoms)
       <|> AtomRecordUpdate <$> recordUpdate
+      <|> AtomBraces <$> withLoc (braces parseExpressionAtoms)
 
 parseExpressionAtoms ::
-  (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
   ParsecS r (ExpressionAtoms 'Parsed)
 parseExpressionAtoms = do
   (_expressionAtoms, _expressionAtomsLoc) <- second Irrelevant <$> interval (P.some expressionAtom)
@@ -830,7 +860,7 @@ parseExpressionAtoms = do
 
 pdoubleBracesExpression ::
   forall r.
-  (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
   ParsecS r (DoubleBracesExpression 'Parsed)
 pdoubleBracesExpression = do
   l <- kw delimDoubleBraceL
@@ -853,7 +883,7 @@ pdoubleBracesExpression = do
 
 iterator ::
   forall r.
-  (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
   ParsecS r (Iterator 'Parsed)
 iterator = do
   (firstIsInit, keywordRef, _iteratorName, pat) <- P.try $ do
@@ -932,12 +962,17 @@ iterator = do
 
 pnamedArgumentFunctionDef ::
   forall r.
-  (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
   ParsecS r (NamedArgumentFunctionDef 'Parsed)
 pnamedArgumentFunctionDef = do
   optional_ stashJudoc
   optional_ stashPragmas
-  fun <- functionDefinition True False Nothing
+  let funSyntax =
+        FunctionSyntaxOptions
+          { _funAllowOmitType = True,
+            _funAllowInstance = False
+          }
+  fun <- functionDefinition funSyntax Nothing
   return
     NamedArgumentFunctionDef
       { _namedArgumentFunctionDef = fun
@@ -945,7 +980,7 @@ pnamedArgumentFunctionDef = do
 
 pnamedArgumentItemPun ::
   forall r.
-  (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
   ParsecS r (NamedArgumentPun 'Parsed)
 pnamedArgumentItemPun = do
   sym <- symbol
@@ -959,7 +994,7 @@ pnamedArgumentItemPun = do
 -- using excessive backtracking.
 manyNamedArgumentNewRBrace ::
   forall r.
-  (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
   ParsecS r [NamedArgumentNew 'Parsed]
 manyNamedArgumentNewRBrace = reverse <$> go []
   where
@@ -1004,9 +1039,10 @@ pisExhaustive = do
 
 namedApplicationNew ::
   forall r.
-  (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
   ParsecS r (NamedApplicationNew 'Parsed)
 namedApplicationNew = P.label "<named application>" $ do
+  checkNoNamedApplicationMissingAt
   (_namedApplicationNewName, _namedApplicationNewExhaustive) <- P.try $ do
     n <- name
     exhaustive <- pisExhaustive
@@ -1016,17 +1052,17 @@ namedApplicationNew = P.label "<named application>" $ do
   let _namedApplicationNewExtra = Irrelevant ()
   return NamedApplicationNew {..}
 
-hole :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (HoleType 'Parsed)
+hole :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (HoleType 'Parsed)
 hole = kw kwHole
 
-parseListPattern :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (ListPattern 'Parsed)
+parseListPattern :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (ListPattern 'Parsed)
 parseListPattern = do
   _listpBracketL <- Irrelevant <$> kw kwBracketL
   _listpItems <- P.sepBy parsePatternAtoms (kw delimSemicolon)
   _listpBracketR <- Irrelevant <$> kw kwBracketR
   return ListPattern {..}
 
-parseList :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (List 'Parsed)
+parseList :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (List 'Parsed)
 parseList = do
   _listBracketL <- Irrelevant <$> kw kwBracketL
   _listItems <- P.sepBy parseExpressionAtoms (kw delimSemicolon)
@@ -1037,15 +1073,15 @@ parseList = do
 -- Literals
 --------------------------------------------------------------------------------
 
-literalInteger :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r LiteralLoc
+literalInteger :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r LiteralLoc
 literalInteger = fmap LitIntegerWithBase <$> integerWithBase
 
-literalString :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r LiteralLoc
+literalString :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r LiteralLoc
 literalString = do
   (x, loc) <- string
   return (WithLoc loc (LitString x))
 
-literal :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r LiteralLoc
+literal :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r LiteralLoc
 literal = do
   l <-
     literalInteger
@@ -1054,19 +1090,25 @@ literal = do
 
 letFunDef ::
   forall r.
-  (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
   ParsecS r (FunctionDef 'Parsed)
 letFunDef = do
   optional_ stashPragmas
-  functionDefinition True False Nothing
+  functionDefinition funSyntax Nothing
+  where
+    funSyntax =
+      FunctionSyntaxOptions
+        { _funAllowOmitType = True,
+          _funAllowInstance = False
+        }
 
-letStatement :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (LetStatement 'Parsed)
+letStatement :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (LetStatement 'Parsed)
 letStatement =
   LetFunctionDef <$> letFunDef
     <|> LetAliasDef <$> (kw kwSyntax >>= aliasDef)
     <|> LetOpen <$> openModule
 
-doBind :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (DoBind 'Parsed)
+doBind :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (DoBind 'Parsed)
 doBind = do
   (_doBindPattern, _doBindArrowKw) <- P.try $ do
     pat <- parsePatternAtoms
@@ -1075,14 +1117,14 @@ doBind = do
   _doBindExpression <- parseExpressionAtoms
   return DoBind {..}
 
-doLet :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (DoLet 'Parsed)
+doLet :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (DoLet 'Parsed)
 doLet = do
   _doLetKw <- Irrelevant <$> kw kwLet
   _doLetStatements <- P.sepEndBy1 letStatement semicolon
   _doLetInKw <- Irrelevant <$> kw kwIn
   return DoLet {..}
 
-doStatements :: forall r. (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (NonEmpty (DoStatement 'Parsed))
+doStatements :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (NonEmpty (DoStatement 'Parsed))
 doStatements =
   P.label "<do statement>" $
     plet
@@ -1106,7 +1148,7 @@ doStatements =
               return (s :| ss)
           | otherwise -> return (pure s)
 
-doBlock :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (Do 'Parsed)
+doBlock :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (Do 'Parsed)
 doBlock = do
   _doKeyword <- Irrelevant <$> kw kwDo
   lbr <- kw delimBraceL
@@ -1119,7 +1161,7 @@ doBlock = do
         ..
       }
 
-letBlock :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (Let 'Parsed)
+letBlock :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (Let 'Parsed)
 letBlock = do
   _letKw <- kw kwLet
   _letFunDefs <- P.sepEndBy1 letStatement semicolon
@@ -1130,7 +1172,7 @@ letBlock = do
 -- | The pipe for the first branch is optional
 sideIfBranch ::
   forall r k.
-  (SingI k, Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  (SingI k, Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
   Bool ->
   ParsecS r (SideIfBranch 'Parsed k)
 sideIfBranch isFirst = do
@@ -1152,7 +1194,7 @@ sideIfBranch isFirst = do
   _sideIfBranchBody <- parseExpressionAtoms
   return SideIfBranch {..}
 
-sideIfs :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (SideIfs 'Parsed)
+sideIfs :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (SideIfs 'Parsed)
 sideIfs = do
   fstBranch <- sideIfBranch True
   moreBranches <- many (sideIfBranch False)
@@ -1163,24 +1205,24 @@ sideIfs = do
       { ..
       }
 
-pcaseBranchRhs :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (CaseBranchRhs 'Parsed)
+pcaseBranchRhs :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (CaseBranchRhs 'Parsed)
 pcaseBranchRhs =
   CaseBranchRhsExpression <$> pcaseBranchRhsExpression
     <|> CaseBranchRhsIf <$> sideIfs
 
-pcaseBranchRhsExpression :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (RhsExpression 'Parsed)
+pcaseBranchRhsExpression :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (RhsExpression 'Parsed)
 pcaseBranchRhsExpression = do
   _rhsExpressionAssignKw <- Irrelevant <$> kw kwAssign
   _rhsExpression <- parseExpressionAtoms
   return RhsExpression {..}
 
-caseBranch :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => Irrelevant (Maybe KeywordRef) -> ParsecS r (CaseBranch 'Parsed)
+caseBranch :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => Irrelevant (Maybe KeywordRef) -> ParsecS r (CaseBranch 'Parsed)
 caseBranch _caseBranchPipe = do
   _caseBranchPattern <- parsePatternAtoms
   _caseBranchRhs <- pcaseBranchRhs
   return CaseBranch {..}
 
-case_ :: forall r. (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (Case 'Parsed)
+case_ :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (Case 'Parsed)
 case_ = P.label "case" $ do
   _caseKw <- kw kwCase
   _caseExpression <- parseExpressionAtoms
@@ -1190,7 +1232,7 @@ case_ = P.label "case" $ do
 
 ifBranch ::
   forall r k.
-  (SingI k, Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  (SingI k, Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
   ParsecS r (IfBranch 'Parsed k)
 ifBranch = do
   _ifBranchPipe <- Irrelevant <$> pipeHelper
@@ -1206,7 +1248,7 @@ ifBranch = do
       SBranchIfBool -> P.try (kw kwPipe <* P.notFollowedBy (kw kwElse))
       SBranchIfElse -> kw kwPipe
 
-multiwayIf :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (If 'Parsed)
+multiwayIf :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (If 'Parsed)
 multiwayIf = do
   _ifKw <- kw kwIf
   _ifBranches <- many ifBranch
@@ -1217,7 +1259,7 @@ multiwayIf = do
 -- Universe expression
 --------------------------------------------------------------------------------
 
-universe :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r Universe
+universe :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r Universe
 universe = do
   i <- kw kwType
   lvl :: Maybe (WithLoc Natural) <- fmap (uncurry (flip WithLoc)) <$> optional decimal
@@ -1243,87 +1285,121 @@ getPragmas = P.lift $ do
   put (Nothing @ParsedPragmas)
   return j
 
-functionDefinition ::
+functionDefinitionLhs ::
   forall r.
-  (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
-  Bool ->
-  Bool ->
+  (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
+  FunctionSyntaxOptions ->
   Maybe (WithLoc BuiltinFunction) ->
-  ParsecS r (FunctionDef 'Parsed)
-functionDefinition allowOmitType allowInstance _signBuiltin = P.label "<function definition>" $ do
-  _signTerminating <- optional (kw kwTerminating)
+  ParsecS r (FunctionLhs 'Parsed)
+functionDefinitionLhs opts _funLhsBuiltin = P.label "<function definition>" $ do
+  let allowInstance = opts ^. funAllowInstance
+      allowOmitType = opts ^. funAllowOmitType
+  _funLhsTerminating <- optional (kw kwTerminating)
   off <- P.getOffset
-  _signCoercion <- optional (kw kwCoercion)
-  unless (allowInstance || isNothing _signCoercion) $
+  _funLhsCoercion <- optional (kw kwCoercion)
+  unless (allowInstance || isNothing _funLhsCoercion) $
     parseFailure off "coercion not allowed here"
   off0 <- P.getOffset
-  _signInstance <- optional (kw kwInstance)
-  unless (allowInstance || isNothing _signInstance) $
+  _funLhsInstance <- optional (kw kwInstance)
+  unless (allowInstance || isNothing _funLhsInstance) $
     parseFailure off0 "instance not allowed here"
-  when (isJust _signCoercion && isNothing _signInstance) $
+  when (isJust _funLhsCoercion && isNothing _funLhsInstance) $
     parseFailure off0 "expected: instance"
-  _signName <- symbol
-  _signArgs <- many parseArg
-  off' <- P.getOffset
-  _signColonKw <-
+  _funLhsName <- symbol
+  _funLhsArgs <- many parseArg
+  _funLhsColonKw <-
     Irrelevant
       <$> if
           | allowOmitType -> optional (kw kwColon)
           | otherwise -> Just <$> kw kwColon
-  _signRetType <-
-    case _signColonKw ^. unIrrelevant of
+  _funLhsRetType <-
+    case _funLhsColonKw ^. unIrrelevant of
       Just {} -> Just <$> parseExpressionAtoms
       Nothing -> return Nothing
+  return
+    FunctionLhs
+      { _funLhsInstance,
+        _funLhsBuiltin,
+        _funLhsCoercion,
+        _funLhsName,
+        _funLhsArgs,
+        _funLhsColonKw,
+        _funLhsRetType,
+        _funLhsTerminating
+      }
+
+parseArg :: forall r. (Members '[ParserResultBuilder, JudocStash, PragmasStash, Error ParserError] r) => ParsecS r (SigArg 'Parsed)
+parseArg = do
+  (openDelim, _sigArgNames, _sigArgImplicit, _sigArgColon) <- P.try $ do
+    (opn, impl) <- implicitOpen
+    let parseArgumentName :: ParsecS r (Argument 'Parsed) =
+          ArgumentSymbol <$> symbol
+            <|> ArgumentWildcard <$> wildcard
+    let parseArgumentNameColon :: ParsecS r (Argument 'Parsed, Irrelevant KeywordRef) = P.try $ do
+          n <- parseArgumentName
+          c <- Irrelevant <$> kw kwColon
+          return (n, c)
+    (ns :: SigArgNames 'Parsed, c) <- case impl of
+      ImplicitInstance -> do
+        ma <- optional parseArgumentNameColon
+        return $ case ma of
+          Just (ns', c') -> (SigArgNames (pure ns'), Just c')
+          Nothing -> (SigArgNamesInstance, Nothing)
+      Implicit -> do
+        ns <- SigArgNames <$> some1 parseArgumentName
+        c <- optional (Irrelevant <$> kw kwColon)
+        return (ns, c)
+      Explicit -> do
+        ns <- SigArgNames <$> some1 parseArgumentName
+        c <- Just . Irrelevant <$> kw kwColon
+        return (ns, c)
+    return (opn, ns, impl, c)
+  _sigArgType <- case _sigArgImplicit of
+    Implicit
+      | isNothing _sigArgColon ->
+          return Nothing
+    _ ->
+      Just <$> parseExpressionAtoms
+  _sigArgDefault <- optional $ do
+    _argDefaultAssign <- Irrelevant <$> kw kwAssign
+    _argDefaultValue <- parseExpressionAtoms
+    return ArgDefault {..}
+  closeDelim <- implicitClose _sigArgImplicit
+  let _sigArgDelims = Irrelevant (openDelim, closeDelim)
+  return SigArg {..}
+
+functionDefinition ::
+  forall r.
+  (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
+  FunctionSyntaxOptions ->
+  Maybe (WithLoc BuiltinFunction) ->
+  ParsecS r (FunctionDef 'Parsed)
+functionDefinition opts _signBuiltin = P.label "<function definition>" $ do
+  FunctionLhs {..} <- functionDefinitionLhs opts _signBuiltin
+  off <- P.getOffset
   _signDoc <- getJudoc
   _signPragmas <- getPragmas
   _signBody <- parseBody
   unless
-    ( isJust (_signColonKw ^. unIrrelevant)
-        || (P.isBodyExpression _signBody && null _signArgs)
+    ( isJust (_funLhsColonKw ^. unIrrelevant)
+        || (P.isBodyExpression _signBody && null _funLhsArgs)
     )
-    $ parseFailure off' "expected result type"
-  return FunctionDef {..}
+    $ parseFailure off "expected result type"
+  return
+    FunctionDef
+      { _signName = _funLhsName,
+        _signArgs = _funLhsArgs,
+        _signColonKw = _funLhsColonKw,
+        _signRetType = _funLhsRetType,
+        _signTerminating = _funLhsTerminating,
+        _signInstance = _funLhsInstance,
+        _signCoercion = _funLhsCoercion,
+        _signBuiltin = _funLhsBuiltin,
+        _signDoc,
+        _signPragmas,
+        _signBody
+      }
   where
-    parseArg :: ParsecS r (SigArg 'Parsed)
-    parseArg = do
-      (openDelim, _sigArgNames, _sigArgImplicit, _sigArgColon) <- P.try $ do
-        (opn, impl) <- implicitOpen
-        let parseArgumentName :: ParsecS r (Argument 'Parsed) =
-              ArgumentSymbol <$> symbol
-                <|> ArgumentWildcard <$> wildcard
-        let parseArgumentNameColon :: ParsecS r (Argument 'Parsed, Irrelevant KeywordRef) = P.try $ do
-              n <- parseArgumentName
-              c <- Irrelevant <$> kw kwColon
-              return (n, c)
-        (ns :: SigArgNames 'Parsed, c) <- case impl of
-          ImplicitInstance -> do
-            ma <- optional parseArgumentNameColon
-            return $ case ma of
-              Just (ns', c') -> (SigArgNames (pure ns'), Just c')
-              Nothing -> (SigArgNamesInstance, Nothing)
-          Implicit -> do
-            ns <- SigArgNames <$> some1 parseArgumentName
-            c <- optional (Irrelevant <$> kw kwColon)
-            return (ns, c)
-          Explicit -> do
-            ns <- SigArgNames <$> some1 parseArgumentName
-            c <- Just . Irrelevant <$> kw kwColon
-            return (ns, c)
-        return (opn, ns, impl, c)
-      _sigArgType <- case _sigArgImplicit of
-        Implicit
-          | isNothing _sigArgColon ->
-              return Nothing
-        _ ->
-          Just <$> parseExpressionAtoms
-      _sigArgDefault <- optional $ do
-        _argDefaultAssign <- Irrelevant <$> kw kwAssign
-        _argDefaultValue <- parseExpressionAtoms
-        return ArgDefault {..}
-      closeDelim <- implicitClose _sigArgImplicit
-      let _sigArgDelims = Irrelevant (openDelim, closeDelim)
-      return SigArg {..}
-
     parseBody :: ParsecS r (FunctionDefBody 'Parsed)
     parseBody =
       SigBodyExpression <$> bodyExpr
@@ -1336,15 +1412,17 @@ functionDefinition allowOmitType allowInstance _signBuiltin = P.label "<function
           _clausenAssignKw <- Irrelevant <$> kw kwAssign
           _clausenBody <- parseExpressionAtoms
           return FunctionClause {..}
+
         bodyClauses :: ParsecS r (NonEmpty (FunctionClause 'Parsed))
         bodyClauses = some1 bodyClause
+
         bodyExpr :: ParsecS r (ExpressionAtoms 'Parsed)
         bodyExpr = do
           void (kw kwAssign)
           parseExpressionAtoms
 
 axiomDef ::
-  (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
   Maybe (WithLoc BuiltinAxiom) ->
   ParsecS r (AxiomDef 'Parsed)
 axiomDef _axiomBuiltin = do
@@ -1361,36 +1439,37 @@ axiomDef _axiomBuiltin = do
 --------------------------------------------------------------------------------
 
 implicitOpenField ::
-  (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
   ParsecS r (KeywordRef, IsImplicitField)
 implicitOpenField =
   (,ImplicitInstanceField) <$> kw delimDoubleBraceL
     <|> (,ExplicitField) <$> kw delimParenL
 
-implicitOpen :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (KeywordRef, IsImplicit)
+implicitOpen :: (Members '[ParserResultBuilder] r) => ParsecS r (KeywordRef, IsImplicit)
 implicitOpen =
   (,ImplicitInstance) <$> kw delimDoubleBraceL
     <|> (,Implicit) <$> kw delimBraceL
     <|> (,Explicit) <$> kw delimParenL
 
 implicitCloseField ::
-  (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
   IsImplicitField ->
   ParsecS r KeywordRef
 implicitCloseField = \case
   ExplicitField -> kw delimParenR
   ImplicitInstanceField -> kw delimDoubleBraceR
 
-implicitClose :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => IsImplicit -> ParsecS r KeywordRef
+implicitClose :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => IsImplicit -> ParsecS r KeywordRef
 implicitClose = \case
   Implicit -> kw delimBraceR
   Explicit -> kw delimParenR
   ImplicitInstance -> kw delimDoubleBraceR
 
-functionParams :: forall r. (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (FunctionParameters 'Parsed)
-functionParams = do
+functionParams :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (FunctionParameters 'Parsed)
+functionParams = P.label "<function type parameters>" $ do
   (openDelim, _paramNames, _paramImplicit, _paramColon) <- P.try $ do
     (opn, impl) <- implicitOpen
+    -- checking that there is a : and not a := is needed to give a better error for missing @ in named application.
     case impl of
       ImplicitInstance -> do
         n <- pName <* kw kwColon
@@ -1409,7 +1488,7 @@ functionParams = do
       FunctionParameterName <$> symbol
         <|> FunctionParameterWildcard <$> kw kwWildcard
 
-function :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (Function 'Parsed)
+function :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (Function 'Parsed)
 function = do
   _funParameters <- functionParams
   _funKw <- kw kwRightArrow
@@ -1420,14 +1499,14 @@ function = do
 -- Lambda expression
 --------------------------------------------------------------------------------
 
-lambdaClause :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => Irrelevant (Maybe KeywordRef) -> ParsecS r (LambdaClause 'Parsed)
+lambdaClause :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => Irrelevant (Maybe KeywordRef) -> ParsecS r (LambdaClause 'Parsed)
 lambdaClause _lambdaPipe = do
   _lambdaParameters <- P.some patternAtom
   _lambdaAssignKw <- Irrelevant <$> kw kwAssign
   _lambdaBody <- parseExpressionAtoms
   return LambdaClause {..}
 
-lambda :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (Lambda 'Parsed)
+lambda :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (Lambda 'Parsed)
 lambda = do
   _lambdaKw <- kw kwLambda
   brl <- kw delimBraceL
@@ -1440,7 +1519,7 @@ lambda = do
 -- Data type construction declaration
 -------------------------------------------------------------------------------
 
-inductiveDef :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => Maybe (WithLoc BuiltinInductive) -> ParsecS r (InductiveDef 'Parsed)
+inductiveDef :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => Maybe (WithLoc BuiltinInductive) -> ParsecS r (InductiveDef 'Parsed)
 inductiveDef _inductiveBuiltin = do
   _inductivePositive <- optional (kw kwPositive)
   _inductiveTrait <- optional (kw kwTrait)
@@ -1460,7 +1539,7 @@ inductiveDef _inductiveBuiltin = do
       P.<?> "<constructor definition>"
   return InductiveDef {..}
 
-inductiveParamsLong :: forall r. (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (InductiveParameters 'Parsed)
+inductiveParamsLong :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (InductiveParameters 'Parsed)
 inductiveParamsLong = parens $ do
   _inductiveParametersNames <- some1 symbol
   colonMay <- optional (Irrelevant <$> kw kwColon)
@@ -1472,7 +1551,7 @@ inductiveParamsLong = parens $ do
       _inductiveParametersType <- parseExpressionAtoms
       return InductiveParametersRhs {..}
 
-inductiveParamsShort :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (InductiveParameters 'Parsed)
+inductiveParamsShort :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (InductiveParameters 'Parsed)
 inductiveParamsShort = do
   _inductiveParametersNames <- some1 symbol
   return
@@ -1481,16 +1560,16 @@ inductiveParamsShort = do
         ..
       }
 
-inductiveParams :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (InductiveParameters 'Parsed)
+inductiveParams :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (InductiveParameters 'Parsed)
 inductiveParams = inductiveParamsLong <|> inductiveParamsShort
 
-rhsGadt :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (RhsGadt 'Parsed)
+rhsGadt :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (RhsGadt 'Parsed)
 rhsGadt = P.label "<constructor gadt>" $ do
   _rhsGadtColon <- Irrelevant <$> kw kwColon
   _rhsGadtType <- parseExpressionAtoms P.<?> "<constructor type>"
   return RhsGadt {..}
 
-recordField :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (RecordField 'Parsed)
+recordField :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (RecordField 'Parsed)
 recordField = do
   _fieldDoc <- optional stashJudoc >> getJudoc
   _fieldPragmas <- optional stashPragmas >> getPragmas
@@ -1503,12 +1582,12 @@ recordField = do
   _fieldType <- parseExpressionAtoms
   return RecordField {..}
 
-rhsAdt :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (RhsAdt 'Parsed)
+rhsAdt :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (RhsAdt 'Parsed)
 rhsAdt = P.label "<constructor arguments>" $ do
   _rhsAdtArguments <- many atomicExpression
   return RhsAdt {..}
 
-rhsRecord :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (RhsRecord 'Parsed)
+rhsRecord :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (RhsRecord 'Parsed)
 rhsRecord = P.label "<constructor record>" $ do
   l <- kw delimBraceL
   _rhsRecordStatements <- P.sepEndBy recordStatement semicolon
@@ -1516,7 +1595,7 @@ rhsRecord = P.label "<constructor record>" $ do
   let _rhsRecordDelim = Irrelevant (l, r)
   return RhsRecord {..}
 
-recordStatement :: forall r. (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (RecordStatement 'Parsed)
+recordStatement :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (RecordStatement 'Parsed)
 recordStatement =
   RecordStatementSyntax <$> syntax
     <|> RecordStatementField <$> recordField
@@ -1527,13 +1606,13 @@ recordStatement =
       RecordSyntaxIterator <$> iteratorSyntaxDef syn
         <|> RecordSyntaxOperator <$> operatorSyntaxDef syn
 
-pconstructorRhs :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (ConstructorRhs 'Parsed)
+pconstructorRhs :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (ConstructorRhs 'Parsed)
 pconstructorRhs =
   ConstructorRhsGadt <$> rhsGadt
     <|> ConstructorRhsRecord <$> rhsRecord
     <|> ConstructorRhsAdt <$> rhsAdt
 
-constructorDef :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => Symbol -> Irrelevant (Maybe KeywordRef) -> ParsecS r (ConstructorDef 'Parsed)
+constructorDef :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => Symbol -> Irrelevant (Maybe KeywordRef) -> ParsecS r (ConstructorDef 'Parsed)
 constructorDef _constructorInductiveName _constructorPipe = do
   _constructorDoc <- optional stashJudoc >> getJudoc
   _constructorPragmas <- optional stashPragmas >> getPragmas
@@ -1541,10 +1620,10 @@ constructorDef _constructorInductiveName _constructorPipe = do
   _constructorRhs <- pconstructorRhs
   return ConstructorDef {..}
 
-wildcard :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r Wildcard
+wildcard :: (Members '[ParserResultBuilder] r) => ParsecS r Wildcard
 wildcard = Wildcard . snd <$> interval (kw kwWildcard)
 
-patternAtomWildcardConstructor :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (WildcardConstructor 'Parsed)
+patternAtomWildcardConstructor :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (WildcardConstructor 'Parsed)
 patternAtomWildcardConstructor = P.try $ do
   _wildcardConstructor <- name
   _wildcardConstructorAtKw <- Irrelevant <$> kw kwAt
@@ -1553,7 +1632,38 @@ patternAtomWildcardConstructor = P.try $ do
   let _wildcardConstructorDelims = Irrelevant (l, r)
   return WildcardConstructor {..}
 
-patternAtomAnon :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (PatternAtom 'Parsed)
+-- | Used to report better errors when the user forgets the @ on a named
+-- application. It tries to parse the lhs of a function definition (up to the
+-- :=). If it succeeds, it reports an error.
+checkNoNamedApplicationMissingAt :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r ()
+checkNoNamedApplicationMissingAt = recoverStashes $ do
+  let funSyntax =
+        FunctionSyntaxOptions
+          { _funAllowOmitType = True,
+            _funAllowInstance = False
+          }
+  x <-
+    P.observing
+      . P.try
+      . interval
+      $ do
+        fun <- symbol
+        lbrace
+        lhs <- functionDefinitionLhs funSyntax Nothing
+        kw kwAssign
+        return (fun, lhs)
+  case x of
+    Left {} -> return ()
+    Right ((fun, lhs), loc) ->
+      P.lift . throw $
+        ErrNamedApplicationMissingAt
+          NamedApplicationMissingAt
+            { _namedApplicationMissingAtLoc = loc,
+              _namedApplicationMissingAtLhs = lhs,
+              _namedApplicationMissingAtFun = fun
+            }
+
+patternAtomAnon :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (PatternAtom 'Parsed)
 patternAtomAnon =
   PatternAtomWildcard <$> wildcard
     <|> PatternAtomDoubleBraces <$> doubleBraces parsePatternAtomsNested
@@ -1561,13 +1671,13 @@ patternAtomAnon =
     <|> PatternAtomBraces <$> braces parsePatternAtomsNested
     <|> PatternAtomList <$> parseListPattern
 
-patternAtomAt :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => Symbol -> ParsecS r PatternBinding
+patternAtomAt :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => Symbol -> ParsecS r PatternBinding
 patternAtomAt _patternBindingName = do
   _patternBindingAtKw <- Irrelevant <$> kw kwAt
   _patternBindingPattern <- patternAtom
   return PatternBinding {..}
 
-recordPatternItem :: forall r. (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (RecordPatternItem 'Parsed)
+recordPatternItem :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (RecordPatternItem 'Parsed)
 recordPatternItem = do
   f <- symbol
   RecordPatternItemAssign <$> recordPatternItemAssign f
@@ -1591,7 +1701,7 @@ recordPatternItem = do
           _fieldPunField = f
         }
 
-patternAtomRecord :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => Name -> ParsecS r (RecordPattern 'Parsed)
+patternAtomRecord :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => Name -> ParsecS r (RecordPattern 'Parsed)
 patternAtomRecord _recordPatternConstructor = do
   -- The try is needed to disambiguate from `at` pattern
   P.try (void (kw kwAt >> kw delimBraceL))
@@ -1601,7 +1711,7 @@ patternAtomRecord _recordPatternConstructor = do
     RecordPattern {..}
 
 -- | A pattern that starts with an identifier
-patternAtomNamed :: forall r. (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => Bool -> ParsecS r (PatternAtom 'Parsed)
+patternAtomNamed :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => Bool -> ParsecS r (PatternAtom 'Parsed)
 patternAtomNamed nested = do
   off <- P.getOffset
   n <- name
@@ -1621,25 +1731,25 @@ patternAtomNamed nested = do
         (not nested && t ^. withLocParam == "=")
         (parseFailure off "expected \":=\" instead of \"=\"")
 
-patternAtomNested :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (PatternAtom 'Parsed)
+patternAtomNested :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (PatternAtom 'Parsed)
 patternAtomNested = patternAtom' True
 
-patternAtom :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (PatternAtom 'Parsed)
+patternAtom :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (PatternAtom 'Parsed)
 patternAtom = patternAtom' False
 
-patternAtom' :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => Bool -> ParsecS r (PatternAtom 'Parsed)
+patternAtom' :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => Bool -> ParsecS r (PatternAtom 'Parsed)
 patternAtom' nested =
   P.label "<pattern>" $
     PatternAtomWildcardConstructor <$> patternAtomWildcardConstructor
       <|> patternAtomNamed nested
       <|> patternAtomAnon
 
-parsePatternAtoms :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (PatternAtoms 'Parsed)
+parsePatternAtoms :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (PatternAtoms 'Parsed)
 parsePatternAtoms = do
   (_patternAtoms, _patternAtomsLoc) <- second Irrelevant <$> interval (P.some patternAtom)
   return PatternAtoms {..}
 
-parsePatternAtomsNested :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (PatternAtoms 'Parsed)
+parsePatternAtomsNested :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (PatternAtoms 'Parsed)
 parsePatternAtomsNested = do
   (_patternAtoms, _patternAtomsLoc) <- second Irrelevant <$> interval (P.some patternAtomNested)
   return PatternAtoms {..}
@@ -1648,12 +1758,12 @@ parsePatternAtomsNested = do
 -- Module declaration
 --------------------------------------------------------------------------------
 
-pmodulePath :: forall t r. (SingI t, Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (ModulePathType 'Parsed t)
+pmodulePath :: forall t r. (SingI t, Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (ModulePathType 'Parsed t)
 pmodulePath = case sing :: SModuleIsTop t of
   SModuleTop -> topModulePath
   SModuleLocal -> symbol
 
-moduleDef :: forall t r. (SingI t, Members '[Error ParserError, ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (Module 'Parsed t)
+moduleDef :: forall t r. (SingI t, Members '[Error ParserError, ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (Module 'Parsed t)
 moduleDef = P.label "<module definition>" $ do
   _moduleKw <- kw kwModule
   _moduleDoc <- getJudoc
@@ -1680,7 +1790,7 @@ moduleDef = P.label "<module definition>" $ do
       SModuleTop -> optional_ (kw kwEnd >> semicolon)
 
 -- | An ExpressionAtom which is a valid expression on its own.
-atomicExpression :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (ExpressionAtoms 'Parsed)
+atomicExpression :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (ExpressionAtoms 'Parsed)
 atomicExpression = do
   (atom, loc) <- interval expressionAtom
   case atom of
@@ -1697,6 +1807,7 @@ openModule ::
     Members
       '[ ParserResultBuilder,
          PragmasStash,
+         Error ParserError,
          JudocStash
        ]
       r
@@ -1711,7 +1822,7 @@ openModule = do
   _openModulePublic <- publicAnn
   return OpenModule {..}
 
-usingOrHiding :: (Members '[ParserResultBuilder, JudocStash, PragmasStash] r) => ParsecS r (UsingHiding 'Parsed)
+usingOrHiding :: (Members '[ParserResultBuilder, JudocStash, PragmasStash, Error ParserError] r) => ParsecS r (UsingHiding 'Parsed)
 usingOrHiding =
   Using <$> pusingList
     <|> Hiding <$> phidingList
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource/ParserResultBuilder.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource/ParserResultBuilder.hs
index e02007538f..f4b4c4234f 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource/ParserResultBuilder.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource/ParserResultBuilder.hs
@@ -68,6 +68,13 @@ registerLiteral l =
 registerItem' :: (Member (State ParserState) r) => ParsedItem -> Sem r ()
 registerItem' i = modify' (over parserStateParsedItems (i :))
 
+evalParserResultBuilder ::
+  (Member HighlightBuilder r) =>
+  ParserState ->
+  Sem (ParserResultBuilder ': r) a ->
+  Sem r a
+evalParserResultBuilder s = fmap snd . runParserResultBuilder s
+
 execParserResultBuilder ::
   (Member HighlightBuilder r) =>
   ParserState ->
diff --git a/src/Juvix/Data/CodeAnn.hs b/src/Juvix/Data/CodeAnn.hs
index 37cfb4f358..01225bc041 100644
--- a/src/Juvix/Data/CodeAnn.hs
+++ b/src/Juvix/Data/CodeAnn.hs
@@ -245,7 +245,7 @@ kwDot :: Doc Ann
 kwDot = delimiter "."
 
 kwAt :: Doc Ann
-kwAt = delimiter Str.at_
+kwAt = keyword Str.at_
 
 code :: Doc Ann -> Doc Ann
 code = annotate AnnCode
diff --git a/src/Juvix/Parser/Error.hs b/src/Juvix/Parser/Error.hs
index d464a50115..a59d1ae607 100644
--- a/src/Juvix/Parser/Error.hs
+++ b/src/Juvix/Parser/Error.hs
@@ -23,10 +23,10 @@ data ParserError
   | ErrWrongTopModuleName WrongTopModuleName
   | ErrWrongTopModuleNameOrphan WrongTopModuleNameOrphan
   | ErrStdinOrFile StdinOrFileError
+  | ErrNamedApplicationMissingAt NamedApplicationMissingAt
   | ErrDanglingJudoc DanglingJudoc
   | ErrMarkdownBackend MarkdownBackendError
   | ErrFlatParseError FlatParseError
-  deriving stock (Show)
 
 instance ToGenericError ParserError where
   genericError = \case
@@ -38,6 +38,7 @@ instance ToGenericError ParserError where
     ErrDanglingJudoc e -> genericError e
     ErrMarkdownBackend e -> genericError e
     ErrFlatParseError e -> genericError e
+    ErrNamedApplicationMissingAt e -> genericError e
 
 newtype FlatParseError = FlatParseError
   { _flatParseErrorLoc :: Interval
@@ -201,3 +202,39 @@ instance ToGenericError DanglingJudoc where
     where
       i :: Interval
       i = getLoc _danglingJudoc
+
+data NamedApplicationMissingAt = NamedApplicationMissingAt
+  { _namedApplicationMissingAtLoc :: Interval,
+    _namedApplicationMissingAtFun :: Symbol,
+    _namedApplicationMissingAtLhs :: FunctionLhs 'Parsed
+  }
+
+instance ToGenericError NamedApplicationMissingAt where
+  genericError NamedApplicationMissingAt {..} = do
+    opts <- fromGenericOptions <$> ask @GenericOptions
+    let lhs :: FunctionLhs 'Parsed = _namedApplicationMissingAtLhs
+        funWord :: Text
+          | null (lhs ^. funLhsArgs) = "assignment"
+          | otherwise = "function definition"
+        fun' = ppCode opts _namedApplicationMissingAtFun
+        msg :: Doc CodeAnn =
+          "Unexpected "
+            <> pretty funWord
+            <+> ppCode opts _namedApplicationMissingAtLhs
+            <+> kwAssign
+              <> "\nPerhaps you intended to write a named application and missed the"
+            <+> kwAt
+            <+> "symbol? That would be something like"
+              <> line
+              <> fun'
+              <> kwAt
+              <> "{arg1 := ...; arg2 := ...; ... }"
+    return
+      GenericError
+        { _genericErrorLoc = i,
+          _genericErrorMessage = mkAnsiText msg,
+          _genericErrorIntervals = [i]
+        }
+    where
+      i :: Interval
+      i = _namedApplicationMissingAtLoc
diff --git a/test/Parsing/Negative.hs b/test/Parsing/Negative.hs
index 2743a84c23..fde6086e4b 100644
--- a/test/Parsing/Negative.hs
+++ b/test/Parsing/Negative.hs
@@ -82,6 +82,13 @@ parserErrorTests =
       $ \case
         ErrMegaparsec {} -> Nothing
         _ -> wrongError,
+    negTest
+      "Missing @ in named application"
+      $(mkRelDir ".")
+      $(mkRelFile "NamedApplicationMissingAt.juvix")
+      $ \case
+        ErrNamedApplicationMissingAt {} -> Nothing
+        _ -> wrongError,
     negTest
       "Error on local instances"
       $(mkRelDir ".")
diff --git a/tests/negative/NamedApplicationMissingAt.juvix b/tests/negative/NamedApplicationMissingAt.juvix
new file mode 100644
index 0000000000..fb23f72064
--- /dev/null
+++ b/tests/negative/NamedApplicationMissingAt.juvix
@@ -0,0 +1,8 @@
+module NamedApplicationMissingAt;
+
+type T := t;
+
+fun (a : T)
+ : T := t;
+
+main : T := fun {a := t};