From 766fb8fd8dc58352447b85b512c78fd51a32cb05 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Thu, 30 Jan 2025 12:38:18 +0100
Subject: [PATCH 1/7] Use CoreError for parser errors unrelated to parsing

---
 app/Commands/Dev/Core/Repl.hs                 |  14 +-
 .../Compiler/Core/Translation/FromSource.hs   | 231 +++++++++---------
 2 files changed, 127 insertions(+), 118 deletions(-)

diff --git a/app/Commands/Dev/Core/Repl.hs b/app/Commands/Dev/Core/Repl.hs
index b04eb381ff..8466d79d77 100644
--- a/app/Commands/Dev/Core/Repl.hs
+++ b/app/Commands/Dev/Core/Repl.hs
@@ -22,7 +22,7 @@ runCommand opts = do
   showReplWelcome
   runRepl opts mempty
 
-parseText :: Core.InfoTable -> Text -> Either Core.MegaparsecError (Core.InfoTable, Maybe Core.Node)
+parseText :: Core.InfoTable -> Text -> Either JuvixError (Core.InfoTable, Maybe Core.Node)
 parseText = Core.runParser replPath defaultModuleId
 
 runRepl :: forall r. (Members '[EmbedIO, App] r) => CoreReplOptions -> Core.InfoTable -> Sem r ()
@@ -40,7 +40,7 @@ runRepl opts tab = do
       ':' : 'p' : ' ' : s' ->
         case parseText tab (fromString s') of
           Left err -> do
-            printJuvixError (JuvixError err)
+            printJuvixError err
             runRepl opts tab
           Right (tab', Just node) -> do
             renderStdOut (Core.ppOut opts node)
@@ -51,7 +51,7 @@ runRepl opts tab = do
       ':' : 'e' : ' ' : s' ->
         case parseText tab (fromString s') of
           Left err -> do
-            printJuvixError (JuvixError err)
+            printJuvixError err
             runRepl opts tab
           Right (tab', Just node) ->
             replEval True tab' node
@@ -60,7 +60,7 @@ runRepl opts tab = do
       ':' : 'n' : ' ' : s' ->
         case parseText tab (fromString s') of
           Left err -> do
-            printJuvixError (JuvixError err)
+            printJuvixError err
             runRepl opts tab
           Right (tab', Just node) ->
             replNormalize tab' node
@@ -69,7 +69,7 @@ runRepl opts tab = do
       ':' : 't' : ' ' : s' ->
         case parseText tab (fromString s') of
           Left err -> do
-            printJuvixError (JuvixError err)
+            printJuvixError err
             runRepl opts tab
           Right (tab', Just node) ->
             replType tab' node
@@ -80,7 +80,7 @@ runRepl opts tab = do
         sf <- someBaseToAbs' (someFile f)
         case Core.runParser sf defaultModuleId mempty s' of
           Left err -> do
-            printJuvixError (JuvixError err)
+            printJuvixError err
             runRepl opts tab
           Right (tab', mnode) -> case mnode of
             Nothing -> runRepl opts tab'
@@ -90,7 +90,7 @@ runRepl opts tab = do
       _ ->
         case parseText tab s of
           Left err -> do
-            printJuvixError (JuvixError err)
+            printJuvixError err
             runRepl opts tab
           Right (tab', Just node) ->
             replEval False tab' node
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs
index 64e931f8b3..cea81fff56 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs
@@ -11,28 +11,33 @@ import Data.List.NonEmpty (fromList)
 import Data.List.NonEmpty qualified as NonEmpty
 import Juvix.Compiler.Core.Data.InfoTable
 import Juvix.Compiler.Core.Data.InfoTableBuilder
+import Juvix.Compiler.Core.Error
 import Juvix.Compiler.Core.Extra
 import Juvix.Compiler.Core.Info qualified as Info
 import Juvix.Compiler.Core.Info.LocationInfo as LocationInfo
 import Juvix.Compiler.Core.Info.NameInfo as NameInfo
 import Juvix.Compiler.Core.Transformation.Eta
 import Juvix.Compiler.Core.Translation.FromSource.Lexer
+import Juvix.Data.CodeAnn (Ann)
 import Juvix.Data.Field
+import Juvix.Data.PPOutput (ppOutput)
 import Juvix.Extra.Strings qualified as Str
 import Juvix.Parser.Error
 import Text.Megaparsec qualified as P
 
 -- | Note: only new symbols and tags that are not in the InfoTable already will be
 -- generated during parsing
-runParser :: Path Abs File -> ModuleId -> InfoTable -> Text -> Either MegaparsecError (InfoTable, Maybe Node)
+runParser :: Path Abs File -> ModuleId -> InfoTable -> Text -> Either JuvixError (InfoTable, Maybe Node)
 runParser fileName mid tab input_ =
   case run $
-    runInfoTableBuilder (Module mid tab mempty) $
-      P.runParserT parseToplevel (fromAbsFile fileName) input_ of
-    (_, Left err) -> Left (MegaparsecError err)
-    (md, Right r) -> Right (md ^. moduleInfoTable, r)
-
-runParserMain :: Path Abs File -> ModuleId -> InfoTable -> Text -> Either MegaparsecError InfoTable
+    runError @CoreError $
+      runInfoTableBuilder (Module mid tab mempty) $
+        P.runParserT parseToplevel (fromAbsFile fileName) input_ of
+    Left err -> Left (JuvixError err)
+    Right (_, Left err) -> Left (JuvixError (MegaparsecError err))
+    Right (md, Right r) -> Right (md ^. moduleInfoTable, r)
+
+runParserMain :: Path Abs File -> ModuleId -> InfoTable -> Text -> Either JuvixError InfoTable
 runParserMain fileName mid tab input_ =
   case runParser fileName mid tab input_ of
     Left err -> Left err
@@ -62,8 +67,16 @@ setupMainFunction mid tab node =
           _identifierArgNames = []
         }
 
+throwCoreError ::
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
+  Location ->
+  Doc Ann ->
+  ParsecS r a
+throwCoreError i msg =
+  lift $ throwError (CoreError (ppOutput msg) Nothing i)
+
 guardSymbolNotDefined ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Symbol ->
   ParsecS r () ->
   ParsecS r ()
@@ -72,7 +85,7 @@ guardSymbolNotDefined sym err = do
   when b err
 
 parseToplevel ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   ParsecS r (Maybe Node)
 parseToplevel = do
   lift declareIOBuiltins
@@ -87,16 +100,15 @@ parseToplevel = do
   return r
 
 statement ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   ParsecS r ()
 statement = statementBuiltin <|> void statementDef <|> statementInductive
 
 statementBuiltin ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   ParsecS r ()
 statementBuiltin = do
-  off <- P.getOffset
-  kw kwBuiltin
+  kref <- kw' kwBuiltin
   sym <- statementDef
   ii <- lift $ getIdentifierInfo sym
   if
@@ -118,33 +130,32 @@ statementBuiltin = do
           lift $ registerIdent (ii ^. identifierName) ii {_identifierBuiltin = Just BuiltinNatLt}
       | ii ^. identifierName == Str.natEq ->
           lift $ registerIdent (ii ^. identifierName) ii {_identifierBuiltin = Just BuiltinNatEq}
-      | otherwise -> parseFailure off "unrecorgnized builtin definition"
+      | otherwise -> throwCoreError (kref ^. keywordRefInterval) "unrecorgnized builtin definition"
 
 statementDef ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   ParsecS r Symbol
 statementDef = do
   kw kwDef
-  off <- P.getOffset
   (txt, i) <- identifierL
   r <- lift (getIdent txt)
   case r of
     Just (IdentFun sym) -> do
       guardSymbolNotDefined
         sym
-        (parseFailure off ("duplicate definition of: " ++ fromText txt))
+        (throwCoreError i ("duplicate definition of: " <> fromText txt))
       tab <- (^. moduleInfoTable) <$> lift getModule
       mty <- optional typeAnnotation
       let fi = fromMaybe impossible $ HashMap.lookup sym (tab ^. infoIdentifiers)
           ty = fromMaybe (fi ^. identifierType) mty
       unless (isDynamic (fi ^. identifierType) || ty == fi ^. identifierType) $
-        parseFailure off "type signature doesn't match earlier definition"
+        throwCoreError i "type signature doesn't match earlier definition"
       parseDefinition sym ty
       return sym
     Just IdentInd {} ->
-      parseFailure off ("duplicate identifier: " ++ fromText txt)
+      throwCoreError i ("duplicate identifier: " <> fromText txt)
     Just IdentConstr {} ->
-      parseFailure off ("duplicate identifier: " ++ fromText txt)
+      throwCoreError i ("duplicate identifier: " <> fromText txt)
     Nothing -> do
       mty <- optional typeAnnotation
       sym <- lift freshSymbol
@@ -166,33 +177,31 @@ statementDef = do
       return sym
 
 parseDefinition ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Symbol ->
   Type ->
   ParsecS r ()
 parseDefinition sym ty = do
   kw kwAssign
-  off <- P.getOffset
-  node <- expression
+  (node, i) <- interval expression
   lift $ registerIdentNode sym node
   let (is, _) = unfoldLambdas node
   when
     ( length is > length (typeArgs ty)
         && not (isDynamic (typeTarget ty))
     )
-    $ parseFailure off "type mismatch: too many lambdas"
+    $ throwCoreError i "type mismatch: too many lambdas"
   lift $ setIdentArgs sym (map (^. lambdaLhsBinder) is)
 
 statementInductive ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   ParsecS r ()
 statementInductive = do
   kw kwInductive
-  off <- P.getOffset
   (txt, i) <- identifierL
   idt <- lift $ getIdent txt
   when (isJust idt) $
-    parseFailure off ("duplicate identifier: " ++ fromText txt)
+    throwCoreError i ("duplicate identifier: " <> fromText txt)
   mty <- optional typeAnnotation
   sym <- lift freshSymbol
   let ii =
@@ -212,15 +221,14 @@ statementInductive = do
   lift $ registerInductive txt ii {_inductiveConstructors = map (^. constructorTag) ctrs}
 
 constrDecl ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Symbol ->
   ParsecS r ConstructorInfo
 constrDecl symInd = do
-  off <- P.getOffset
   (txt, i) <- identifierL
   idt <- lift $ getIdent txt
   when (isJust idt) $
-    parseFailure off ("duplicate identifier: " ++ fromText txt)
+    throwCoreError i ("duplicate identifier: " <> fromText txt)
   tag <- lift freshTag
   ty <- typeAnnotation
   let argsNum = length (typeArgs ty)
@@ -241,14 +249,14 @@ constrDecl symInd = do
   return ci
 
 typeAnnotation ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   ParsecS r Type
 typeAnnotation = do
   kw kwColon
   expression
 
 expression ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   ParsecS r Node
 expression = do
   node <- expr 0 mempty
@@ -256,7 +264,7 @@ expression = do
   return $ etaExpandApps md node
 
 expr ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   -- | current de Bruijn index, i.e., the number of binders upwards
   Index ->
   -- | reverse de Bruijn indices (de Bruijn levels)
@@ -265,14 +273,14 @@ expr ::
 expr = typeExpr
 
 bracedExpr ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r Node
 bracedExpr varsNum vars = braces (expr varsNum vars) <|> expr varsNum vars
 
 typeAnnot ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r Node
@@ -281,14 +289,14 @@ typeAnnot varsNum vars = do
   expr varsNum vars
 
 typeExpr ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r Node
 typeExpr varsNum vars = seqqExpr varsNum vars >>= typeExpr' varsNum vars
 
 typeExpr' ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   Node ->
@@ -298,7 +306,7 @@ typeExpr' varsNum vars node =
     <|> return node
 
 typeFunExpr' ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   Node ->
@@ -309,7 +317,7 @@ typeFunExpr' varsNum vars l = do
   return $ mkPi' l r
 
 seqqExpr ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r Node
@@ -318,7 +326,7 @@ seqqExpr varsNum vars = do
   seqqExpr' varsNum vars node <|> return node
 
 seqqExpr' ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   Node ->
@@ -329,14 +337,14 @@ seqqExpr' varsNum vars node = do
   return $ mkBuiltinApp' OpSeq [node, node']
 
 ioExpr ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r Node
 ioExpr varsNum vars = cmpExpr varsNum vars >>= ioExpr' varsNum vars
 
 ioExpr' ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   Node ->
@@ -347,7 +355,7 @@ ioExpr' varsNum vars node =
     <|> return node
 
 bindExpr' ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   Node ->
@@ -358,7 +366,7 @@ bindExpr' varsNum vars node = do
   ioExpr' varsNum vars (mkConstr Info.empty (BuiltinTag TagBind) [node, node'])
 
 seqExpr' ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   Node ->
@@ -373,14 +381,14 @@ seqExpr' varsNum vars node = do
       [node, mkLambda mempty (Binder "_" (Just i) mkDynamic') node']
 
 cmpExpr ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r Node
 cmpExpr varsNum vars = arithExpr varsNum vars >>= cmpExpr' varsNum vars
 
 cmpExpr' ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   Node ->
@@ -394,7 +402,7 @@ cmpExpr' varsNum vars node =
     <|> return node
 
 eqExpr' ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   Node ->
@@ -405,7 +413,7 @@ eqExpr' varsNum vars node = do
   return $ mkBuiltinApp' OpEq [node, node']
 
 ltExpr' ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   Node ->
@@ -416,7 +424,7 @@ ltExpr' varsNum vars node = do
   return $ mkBuiltinApp' OpIntLt [node, node']
 
 leExpr' ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   Node ->
@@ -427,7 +435,7 @@ leExpr' varsNum vars node = do
   return $ mkBuiltinApp' OpIntLe [node, node']
 
 gtExpr' ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   Node ->
@@ -438,7 +446,7 @@ gtExpr' varsNum vars node = do
   return $ mkBuiltinApp' OpIntLt [node', node]
 
 geExpr' ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   Node ->
@@ -449,14 +457,14 @@ geExpr' varsNum vars node = do
   return $ mkBuiltinApp' OpIntLe [node', node]
 
 arithExpr ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r Node
 arithExpr varsNum vars = factorExpr varsNum vars >>= arithExpr' varsNum vars
 
 arithExpr' ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   Node ->
@@ -467,7 +475,7 @@ arithExpr' varsNum vars node =
     <|> return node
 
 plusExpr' ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   Node ->
@@ -478,7 +486,7 @@ plusExpr' varsNum vars node = do
   arithExpr' varsNum vars (mkBuiltinApp' OpIntAdd [node, node'])
 
 minusExpr' ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   Node ->
@@ -489,14 +497,14 @@ minusExpr' varsNum vars node = do
   arithExpr' varsNum vars (mkBuiltinApp' OpIntSub [node, node'])
 
 factorExpr ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r Node
 factorExpr varsNum vars = appExpr varsNum vars >>= factorExpr' varsNum vars
 
 factorExpr' ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   Node ->
@@ -508,7 +516,7 @@ factorExpr' varsNum vars node =
     <|> return node
 
 mulExpr' ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   Node ->
@@ -519,7 +527,7 @@ mulExpr' varsNum vars node = do
   factorExpr' varsNum vars (mkBuiltinApp' OpIntMul [node, node'])
 
 divExpr' ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   Node ->
@@ -530,7 +538,7 @@ divExpr' varsNum vars node = do
   factorExpr' varsNum vars (mkBuiltinApp' OpIntDiv [node, node'])
 
 modExpr' ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   Node ->
@@ -541,14 +549,14 @@ modExpr' varsNum vars node = do
   factorExpr' varsNum vars (mkBuiltinApp' OpIntMod [node, node'])
 
 appExpr ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r Node
 appExpr varsNum vars = builtinAppExpr varsNum vars <|> atoms varsNum vars
 
 builtinAppExpr ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r Node
@@ -608,7 +616,7 @@ builtinAppExpr varsNum vars = do
   return $ mkBuiltinApp' op args
 
 atoms ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r Node
@@ -617,7 +625,7 @@ atoms varsNum vars = do
   return $ mkApps' (head es) (NonEmpty.tail es)
 
 atom ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r Node
@@ -669,7 +677,7 @@ exprUniverse = do
 exprDynamic :: ParsecS r Type
 exprDynamic = kw kwAny $> mkDynamic'
 
-exprBottom :: (Members '[InfoTableBuilder] r) => ParsecS r Node
+exprBottom :: (Members '[Error CoreError, InfoTableBuilder] r) => ParsecS r Node
 exprBottom = do
   (ty, loc) <- interval $ do
     kw kwBottom
@@ -689,7 +697,7 @@ parseLocalName = parseWildcardName <|> parseIdentName
 
 parseLocalBinder ::
   forall r.
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r ((Text, Location), Type)
@@ -710,7 +718,7 @@ parseLocalBinder varsNum vars = parseBinder <|> parseName
       return (n, mkDynamic')
 
 exprPi ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r Node
@@ -725,7 +733,7 @@ exprPi varsNum vars = do
   return $ mkPi mempty bi body
 
 exprLambda ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r Node
@@ -747,7 +755,7 @@ exprLambda varsNum vars = do
         <|> (\n -> (n, Nothing)) <$> parseLocalName
 
 exprLetrecOne ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r Node
@@ -765,15 +773,14 @@ exprLetrecOne varsNum vars = do
   return $ mkLetRec mempty (pure item) body
 
 exprLetrecMany ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r Node
 exprLetrecMany varsNum vars = do
-  off <- P.getOffset
-  defNames <- P.try (kw kwLetRec >> letrecNames)
+  (defNames, i) <- P.try (kw kwLetRec >> interval letrecNames)
   when (null defNames) $
-    parseFailure off "expected at least one identifier name in letrec signature"
+    throwCoreError i "expected at least one identifier name in letrec signature"
   let (vars', varsNum') = foldl' (\(vs, k) txt -> (HashMap.insert txt k vs, k + 1)) (vars, varsNum) defNames
   defs <- letrecDefs defNames varsNum vars varsNum' vars'
   kw kwIn
@@ -785,7 +792,7 @@ letrecNames = P.between (symbol "[") (symbol "]") (NonEmpty.some identifier)
 
 letrecDefs ::
   forall r.
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   NonEmpty Text ->
   Index ->
   HashMap Text Level ->
@@ -796,11 +803,10 @@ letrecDefs names varsNum0 vars0 varsNum vars = forM names letrecItem
   where
     letrecItem :: Text -> ParsecS r LetItem
     letrecItem n = do
-      off <- P.getOffset
       (txt, i) <- identifierL
       mty <- optional (typeAnnot varsNum0 vars0)
       when (n /= txt) $
-        parseFailure off "identifier name doesn't match letrec signature"
+        throwCoreError i "identifier name doesn't match letrec signature"
       kw kwAssign
       v <- bracedExpr varsNum vars
       kw delimSemicolon
@@ -808,7 +814,7 @@ letrecDefs names varsNum0 vars0 varsNum vars = forM names letrecItem
       return $ LetItem (Binder txt (Just i) ty) v
 
 letrecDef ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r (Text, Location, Node)
@@ -819,7 +825,7 @@ letrecDef varsNum vars = do
   return (txt, i, v)
 
 exprLet ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r Node
@@ -836,7 +842,7 @@ exprLet varsNum vars = do
   return $ mkLet mempty binder value body
 
 exprCase ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r Node
@@ -849,7 +855,7 @@ exprCase varsNum vars = do
     <|> exprCase' off value varsNum vars
 
 exprCase' ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Int ->
   Node ->
   Index ->
@@ -880,7 +886,7 @@ exprCase' off value varsNum vars = do
           parseFailure off "multiple default branches"
 
 caseBranchP ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r (Either CaseBranch Node)
@@ -889,7 +895,7 @@ caseBranchP varsNum vars =
     <|> (caseMatchingBranch varsNum vars <&> Left)
 
 caseDefaultBranch ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r Node
@@ -899,7 +905,7 @@ caseDefaultBranch varsNum vars = do
   bracedExpr varsNum vars
 
 parseCaseBranchBinders ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r [((Text, Location), Type)]
@@ -913,26 +919,25 @@ parseCaseBranchBinders varsNum vars = do
       return []
 
 caseMatchingBranch ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r CaseBranch
 caseMatchingBranch varsNum vars = do
-  off <- P.getOffset
-  txt <- identifier
+  (txt, i) <- identifierL
   r <- lift (getIdent txt)
   case r of
     Just IdentFun {} ->
-      parseFailure off ("not a constructor: " ++ fromText txt)
+      throwCoreError i ("not a constructor: " <> fromText txt)
     Just IdentInd {} ->
-      parseFailure off ("not a constructor: " ++ fromText txt)
+      throwCoreError i ("not a constructor: " <> fromText txt)
     Just (IdentConstr tag) -> do
       bs :: [((Text, Location), Type)] <- parseCaseBranchBinders varsNum vars
       let bindersNum = length bs
       ci <- lift $ getConstructorInfo tag
       when
         (ci ^. constructorArgsNum /= bindersNum)
-        (parseFailure off "wrong number of constructor arguments")
+        (throwCoreError i "wrong number of constructor arguments")
       kw kwAssign
       let vars' =
             fst $
@@ -953,10 +958,10 @@ caseMatchingBranch varsNum vars = do
               (typeArgs (ci ^. constructorType) ++ repeat mkDynamic')
       return $ CaseBranch info tag binders bindersNum br
     Nothing ->
-      parseFailure off ("undeclared identifier: " ++ fromText txt)
+      throwCoreError i ("undeclared identifier: " <> fromText txt)
 
 exprIf ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r Node
@@ -971,7 +976,7 @@ exprIf varsNum vars = do
   return $ mkIf mempty sym value br1 br2
 
 exprMatch ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r Node
@@ -985,14 +990,14 @@ exprMatch varsNum vars = do
     <|> exprMatch' vals rty varsNum vars
 
 exprMatchValue ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r (Node, Type)
 exprMatchValue varsNum vars = parens (exprMatchValue' varsNum vars) <|> exprMatchValue' varsNum vars
 
 exprMatchValue' ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r (Node, Type)
@@ -1002,7 +1007,7 @@ exprMatchValue' varsNum vars = do
   return (val, fromMaybe mkDynamic' mty)
 
 exprMatch' ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   [(Node, Type)] ->
   Type ->
   Index ->
@@ -1015,7 +1020,7 @@ exprMatch' vals rty varsNum vars = do
   return $ mkMatch' (fromList types) rty (fromList values) bs
 
 matchBranch ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Int ->
   Index ->
   HashMap Text Level ->
@@ -1027,7 +1032,7 @@ matchBranch patsNum varsNum vars = do
   return $ MatchBranch Info.empty (fromList pats) rhs
 
 branchRhs ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Int ->
   [Pattern] ->
   Int ->
@@ -1039,7 +1044,7 @@ branchRhs off pats patsNum varsNum vars =
     <|> branchRhsIf off pats patsNum varsNum vars
 
 branchRhsExpr ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Int ->
   [Pattern] ->
   Int ->
@@ -1063,7 +1068,7 @@ branchRhsExpr off pats patsNum varsNum vars = do
   return $ MatchBranchRhsExpression br
 
 branchRhsIf ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Int ->
   [Pattern] ->
   Int ->
@@ -1075,7 +1080,7 @@ branchRhsIf off pats patsNum varsNum vars = do
   return $ MatchBranchRhsIfs ifs
 
 sideIfs ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Int ->
   [Pattern] ->
   Int ->
@@ -1101,7 +1106,7 @@ sideIfs off pats patsNum varsNum vars = do
   return $ SideIfBranch Info.empty cond br :| maybe [] toList conds
 
 branchCond ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r Node
@@ -1110,7 +1115,7 @@ branchCond varsNum vars = do
   expr varsNum vars
 
 branchPatterns ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r [Pattern]
@@ -1120,7 +1125,7 @@ branchPatterns varsNum vars = do
   return (pat : pats)
 
 branchPattern ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r (Pattern, (Index, HashMap Text Level))
@@ -1130,7 +1135,7 @@ branchPattern varsNum vars =
     <|> branchPattern' varsNum vars
 
 branchPatternWildcard ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r (Pattern, (Index, HashMap Text Level))
@@ -1141,12 +1146,11 @@ branchPatternWildcard varsNum vars = do
   return (PatWildcard (PatternWildcard mempty binder), (varsNum + 1, vars))
 
 branchPattern' ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r (Pattern, (Index, HashMap Text Level))
 branchPattern' varsNum vars = do
-  off <- P.getOffset
   (txt, i) <- identifierL
   r <- lift (getIdent txt)
   case r of
@@ -1156,7 +1160,7 @@ branchPattern' varsNum vars = do
       ci <- lift $ getConstructorInfo tag
       when
         (ci ^. constructorArgsNum /= length ps)
-        (parseFailure off "wrong number of constructor arguments")
+        (throwCoreError i "wrong number of constructor arguments")
       let info = setInfoName (ci ^. constructorName) Info.empty
           ty = fromMaybe mkDynamic' mty
           binder = Binder "_" (Just i) ty
@@ -1198,7 +1202,7 @@ branchPattern' varsNum vars = do
           return (PatWildcard (PatternWildcard mempty binder), (varsNum + 1, vars1))
 
 constrArgPatterns ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r ([Pattern], (Index, HashMap Text Level))
@@ -1212,12 +1216,11 @@ constrArgPatterns varsNum vars = do
       return ([], (varsNum, vars))
 
 exprNamed ::
-  (Member InfoTableBuilder r) =>
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
   HashMap Text Level ->
   ParsecS r Node
 exprNamed varsNum vars = do
-  off <- P.getOffset
   (txt, i) <- identifierL
   case txt of
     "Int" -> return mkTypeInteger'
@@ -1239,4 +1242,10 @@ exprNamed varsNum vars = do
             Just (IdentConstr tag) -> do
               return $ mkConstr (Info.insert (LocationInfo i) (Info.singleton (NameInfo txt))) tag []
             Nothing ->
-              parseFailure off ("undeclared identifier: " ++ fromText txt)
+              lift $
+                throw
+                  CoreError
+                    { _coreErrorMsg = ppOutput $ "undeclared identifier: " <> fromText txt,
+                      _coreErrorNode = Nothing,
+                      _coreErrorLoc = i
+                    }

From 0f51e6c05d64a979f51ddad6ffe1b2a1243b9f1f Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Thu, 30 Jan 2025 12:43:42 +0100
Subject: [PATCH 2/7] fix tests

---
 test/Core/Asm/Base.hs       | 2 +-
 test/Core/Compile/Base.hs   | 2 +-
 test/Core/Eval/Base.hs      | 4 ++--
 test/Core/Normalize/Base.hs | 2 +-
 test/Core/Print/Base.hs     | 4 ++--
 test/Core/VampIR/Base.hs    | 2 +-
 test/Main.hs                | 4 ++--
 7 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/test/Core/Asm/Base.hs b/test/Core/Asm/Base.hs
index 651ca941f6..c30c978aa9 100644
--- a/test/Core/Asm/Base.hs
+++ b/test/Core/Asm/Base.hs
@@ -46,7 +46,7 @@ coreAsmAssertion root' mainFile expectedFile step = do
   step "Parse"
   r <- parseFile mainFile
   case r of
-    Left err -> assertFailure (prettyString err)
+    Left err -> assertFailure (prettyString (fromJuvixError @GenericError err))
     Right (_, Nothing) -> do
       step "Empty program: compare expected and actual program output"
       expected <- readFile expectedFile
diff --git a/test/Core/Compile/Base.hs b/test/Core/Compile/Base.hs
index 373264e8fc..242a043da8 100644
--- a/test/Core/Compile/Base.hs
+++ b/test/Core/Compile/Base.hs
@@ -72,7 +72,7 @@ coreCompileAssertion root' mainFile expectedFile stdinText step = do
   step "Parse"
   r <- parseFile mainFile
   case r of
-    Left err -> assertFailure (prettyString err)
+    Left err -> assertFailure (prettyString (fromJuvixError @GenericError err))
     Right (_, Nothing) -> do
       step "Empty program: compare expected and actual program output"
       expected <- readFile expectedFile
diff --git a/test/Core/Eval/Base.hs b/test/Core/Eval/Base.hs
index 406665573a..1f00051bb9 100644
--- a/test/Core/Eval/Base.hs
+++ b/test/Core/Eval/Base.hs
@@ -143,7 +143,7 @@ coreEvalAssertion mainFile expectedFile trans testTrans step = do
   step "Parse"
   r <- parseFile mainFile
   case r of
-    Left err -> assertFailure (prettyString err)
+    Left err -> assertFailure (prettyString (fromJuvixError @GenericError err))
     Right (_, Nothing) -> do
       step "Compare expected and actual program output"
       expected <- readFile expectedFile
@@ -177,7 +177,7 @@ coreEvalErrorAssertion mainFile step = do
               Right _ -> assertFailure "no error"
         )
 
-parseFile :: Path Abs File -> IO (Either MegaparsecError (InfoTable, Maybe Node))
+parseFile :: Path Abs File -> IO (Either JuvixError (InfoTable, Maybe Node))
 parseFile f = do
   s <- readFile f
   return (runParser f defaultModuleId mempty s)
diff --git a/test/Core/Normalize/Base.hs b/test/Core/Normalize/Base.hs
index 538286f973..b99f79b032 100644
--- a/test/Core/Normalize/Base.hs
+++ b/test/Core/Normalize/Base.hs
@@ -19,7 +19,7 @@ coreNormalizeAssertion mainFile expectedFile step = do
   step "Parse"
   r <- parseFile mainFile
   case r of
-    Left err -> assertFailure (prettyString err)
+    Left err -> assertFailure (prettyString (fromJuvixError @GenericError err))
     Right (_, Nothing) -> assertFailure "Empty program"
     Right (tabIni, Just node) -> do
       step "Transform"
diff --git a/test/Core/Print/Base.hs b/test/Core/Print/Base.hs
index 7860430283..d6ce24a479 100644
--- a/test/Core/Print/Base.hs
+++ b/test/Core/Print/Base.hs
@@ -39,7 +39,7 @@ corePrintAssertion mainFile expectedFile step = do
   step "Parse"
   r <- parseFile mainFile
   case r of
-    Left err -> assertFailure (prettyString err)
+    Left err -> assertFailure (prettyString (fromJuvixError @GenericError err))
     Right (_, Nothing) -> do
       step "Empty program: compare expected and actual program output"
       expected <- readFile expectedFile
@@ -50,5 +50,5 @@ corePrintAssertion mainFile expectedFile step = do
       step "Print and parse back"
       let r' = runParserMain mainFile defaultModuleId mempty (ppPrint tab)
       case r' of
-        Left err -> assertFailure (prettyString err)
+        Left err -> assertFailure (prettyString (fromJuvixError @GenericError err))
         Right tab' -> coreEvalAssertion' EvalModePlain tab' mainFile expectedFile step
diff --git a/test/Core/VampIR/Base.hs b/test/Core/VampIR/Base.hs
index bd6dcafa76..9d1d5109bd 100644
--- a/test/Core/VampIR/Base.hs
+++ b/test/Core/VampIR/Base.hs
@@ -18,7 +18,7 @@ coreVampIRAssertion transforms mainFile expectedFile step = do
   step "Parse"
   r <- parseFile mainFile
   case r of
-    Left err -> assertFailure (prettyString err)
+    Left err -> assertFailure (prettyString (fromJuvixError @GenericError err))
     Right (_, Nothing) -> assertFailure "Empty program"
     Right (tabIni, Just node) -> do
       coreVampIRAssertion' (setupMainFunction defaultModuleId tabIni node) transforms mainFile expectedFile step
diff --git a/test/Main.hs b/test/Main.hs
index 6f7dd375ab..73cc803c11 100644
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -28,9 +28,9 @@ import Typecheck qualified
 
 slowTests :: IO TestTree
 slowTests =
-  sequentialTestGroup
+  testGroup
     "Juvix slow tests"
-    AllFinish
+    --    AllFinish
     <$> sequence
       [ return Runtime.allTests,
         return Reg.allTests,

From cf32b3dddeb5637a8b438de65aecd3c06ab58e55 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Thu, 30 Jan 2025 12:47:17 +0100
Subject: [PATCH 3/7] fix builtin parsing

---
 src/Juvix/Compiler/Core/Translation/FromSource.hs | 4 ++--
 test/Main.hs                                      | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs
index cea81fff56..0ef5d325e3 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs
@@ -108,7 +108,7 @@ statementBuiltin ::
   (Members '[Error CoreError, InfoTableBuilder] r) =>
   ParsecS r ()
 statementBuiltin = do
-  kref <- kw' kwBuiltin
+  ((), i) <- interval $ kw kwBuiltin
   sym <- statementDef
   ii <- lift $ getIdentifierInfo sym
   if
@@ -130,7 +130,7 @@ statementBuiltin = do
           lift $ registerIdent (ii ^. identifierName) ii {_identifierBuiltin = Just BuiltinNatLt}
       | ii ^. identifierName == Str.natEq ->
           lift $ registerIdent (ii ^. identifierName) ii {_identifierBuiltin = Just BuiltinNatEq}
-      | otherwise -> throwCoreError (kref ^. keywordRefInterval) "unrecorgnized builtin definition"
+      | otherwise -> throwCoreError i "unrecorgnized builtin definition"
 
 statementDef ::
   (Members '[Error CoreError, InfoTableBuilder] r) =>
diff --git a/test/Main.hs b/test/Main.hs
index 73cc803c11..6f7dd375ab 100644
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -28,9 +28,9 @@ import Typecheck qualified
 
 slowTests :: IO TestTree
 slowTests =
-  testGroup
+  sequentialTestGroup
     "Juvix slow tests"
-    --    AllFinish
+    AllFinish
     <$> sequence
       [ return Runtime.allTests,
         return Reg.allTests,

From 2b1449fbfac272786404c8b9583e72e4639d0835 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Thu, 30 Jan 2025 19:53:05 +0100
Subject: [PATCH 4/7] negative tests & match side-conditions fix

---
 .../Compiler/Core/Translation/FromSource.hs   | 102 ++++++-------
 test/Core/Eval/Base.hs                        |   4 +-
 test/Core/Print.hs                            |   3 +-
 test/Core/Print/Base.hs                       |   8 ++
 test/Core/Print/Negative.hs                   | 134 ++++++++++++++++++
 test/Core/Print/Positive.hs                   |   2 +-
 tests/Core/negative/parsing/test001.jvc       |   3 +
 tests/Core/negative/parsing/test002.jvc       |   2 +
 tests/Core/negative/parsing/test003.jvc       |   2 +
 tests/Core/negative/parsing/test004.jvc       |   5 +
 tests/Core/negative/parsing/test005.jvc       |   7 +
 tests/Core/negative/parsing/test006.jvc       |   3 +
 tests/Core/negative/parsing/test007.jvc       |   3 +
 tests/Core/negative/parsing/test008.jvc       |   1 +
 tests/Core/negative/parsing/test009.jvc       |   5 +
 tests/Core/negative/parsing/test010.jvc       |   5 +
 tests/Core/negative/parsing/test011.jvc       |   1 +
 tests/Core/negative/parsing/test012.jvc       |   1 +
 tests/Core/negative/parsing/test013.jvc       |   5 +
 tests/Core/negative/parsing/test014.jvc       |   5 +
 tests/Core/negative/parsing/test015.jvc       |   9 ++
 tests/Core/negative/parsing/test016.jvc       |   7 +
 tests/Core/negative/parsing/test017.jvc       |   6 +
 tests/Core/negative/parsing/test018.jvc       |   8 ++
 tests/Core/negative/parsing/test019.jvc       |   9 ++
 tests/Core/negative/parsing/test020.jvc       |   7 +
 tests/Core/negative/parsing/test021.jvc       |   7 +
 tests/Core/negative/parsing/test022.jvc       |  12 ++
 tests/Core/negative/parsing/test023.jvc       |  16 +++
 tests/Core/negative/parsing/test024.jvc       |  16 +++
 tests/Core/negative/test003.jvc               |   7 +-
 tests/Core/negative/test005.jvc               |   4 +-
 tests/Core/negative/test009.jvc               |  12 +-
 tests/Core/negative/test010.jvc               |   1 -
 34 files changed, 352 insertions(+), 70 deletions(-)
 create mode 100644 test/Core/Print/Negative.hs
 create mode 100644 tests/Core/negative/parsing/test001.jvc
 create mode 100644 tests/Core/negative/parsing/test002.jvc
 create mode 100644 tests/Core/negative/parsing/test003.jvc
 create mode 100644 tests/Core/negative/parsing/test004.jvc
 create mode 100644 tests/Core/negative/parsing/test005.jvc
 create mode 100644 tests/Core/negative/parsing/test006.jvc
 create mode 100644 tests/Core/negative/parsing/test007.jvc
 create mode 100644 tests/Core/negative/parsing/test008.jvc
 create mode 100644 tests/Core/negative/parsing/test009.jvc
 create mode 100644 tests/Core/negative/parsing/test010.jvc
 create mode 100644 tests/Core/negative/parsing/test011.jvc
 create mode 100644 tests/Core/negative/parsing/test012.jvc
 create mode 100644 tests/Core/negative/parsing/test013.jvc
 create mode 100644 tests/Core/negative/parsing/test014.jvc
 create mode 100644 tests/Core/negative/parsing/test015.jvc
 create mode 100644 tests/Core/negative/parsing/test016.jvc
 create mode 100644 tests/Core/negative/parsing/test017.jvc
 create mode 100644 tests/Core/negative/parsing/test018.jvc
 create mode 100644 tests/Core/negative/parsing/test019.jvc
 create mode 100644 tests/Core/negative/parsing/test020.jvc
 create mode 100644 tests/Core/negative/parsing/test021.jvc
 create mode 100644 tests/Core/negative/parsing/test022.jvc
 create mode 100644 tests/Core/negative/parsing/test023.jvc
 create mode 100644 tests/Core/negative/parsing/test024.jvc
 delete mode 100644 tests/Core/negative/test010.jvc

diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs
index 0ef5d325e3..f8bd753fb4 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs
@@ -1,6 +1,8 @@
 module Juvix.Compiler.Core.Translation.FromSource
-  ( module Juvix.Compiler.Core.Translation.FromSource,
-    module Juvix.Parser.Error,
+  ( module Juvix.Parser.Error,
+    runParser,
+    runParserMain,
+    setupMainFunction,
   )
 where
 
@@ -813,17 +815,6 @@ letrecDefs names varsNum0 vars0 varsNum vars = forM names letrecItem
       let ty = fromMaybe mkDynamic' mty
       return $ LetItem (Binder txt (Just i) ty) v
 
-letrecDef ::
-  (Members '[Error CoreError, InfoTableBuilder] r) =>
-  Index ->
-  HashMap Text Level ->
-  ParsecS r (Text, Location, Node)
-letrecDef varsNum vars = do
-  (txt, i) <- identifierL
-  kw kwAssign
-  v <- bracedExpr varsNum vars
-  return (txt, i, v)
-
 exprLet ::
   (Members '[Error CoreError, InfoTableBuilder] r) =>
   Index ->
@@ -847,21 +838,20 @@ exprCase ::
   HashMap Text Level ->
   ParsecS r Node
 exprCase varsNum vars = do
-  off <- P.getOffset
-  kw kwCase
+  ((), i) <- interval $ kw kwCase
   value <- bracedExpr varsNum vars
   kw kwOf
-  braces (exprCase' off value varsNum vars)
-    <|> exprCase' off value varsNum vars
+  braces (exprCase' i value varsNum vars)
+    <|> exprCase' i value varsNum vars
 
 exprCase' ::
   (Members '[Error CoreError, InfoTableBuilder] r) =>
-  Int ->
+  Interval ->
   Node ->
   Index ->
   HashMap Text Level ->
   ParsecS r Node
-exprCase' off value varsNum vars = do
+exprCase' i value varsNum vars = do
   bs <- P.sepEndBy (caseBranchP varsNum vars) (kw delimSemicolon)
   let bss = map fromLeft' $ filter isLeft bs
   let def' = map fromRight' $ filter isRight bs
@@ -875,15 +865,15 @@ exprCase' off value varsNum vars = do
         [] ->
           return $ mkCase' sym value bss Nothing
         _ ->
-          parseFailure off "multiple default branches"
+          throwCoreError i "multiple default branches"
     [] ->
       case def' of
         [_] ->
-          parseFailure off "case with only the default branch not allowed"
+          throwCoreError i "case with only the default branch not allowed"
         [] ->
-          parseFailure off "case without branches not allowed"
+          throwCoreError i "case without branches not allowed"
         _ ->
-          parseFailure off "multiple default branches"
+          throwCoreError i "multiple default branches"
 
 caseBranchP ::
   (Members '[Error CoreError, InfoTableBuilder] r) =>
@@ -1026,35 +1016,28 @@ matchBranch ::
   HashMap Text Level ->
   ParsecS r MatchBranch
 matchBranch patsNum varsNum vars = do
-  off <- P.getOffset
-  pats <- branchPatterns varsNum vars
-  rhs <- branchRhs off pats patsNum varsNum vars
+  (pats, i) <- interval $ branchPatterns varsNum vars
+  rhs <- branchRhs i pats patsNum varsNum vars
   return $ MatchBranch Info.empty (fromList pats) rhs
 
 branchRhs ::
   (Members '[Error CoreError, InfoTableBuilder] r) =>
-  Int ->
+  Interval ->
   [Pattern] ->
   Int ->
   Index ->
   HashMap Text Level ->
   ParsecS r MatchBranchRhs
-branchRhs off pats patsNum varsNum vars =
-  branchRhsExpr off pats patsNum varsNum vars
-    <|> branchRhsIf off pats patsNum varsNum vars
+branchRhs i pats patsNum varsNum vars =
+  branchRhsExpr i pats patsNum varsNum vars
+    <|> branchRhsIf i pats patsNum varsNum vars
 
-branchRhsExpr ::
-  (Members '[Error CoreError, InfoTableBuilder] r) =>
-  Int ->
+updateVarsByPatternBinders ::
   [Pattern] ->
-  Int ->
   Index ->
   HashMap Text Level ->
-  ParsecS r MatchBranchRhs
-branchRhsExpr off pats patsNum varsNum vars = do
-  kw kwAssign
-  unless (length pats == patsNum) $
-    parseFailure off "wrong number of patterns"
+  (Index, HashMap Text Level)
+updateVarsByPatternBinders pats varsNum vars =
   let pis :: [Binder]
       pis = concatMap getPatternBinders pats
       (vars', varsNum') =
@@ -1064,45 +1047,52 @@ branchRhsExpr off pats patsNum varsNum vars = do
           )
           (vars, varsNum)
           (map (^. binderName) pis)
+   in (varsNum', vars')
+
+branchRhsExpr ::
+  (Members '[Error CoreError, InfoTableBuilder] r) =>
+  Interval ->
+  [Pattern] ->
+  Int ->
+  Index ->
+  HashMap Text Level ->
+  ParsecS r MatchBranchRhs
+branchRhsExpr i pats patsNum varsNum vars = do
+  kw kwAssign
+  unless (length pats == patsNum) $
+    throwCoreError i "wrong number of patterns"
+  let (varsNum', vars') = updateVarsByPatternBinders pats varsNum vars
   br <- bracedExpr varsNum' vars'
   return $ MatchBranchRhsExpression br
 
 branchRhsIf ::
   (Members '[Error CoreError, InfoTableBuilder] r) =>
-  Int ->
+  Interval ->
   [Pattern] ->
   Int ->
   Index ->
   HashMap Text Level ->
   ParsecS r MatchBranchRhs
-branchRhsIf off pats patsNum varsNum vars = do
-  ifs <- sideIfs off pats patsNum varsNum vars
+branchRhsIf i pats patsNum varsNum vars = do
+  ifs <- sideIfs i pats patsNum varsNum vars
   return $ MatchBranchRhsIfs ifs
 
 sideIfs ::
   (Members '[Error CoreError, InfoTableBuilder] r) =>
-  Int ->
+  Interval ->
   [Pattern] ->
   Int ->
   Index ->
   HashMap Text Level ->
   ParsecS r (NonEmpty SideIfBranch)
-sideIfs off pats patsNum varsNum vars = do
-  cond <- branchCond varsNum vars
+sideIfs i pats patsNum varsNum vars = do
+  let (varsNum', vars') = updateVarsByPatternBinders pats varsNum vars
+  cond <- branchCond varsNum' vars'
   kw kwAssign
   unless (length pats == patsNum) $
-    parseFailure off "wrong number of patterns"
-  let pis :: [Binder]
-      pis = concatMap getPatternBinders pats
-      (vars', varsNum') =
-        foldl'
-          ( \(vs, k) name ->
-              (HashMap.insert name k vs, k + 1)
-          )
-          (vars, varsNum)
-          (map (^. binderName) pis)
+    throwCoreError i "wrong number of patterns"
   br <- bracedExpr varsNum' vars'
-  conds <- optional (sideIfs off pats patsNum varsNum vars)
+  conds <- optional (sideIfs i pats patsNum varsNum vars)
   return $ SideIfBranch Info.empty cond br :| maybe [] toList conds
 
 branchCond ::
diff --git a/test/Core/Eval/Base.hs b/test/Core/Eval/Base.hs
index 1f00051bb9..8c1443e4ec 100644
--- a/test/Core/Eval/Base.hs
+++ b/test/Core/Eval/Base.hs
@@ -162,7 +162,7 @@ coreEvalErrorAssertion mainFile step = do
   step "Parse"
   r <- parseFile mainFile
   case r of
-    Left _ -> assertBool "" True
+    Left _ -> assertFailure "error parsing file"
     Right (_, Nothing) -> assertFailure "no error"
     Right (tab, Just node) -> do
       withTempDir'
@@ -173,7 +173,7 @@ coreEvalErrorAssertion mainFile step = do
             r' <- doEval mainFile hout tab node
             hClose hout
             case r' of
-              Left _ -> assertBool "" True
+              Left _ -> return ()
               Right _ -> assertFailure "no error"
         )
 
diff --git a/test/Core/Print.hs b/test/Core/Print.hs
index 1ab0a8c988..1fe3852c91 100644
--- a/test/Core/Print.hs
+++ b/test/Core/Print.hs
@@ -1,7 +1,8 @@
 module Core.Print where
 
 import Base
+import Core.Print.Negative qualified as N
 import Core.Print.Positive qualified as P
 
 allTests :: TestTree
-allTests = testGroup "JuvixCore print" [P.allTests]
+allTests = testGroup "JuvixCore parse and print" [P.allTests, N.allTests]
diff --git a/test/Core/Print/Base.hs b/test/Core/Print/Base.hs
index d6ce24a479..b5323ed7c3 100644
--- a/test/Core/Print/Base.hs
+++ b/test/Core/Print/Base.hs
@@ -52,3 +52,11 @@ corePrintAssertion mainFile expectedFile step = do
       case r' of
         Left err -> assertFailure (prettyString (fromJuvixError @GenericError err))
         Right tab' -> coreEvalAssertion' EvalModePlain tab' mainFile expectedFile step
+
+coreParseErrorAssertion :: Path Abs File -> (String -> IO ()) -> Assertion
+coreParseErrorAssertion mainFile step = do
+  step "Parse"
+  r <- parseFile mainFile
+  case r of
+    Left _ -> return ()
+    Right _ -> assertFailure "no error"
diff --git a/test/Core/Print/Negative.hs b/test/Core/Print/Negative.hs
new file mode 100644
index 0000000000..b3885ac346
--- /dev/null
+++ b/test/Core/Print/Negative.hs
@@ -0,0 +1,134 @@
+module Core.Print.Negative where
+
+import Base
+import Core.Eval.Base
+import Core.Print.Base
+
+data NegTest = NegTest
+  { _name :: String,
+    _relDir :: Path Rel Dir,
+    _file :: Path Rel File
+  }
+
+root :: Path Abs Dir
+root = relToProject $(mkRelDir "tests/Core/negative/parsing")
+
+testDescr :: NegTest -> TestDescr
+testDescr NegTest {..} =
+  let tRoot = root <//> _relDir
+      file' = tRoot <//> _file
+   in TestDescr
+        { _testName = _name,
+          _testRoot = tRoot,
+          _testAssertion = Steps $ coreParseErrorAssertion file'
+        }
+
+allTests :: TestTree
+allTests =
+  testGroup
+    "JuvixCore parsing negative tests"
+    (map (mkTest . testDescr) tests)
+
+tests :: [NegTest]
+tests =
+  [ NegTest
+      "Undeclared identifier"
+      $(mkRelDir ".")
+      $(mkRelFile "test001.jvc"),
+    NegTest
+      "Let not recursive"
+      $(mkRelDir ".")
+      $(mkRelFile "test002.jvc"),
+    NegTest
+      "Duplicate definition"
+      $(mkRelDir ".")
+      $(mkRelFile "test003.jvc"),
+    NegTest
+      "Duplicate identifier"
+      $(mkRelDir ".")
+      $(mkRelFile "test004.jvc"),
+    NegTest
+      "Duplicate constructor"
+      $(mkRelDir ".")
+      $(mkRelFile "test005.jvc"),
+    NegTest
+      "Type signature mismatch"
+      $(mkRelDir ".")
+      $(mkRelFile "test006.jvc"),
+    NegTest
+      "Signature after definition"
+      $(mkRelDir ".")
+      $(mkRelFile "test007.jvc"),
+    NegTest
+      "Too many lambdas"
+      $(mkRelDir ".")
+      $(mkRelFile "test008.jvc"),
+    NegTest
+      "Duplicate identifier (def vs type)"
+      $(mkRelDir ".")
+      $(mkRelFile "test009.jvc"),
+    NegTest
+      "Duplicate identifier (def vs constructor)"
+      $(mkRelDir ".")
+      $(mkRelFile "test010.jvc"),
+    NegTest
+      "Duplicate identifier (def vs constructor)"
+      $(mkRelDir ".")
+      $(mkRelFile "test010.jvc"),
+    NegTest
+      "Unrecognized builtin"
+      $(mkRelDir ".")
+      $(mkRelFile "test011.jvc"),
+    NegTest
+      "Empty letrec"
+      $(mkRelDir ".")
+      $(mkRelFile "test012.jvc"),
+    NegTest
+      "Wrong definition order in letrec"
+      $(mkRelDir ".")
+      $(mkRelFile "test013.jvc"),
+    NegTest
+      "Wrong name in letrec signature"
+      $(mkRelDir ".")
+      $(mkRelFile "test014.jvc"),
+    NegTest
+      "Case: multiple default branches"
+      $(mkRelDir ".")
+      $(mkRelFile "test015.jvc"),
+    NegTest
+      "Case: default branch only"
+      $(mkRelDir ".")
+      $(mkRelFile "test016.jvc"),
+    NegTest
+      "Case: no branches"
+      $(mkRelDir ".")
+      $(mkRelFile "test017.jvc"),
+    NegTest
+      "Case: multiple default branches only"
+      $(mkRelDir ".")
+      $(mkRelFile "test018.jvc"),
+    NegTest
+      "Case: not a constructor"
+      $(mkRelDir ".")
+      $(mkRelFile "test019.jvc"),
+    NegTest
+      "Case: undeclared identifier"
+      $(mkRelDir ".")
+      $(mkRelFile "test020.jvc"),
+    NegTest
+      "Case: wrong number of constructor arguments"
+      $(mkRelDir ".")
+      $(mkRelFile "test021.jvc"),
+    NegTest
+      "Match: wrong number of constructor arguments"
+      $(mkRelDir ".")
+      $(mkRelFile "test022.jvc"),
+    NegTest
+      "Match: wrong number of patterns"
+      $(mkRelDir ".")
+      $(mkRelFile "test023.jvc"),
+    NegTest
+      "Match: wrong number of patterns with side-conditions"
+      $(mkRelDir ".")
+      $(mkRelFile "test024.jvc")
+  ]
diff --git a/test/Core/Print/Positive.hs b/test/Core/Print/Positive.hs
index c80099d10c..f2d17c98c9 100644
--- a/test/Core/Print/Positive.hs
+++ b/test/Core/Print/Positive.hs
@@ -5,7 +5,7 @@ import Core.Eval.Positive qualified as Eval
 import Core.Print.Base
 
 allTests :: TestTree
-allTests = testGroup "JuvixCore print tests" (map liftTest Eval.tests)
+allTests = testGroup "JuvixCore parse and print positive tests" (map liftTest Eval.tests)
 
 liftTest :: Eval.PosTest -> TestTree
 liftTest _testEval =
diff --git a/tests/Core/negative/parsing/test001.jvc b/tests/Core/negative/parsing/test001.jvc
new file mode 100644
index 0000000000..b7b9cb42bc
--- /dev/null
+++ b/tests/Core/negative/parsing/test001.jvc
@@ -0,0 +1,3 @@
+def main := f 0;
+
+def f := \x x;
diff --git a/tests/Core/negative/parsing/test002.jvc b/tests/Core/negative/parsing/test002.jvc
new file mode 100644
index 0000000000..41009a1f8b
--- /dev/null
+++ b/tests/Core/negative/parsing/test002.jvc
@@ -0,0 +1,2 @@
+def main :=
+  let x := x + 1 in x;
diff --git a/tests/Core/negative/parsing/test003.jvc b/tests/Core/negative/parsing/test003.jvc
new file mode 100644
index 0000000000..ce6003fdd8
--- /dev/null
+++ b/tests/Core/negative/parsing/test003.jvc
@@ -0,0 +1,2 @@
+def main := 1;
+def main := 2;
diff --git a/tests/Core/negative/parsing/test004.jvc b/tests/Core/negative/parsing/test004.jvc
new file mode 100644
index 0000000000..c9863895f0
--- /dev/null
+++ b/tests/Core/negative/parsing/test004.jvc
@@ -0,0 +1,5 @@
+type Unit {
+  unit : Unit;
+};
+
+def unit := 0;
diff --git a/tests/Core/negative/parsing/test005.jvc b/tests/Core/negative/parsing/test005.jvc
new file mode 100644
index 0000000000..3e2920ae8c
--- /dev/null
+++ b/tests/Core/negative/parsing/test005.jvc
@@ -0,0 +1,7 @@
+type Unit {
+  unit : Unit;
+};
+
+type Unit' {
+  unit : Unit';
+};
diff --git a/tests/Core/negative/parsing/test006.jvc b/tests/Core/negative/parsing/test006.jvc
new file mode 100644
index 0000000000..3652fc598d
--- /dev/null
+++ b/tests/Core/negative/parsing/test006.jvc
@@ -0,0 +1,3 @@
+def f : Int -> Int;
+
+def f : Int := 0;
diff --git a/tests/Core/negative/parsing/test007.jvc b/tests/Core/negative/parsing/test007.jvc
new file mode 100644
index 0000000000..dc599f117d
--- /dev/null
+++ b/tests/Core/negative/parsing/test007.jvc
@@ -0,0 +1,3 @@
+def f : Int := 0;
+
+def f : Int;
diff --git a/tests/Core/negative/parsing/test008.jvc b/tests/Core/negative/parsing/test008.jvc
new file mode 100644
index 0000000000..1182d371d0
--- /dev/null
+++ b/tests/Core/negative/parsing/test008.jvc
@@ -0,0 +1 @@
+def f : Int -> Int := \x \y x + y;
diff --git a/tests/Core/negative/parsing/test009.jvc b/tests/Core/negative/parsing/test009.jvc
new file mode 100644
index 0000000000..dd4a4b7b73
--- /dev/null
+++ b/tests/Core/negative/parsing/test009.jvc
@@ -0,0 +1,5 @@
+def Unit := 0;
+
+type Unit {
+  unit : Unit;
+};
diff --git a/tests/Core/negative/parsing/test010.jvc b/tests/Core/negative/parsing/test010.jvc
new file mode 100644
index 0000000000..299fab4f2b
--- /dev/null
+++ b/tests/Core/negative/parsing/test010.jvc
@@ -0,0 +1,5 @@
+def unit := 0;
+
+type Unit {
+  unit : Unit;
+};
diff --git a/tests/Core/negative/parsing/test011.jvc b/tests/Core/negative/parsing/test011.jvc
new file mode 100644
index 0000000000..0fe393486c
--- /dev/null
+++ b/tests/Core/negative/parsing/test011.jvc
@@ -0,0 +1 @@
+builtin def f := 0;
diff --git a/tests/Core/negative/parsing/test012.jvc b/tests/Core/negative/parsing/test012.jvc
new file mode 100644
index 0000000000..1e0a220cbe
--- /dev/null
+++ b/tests/Core/negative/parsing/test012.jvc
@@ -0,0 +1 @@
+letrec [] in 0
diff --git a/tests/Core/negative/parsing/test013.jvc b/tests/Core/negative/parsing/test013.jvc
new file mode 100644
index 0000000000..5852f62107
--- /dev/null
+++ b/tests/Core/negative/parsing/test013.jvc
@@ -0,0 +1,5 @@
+letrec [f g]
+  g := \x f (x - 1);
+  f := \x if x <= 0 then x else x + g (x - 1);
+in
+f 100
diff --git a/tests/Core/negative/parsing/test014.jvc b/tests/Core/negative/parsing/test014.jvc
new file mode 100644
index 0000000000..53f3fb18d9
--- /dev/null
+++ b/tests/Core/negative/parsing/test014.jvc
@@ -0,0 +1,5 @@
+letrec [a b']
+  a := 0;
+  b := 0;
+in
+a + b
diff --git a/tests/Core/negative/parsing/test015.jvc b/tests/Core/negative/parsing/test015.jvc
new file mode 100644
index 0000000000..35ed20c6e0
--- /dev/null
+++ b/tests/Core/negative/parsing/test015.jvc
@@ -0,0 +1,9 @@
+type Unit {
+  unit : Unit;
+};
+
+case unit of {
+  unit := 0;
+  _ := 1;
+  _ := 2;
+}
diff --git a/tests/Core/negative/parsing/test016.jvc b/tests/Core/negative/parsing/test016.jvc
new file mode 100644
index 0000000000..2b743dec7a
--- /dev/null
+++ b/tests/Core/negative/parsing/test016.jvc
@@ -0,0 +1,7 @@
+type Unit {
+  unit : Unit;
+};
+
+case unit of {
+  _ := 0;
+}
diff --git a/tests/Core/negative/parsing/test017.jvc b/tests/Core/negative/parsing/test017.jvc
new file mode 100644
index 0000000000..84aa2e0b4d
--- /dev/null
+++ b/tests/Core/negative/parsing/test017.jvc
@@ -0,0 +1,6 @@
+type Unit {
+  unit : Unit;
+};
+
+case unit of {
+}
diff --git a/tests/Core/negative/parsing/test018.jvc b/tests/Core/negative/parsing/test018.jvc
new file mode 100644
index 0000000000..f0ac204540
--- /dev/null
+++ b/tests/Core/negative/parsing/test018.jvc
@@ -0,0 +1,8 @@
+type Unit {
+  unit : Unit;
+};
+
+case unit of {
+  _ := 1;
+  _ := 2;
+}
diff --git a/tests/Core/negative/parsing/test019.jvc b/tests/Core/negative/parsing/test019.jvc
new file mode 100644
index 0000000000..f54124dab3
--- /dev/null
+++ b/tests/Core/negative/parsing/test019.jvc
@@ -0,0 +1,9 @@
+type Unit {
+  unit : Unit;
+};
+
+def unit' := unit;
+
+case unit of {
+  unit' := 0;
+}
diff --git a/tests/Core/negative/parsing/test020.jvc b/tests/Core/negative/parsing/test020.jvc
new file mode 100644
index 0000000000..934d2f47c6
--- /dev/null
+++ b/tests/Core/negative/parsing/test020.jvc
@@ -0,0 +1,7 @@
+type Unit {
+  unit : Unit;
+};
+
+case unit of {
+  unit' := 0;
+}
diff --git a/tests/Core/negative/parsing/test021.jvc b/tests/Core/negative/parsing/test021.jvc
new file mode 100644
index 0000000000..3f5fb6da2a
--- /dev/null
+++ b/tests/Core/negative/parsing/test021.jvc
@@ -0,0 +1,7 @@
+type Unit {
+  unit : Unit;
+};
+
+case unit of {
+  unit x := 0;
+}
diff --git a/tests/Core/negative/parsing/test022.jvc b/tests/Core/negative/parsing/test022.jvc
new file mode 100644
index 0000000000..6d910f2ffa
--- /dev/null
+++ b/tests/Core/negative/parsing/test022.jvc
@@ -0,0 +1,12 @@
+type Unit {
+  unit : Unit;
+};
+
+type Box {
+  box : Any -> Box;
+};
+
+def f := \x
+  match x with {
+    box box := 0;
+  };
diff --git a/tests/Core/negative/parsing/test023.jvc b/tests/Core/negative/parsing/test023.jvc
new file mode 100644
index 0000000000..637c1e3c9a
--- /dev/null
+++ b/tests/Core/negative/parsing/test023.jvc
@@ -0,0 +1,16 @@
+type Unit {
+  unit : Unit;
+};
+
+type Box {
+  box : Any -> Box;
+};
+
+def f := \x
+  match x with {
+    box y := 1;
+    box y, unit := 0;
+    _ := 11;
+  };
+
+f (box 10)
diff --git a/tests/Core/negative/parsing/test024.jvc b/tests/Core/negative/parsing/test024.jvc
new file mode 100644
index 0000000000..f1f8fc6d90
--- /dev/null
+++ b/tests/Core/negative/parsing/test024.jvc
@@ -0,0 +1,16 @@
+type Unit {
+  unit : Unit;
+};
+
+type Box {
+  box : Any -> Box;
+};
+
+def f := \x
+  match x, unit with {
+    box y if y = 0 := 1;
+    box y, unit if y > 0 := 0;
+    _, _ := 11;
+  };
+
+f (box 10)
diff --git a/tests/Core/negative/test003.jvc b/tests/Core/negative/test003.jvc
index f25a2508e2..ce294c9150 100644
--- a/tests/Core/negative/test003.jvc
+++ b/tests/Core/negative/test003.jvc
@@ -1,3 +1,8 @@
 -- matching on non-data
 
-case \x x of nil -> nil
+type List {
+  nil : List;
+  cons : Any -> List -> List;
+};
+
+case \x x of nil := nil
diff --git a/tests/Core/negative/test005.jvc b/tests/Core/negative/test005.jvc
index 0063bba359..c35427a106 100644
--- a/tests/Core/negative/test005.jvc
+++ b/tests/Core/negative/test005.jvc
@@ -2,9 +2,9 @@
 
 type list {
   nil : list;
-  cons : any -> list -> list;
+  cons : Any -> list -> list;
 };
 
 case cons 1 nil of {
-  nil -> true
+  nil := true
 }
diff --git a/tests/Core/negative/test009.jvc b/tests/Core/negative/test009.jvc
index 5678596568..67b5b1e722 100644
--- a/tests/Core/negative/test009.jvc
+++ b/tests/Core/negative/test009.jvc
@@ -1,19 +1,19 @@
 -- erroneous Church numerals
 
 type product {
-  pair : any -> any -> product;
+  pair : Any -> Any -> product;
 };
 
-def fst := \p case p of { pair x _ -> x };
-def snd := \p case p of { pair _ x -> x };
+def fst := \p case p of { pair x _ := x };
+def snd := \p case p of { pair _ x := x };
 
 def compose := \f \g \x f (g x);
 
-def zero := \f \x x;
+def czero := \f \x x;
 
 def num := \n
   if n = 0 then
-    zero
+    czero
   else
     \f compose f (num (n - 1) f);
 
@@ -28,7 +28,7 @@ def pred := \n
           pair (fst x) (succ (snd x))
         else
           pair (succ (fst x)) (succ (snd x)))
-      (pair zero zero)
+      (pair czero czero)
   );
 
 def toInt := \n n (+ 1) 0;
diff --git a/tests/Core/negative/test010.jvc b/tests/Core/negative/test010.jvc
deleted file mode 100644
index 538f239b12..0000000000
--- a/tests/Core/negative/test010.jvc
+++ /dev/null
@@ -1 +0,0 @@
-letrec { } in 0

From 97fa776a292f858723cff7357114dc961cc4be7b Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Thu, 30 Jan 2025 20:00:11 +0100
Subject: [PATCH 5/7] fix tests

---
 test/Core/Print/Base.hs     | 23 -----------------------
 test/Core/Print/Negative.hs |  1 -
 test/Core/Print/Positive.hs | 22 ++++++++++++++++++++++
 3 files changed, 22 insertions(+), 24 deletions(-)

diff --git a/test/Core/Print/Base.hs b/test/Core/Print/Base.hs
index b5323ed7c3..38d93031a7 100644
--- a/test/Core/Print/Base.hs
+++ b/test/Core/Print/Base.hs
@@ -2,34 +2,11 @@ module Core.Print.Base where
 
 import Base
 import Core.Eval.Base
-import Core.Eval.Positive qualified as Eval
 import Juvix.Compiler.Core.Data.Module (computeCombinedInfoTable, moduleFromInfoTable)
 import Juvix.Compiler.Core.Pretty
 import Juvix.Compiler.Core.Transformation.DisambiguateNames (disambiguateNames)
 import Juvix.Compiler.Core.Translation.FromSource
 
-newtype Test = Test
-  { _testEval :: Eval.PosTest
-  }
-
-fromTest :: Test -> TestTree
-fromTest = mkTest . toTestDescr
-
-root :: Path Abs Dir
-root = relToProject $(mkRelDir "tests/Core/positive/")
-
-toTestDescr :: Test -> TestDescr
-toTestDescr Test {..} =
-  let Eval.PosTest {..} = _testEval
-      tRoot = root <//> _relDir
-      file' = tRoot <//> _file
-      expected' = tRoot <//> _expectedFile
-   in TestDescr
-        { _testName = _name,
-          _testRoot = tRoot,
-          _testAssertion = Steps $ corePrintAssertion file' expected'
-        }
-
 corePrintAssertion ::
   Path Abs File ->
   Path Abs File ->
diff --git a/test/Core/Print/Negative.hs b/test/Core/Print/Negative.hs
index b3885ac346..43e9135187 100644
--- a/test/Core/Print/Negative.hs
+++ b/test/Core/Print/Negative.hs
@@ -1,7 +1,6 @@
 module Core.Print.Negative where
 
 import Base
-import Core.Eval.Base
 import Core.Print.Base
 
 data NegTest = NegTest
diff --git a/test/Core/Print/Positive.hs b/test/Core/Print/Positive.hs
index f2d17c98c9..8f8ea53bb5 100644
--- a/test/Core/Print/Positive.hs
+++ b/test/Core/Print/Positive.hs
@@ -13,3 +13,25 @@ liftTest _testEval =
     Test
       { _testEval
       }
+
+newtype Test = Test
+  { _testEval :: Eval.PosTest
+  }
+
+fromTest :: Test -> TestTree
+fromTest = mkTest . toTestDescr
+
+root :: Path Abs Dir
+root = relToProject $(mkRelDir "tests/Core/positive/")
+
+toTestDescr :: Test -> TestDescr
+toTestDescr Test {..} =
+  let Eval.PosTest {..} = _testEval
+      tRoot = root <//> _relDir
+      file' = tRoot <//> _file
+      expected' = tRoot <//> _expectedFile
+   in TestDescr
+        { _testName = _name,
+          _testRoot = tRoot,
+          _testAssertion = Steps $ corePrintAssertion file' expected'
+        }

From 3baa8a10ba456acf4e785431a2420d47eed6153d Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Thu, 30 Jan 2025 20:17:42 +0100
Subject: [PATCH 6/7] eval test for match side-conditions

---
 test/Core/Eval/Negative.hs          |  6 +-----
 test/Core/Eval/Positive.hs          |  7 ++++++-
 tests/Core/positive/out/test066.out |  1 +
 tests/Core/positive/test066.jvc     | 17 +++++++++++++++++
 4 files changed, 25 insertions(+), 6 deletions(-)
 create mode 100644 tests/Core/positive/out/test066.out
 create mode 100644 tests/Core/positive/test066.jvc

diff --git a/test/Core/Eval/Negative.hs b/test/Core/Eval/Negative.hs
index 04c3cd0bf2..20411488f4 100644
--- a/test/Core/Eval/Negative.hs
+++ b/test/Core/Eval/Negative.hs
@@ -65,9 +65,5 @@ tests =
     NegTest
       "Erroneous Church numerals"
       $(mkRelDir ".")
-      $(mkRelFile "test009.jvc"),
-    NegTest
-      "Empty letrec"
-      $(mkRelDir ".")
-      $(mkRelFile "test010.jvc")
+      $(mkRelFile "test009.jvc")
   ]
diff --git a/test/Core/Eval/Positive.hs b/test/Core/Eval/Positive.hs
index ade2bec210..79658eaf60 100644
--- a/test/Core/Eval/Positive.hs
+++ b/test/Core/Eval/Positive.hs
@@ -367,5 +367,10 @@ tests =
       "Test065: Let / LetRec type inference"
       $(mkRelDir ".")
       $(mkRelFile "test065.jvc")
-      $(mkRelFile "out/test065.out")
+      $(mkRelFile "out/test065.out"),
+    PosTest
+      "Test066: Match side-conditions"
+      $(mkRelDir ".")
+      $(mkRelFile "test066.jvc")
+      $(mkRelFile "out/test066.out")
   ]
diff --git a/tests/Core/positive/out/test066.out b/tests/Core/positive/out/test066.out
new file mode 100644
index 0000000000..45a4fb75db
--- /dev/null
+++ b/tests/Core/positive/out/test066.out
@@ -0,0 +1 @@
+8
diff --git a/tests/Core/positive/test066.jvc b/tests/Core/positive/test066.jvc
new file mode 100644
index 0000000000..236b38584e
--- /dev/null
+++ b/tests/Core/positive/test066.jvc
@@ -0,0 +1,17 @@
+type Unit {
+  unit : Unit;
+};
+
+type Box {
+  box : Any -> Box;
+};
+
+def f := \x
+  match box 9, x, unit with {
+    box z, box y, unit if y < z := 1;
+    box z, box y, unit if y = z + 1 := 0;
+    box z, box y, unit if y > z := 10;
+    _, _, _ := 11;
+  };
+
+3 * f (box 11) * f (box 7) - f (box 10) - 2 * f (box 9)

From bd31f6ac77348b59745bb94fb0d579c04d5b1e15 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Fri, 31 Jan 2025 10:44:20 +0100
Subject: [PATCH 7/7] fix detection of redundant patterns with sid-conditions

---
 src/Juvix/Compiler/Core/Extra/Base.hs                | 12 ++++++++++++
 .../Transformation/DetectConstantSideConditions.hs   |  2 +-
 .../Core/Transformation/DetectRedundantPatterns.hs   |  2 +-
 3 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Extra/Base.hs b/src/Juvix/Compiler/Core/Extra/Base.hs
index 5d2a798b81..0e7ba56462 100644
--- a/src/Juvix/Compiler/Core/Extra/Base.hs
+++ b/src/Juvix/Compiler/Core/Extra/Base.hs
@@ -405,6 +405,18 @@ isPatConstr = \case
   PatConstr {} -> True
   PatWildcard {} -> False
 
+{------------------------------------------------------------------------}
+{- match branch -}
+
+isMatchBranchRhsExpression :: MatchBranch -> Bool
+isMatchBranchRhsExpression MatchBranch {..} =
+  case _matchBranchRhs of
+    MatchBranchRhsExpression {} -> True
+    MatchBranchRhsIfs {} -> False
+
+isMatchBranchRhsIf :: MatchBranch -> Bool
+isMatchBranchRhsIf = not . isMatchBranchRhsExpression
+
 {------------------------------------------------------------------------}
 {- generic Node destruction -}
 
diff --git a/src/Juvix/Compiler/Core/Transformation/DetectConstantSideConditions.hs b/src/Juvix/Compiler/Core/Transformation/DetectConstantSideConditions.hs
index aa08193674..6005fbebb0 100644
--- a/src/Juvix/Compiler/Core/Transformation/DetectConstantSideConditions.hs
+++ b/src/Juvix/Compiler/Core/Transformation/DetectConstantSideConditions.hs
@@ -35,7 +35,7 @@ detectConstantSideConditions md = mapAllNodesM (umapM go) md
                 Just ifs0' -> return $ Just $ set matchBranchRhs (MatchBranchRhsIfs ifs0') br
             SideIfBranch {..} : ifs1' -> do
               fCoverage <- asks (^. optCheckCoverage)
-              unless (not fCoverage || null ifs1') $
+              when (fCoverage && not (null ifs1')) $
                 throw
                   CoreError
                     { _coreErrorMsg = "Redundant side condition",
diff --git a/src/Juvix/Compiler/Core/Transformation/DetectRedundantPatterns.hs b/src/Juvix/Compiler/Core/Transformation/DetectRedundantPatterns.hs
index 42b737ef7c..53b7cd033c 100644
--- a/src/Juvix/Compiler/Core/Transformation/DetectRedundantPatterns.hs
+++ b/src/Juvix/Compiler/Core/Transformation/DetectRedundantPatterns.hs
@@ -40,7 +40,7 @@ goDetectRedundantPatterns md node = case node of
     defaultLoc = singletonInterval (mkInitialLoc mockFile)
 
     checkMatch :: Match -> Sem r ()
-    checkMatch Match {..} = case _matchBranches of
+    checkMatch Match {..} = case dropWhile isMatchBranchRhsIf $ _matchBranches of
       [] -> return ()
       MatchBranch {..} : brs -> go [toList _matchBranchPatterns] brs
       where