merge typechecker negative tests

anoma · Oct 1, 2024 · 9ae0e9a · 9ae0e9a
1 parent eaec932
commit 9ae0e9a
Show file tree

Hide file tree

Showing 2 changed files with 109 additions and 163 deletions.
diff --git 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