From 9ae0e9a351f59838e350e67f415711a688083ee0 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 1 Oct 2024 12:12:51 +0200
Subject: [PATCH] merge typechecker negative tests

---
 test/Typecheck/Negative.hs    | 110 ++++++++++++++++++++++-
 test/Typecheck/NegativeNew.hs | 162 ----------------------------------
 2 files changed, 109 insertions(+), 163 deletions(-)
 delete mode 100644 test/Typecheck/NegativeNew.hs

diff --git a/test/Typecheck/Negative.hs b/test/Typecheck/Negative.hs
index 9c957268ba..591e240e60 100644
--- a/test/Typecheck/Negative.hs
+++ b/test/Typecheck/Negative.hs
@@ -40,7 +40,10 @@ allTests =
         (map (mkTest . testDescr) tests),
       testGroup
         "Non-strictly positive data types"
-        (map (mkTest . testDescr) negPositivityTests)
+        (map (mkTest . testDescr) negPositivityTests),
+      testGroup
+        "Arity tests"
+        (map (mkTest . testDescr) arityTests)
     ]
 
 root :: Path Abs Dir
@@ -313,3 +316,108 @@ negPositivityTests =
         ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing
         _ -> wrongError
   ]
+
+arityTests :: [NegTest]
+arityTests =
+  [ negTest
+      "Too many arguments in expression"
+      $(mkRelDir "Internal")
+      $(mkRelFile "TooManyArguments.juvix")
+      $ \case
+        ErrExpectedFunctionType {} -> Nothing
+        _ -> wrongError,
+    negTest
+      "Pattern match a function type"
+      $(mkRelDir "Internal")
+      $(mkRelFile "FunctionPattern.juvix")
+      $ \case
+        ErrInvalidPatternMatching {} -> Nothing
+        _ -> wrongError,
+    negTest
+      "Function type (* → *) application"
+      $(mkRelDir "Internal")
+      $(mkRelFile "FunctionApplied.juvix")
+      $ \case
+        ErrExpectedFunctionType {} -> Nothing
+        _ -> wrongError,
+    negTest
+      "Implicit name argument without name"
+      $(mkRelDir "Internal")
+      $(mkRelFile "issue3074.juvix")
+      $ \case
+        ErrUnsolvedMeta {} -> Nothing
+        _ -> wrongError,
+    negArityTest
+      "Expected explicit pattern"
+      $(mkRelDir "Internal")
+      $(mkRelFile "ExpectedExplicitPattern.juvix")
+      $ \case
+        ErrWrongPatternIsImplicit {} -> Nothing
+        _ -> wrongError,
+    negArityTest
+      "Expected explicit argument"
+      $(mkRelDir "Internal")
+      $(mkRelFile "ExpectedExplicitArgument.juvix")
+      $ \case
+        ErrExpectedExplicitArgument {} -> Nothing
+        _ -> wrongError,
+    negArityTest
+      "Function clause with two many patterns in the lhs"
+      $(mkRelDir "Internal")
+      $(mkRelFile "LhsTooManyPatterns.juvix")
+      $ \case
+        ErrLhsTooManyPatterns {} -> Nothing
+        _ -> wrongError,
+    negTest
+      "Too many arguments for the return type of a constructor"
+      $(mkRelDir "Internal")
+      $(mkRelFile "WrongReturnTypeTooManyArguments.juvix")
+      $ \case
+        ErrExpectedFunctionType {} -> Nothing
+        _ -> wrongError,
+    negArityTest
+      "Lazy builtin not fully applied"
+      $(mkRelDir "Internal")
+      $(mkRelFile "LazyBuiltin.juvix")
+      $ \case
+        ErrBuiltinNotFullyApplied {} -> Nothing
+        _ -> wrongError,
+    negArityTest
+      "issue 2293: Non-terminating function with arity error"
+      $(mkRelDir "Internal")
+      $(mkRelFile "issue2293.juvix")
+      $ \case
+        ErrWrongConstructorAppLength {} -> Nothing
+        _ -> wrongError,
+    negTest
+      "Detect default argument cycle in the arity checker"
+      $(mkRelDir "Internal")
+      $(mkRelFile "DefaultArgCycleArity.juvix")
+      $ \case
+        ErrDefaultArgLoop {} -> Nothing
+        _ -> wrongError,
+    negTest "Evil: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "Evil.juvix") $
+      \case
+        ErrNonStrictlyPositive ErrTypeAsArgumentOfBoundVar {} -> Nothing
+        _ -> wrongError,
+    negTest "Evil: issue 2540 using Axiom" $(mkRelDir "Internal/Positivity") $(mkRelFile "EvilWithAxiom.juvix") $
+      \case
+        ErrNonStrictlyPositive (ErrTypeAsArgumentOfBoundVar {}) -> Nothing
+        _ -> wrongError,
+    negTest "FreeT: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "FreeT.juvix") $
+      \case
+        ErrNonStrictlyPositive (ErrTypeAsArgumentOfBoundVar {}) -> Nothing
+        _ -> wrongError
+  ]
+
+negArityTest :: String -> Path Rel Dir -> Path Rel File -> (ArityCheckerError -> Maybe FailMsg) -> NegTest
+negArityTest _name rdir rfile ariErr =
+  let _dir = root <//> rdir
+   in NegTest
+        { _file = _dir <//> rfile,
+          _checkErr = \case
+            ErrArityCheckerError e -> ariErr e
+            e -> error (show e),
+          _name,
+          _dir
+        }
diff --git a/test/Typecheck/NegativeNew.hs b/test/Typecheck/NegativeNew.hs
deleted file mode 100644
index 3fcfb9a8a0..0000000000
--- a/test/Typecheck/NegativeNew.hs
+++ /dev/null
@@ -1,162 +0,0 @@
-module Typecheck.NegativeNew where
-
-import Base
-import Data.HashSet qualified as HashSet
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error
-import Typecheck.Negative qualified as Old
-
-type FailMsg = String
-
-root :: Path Abs Dir
-root = relToProject $(mkRelDir "tests/negative")
-
-negTest :: String -> Path Rel Dir -> Path Rel File -> (TypeCheckerError -> Maybe FailMsg) -> Old.NegTest
-negTest _name rdir rfile _checkErr =
-  let _dir = root <//> rdir
-   in Old.NegTest
-        { _file = _dir <//> rfile,
-          _name,
-          _dir,
-          _checkErr
-        }
-
-testDescr :: Old.NegTest -> TestDescr
-testDescr Old.NegTest {..} =
-  let tRoot = _dir
-      file' = _file
-   in TestDescr
-        { _testName = _name,
-          _testRoot = tRoot,
-          _testAssertion = Single $ do
-            entryPoint <- testDefaultEntryPointIO tRoot file'
-            result <- testRunIOEither entryPoint upToCore
-            case mapLeft fromJuvixError result of
-              Left (Just tyError) -> whenJust (_checkErr tyError) assertFailure
-              Left Nothing -> assertFailure "An error occurred but it was not in the type checker."
-              Right _ -> assertFailure "The type checker did not find an error."
-        }
-
-allTests :: TestTree
-allTests =
-  testGroup
-    "New typechecker negative tests"
-    [ testGroup
-        "New typechecker General negative typechecking tests"
-        (map (mkTest . testDescr) (filter (not . isIgnored) Old.tests)),
-      testGroup
-        "Non-strictly positive data types"
-        (map (mkTest . testDescr) Old.negPositivityTests),
-      testGroup
-        "Arity tests"
-        (map (mkTest . testDescr) arityTests)
-    ]
-
-isIgnored :: Old.NegTest -> Bool
-isIgnored t = HashSet.member (t ^. Old.name) ignored
-
-ignored :: HashSet String
-ignored =
-  HashSet.fromList
-    []
-
-wrongError :: Maybe FailMsg
-wrongError = Just "Incorrect error"
-
-negArityTest :: String -> Path Rel Dir -> Path Rel File -> (ArityCheckerError -> Maybe FailMsg) -> Old.NegTest
-negArityTest _name rdir rfile ariErr =
-  let _dir = root <//> rdir
-   in Old.NegTest
-        { _file = _dir <//> rfile,
-          _checkErr = \case
-            ErrArityCheckerError e -> ariErr e
-            e -> error (show e),
-          _name,
-          _dir
-        }
-
-arityTests :: [Old.NegTest]
-arityTests =
-  [ negTest
-      "Too many arguments in expression"
-      $(mkRelDir "Internal")
-      $(mkRelFile "TooManyArguments.juvix")
-      $ \case
-        ErrExpectedFunctionType {} -> Nothing
-        _ -> wrongError,
-    negTest
-      "Pattern match a function type"
-      $(mkRelDir "Internal")
-      $(mkRelFile "FunctionPattern.juvix")
-      $ \case
-        ErrInvalidPatternMatching {} -> Nothing
-        _ -> wrongError,
-    negTest
-      "Function type (* → *) application"
-      $(mkRelDir "Internal")
-      $(mkRelFile "FunctionApplied.juvix")
-      $ \case
-        ErrExpectedFunctionType {} -> Nothing
-        _ -> wrongError,
-    negArityTest
-      "Expected explicit pattern"
-      $(mkRelDir "Internal")
-      $(mkRelFile "ExpectedExplicitPattern.juvix")
-      $ \case
-        ErrWrongPatternIsImplicit {} -> Nothing
-        _ -> wrongError,
-    negArityTest
-      "Expected explicit argument"
-      $(mkRelDir "Internal")
-      $(mkRelFile "ExpectedExplicitArgument.juvix")
-      $ \case
-        ErrExpectedExplicitArgument {} -> Nothing
-        _ -> wrongError,
-    negArityTest
-      "Function clause with two many patterns in the lhs"
-      $(mkRelDir "Internal")
-      $(mkRelFile "LhsTooManyPatterns.juvix")
-      $ \case
-        ErrLhsTooManyPatterns {} -> Nothing
-        _ -> wrongError,
-    negTest
-      "Too many arguments for the return type of a constructor"
-      $(mkRelDir "Internal")
-      $(mkRelFile "WrongReturnTypeTooManyArguments.juvix")
-      $ \case
-        ErrExpectedFunctionType {} -> Nothing
-        _ -> wrongError,
-    negArityTest
-      "Lazy builtin not fully applied"
-      $(mkRelDir "Internal")
-      $(mkRelFile "LazyBuiltin.juvix")
-      $ \case
-        ErrBuiltinNotFullyApplied {} -> Nothing
-        _ -> wrongError,
-    negArityTest
-      "issue 2293: Non-terminating function with arity error"
-      $(mkRelDir "Internal")
-      $(mkRelFile "issue2293.juvix")
-      $ \case
-        ErrWrongConstructorAppLength {} -> Nothing
-        _ -> wrongError,
-    negTest
-      "Detect default argument cycle in the arity checker"
-      $(mkRelDir "Internal")
-      $(mkRelFile "DefaultArgCycleArity.juvix")
-      $ \case
-        ErrDefaultArgLoop {} -> Nothing
-        _ -> wrongError,
-    negTest "Evil: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "Evil.juvix") $
-      \case
-        ErrNonStrictlyPositive ErrTypeAsArgumentOfBoundVar {} -> Nothing
-        _ -> wrongError,
-    negTest "Evil: issue 2540 using Axiom" $(mkRelDir "Internal/Positivity") $(mkRelFile "EvilWithAxiom.juvix") $
-      \case
-        ErrNonStrictlyPositive (ErrTypeAsArgumentOfBoundVar {}) -> Nothing
-        _ -> wrongError,
-    negTest "FreeT: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "FreeT.juvix") $
-      \case
-        ErrNonStrictlyPositive (ErrTypeAsArgumentOfBoundVar {}) -> Nothing
-        _ -> wrongError
-  ]