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 9878dca050..25c122fc75 100644
--- a/src/Juvix/Compiler/Concrete/Language/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Language/Base.hs
@@ -2801,15 +2801,15 @@ deriving stock instance Ord (JudocAtom 'Parsed)
 
 deriving stock instance Ord (JudocAtom 'Scoped)
 
-data FunctionLhs = FunctionLhs
-  { _funLhsInstance :: Maybe KeywordRef,
+data FunctionLhs (s :: Stage) = FunctionLhs
+  { _funLhsBuiltin :: Maybe (WithLoc BuiltinFunction),
+    _funLhsTerminating :: Maybe KeywordRef,
+    _funLhsInstance :: Maybe KeywordRef,
     _funLhsCoercion :: Maybe KeywordRef,
-    _funLhsName :: FunctionName 'Parsed,
-    _funLhsArgs :: [SigArg 'Parsed],
+    _funLhsName :: FunctionName s,
+    _funLhsArgs :: [SigArg s],
     _funLhsColonKw :: Irrelevant (Maybe KeywordRef),
-    _funLhsRetType :: Maybe (ExpressionType 'Parsed),
-    _funLhsTerminating :: Maybe KeywordRef,
-    _funLhsAfterLastArgOff :: Int
+    _funLhsRetType :: Maybe (ExpressionType s)
   }
 
 makeLenses ''SideIfs
@@ -2900,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 f956300513..5fab4fc798 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@@ -849,10 +849,7 @@ expressionAtom =
       <|> AtomParens <$> parens parseExpressionAtoms
       <|> AtomDoubleBraces <$> pdoubleBracesExpression
       <|> AtomRecordUpdate <$> recordUpdate
-      <|> ( do
-              checkNoNamedApplication
-              AtomBraces <$> withLoc (braces parseExpressionAtoms)
-          )
+      <|> AtomBraces <$> withLoc (braces parseExpressionAtoms)
 
 parseExpressionAtoms ::
   (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
@@ -1045,6 +1042,7 @@ namedApplicationNew ::
   (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
@@ -1287,8 +1285,13 @@ getPragmas = P.lift $ do
   put (Nothing @ParsedPragmas)
   return j
 
-functionDefinitionLhs :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => FunctionSyntaxOptions -> ParsecS r FunctionLhs
-functionDefinitionLhs opts = P.label "<function definition>" $ do
+functionDefinitionLhs ::
+  forall r.
+  (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
+  FunctionSyntaxOptions ->
+  Maybe (WithLoc BuiltinFunction) ->
+  ParsecS r (FunctionLhs 'Parsed)
+functionDefinitionLhs opts _funLhsBuiltin = P.label "<function definition>" $ do
   let allowInstance = opts ^. funAllowInstance
       allowOmitType = opts ^. funAllowOmitType
   _funLhsTerminating <- optional (kw kwTerminating)
@@ -1304,7 +1307,6 @@ functionDefinitionLhs opts = P.label "<function definition>" $ do
     parseFailure off0 "expected: instance"
   _funLhsName <- symbol
   _funLhsArgs <- many parseArg
-  _funLhsAfterLastArgOff <- P.getOffset
   _funLhsColonKw <-
     Irrelevant
       <$> if
@@ -1317,8 +1319,8 @@ functionDefinitionLhs opts = P.label "<function definition>" $ do
   return
     FunctionLhs
       { _funLhsInstance,
+        _funLhsBuiltin,
         _funLhsCoercion,
-        _funLhsAfterLastArgOff,
         _funLhsName,
         _funLhsArgs,
         _funLhsColonKw,
@@ -1373,7 +1375,8 @@ functionDefinition ::
   Maybe (WithLoc BuiltinFunction) ->
   ParsecS r (FunctionDef 'Parsed)
 functionDefinition opts _signBuiltin = P.label "<function definition>" $ do
-  FunctionLhs {..} <- functionDefinitionLhs opts
+  FunctionLhs {..} <- functionDefinitionLhs opts _signBuiltin
+  off <- P.getOffset
   _signDoc <- getJudoc
   _signPragmas <- getPragmas
   _signBody <- parseBody
@@ -1381,7 +1384,7 @@ functionDefinition opts _signBuiltin = P.label "<function definition>" $ do
     ( isJust (_funLhsColonKw ^. unIrrelevant)
         || (P.isBodyExpression _signBody && null _funLhsArgs)
     )
-    $ parseFailure _funLhsAfterLastArgOff "expected result type"
+    $ parseFailure off "expected result type"
   return
     FunctionDef
       { _signName = _funLhsName,
@@ -1391,7 +1394,10 @@ functionDefinition opts _signBuiltin = P.label "<function definition>" $ do
         _signTerminating = _funLhsTerminating,
         _signInstance = _funLhsInstance,
         _signCoercion = _funLhsCoercion,
-        ..
+        _signBuiltin = _funLhsBuiltin,
+        _signDoc,
+        _signPragmas,
+        _signBody
       }
   where
     parseBody :: ParsecS r (FunctionDefBody 'Parsed)
@@ -1464,17 +1470,13 @@ 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.
-    let kwColon' :: ParsecS r KeywordRef =
-          do
-            P.notFollowedBy (kw kwAssign)
-            kw kwColon
     case impl of
       ImplicitInstance -> do
-        n <- pName <* kwColon'
+        n <- pName <* kw kwColon
         return (opn, [n], impl, Irrelevant Nothing)
       _ -> do
         n <- some pName
-        c <- Irrelevant . Just <$> kwColon'
+        c <- Irrelevant . Just <$> kw kwColon
         return (opn, n, impl, c)
   _paramType <- parseExpressionAtoms
   closeDelim <- implicitClose _paramImplicit
@@ -1633,8 +1635,8 @@ patternAtomWildcardConstructor = P.try $ do
 -- | 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.
-checkNoNamedApplication :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r ()
-checkNoNamedApplication = recoverStashes $ do
+checkNoNamedApplicationMissingAt :: forall r. (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r ()
+checkNoNamedApplicationMissingAt = recoverStashes $ do
   let funSyntax =
         FunctionSyntaxOptions
           { _funAllowOmitType = True,
@@ -1644,15 +1646,21 @@ checkNoNamedApplication = recoverStashes $ do
     P.observing
       . P.try
       . interval
-      $ lbrace >> functionDefinitionLhs funSyntax <* kw kwAssign
+      $ do
+        fun <- symbol
+        lbrace
+        lhs <- functionDefinitionLhs funSyntax Nothing
+        kw kwAssign
+        return (fun, lhs)
   case x of
     Left {} -> return ()
-    Right (lhs, loc) ->
+    Right ((fun, lhs), loc) ->
       P.lift . throw $
         ErrNamedApplicationMissingAt
           NamedApplicationMissingAt
             { _namedApplicationMissingAtLoc = loc,
-              _namedApplicationMissingAtLhs = lhs
+              _namedApplicationMissingAtLhs = lhs,
+              _namedApplicationMissingAtFun = fun
             }
 
 patternAtomAnon :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (PatternAtom 'Parsed)
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 1eb8ea58ff..a59d1ae607 100644
--- a/src/Juvix/Parser/Error.hs
+++ b/src/Juvix/Parser/Error.hs
@@ -205,20 +205,30 @@ instance ToGenericError DanglingJudoc where
 
 data NamedApplicationMissingAt = NamedApplicationMissingAt
   { _namedApplicationMissingAtLoc :: Interval,
-    _namedApplicationMissingAtLhs :: FunctionLhs
+    _namedApplicationMissingAtFun :: Symbol,
+    _namedApplicationMissingAtLhs :: FunctionLhs 'Parsed
   }
 
 instance ToGenericError NamedApplicationMissingAt where
   genericError NamedApplicationMissingAt {..} = do
-    let lhs :: FunctionLhs = _namedApplicationMissingAtLhs
-    let funWord :: Text
+    opts <- fromGenericOptions <$> ask @GenericOptions
+    let lhs :: FunctionLhs 'Parsed = _namedApplicationMissingAtLhs
+        funWord :: Text
           | null (lhs ^. funLhsArgs) = "assignment"
           | otherwise = "function definition"
-
-    let msg =
+        fun' = ppCode opts _namedApplicationMissingAtFun
+        msg :: Doc CodeAnn =
           "Unexpected "
-            <> funWord
-            <> ".\nPerhaps you intended to use the @{ .. } syntax for named applications?"
+            <> 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,